Commit 8e850a73 authored by MARCHE Claude's avatar MARCHE Claude

compute: more built-in simplifications

parent 0f48a6f6
......@@ -59,7 +59,15 @@ let to_bool b = if b then t_true else t_false
let t_app_value ls l ty =
Term (t_app ls (List.map term_of_value l) ty)
let eval_int_op op ls l ty =
let is_zero v =
try BigInt.eq (big_int_of_value v) BigInt.zero
with NotNum -> false
let is_one v =
try BigInt.eq (big_int_of_value v) BigInt.one
with NotNum -> false
let eval_int_op op simpl ls l ty =
match l with
| [t1 ; t2] ->
begin
......@@ -68,10 +76,40 @@ let eval_int_op op ls l ty =
let n2 = big_int_of_value t2 in
Int (op n1 n2)
with NotNum | Division_by_zero ->
t_app_value ls l ty
simpl ls t1 t2 ty
end
| _ -> t_app_value ls l ty
let simpl_none ls t1 t2 ty =
t_app_value ls [t1;t2] ty
let simpl_add ls t1 t2 ty =
if is_zero t1 then t2 else
if is_zero t2 then t1 else
t_app_value ls [t1;t2] ty
let simpl_sub ls t1 t2 ty =
if is_zero t2 then t1 else
t_app_value ls [t1;t2] ty
let simpl_mul ls t1 t2 ty =
if is_zero t1 then t1 else
if is_zero t2 then t2 else
if is_one t1 then t2 else
if is_one t2 then t1 else
t_app_value ls [t1;t2] ty
let simpl_divmod ls t1 t2 ty =
if is_zero t1 then t1 else
if is_one t2 then t1 else
t_app_value ls [t1;t2] ty
let simpl_minmax ls v1 v2 ty =
match v1,v2 with
| Term t1, Term t2 ->
if t_equal t1 t2 then v1 else t_app_value ls [v1;v2] ty
| _ -> t_app_value ls [v1;v2] ty
let eval_int_rel op ls l ty =
match l with
| [t1 ; t2] ->
......@@ -106,9 +144,9 @@ let built_in_theories =
] ;
*)
["int"],"Int", [],
[ "infix +", None, eval_int_op BigInt.add;
"infix -", None, eval_int_op BigInt.sub;
"infix *", None, eval_int_op BigInt.mul;
[ "infix +", None, eval_int_op BigInt.add simpl_add;
"infix -", None, eval_int_op BigInt.sub simpl_sub;
"infix *", None, eval_int_op BigInt.mul simpl_mul;
"prefix -", Some ls_minus, eval_int_uop BigInt.minus;
"infix <", None, eval_int_rel BigInt.lt;
"infix <=", None, eval_int_rel BigInt.le;
......@@ -116,16 +154,16 @@ let built_in_theories =
"infix >=", None, eval_int_rel BigInt.ge;
] ;
["int"],"MinMax", [],
[ "min", None, eval_int_op BigInt.min;
"max", None, eval_int_op BigInt.max;
[ "min", None, eval_int_op BigInt.min simpl_minmax;
"max", None, eval_int_op BigInt.max simpl_minmax;
] ;
["int"],"ComputerDivision", [],
[ "div", None, eval_int_op BigInt.computer_div;
"mod", None, eval_int_op BigInt.computer_mod;
[ "div", None, eval_int_op BigInt.computer_div simpl_divmod;
"mod", None, eval_int_op BigInt.computer_mod simpl_divmod;
] ;
["int"],"EuclideanDivision", [],
[ "div", None, eval_int_op BigInt.euclidean_div;
"mod", None, eval_int_op BigInt.euclidean_mod;
[ "div", None, eval_int_op BigInt.euclidean_div simpl_divmod;
"mod", None, eval_int_op BigInt.euclidean_mod simpl_divmod;
] ;
(*
["map"],"Map", ["map", builtin_map_type],
......@@ -250,7 +288,7 @@ let first_order_matching (vars : Svs.t) (largs : term list)
else
raise NoMatch
with Not_found ->
try
try
let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
loop (ts,Mvs.add vs t2 mv) r1 r2
with Ty.TypeMismatch _ -> raise NoMatch
......@@ -497,7 +535,7 @@ and reduce_eval st t sigma rem =
and reduce_app engine st ls ty rem_cont =
if ls_equal ls ps_equ then
match st with
| t2 :: t1 :: rem_st ->
| t2 :: t1 :: rem_st ->
begin
try
reduce_equ rem_st t1 t2 rem_cont
......@@ -659,6 +697,11 @@ and reduce_equ (* engine *) st v1 v2 cont =
*)
and reduce_term_equ st t1 t2 cont =
if t_equal t1 t2 then
{ value_stack = Term t_true :: st;
cont_stack = cont;
}
else
match (t1.t_node,t2.t_node) with
| Tconst c1, Tconst c2 ->
begin
......
......@@ -65,6 +65,32 @@ theory TestArith
*)
goal k1: power 4 3 = 64
constant n : int
goal l1: n+0 = n
goal l2: 0+n = n
goal l3: n+1 = n
goal l4: n*0 = n
goal l5: 0*n = n
goal l6: n*1 = n
goal l7: 1*n = n
goal l8: n-0 = n
goal l9: 0-n = n
use import int.ComputerDivision
goal m1: div 0 1 = 42
goal m2: div n 1 = 42
goal m3: div 0 n = 42
goal m4: div n n = 42
use import int.MinMax
goal n1: max 3 4 = n
goal n2: max n n = 42
goal n3: min n n = 42
goal n4: min 3 4 = n
end
theory TestRecord
......
......@@ -3,36 +3,36 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../test_compute.why" expanded="true">
<theory name="A" sum="0e4355327797e8f3d23d6df80a329362" expanded="true">
<goal name="G1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<theory name="A" sum="0e4355327797e8f3d23d6df80a329362">
<goal name="G1">
<transf name="compute_in_goal">
<goal name="G1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="G2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="G2">
<transf name="compute_in_goal">
<goal name="G2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="G3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="G3">
<transf name="compute_in_goal">
<goal name="G3.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="Test" sum="cd473d7e70fa0fdfbc7f9f5523952c9e" expanded="true">
<theory name="Test" sum="cd473d7e70fa0fdfbc7f9f5523952c9e">
<goal name="g1">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2" expanded="true">
<goal name="g2">
</goal>
<goal name="g3">
<transf name="compute_in_goal">
......@@ -47,7 +47,7 @@
</transf>
</goal>
</theory>
<theory name="TestArith" sum="f1129b666ed1de800b375bd439ec5cbf" expanded="true">
<theory name="TestArith" sum="c65bbe94a2f17b37cf20ea306cff2375" expanded="true">
<goal name="h1">
<transf name="compute_in_goal">
</transf>
......@@ -66,6 +66,86 @@
</goal>
<goal name="k1" expanded="true">
</goal>
<goal name="l1" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="l2" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="l3" expanded="true">
</goal>
<goal name="l4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l4.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="l5" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="l5.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="l6" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="l7" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="l8" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="l9" expanded="true">
</goal>
<goal name="m1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="m3.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="m4" expanded="true">
</goal>
<goal name="n1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n1.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n2.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n3" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n3.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="n4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="n4.1" expl="1.">
</goal>
</transf>
</goal>
</theory>
<theory name="TestRecord" sum="01e5c2659bedbfaf6934498a0580aaef">
<goal name="i1">
......@@ -164,8 +244,6 @@
</goal>
<goal name="g01">
<transf name="compute_in_goal">
<goal name="g01.1" expl="1.">
</goal>
</transf>
</goal>
<goal name="g1">
......@@ -176,8 +254,6 @@
</goal>
<goal name="g2">
<transf name="compute_in_goal">
<goal name="g2.1" expl="1.">
</goal>
</transf>
</goal>
</theory>
......
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