Fix initialization

    Forgotten substitution of the arguments

src_colibri2/solver/scheduler.ml

@@ -73,6 +73,7 @@ type bp =
     pre_prev_scheduler_state : bp option;
     pre_backtrack_point      : Context.bp;
     pre_choices              : (Egraph.t -> unit) list;
+    pre_level                : int;
   }
 
 type t =
@@ -85,6 +86,7 @@ type t =
     decprio : Att.db;
     var_inc  : float ref;
     context : Context.context;
+    mutable level: int;
   }
 (** To treat in the reverse order *)
 
@@ -94,7 +96,7 @@ let print_level fmt t =
   let nb_dec =
     Prio.fold (fun acc x _ -> match x with Att.Decision _ -> acc + 1 | _ -> acc)
       0 t.wakeup_daemons in
-  Format.fprintf fmt "(dec waiting:%i)" nb_dec
+  Format.fprintf fmt "%i (dec waiting:%i)" t.level nb_dec
 
 (* let new_handler t =
  *   if t.delayed <> None then raise NeedStopDelayed;
@@ -117,6 +119,7 @@ let new_solver () =
     delayed    = None;
     decprio = Node.H.create 100;
     var_inc = ref 1.;
+    level = 0;
   }
 
 let push t =
@@ -128,7 +131,10 @@ let push t =
       pre_prev_scheduler_state = t.prev_scheduler_state;
       pre_backtrack_point      = Context.bp t.context;
       pre_choices = t.choices;
+      pre_level = t.level;
     } in
+  t.choices <- [];
+  t.level <- t.level + 1;
   t.prev_scheduler_state <- Some prev;
   ignore (Context.push t.context);
   prev
@@ -180,6 +186,8 @@ let pop_to t prev =
     print_level t;
   t.wakeup_daemons <- prev.pre_wakeup_daemons;
   t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
+  t.choices <- prev.pre_choices;
+  t.level <- prev.pre_level;
   Context.pop prev.pre_backtrack_point;
   let d = new_delayed t in
   Egraph.Backtrackable.draw_graph t.solver_state;

src_colibri2/tests/solve/dimacs/sat/dune

 (include dune.inc)
 
 (rule
+ (alias runtest)
  (deps (glob_files *.cnf) (glob_files *.smt2))
  (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
  (mode promote)

src_colibri2/tests/solve/dimacs/unsat/dune

+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps (glob_files *.cnf) (glob_files *.smt2))
+ (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote)
+)

src_colibri2/tests/solve/dimacs/unsat/dune.inc

+(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold.cnf))))
+(rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
+(rule (action (with-stdout-to modus_ponens.cnf.res (run colibri2 --max-step 1000 modus_ponens.cnf))))
+(rule (alias runtest) (action (diff oracle modus_ponens.cnf.res)))
+(rule (action (with-stdout-to pigeon-1.cnf.res (run colibri2 --max-step 1000 pigeon-1.cnf))))
+(rule (alias runtest) (action (diff oracle pigeon-1.cnf.res)))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run colibri2 --max-step 1000 pigeon-2.cnf))))
+(rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run colibri2 --max-step 1000 pigeon-3.cnf))))
+(rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run colibri2 --max-step 1000 pigeon-4.cnf))))
+(rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))

src_colibri2/tests/solve/smt_lra/sat/dune

+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps (glob_files *.cnf) (glob_files *.smt2))
+ (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote)
+)

src_colibri2/tests/solve/smt_lra/sat/dune.inc

+(rule (action (with-stdout-to oracle (echo "sat\n"))))
+(rule (action (with-stdout-to arith_merge_case_4.smt2.res (run colibri2 --max-step 1000 arith_merge_case_4.smt2))))
+(rule (alias runtest) (action (diff oracle arith_merge_case_4.smt2.res)))
+(rule (action (with-stdout-to arith_zero_dom.smt2.res (run colibri2 --max-step 1000 arith_zero_dom.smt2))))
+(rule (alias runtest) (action (diff oracle arith_zero_dom.smt2.res)))

src_colibri2/tests/tests_LRA.ml

@@ -178,7 +178,7 @@ let solve5 _ =
            Shuffle.seql' (register env) [t3;t3'];)
       ]
   in
-  assert_bool "a+(b-c) = 2 => a = 2 => b + c = 2b" (is_equal env t3 t3')
+  assert_bool "a+(b-c) = 2 => a = 2 => b + c = b + b" (is_equal env t3 t3')
 
 
 let basic = "LRA.Basic" &:

src_colibri2/theories/LRA/LRA.ml

@@ -114,7 +114,14 @@ let add_used d cl' new_cl =
   Node.M.iter (fun used _ ->
       Node.HC.change (function
           | Some b -> Some (Bag.append b cl')
-          | None -> Some (Bag.elt cl')
+          | None ->
+            begin match Egraph.get_dom d dom_poly used with
+              | None -> Egraph.set_dom d dom_poly used (Polynome.monome Q.one used)
+              | Some p ->
+                Format.eprintf "used=%a p=%a@." Node.pp used Polynome.pp p;
+                assert (Polynome.equal (Polynome.monome Q.one used) p)
+            end;
+            Some (Bag.elt cl')
         ) used_in_poly d used
     ) new_cl
 
@@ -206,7 +213,8 @@ module Th = struct
       | Some p2 ->
         let diff = Polynome.sub p1 p2 in
         (* 0 = p1 - p2 = diff *)
-        Debug.dprintf2 debug "[Arith] @[solve in init 0=%a@]" Polynome.pp diff;
+        Debug.dprintf8 debug "[Arith] @[solve in init %a 0=(%a)-(%a)=%a@]"
+          Node.pp cl Polynome.pp p1 Polynome.pp p2 Polynome.pp diff;
         begin match Polynome.extract diff with
           | Zero -> ()
           | Cst _ ->
@@ -344,7 +352,12 @@ module DaemonPropa = struct
            Demon.Create.EventValue(cl2, real, s);
           ];
         let cl = (SE.node s) in
-        let p1 = Polynome.of_list Q.zero [cl1,c1;cl2,c2] in
+        let add acc c cl =
+          match Egraph.get_dom d dom_poly cl with
+          | None -> Polynome.add acc (Polynome.monome c cl)
+          | Some p -> Polynome.add acc p
+        in
+        let p1 = add (add Polynome.zero c1 cl1) c2 cl2 in
         Th.solve_one d cl p1
       | GZero (node,_) ->
         Egraph.register d node;