diff --git a/colibri2/tests/solve/smt_lra/sat/dune.inc b/colibri2/tests/solve/smt_lra/sat/dune.inc
index 90012dedc555dba89b707afbd3d404e89f899892..c446915ed82e8d3c6af0af68544449231cfc3f2d 100644
--- a/colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -62,6 +62,9 @@
--dont-print-result %{dep:attach_only_when_dom_present.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:attach_only_when_dom_present.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:factorization.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:factorization.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
--dont-print-result %{dep:init_not_repr.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:init_not_repr.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
diff --git a/colibri2/tests/solve/smt_lra/sat/factorization.smt2 b/colibri2/tests/solve/smt_lra/sat/factorization.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..7aafb276efd54f9e2fef05806fd5990b55ade170
--- /dev/null
+++ b/colibri2/tests/solve/smt_lra/sat/factorization.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-fun m () Real)
+(assert (> m (- m)))
+(check-sat)
diff --git a/colibri2/tests/solve/smt_nra/unsat/divisible.smt2 b/colibri2/tests/solve/smt_nra/unsat/divisible.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..0de140dc5f09115e01bf3f3ee3658a485ac80b8e
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/unsat/divisible.smt2
@@ -0,0 +1,3 @@
+(set-logic NIRA)
+(assert ((_ divisible 2) 1))
+(check-sat)
diff --git a/colibri2/tests/solve/smt_nra/unsat/dune.inc b/colibri2/tests/solve/smt_nra/unsat/dune.inc
index 9fc52a254a91fc73bf87cac16640e04b60317121..8cda5df03dec65ba3e8f0644b07dc06c0d330043 100644
--- a/colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -11,6 +11,9 @@
--dont-print-result %{dep:div_pos_lt_to_real.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt_to_real.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:divisible.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:divisible.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:floor.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:floor.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
diff --git a/colibri2/theories/LRA/dom_product.ml b/colibri2/theories/LRA/dom_product.ml
index fd53c56057254b3d01d1a4252749412802b63f25..8093a36ca887219e0871f16d7891d17bad5d3c38 100644
--- a/colibri2/theories/LRA/dom_product.ml
+++ b/colibri2/theories/LRA/dom_product.ml
@@ -263,8 +263,8 @@ let factorize res a coef b d _ =
let abs = Product.div abs common_abs in
let sign = Sign_product.mul sign common_sign in
match (Product.classify abs, Sign_product.classify sign) with
- | CST cst', PLUS_ONE -> (A.add (A.mul cst' v) cst, acc)
- | CST cst', MINUS_ONE -> (A.sub (A.mul cst' v) cst, acc)
+ | CST cst', PLUS_ONE -> (A.add cst (A.mul cst' v), acc)
+ | CST cst', MINUS_ONE -> (A.sub cst (A.mul cst' v), acc)
| NODE (cst', n), NODE (cst'', n') when Egraph.is_equal d n n'
->
(cst, (n, A.mul (Sign_product.mul_cst cst'' cst') v) :: acc)
@@ -278,10 +278,13 @@ let factorize res a coef b d _ =
let p = Polynome.of_list cst l in
let n = Dom_polynome.node_of_polynome d p in
let pp_coef fmt coef =
- if A.equal A.one coef then Fmt.pf fmt "+" else Fmt.pf fmt "-"
+ if A.equal A.one coef then Fmt.pf fmt "+"
+ else if A.equal A.minus_one coef then Fmt.pf fmt "-"
+ else Fmt.pf fmt "(%a)" A.pp coef
in
- Debug.dprintf10 debug "[Factorize] %a = %a %a %a into %a" Node.pp res
- Node.pp a pp_coef coef Node.pp b Polynome.pp p;
+ Debug.dprintf14 debug "[Factorize] %a = %a %a %a into %a * %a * %a"
+ Node.pp res Node.pp a pp_coef coef Node.pp b Polynome.pp p
+ Product.pp common_abs Sign_product.pp common_sign;
Egraph.register d n;
Dom_polynome.assume_equality d n p;
let abs = Product.mul (Product.monome n Q.one) common_abs in
diff --git a/colibri2/theories/LRA/realValue.ml b/colibri2/theories/LRA/realValue.ml
index 36fd2dd4b237efb747f8d92da776fa8853dd3e6b..5b1b4d8fb18d460cb73372826615251690e60a17 100644
--- a/colibri2/theories/LRA/realValue.ml
+++ b/colibri2/theories/LRA/realValue.ml
@@ -312,6 +312,9 @@ module Check = struct
| { app = { builtin = Expr.Rational s }; tyargs = []; args; ty = _ } ->
assert (IArray.is_empty args);
!<(A.of_string_decimal s)
+ | { app = { builtin = Expr.Is_int _ }; tyargs = []; args; ty = _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(A.is_integer !>a)
| { app = { builtin = Expr.Add _ }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
!<(A.add !>a !>b)
@@ -357,6 +360,11 @@ module Check = struct
let b = !>b in
let s = A.sign b in
if s = 0 then `Uninterp else !<(A.mod_t !>a b)
+ | { app = { builtin = Expr.Divisible }; tyargs = []; args; ty = _ } ->
+ let b, a = IArray.extract2_exn args in
+ let b = !>b in
+ let s = A.sign b in
+ if s = 0 then `Uninterp else !<<(A.is_zero (A.mod_t !>a b))
| { app = { builtin = Builtin.Pow_int_int }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let a = !>a in
@@ -723,6 +731,13 @@ let converter d (f : Ground.t) =
set b
(let* va = get a and+ vr = get r in
if A.is_zero vr then None else Some (A.div va vr)))
+ | { app = { builtin = Expr.Divisible }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b
+ | { app = { builtin = Expr.Is_int _ }; tyargs = []; args; ty = _ } ->
+ let a = IArray.extract1_exn args in
+ reg a
| { app = { builtin = Expr.Minus _ }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
reg a;
diff --git a/common/float_interval.mlw b/common/float_interval.mlw
index 3bc0db45e7c80ed041f6b6201522a0ee23ef606c..37f1ac629943602bef9815c079afc1c448cc62d4 100644
--- a/common/float_interval.mlw
+++ b/common/float_interval.mlw
@@ -1012,14 +1012,17 @@ module Float_interval
requires { F.(not (is_nan (add m f1 f3))) }
requires { F.(not (is_nan (add m f2 f3))) }
requires { F.(le f1 f2) }
- ensures { F.(le (add m f1 f3) (add m f2 f3)) } ()
-
+ ensures { F.(le (add m f1 f3) (add m f2 f3)) }
+ assert { not (F.is_nan f1)};
+ assert { not (F.is_nan f2)};
+ assert { not (F.is_nan f3)}; ()
+(*
let ghost monotone_add2 (m:F.mode) (f3:F.t) (f1:F.t) (f2:F.t) =
requires { F.(not (is_nan (add m f3 f1))) }
requires { F.(not (is_nan (add m f3 f2))) }
requires { F.(le f1 f2) }
ensures { F.(le (add m f3 f1) (add m f3 f2)) } ()
-
+*)
let ghost le_trans (f1 f2 f3:F.t)
requires { F.le f1 f2 }
requires { F.le f2 f3 }
@@ -1031,7 +1034,7 @@ module Float_interval
requires { F.(le l1 h1) }
requires { F.(le l2 h2) }
ensures { F.(le (add m l1 l2) (add m h1 h2)) } ()
-
+(*
let cadd (m : F.mode) (i1 i2: t) : t
requires { valid i1 }
requires { valid i2 }
@@ -1070,7 +1073,7 @@ module Float_interval
F.(andb (F.is_plus_infinity h1) (F.is_minus_infinity l2)))
F.(andb (F.is_plus_infinity h2) (F.is_minus_infinity l1)))
end
-
+*)
(* let ghost add_nan (m:mode) (f1:F.t) (f2:F.t) F.is_not_nan f1 -> F.is_not_nan f2 -> F.is_nan (F.add m f1 f2) -> F.diff_sign f1 f2 /\ F.is_infinite f1 /\ F.is_infinite f2 *)
let ghost add_nan (m:F.mode) (f1:F.t) (f2:F.t)
@@ -1092,7 +1095,7 @@ module Float_interval
goal add_not_nan: forall m f1 f2[F.is_nan (F.add m f1 f2)]. not (F.is_nan f1) -> not (F.is_nan f2) -> not (F.is_nan (F.add m f1 f2)) ->
(F.same_sign f1 f2 /\ F.is_infinite f1 /\ F.is_infinite f2) \/ F.is_finite f1 \/ F.is_finite f2
-
+(*
let cadd2 (m : F.mode) (i1 i2: t) : t
requires { valid i1 }
requires { valid i2 }
@@ -1117,7 +1120,7 @@ module Float_interval
F.(andb (F.is_plus_infinity h1) (F.is_minus_infinity l2)))
F.(andb (F.is_plus_infinity h2) (F.is_minus_infinity l1)))
end
-
+*)
let cadd3 (m : F.mode) (i1 i2: t) : t
requires { valid i1 }
requires { valid i2 }
@@ -1145,7 +1148,9 @@ module Float_interval
requires { mem f2 i2 }
ensures { mem (F.add m f1 f2) r }
if F.is_nan (F.add m f1 f2) then
- add_nan m f1 f2
+ if F.is_nan f1 then assert { b1 }
+ else if F.is_nan f2 then assert { b2 }
+ else add_nan m f1 f2
else begin
monotone_add3 m l1 l2 f1 f2;
monotone_add3 m f1 f2 h1 h2;
diff --git a/fuzzing/ddsmt_colibri2_cvc4.sh b/fuzzing/ddsmt_colibri2_cvc4.sh
new file mode 100755
index 0000000000000000000000000000000000000000..20ff8eb103210c5f0d59b263e8da7fca3e8157cf
--- /dev/null
+++ b/fuzzing/ddsmt_colibri2_cvc4.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+trap 'kill $(jobs -p)' SIGABRT
+
+colibri2 --lang=smt2.6 --time=5s $1
+cvc5 --tlimit=5000 $1