Commit ae28438f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Execution: support for div/mod operators. Test with

why3 -P alt-ergo examples/tests-provers/div.why -T EuclideanDivTest --eval div_m1_2 --eval mod_m1_2 --eval div_1_m2 --eval mod_1_m2 --eval div_m1_m2 --eval mod_m1_m2

why3 -P alt-ergo examples/tests-provers/div.why -T ComputerDivTest --eval div_m1_2 --eval mod_m1_2 --eval div_1_m2 --eval mod_1_m2 --eval div_m1_m2 --eval mod_m1_m2

why3 examples/euler001.mlw --exec Euler001.run
parent 8f52fab5
......@@ -168,4 +168,6 @@ module Euler001
let n15 = div (n-1) 15 in
div (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) 2
let run () = solve 1000
end
......@@ -4,14 +4,26 @@ theory EuclideanDivTest
use import int.Int
use import int.EuclideanDivision
goal ok1 : div (-1) 2 = -1
goal ok2 : mod (-1) 2 = 1
goal ok3 : div (-1) (-2) = 1
goal ok4 : mod (-1) (-2) = 1
goal smoke1 : div (-1) 2 = 0
goal smoke2 : mod (-1) 2 = -1
goal smoke3 : div (-1) (-2) = 0
goal smoke4 : mod (-1) (-2) = -1
constant div_m1_2 : int = div (-1) 2
constant mod_m1_2 : int = mod (-1) 2
constant div_1_m2 : int = div 1 (-2)
constant mod_1_m2 : int = mod 1 (-2)
constant div_m1_m2 : int = div (-1) (-2)
constant mod_m1_m2 : int = mod (-1) (-2)
goal ok1 : div_m1_2 = -1
goal ok2 : mod_m1_2 = 1
goal ok3 : div_1_m2 = 0
goal ok4 : mod_1_m2 = 1
goal ok5 : div_m1_m2 = 1
goal ok6 : mod_m1_m2 = 1
goal smoke1 : div_m1_2 = 0
goal smoke2 : mod_m1_2 = -1
goal smoke3 : div_1_m2 = 1
goal smoke4 : mod_1_m2 = -1
goal smoke5 : div_m1_m2 = 0
goal smoke6 : mod_m1_m2 = -1
end
......@@ -20,13 +32,25 @@ theory ComputerDivTest
use import int.Int
use import int.ComputerDivision
goal ok1 : div (-1) 2 = 0
goal ok2 : mod (-1) 2 = -1
goal ok3 : div (-1) (-2) = 0
goal ok4 : mod (-1) (-2) = -1
goal smoke1 : div (-1) 2 = -1
goal smoke2 : mod (-1) 2 = 1
goal smoke3 : div (-1) (-2) = -1
goal smoke4 : mod (-1) (-2) = 1
constant div_m1_2 : int = div (-1) 2
constant mod_m1_2 : int = mod (-1) 2
constant div_1_m2 : int = div 1 (-2)
constant mod_1_m2 : int = mod 1 (-2)
constant div_m1_m2 : int = div (-1) (-2)
constant mod_m1_m2 : int = mod (-1) (-2)
goal ok1 : div_m1_2 = 0
goal ok2 : mod_m1_2 = -1
goal ok3 : div_1_m2 = 0
goal ok4 : mod_1_m2 = 1
goal ok5 : div_m1_m2 = 0
goal ok6 : mod_m1_m2 = -1
goal smoke1 : div_m1_2 = -1
goal smoke2 : mod_m1_2 = 1
goal smoke3 : div_1_m2 = -1
goal smoke4 : mod_1_m2 = -1
goal smoke5 : div_m1_m2 = -1
goal smoke6 : mod_m1_m2 = 1
end
\ No newline at end of file
......@@ -45,6 +45,22 @@ let rec matching env t p =
(* builtin symbols *)
let computer_div_mod_big_int x y =
let q,r = Big_int.quomod_big_int x y in
(* we have x = q*y + r with 0 <= r < |y| *)
if Big_int.sign_big_int x < 0 then
if Big_int.sign_big_int y < 0 then
(Big_int.pred_big_int q, Big_int.add_big_int r y)
else
(Big_int.succ_big_int q, Big_int.sub_big_int r y)
else (q,r)
let computer_div_big_int x y =
fst (computer_div_mod_big_int x y)
let computer_mod_big_int x y =
snd (computer_div_mod_big_int x y)
let builtins = Hls.create 17
let ls_minus = ref ps_equ (* temporary *)
......@@ -77,7 +93,7 @@ let eval_int_op op ls l =
let i1 = big_int_of_term t1 in
let i2 = big_int_of_term t2 in
term_of_big_int (op i1 i2)
with NotNum ->
with NotNum | Division_by_zero ->
t_app_infer ls [t1;t2]
end
| _ -> assert false
......@@ -124,7 +140,6 @@ let eval_equ _ls l =
end
| _ -> assert false
let built_in_theories =
[ ["int"],"Int",
[ "infix +", eval_int_op Big_int.add_big_int;
......@@ -135,7 +150,15 @@ let built_in_theories =
"infix <=", eval_int_rel Big_int.le_big_int;
"infix >", eval_int_rel Big_int.gt_big_int;
"infix >=", eval_int_rel Big_int.ge_big_int;
]
] ;
["int"],"ComputerDivision",
[ "div", eval_int_op computer_div_big_int;
"mod", eval_int_op computer_mod_big_int;
] ;
["int"],"EuclideanDivision",
[ "div", eval_int_op Big_int.div_big_int;
"mod", eval_int_op Big_int.mod_big_int;
] ;
]
let add_builtin_th env (l,n,d) =
......@@ -295,7 +318,7 @@ let rec eval_expr env (e : expr) : result =
end
| LetA _ -> Irred e
end
| Eapp(e,pvs,spec) ->
| Eapp(e,pvs,_spec) ->
begin match eval_expr env e with
| Fun ps ->
begin
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment