[Product] Fix a * b = 0

They are not all equal to zero

colibri2/tests/solve/smt_nra/sat/dune.inc

@@ -20,5 +20,8 @@
 --dont-print-result %{dep:mul_pos_lt.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:mul_pos_lt.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:mul_zero.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:mul_zero.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:sqrt_tower.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:sqrt_tower.smt2})) (package colibri2))

colibri2/tests/solve/smt_nra/sat/mul_zero.smt2

+(set-logic ALL)
+
+(declare-fun a () Real)
+(declare-fun b () Real)
+
+(assert (= 0.0 (* a b)))
+(assert (distinct a b))
+
+(check-sat)

colibri2/tests/solve/smt_nra/unsat/dune.inc

@@ -38,6 +38,9 @@
 --dont-print-result %{dep:mult_sqrt_hard.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:mult_sqrt_hard.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:product_subst_zero_in_denominator.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:product_subst_zero_in_denominator.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:sqrt.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:sqrt.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 

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

+(set-logic ALL)
+(assert (forall ((x Real) (y Real) (z Real)) (= (/ z (+ x y)) (+ z (/ 1.0 z)))))
+(define-fun n ((z Real) (y Real)) Bool (< z 0.0))
+(declare-fun m () Real)
+(declare-fun r (Real) Real)
+(assert (forall ((x Real) (y Real)) (ite (n x 0.0) true (n (r y) x))))
+(assert (or (not (n (r 0.0) m)) (= 0.0 (/ (+ m 1) (+ m 1)))))
+(check-sat)

colibri2/theories/LRA/dom_product.ml

@@ -141,13 +141,16 @@ end = Pivot.WithUnsolved (struct
   let solve (_, notz1, unk1, p1) (_, notz2, unk2, p2) :
       _ Pivot.solve_with_unsolved =
     let exception Solved of Node.t * Product.t in
-    let all_zero (p : Product.t) : _ Pivot.solve_with_unsolved =
-      if Node.M.is_empty p.poly then
+    let some_zero unk (p : Product.t) : _ Pivot.solve_with_unsolved =
+      (* Use the one unknown to not be null *)
+      if Node.M.is_empty unk then
         if A.is_zero p.cst then AlreadyEqual else Contradiction
-      else Subst (Node.M.map (fun _ -> Product.zero) p.poly)
+      else if Node.M.is_num_elt 1 unk then
+        Subst (Node.M.map (fun _ -> Product.zero) unk)
+      else Unsolved
     in
-    if Product.is_zero p1 then all_zero p2
-    else if Product.is_zero p2 then all_zero p1
+    if Product.is_zero p1 then some_zero unk2 p2
+    else if Product.is_zero p2 then some_zero unk1 p1
     else if
       Node.M.is_empty notz1 && Node.M.is_empty unk1 && Node.M.is_empty notz2
       && Node.M.is_empty unk2