diff --git a/src_colibri2/tests/solve/all/sat/div_abs.smt2 b/src_colibri2/tests/solve/all/sat/div_abs.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..8d12bd08eab028c0908826f33cf79720c817b109
--- /dev/null
+++ b/src_colibri2/tests/solve/all/sat/div_abs.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-const x Real)
+(declare-const y Real)
+
+(assert (< y 0.0))
+
+(assert
+ (= (colibri_abs_real (/ x y))
+ (/ (colibri_abs_real x) (colibri_abs_real y))))
+(check-sat)
diff --git a/src_colibri2/tests/solve/all/sat/div_abs2.smt2 b/src_colibri2/tests/solve/all/sat/div_abs2.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..e0871e29c8248bfe8dc6af411ef25607a5dc8cbb
--- /dev/null
+++ b/src_colibri2/tests/solve/all/sat/div_abs2.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-const x Real)
+(declare-const y Real)
+
+(assert
+ (not (= (colibri_abs_real (/ x y))
+ (/ (colibri_abs_real x) (colibri_abs_real y)))))
+(check-sat)
diff --git a/src_colibri2/tests/solve/all/sat/dune b/src_colibri2/tests/solve/all/sat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..137bdf589269179a3ae42355c4024e65ca273535
--- /dev/null
+++ b/src_colibri2/tests/solve/all/sat/dune
@@ -0,0 +1,13 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2)
+ (glob_files *.psmt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/all/sat/dune.inc b/src_colibri2/tests/solve/all/sat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..aca73444f0d4e5534f76b17b6ead8815ff6700e6
--- /dev/null
+++ b/src_colibri2/tests/solve/all/sat/dune.inc
@@ -0,0 +1,6 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:div_abs.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:div_abs2.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs2.smt2})))
diff --git a/src_colibri2/tests/solve/all/unsat/div_abs.smt2 b/src_colibri2/tests/solve/all/unsat/div_abs.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..62465424103aee5dc8b9348d373fcaca57fc879e
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/div_abs.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-const x Real)
+(declare-const y Real)
+
+(assert (< y 0.0))
+
+(assert
+ (not (= (colibri_abs_real (/ x y))
+ (/ (colibri_abs_real x) (colibri_abs_real y)))))
+(check-sat)
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 0b55ae9be6c6f5798936b861fe65579fa5085103..0c02372cf204487ed05c2de668ff6475ca9d257b 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -2,6 +2,9 @@
--dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:div_abs.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_abs.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat
@@ -10,3 +13,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:mul_abs.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_abs.smt2})))
diff --git a/src_colibri2/tests/solve/all/unsat/mul_abs.smt2 b/src_colibri2/tests/solve/all/unsat/mul_abs.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..4799c11cbd5ca98d795b9feb11f45fef750d385a
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/mul_abs.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(declare-fun a () Real)
+(declare-fun b () Real)
+
+(assert (not (= (* (colibri_abs_real a) (colibri_abs_real b)) (colibri_abs_real (* a b)))))
+
+(check-sat)
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 62d3bbffcf449cbb7d152b5cbc93c5e725b70cf5..c726fd0ddc59e524be6ae4e1266dd9218041c88a 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -192,7 +192,7 @@ and SolveSign : sig
_ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
val reshape :
- Egraph.wt -> Node.t -> f:(Sign_product.t -> Sign_product.t) -> unit
+ Egraph.wt -> Node.t -> f:(Sign_product.t -> Sign_product.t option) -> unit
end = Pivot.WithUnsolved (struct
let name = "ARITH_SIGN"
@@ -333,12 +333,21 @@ let converter d (f : Ground.t) =
SolveAbs.attach_repr_change d ~node (factorize res a Q.minus_one b);
SolveSign.attach_repr_change d ~node (factorize res a Q.minus_one b))
[ a; b ]
+ | {
+ app = { builtin = Expr.Abs | RealValue.Builtin.Abs_real };
+ tyargs = [];
+ args;
+ _;
+ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ SolveAbs.assume_equality d res (Product.of_list [ (a, Q.one) ]);
+ SolveSign.assume_equality d res Sign_product.one
| _ -> ()
let reshape_non_zero d n =
let q = Sign_product.of_one_node_non_zero n in
- SolveSign.reshape d n ~f:(fun p ->
- Option.value ~default:p (Sign_product.subst p n q))
+ SolveSign.reshape d n ~f:(fun p -> Sign_product.subst p n q)
let init env =
SolveAbs.init env;
@@ -352,16 +361,26 @@ let init env =
let p1 = Product.of_list [ (cl, Q.one) ] in
Debug.dprintf4 debug "[Polynome->Product] propagate %a is %a"
Node.pp n Node.pp cl;
- SolveAbs.assume_equality d n p1));
- SolveAbs.attach_eqs_change env (fun d n ->
- SolveAbs.iter_eqs d n ~f:(fun p ->
- if Node.M.is_num_elt 1 p.poly then
- let cl, q = Node.M.choose p.poly in
- if Q.equal q Q.one then (
- let p1 = Polynome.of_list Q.zero [ (cl, Q.one) ] in
- Debug.dprintf4 debug "[Product->Polynome] propagate %a is %a"
- Node.pp n Node.pp cl;
- Dom_polynome.assume_equality d n p1)));
+ SolveAbs.assume_equality d n p1;
+ SolveSign.assume_equality d n (Sign_product.of_one_node cl)));
+ let product_polynome d n =
+ (* todo more efficient *)
+ SolveAbs.iter_eqs d n ~f:(fun p ->
+ match Product.is_one_node p with
+ | None -> ()
+ | Some cl ->
+ SolveSign.iter_eqs d n ~f:(fun p ->
+ match Sign_product.is_one_node p with
+ | Some cl' when Egraph.is_equal d cl cl' ->
+ let p1 = Polynome.of_list Q.zero [ (cl, Q.one) ] in
+ Debug.dprintf4 debug
+ "[Product->Polynome] propagate %a is %a" Node.pp n Node.pp
+ cl;
+ Dom_polynome.assume_equality d n p1
+ | _ -> ()))
+ in
+ SolveAbs.attach_eqs_change env product_polynome;
+ SolveSign.attach_eqs_change env product_polynome;
DaemonWithFilter.attach_any_dom env Dom_interval.dom (fun d n ->
match Dom_interval.zero_is d n with
| Eq -> Some (fun d -> SolveSign.assume_equality d n Sign_product.zero)
diff --git a/src_colibri2/theories/LRA/pivot.ml b/src_colibri2/theories/LRA/pivot.ml
index c5199deb8cfdd61017c1fa738fbd4d0139a525b4..100d4f5ddf2e07f3072b044ec4bc47921022734e 100644
--- a/src_colibri2/theories/LRA/pivot.ml
+++ b/src_colibri2/theories/LRA/pivot.ml
@@ -71,7 +71,7 @@ end) : sig
val attach_eqs_change :
_ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
- val reshape : Egraph.wt -> Node.t -> f:(P.t -> P.t) -> unit
+ val reshape : Egraph.wt -> Node.t -> f:(P.t -> P.t option) -> unit
end = struct
type t = {
repr : P.t;
@@ -125,36 +125,6 @@ end = struct
add_used_product d cl' (P.nodes t.repr);
P.S.iter (fun p -> add_used_product d cl' (P.nodes p)) t.eqs
- let subst_doms d cl p =
- let b =
- match Node.HC.find used_in_poly d cl with
- | exception Not_found -> Node.S.empty
- | b -> b
- in
- Node.S.iter
- (fun cl' ->
- match Egraph.get_dom d dom cl' with
- | None -> assert false (* absurd: can't be used and absent *)
- | Some q ->
- let fold (new_cl, acc, chg) (q : P.t) =
- let new_cl =
- Node.M.set_union new_cl
- (Node.M.set_diff (P.nodes p) (P.nodes q))
- in
- match P.subst q cl p with
- | None -> (new_cl, P.S.add q acc, chg)
- | Some q' -> (new_cl, P.S.add q' acc, (q, q') :: chg)
- in
- let new_cl, acc, chg = fold (Node.M.empty, P.S.empty, []) q.repr in
- let repr = P.S.choose acc in
- let new_cl, acc, chg =
- P.S.fold_left fold (new_cl, acc, chg) q.eqs
- in
- let eqs = P.S.remove repr acc in
- add_used_product d cl' new_cl;
- set_poly d cl' { repr; eqs } chg)
- b
-
let norm_product d p =
P.normalize p ~f:(fun cl ->
let cl = Egraph.find d cl in
@@ -259,10 +229,47 @@ end = struct
| Some p ->
assert (Option.equal Node.equal (P.is_one_node p.repr) (Some cl));
subst_doms d cl eq;
+ let eq = norm_product d eq in
assert (
P.equal eq (Base.Option.value_exn (Egraph.get_dom d dom cl)).repr);
merge_one_new_eq d cl eq
+ and subst_doms d cl p =
+ let b =
+ match Node.HC.find used_in_poly d cl with
+ | exception Not_found -> Node.S.empty
+ | b -> b
+ in
+ let touched = Node.H.create 10 in
+ Node.S.iter
+ (fun cl' ->
+ match Egraph.get_dom d dom cl' with
+ | None -> assert false (* absurd: can't be used and absent *)
+ | Some q ->
+ let fold (new_cl, acc, chg) (q : P.t) =
+ let new_cl =
+ Node.M.set_union new_cl
+ (Node.M.set_diff (P.nodes p) (P.nodes q))
+ in
+ match P.subst q cl p with
+ | None -> (new_cl, P.S.add q acc, chg)
+ | Some q' ->
+ Node.H.replace touched cl' ();
+ (new_cl, P.S.add q' acc, (q, q') :: chg)
+ in
+ let new_cl, acc, chg =
+ fold (Node.M.empty, P.S.empty, []) q.repr
+ in
+ let repr = P.S.choose acc in
+ let new_cl, acc, chg =
+ P.S.fold_left fold (new_cl, acc, chg) q.eqs
+ in
+ let eqs = P.S.remove repr acc in
+ add_used_product d cl' new_cl;
+ set_poly d cl' { repr; eqs } chg)
+ b;
+ Node.H.iter (recheck d) touched
+
and part d l = List.map (fun p -> P.info d p) l
and solve d l =
@@ -284,6 +291,19 @@ end = struct
`Solved
| () -> `Not_solved
+ and recheck d n () =
+ match Egraph.get_dom d dom n with
+ | None -> assert false (* absurd: can't be used and absent *)
+ | Some p -> (
+ match
+ solve d
+ (Base.List.cartesian_product
+ (part d (p.repr :: P.S.elements p.eqs))
+ (part d (p.repr :: P.S.elements p.eqs)))
+ with
+ | `Solved -> recheck d n ()
+ | `Not_solved -> ())
+
let key = dom
type nonrec t = t
@@ -311,24 +331,35 @@ end = struct
let p = norm_product d p in
Th.merge_one_new_eq d n p
- let reshape d cl ~(f : P.t -> P.t) =
+ let reshape d cl ~(f : P.t -> P.t option) =
match Node.HC.find used_in_poly d cl with
| exception Not_found -> ()
| b ->
+ let touched = Node.H.create 10 in
Node.S.iter
(fun cl' ->
match Egraph.get_dom d dom cl' with
| None -> assert false (* absurd: can't be used and absent *)
| Some q ->
+ let replace p =
+ match f p with
+ | None -> p
+ | Some p ->
+ Node.H.replace touched cl' ();
+ p
+ in
let eqs =
- P.S.fold (fun p acc -> P.S.add (f p) acc) q.eqs P.S.empty
+ P.S.fold
+ (fun p acc -> P.S.add (replace p) acc)
+ q.eqs P.S.empty
in
- let q' = { repr = f q.repr; eqs } in
+ let q' = { repr = replace q.repr; eqs } in
Egraph.set_dom d dom cl' q';
let l = Th.part d (q'.repr :: P.S.elements q'.eqs) in
let l = Base.List.cartesian_product l l in
ignore (Th.solve d l))
- b
+ b;
+ Node.H.iter (Th.recheck d) touched
module ChangeInfo = struct
type runable = Node.S.t
diff --git a/src_colibri2/theories/LRA/pivot.mli b/src_colibri2/theories/LRA/pivot.mli
index ee9fc530676a5e195404b4799423fbfe9dae9978..1112944c7f41b68a5ebcfcd04bec5d092270119c 100644
--- a/src_colibri2/theories/LRA/pivot.mli
+++ b/src_colibri2/theories/LRA/pivot.mli
@@ -88,7 +88,7 @@ end) : sig
val attach_eqs_change :
_ Egraph.t -> ?node:Node.t -> (Egraph.wt -> Node.t -> unit) -> unit
- val reshape : Egraph.wt -> Node.t -> f:(P.t -> P.t) -> unit
+ val reshape : Egraph.wt -> Node.t -> f:(P.t -> P.t option) -> unit
(** Apply the given function to all the normalized form which contains this node.
The resulting normalized form should contain the same or less nodes than before.
*)