diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 4461c9feb28b7ed1b848290e79e26e51567bd824..f0d3824a9f2bc9c3c4484d96290a64071b92b405 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/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;
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune b/src_colibri2/tests/solve/dimacs/sat/dune
index 74e69b2c52ff290765701e5e65358570a665fafc..47c20f59db19181b6fa81ba0b8d9d7e956ce111f 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune
+++ b/src_colibri2/tests/solve/dimacs/sat/dune
@@ -1,6 +1,7 @@
(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)
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune b/src_colibri2/tests/solve/dimacs/unsat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..9ca94f8953f83cc072987091ba8429012ab24703
--- /dev/null
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune
@@ -0,0 +1,8 @@
+(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)
+)
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..71418ed37340d018fe77764a9de301eeb595752b
--- /dev/null
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -0,0 +1,13 @@
+(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)))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune b/src_colibri2/tests/solve/smt_lra/sat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..47c20f59db19181b6fa81ba0b8d9d7e956ce111f
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune
@@ -0,0 +1,8 @@
+(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)
+)
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..0692f72d9f5884b1c33f3779b0a90b00409fc7c0
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -0,0 +1,5 @@
+(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)))
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index ca8db34a7be66095bb96a64e8456547d26f87041..cd1b22a0d2dc46dffc00725c8756ca26d5cef7f9 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/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" &:
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index d0363923d25a10874da9f727005159c7ee44ce3c..f8491a49bf4738c52a474be4c7ec2c7bec71831d 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/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;