diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 158dbfb654811f89857a648a91f73fac03bc27a7..15e7954362f0fe2c08eceacac40b83757b38cd13 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -7,6 +7,8 @@
(rule (alias runtest) (action (diff oracle le.smt2.res)))
(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:le2.smt2}))))
(rule (alias runtest) (action (diff oracle le2.smt2.res)))
+(rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:mul.smt2}))))
+(rule (alias runtest) (action (diff oracle mul.smt2.res)))
(rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_merge_itself_repr_empty.smt2}))))
(rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res)))
(rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_set_sem_merge_sign.smt2}))))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/mul.smt2 b/src_colibri2/tests/solve/smt_lra/unsat/mul.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..d35edbc7f6495e63f987ce0e0c38ce82edc6339c
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_lra/unsat/mul.smt2
@@ -0,0 +1,17 @@
+(set-logic ALL)
+
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun t1 () Real)
+(declare-fun t1_ () Real)
+(declare-fun t2 () Real)
+
+(assert (= t1 (- a b)))
+(assert (= t1_ (* a b)))
+(assert (= t2 (* 2.0 b)))
+
+(assert (= t1 t1_))
+(assert (= a 1.0))
+(assert (not (= 1.0 t2)))
+
+(check-sat)
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index 2929d544f4c5807502a95d3bf877382514921d48..7c6aac47964728e7ecaae55f070f81e970d0faef 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -50,18 +50,18 @@ let solve0a _ =
in
assert_bool "a+1 = 1 => a = 0" (is_equal env a LRA.RealValue.zero)
-(* let solve0b _ =
- * let a = fresh Term._Real "ar" in
- * let _1 = LRA.RealValue.cst Q.one in
- * let _2 = LRA.RealValue.cst Q.two in
- * let _4 = LRA.RealValue.cst (Q.of_int 4) in
- * let a1 = LRA.add a _1 in
- * let _2a2 = LRA.add' Q.two a Q.one _2 in
- * let env = run $$ fun env ->
- * List.iter (register env) [a1;_1;_2;_4;_2a2];
- * merge env a1 _2
- * in
- * assert_bool "a+1 = 2 => 2*a+2 = 4" (is_equal env _2a2 _4) *)
+let solve0b _ =
+ let a = fresh Ty.real "ar" in
+ let _1 = LRA.RealValue.cst Q.one in
+ let _2 = LRA.RealValue.cst Q.two in
+ let _4 = LRA.RealValue.cst (Q.of_int 4) in
+ let a1 = LRA.add a _1 in
+ let _2a2 = LRA.add' Q.two a Q.one _2 in
+ let env = run $$ fun env ->
+ List.iter (register env) [a1;_1;_2;_4;_2a2];
+ merge env a1 _2
+ in
+ assert_bool "a+1 = 2 => 2*a+2 = 4" (is_equal env _2a2 _4)
let solve0c _ =
let a = fresh Ty.real "ar" in
@@ -192,66 +192,65 @@ let basic = "LRA.Basic" &:
solve5
]
-(* let mult0 _ =
- * let a = fresh Ty.real "ar" in
- * let b = fresh Ty.real "br" in
- * let t1 = LRA.sub a b in
- * let t1' = LRA.mult a b in
- * let t2 = a in
- * let t2' = LRA.RealValue.cst (Q.of_int 1) in
- * let t3 = LRA.mult_cst (Q.of_int 2) b in
- * let t3' = LRA.RealValue.cst (Q.of_int 1) in
- * let env = run $$ fun env ->
- * Shuffle.seql [
- * (fun () ->
- * Shuffle.seql' (register env) [t1;t1'];
- * merge env t1 t1');
- * (fun () ->
- * Shuffle.seql' (register env) [t2;t2'];
- * merge env t2 t2');
- * (fun () ->
- * Shuffle.seql' (register env) [t3;t3'];)
- * ]
- * in
- * assert_bool "a - b = a * b -> a = 1 -> 1 = 2b" (is_equal env t3 t3')
- *
- * (\** test that mult normalization trigger the needed solve *\)
- * let mult1 _ =
- * let a = fresh Ty.real "ar" in
- * let b = fresh Ty.real "br" in
- * let c = fresh Ty.real "cr" in
- * let t1 = LRA.mult a b in
- * let t1 = LRA.add a t1 in
- * let t1' = LRA.add b c in
- * let t1' = LRA.mult t1' a in
- * let t2 = a in
- * let t2' = LRA.RealValue.cst (Q.of_int 2) in
- * let t3 = c in
- * let t3' = LRA.RealValue.cst (Q.of_int 1) in
- * let env = run $$ fun env ->
- * Shuffle.seql [
- * (fun () ->
- * Shuffle.seql' (register env) [t1;t1'];
- * merge env t1 t1');
- * (fun () ->
- * Shuffle.seql' (register env) [t2;t2'];
- * merge env t2 t2');
- * (fun () ->
- * Shuffle.seql' (register env) [t3;t3'];)
- * ]
- * in
- * assert_bool "a + (a * b) = (b + c) * a -> a = 2 -> c = 1"
- * (is_equal env t3 t3')
- *
- * let mult = "LRA.Mult" &: [mult0;mult1]
- *
- *
- * let files = ["tests/tests_altergo_arith.split";
+let mult0 _ =
+ let a = fresh Ty.real "ar" in
+ let b = fresh Ty.real "br" in
+ let t1 = LRA.sub a b in
+ let t1' = LRA.mult a b in
+ let t2 = a in
+ let t2' = LRA.RealValue.cst (Q.of_int 1) in
+ let t3 = LRA.mult_cst (Q.of_int 2) b in
+ let t3' = LRA.RealValue.cst (Q.of_int 1) in
+ let env = run $$ fun env ->
+ Shuffle.seql [
+ (fun () ->
+ Shuffle.seql' (register env) [t1;t1'];
+ merge env t1 t1');
+ (fun () ->
+ Shuffle.seql' (register env) [t2;t2'];
+ merge env t2 t2');
+ (fun () ->
+ Shuffle.seql' (register env) [t3;t3'];)
+ ]
+ in
+ assert_bool "a - b = a * b -> a = 1 -> 1 = 2b" (is_equal env t3 t3')
+
+(** test that mult normalization trigger the needed solve *)
+let mult1 _ =
+ let a = fresh Ty.real "ar" in
+ let b = fresh Ty.real "br" in
+ let c = fresh Ty.real "cr" in
+ let t1 = LRA.mult a b in
+ let t1 = LRA.add a t1 in
+ let t1' = LRA.add b c in
+ let t1' = LRA.mult t1' a in
+ let t2 = a in
+ let t2' = LRA.RealValue.cst (Q.of_int 2) in
+ let t3 = c in
+ let t3' = LRA.RealValue.cst (Q.of_int 1) in
+ let env = run $$ fun env ->
+ Shuffle.seql [
+ (fun () ->
+ Shuffle.seql' (register env) [t1;t1'];
+ merge env t1 t1');
+ (fun () ->
+ Shuffle.seql' (register env) [t2;t2'];
+ merge env t2 t2');
+ (fun () ->
+ Shuffle.seql' (register env) [t3;t3'];)
+ ]
+ in
+ assert_bool "a + (a * b) = (b + c) * a -> a = 2 -> c = 1"
+ (is_equal env t3 t3')
+
+let mult = "LRA.Mult" &: [mult0;mult1]
+
+
+(* let files = ["tests/tests_altergo_arith.split";
* "tests/tests_popop.split";
* "tests/tests_altergo_qualif.split"
* ]
*
- * let altergo = TestList (List.map Tests_lib.test_split files)
-*)
+ * let altergo = TestList (List.map Tests_lib.test_split files) *)
-let tests = test_list [basic;(* (\* mult;*\)altergo;*) (* smtlib2sat; smtlib2unsat *)]
+let tests = test_list [basic;mult; (* altergo;*) (* smtlib2sat; smtlib2unsat *)]
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index cb4ce0a571f81acc268c52eae69a7204f81c6f71..f73a862fc6d3e6dc8edf4748dccef211327aa290 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -61,6 +61,7 @@ let th_register env =
Dom_polynome.init env;
RealValue.init env;
Fourier.init env;
+ Mul.init env;
()
let () = Egraph.add_default_theory th_register
diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml
index cbb9a2d40bcadac0c6d9da0f467546ec6e4ba619..2daa4f5bcce43ffb06e1fdc88f491f96a43d0cfd 100644
--- a/src_colibri2/theories/LRA/mul.ml
+++ b/src_colibri2/theories/LRA/mul.ml
@@ -16,8 +16,6 @@ let converter d (f:Ground.t) =
end
| _ -> ()
-let th_register env =
+let init env =
init env;
Ground.register_converter env converter
-
-let () = Egraph.add_default_theory th_register
diff --git a/src_colibri2/theories/LRA/mul.mli b/src_colibri2/theories/LRA/mul.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d8be888cc36ed8675a495c4a6d0be604b343f714
--- /dev/null
+++ b/src_colibri2/theories/LRA/mul.mli
@@ -0,0 +1 @@
+val init: Egraph.t -> unit