[Mul] register it also for unit tests

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}))))

src_colibri2/tests/solve/smt_lra/unsat/mul.smt2

+(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)

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 *)]

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

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

src_colibri2/theories/LRA/mul.mli

+val init: Egraph.t -> unit