[Real] Propagate division on constants

src_colibri2/tests/solve/all/unsat/dune.inc

@@ -3,3 +3,5 @@
 (rule (alias runtest) (action (diff oracle bag-BagImpl-createqtvc.psmt2.res)))
 (rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:fact-FactRecursive-fact_recqtvc.psmt2}))))
 (rule (alias runtest) (action (diff oracle fact-FactRecursive-fact_recqtvc.psmt2.res)))
+(rule (action (with-stdout-to interval-Convexe-exists_memqtvc_1.psmt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:interval-Convexe-exists_memqtvc_1.psmt2}))))
+(rule (alias runtest) (action (diff oracle interval-Convexe-exists_memqtvc_1.psmt2.res)))

src_colibri2/tests/solve/all/unsat/interval-Convexe-exists_memqtvc_1.psmt2

+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: real arithmetic
+;;; SMT-LIB2: integer arithmetic
+
+(declare-sort t 0)
+
+(declare-fun num (t) Int)
+
+(declare-fun den (t) Int)
+
+(define-fun real ((q t)) Real (/ (to_real (num q)) (to_real (den q))))
+
+(define-fun infix_ls ((a11 t) (b1 t)) Bool (< (real a11) (real b1)))
+
+(declare-datatypes ((t2 0))
+(((Strict) (Large))))
+
+(declare-datatypes ((t3 0))
+(((Finite
+  (Finite_proj_1 t)(Finite_proj_2 t2)(Finite_proj_3 t)(Finite_proj_4 t2))
+ (InfFinite (InfFinite_proj_1 t)(InfFinite_proj_2 t2))
+ (FiniteInf (FiniteInf_proj_1 t)(FiniteInf_proj_2 t2)) (Inf))))
+(declare-sort tqt 0)
+
+(declare-fun a11 (tqt) t3)
+
+(declare-fun e () tqt)
+
+(declare-fun result () Real)
+
+(declare-fun x13 () t)
+
+(declare-fun x14 () t2)
+
+(declare-fun x15 () t)
+
+(declare-fun x16 () t2)
+
+;; H
+  (assert (= (a11 e) (Finite x13 x14 x15 x16)))
+
+;; H
+  (assert
+  (= result (+ (* (/ 75.0 100.0) (real x13)) (* (/ 25.0 100.0) (real x15)))))
+
+(declare-fun x17 () t)
+
+(declare-fun x18 () t)
+
+(declare-fun x19 () t2)
+
+;; H
+  (assert (= (a11 e) (Finite x17 Strict x18 x19)))
+
+;; h
+  (assert (infix_ls x13 x15))
+
+(assert
+;; exists_memqtvc
+ ;; File "/home/bobot/Sources/colibrics/src_common/interval.mlw", line 45, characters 12-22
+  (not (< (real x17) result)))
+(check-sat)

src_colibri2/theories/LRA/realValue.ml

@@ -257,6 +257,16 @@ assert ( IArray.is_empty args);
     set b (let* va = get a and+ vr = get r in if Q.is_zero va then None else Some (Q.div vr va))
   in
   List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
+  | { app = {builtin = Expr.Div}; tyargs = []; args; _ } ->
+  let a,b = IArray.extract2_exn args in
+  reg a; reg b; Check.attach d f;
+  let wait =
+    set r (let* va = get a and+ vb = get b in if Q.is_zero vb then None else Some (Q.div va vb)) &&
+    set a (let* vb = get b and+ vr = get r in if Q.is_zero vb then None else Some (Q.mul vr vb)) &&
+    (* if va is 0, and vr is not 0, b can't be not zero because vr would be 0. So b is 0. *)
+    set b (let* va = get a and+ vr = get r in if Q.is_zero vr then None else Some (Q.div va vr))
+  in
+  List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b;r]
   | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
     let a = IArray.extract1_exn args in
     reg a; Check.attach d f;