[LRA] Fix factorization

      Add divisible and is_int

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 

colibri2/tests/solve/smt_lra/sat/factorization.smt2

+(set-logic ALL)
+(declare-fun m () Real)
+(assert (> m (- m)))
+(check-sat)

colibri2/tests/solve/smt_nra/unsat/divisible.smt2

+(set-logic NIRA)
+(assert ((_ divisible 2) 1))
+(check-sat)

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 

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

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;

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;

fuzzing/ddsmt_colibri2_cvc4.sh

+#!/bin/bash
+
+trap 'kill $(jobs -p)' SIGABRT
+
+colibri2 --lang=smt2.6 --time=5s $1
+cvc5 --tlimit=5000 $1