[Quant] Fix unsoundness in smart subst

Makefile

@@ -19,7 +19,8 @@
 ##########################################################################
 
 all:
-	dune build --root=$$(pwd) @install colibri2.opam colibrics.opam colibrilib.opam
+	dune build --root=$$(pwd) @install colibri2.opam colibrics.opam colibrilib.opam \
+	src_colibri2/bin/colibri2_stage0.exe
 
 test:
 	dune runtest --root=$$(pwd)

src_colibri2/tests/solve/all/unknown/dune

+(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} . unknown)))
+ (mode promote))

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

+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unknown 
+--dont-print-result %{dep:float_interval-GenericFloat-div_finite_rev_1.psmt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unknown --learning --dont-print-result %{dep:float_interval-GenericFloat-div_finite_rev_1.psmt2})) (package colibri2))

src_colibri2/tests/solve/all/unknown/float_interval-GenericFloat-div_finite_rev_1.psmt2

+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+
+;; infix *.
+(declare-fun infix_asdt (Real
+  Real) Real)
+
+;; infix >=.
+(declare-fun infix_gteqdt (Real
+  Real) Bool)
+
+(declare-datatypes ((tuple1 1))
+  ((par (a) ((Tuple1 (Tuple1_proj_1 a))))))
+
+(declare-sort finite 0)
+
+;; r
+(declare-fun r (finite) Real)
+
+;; mk_finite
+(declare-fun mk_finite (Real) finite)
+
+(declare-datatypes ((t 0))
+  (((Zero (Zero_proj_1 Bool)) (Infinity (Infinity_proj_1 Bool))
+   (Finite (Finite_proj_1 finite)))))
+
+;; zeroF
+(define-fun zeroF () t (Zero false))
+
+;; prefix .-
+(declare-fun prefix_dtmn (t) t)
+
+;; to_real
+(declare-fun to_real1 (t) Real)
+
+;; is_positive
+(declare-fun is_positive (t) Bool)
+
+(declare-datatypes ((classify 0))
+  (((Is_normal) (Is_subnormal) (Is_zero) (Is_infinite))))
+
+;; first_normal
+(declare-fun first_normal () Real)
+
+;; classify
+(declare-fun classify1 (t) classify)
+
+(declare-datatypes ((tuple2 2))
+  ((par (a1 a2) ((Tuple2 (Tuple2_proj_1 a1)(Tuple2_proj_2 a2))))))
+
+;; infix .=
+(declare-fun infix_dteq (t
+  t) Bool)
+
+;; is_zero
+(define-fun is_zero ((f t)) Bool ((_ is Zero) f))
+
+;; is_finite
+(define-fun is_finite ((f t)) Bool
+  (ite ((_ is Zero) f) true (ite ((_ is Finite) f) true (ite ((_ is Infinity) f) false false))))
+
+;; zeroF_is_positive
+(assert (is_positive zeroF))
+
+;; zeroF_is_zero
+(assert (is_zero zeroF))
+
+;; same_sign
+ (define-fun same_sign ((x t) (y t)) Bool
+   (or
+     (and (is_positive x) (is_positive y))
+     (and (not (is_positive x)) (not (is_positive y)))))
+;;(declare-fun same_sign (t t) Bool)
+
+
+(assert (not (is_positive (Zero true))))
+(assert (is_finite (Zero true)))
+
+(assert (not (same_sign zeroF (prefix_dtmn zeroF))))
+(assert (not (same_sign (Zero false) (Zero true))))
+
+(assert (= (prefix_dtmn zeroF) (Zero true)))
+
+(assert (= (to_real1 zeroF) 0.0))
+(assert (= (to_real1 (Zero true)) 0.0))
+
+;; eq_zero
+(assert (infix_dteq zeroF (prefix_dtmn zeroF)))
+
+;; eq_special
+(assert
+  (forall ((x t) (y t))
+    (=>
+      (infix_dteq x y)
+          (or
+            (and (is_finite x) (is_finite y))
+            (and (not (is_finite x)) (and (not (is_finite y)) (same_sign x y)))))))
+
+(assert    (=>
+      (and (is_finite zeroF) (and (is_finite (prefix_dtmn zeroF)) (same_sign zeroF (prefix_dtmn zeroF))))
+      (infix_gteqdt (infix_asdt (to_real1 zeroF) (to_real1 (prefix_dtmn zeroF))) 0.0)))
+
+
+(assert (infix_gteqdt (infix_asdt (to_real1 zeroF) (to_real1 (prefix_dtmn zeroF))) 0.0))
+
+;; Goal div_finite_rev
+;; File "/home/bobot/Sources/colibrics/src_common/float_interval.mlw", line 584, characters 8-22
+(assert
+  (not
+    (=>
+         true
+           (not (is_zero zeroF))
+           )))
+
+(check-sat)

src_colibri2/theories/quantifier/pattern.ml

@@ -269,28 +269,31 @@ and find_existing_app d subst pf ptyl nodes_args =
       in
       nodes
     in
-    let inter s1 s2 =
-      (* intersection modulo equality which keeps original node *)
-      (* Debug.dprintf4 debug "inter: %a -- %a" Node.S.pp s1 Node.S.pp s2; *)
-      let cmp_with_repr n1 n2 =
-        Node.compare (Egraph.find d n1) (Egraph.find d n2)
-      in
-      let s1 = Node.S.elements s1 |> List.sort_uniq cmp_with_repr in
-      let s2 = Node.S.elements s2 |> List.sort_uniq cmp_with_repr in
-      let rec inter l1 l2 acc =
-        match (l1, l2) with
-        | [], _ | _, [] -> acc
-        | a :: l1', b :: l2' ->
-            let c = cmp_with_repr a b in
-            if c = 0 then inter l1' l2' (a :: acc)
-            else if c < 0 then inter l1' l2 acc
-            else inter l1 l2' acc
-      in
-      Node.S.of_list (inter s1 s2 [])
-    in
+    (* let inter s1 s2 =
+     *   (\* intersection modulo equality which keeps original node *\)
+     *   Debug.dprintf4 debug "inter: %a -- %a" Node.S.pp s1 Node.S.pp s2;
+     *   let cmp_with_repr n1 n2 =
+     *     Node.compare (Egraph.find d n1) (Egraph.find d n2)
+     *   in
+     *   let s1 = Node.S.elements s1 |> List.sort_uniq cmp_with_repr in
+     *   let s2 = Node.S.elements s2 |> List.sort_uniq cmp_with_repr in
+     *   let rec inter l1 l2 acc =
+     *     match (l1, l2) with
+     *     | [], _ | _, [] -> acc
+     *     | a :: l1', b :: l2' ->
+     *         let c = cmp_with_repr a b in
+     *         if c = 0 then inter l1' l2' (a :: acc)
+     *         else if c < 0 then inter l1' l2 acc
+     *         else inter l1 l2' acc
+     *   in
+     *   Node.S.of_list (inter s1 s2 [])
+     * in *)
     let nodes =
       IArray.foldi_non_empty_exn
-        ~f:(fun i acc nodes_arg -> inter acc (get_parents i nodes_arg))
+        ~f:(fun i acc nodes_arg ->
+          (* It is important to just use [Node.S.inter] because we want to do
+             [Ground.S.inter] so we should not take the representative *)
+          Node.S.inter acc (get_parents i nodes_arg))
         ~init:(get_parents 0) nodes_args
     in
     nodes

src_colibri2/theories/quantifier/subst.ml

@@ -80,6 +80,8 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
           args
       in
       let nodes = Pattern.find_existing_app d subst cst tyargs args in
+      Debug.dprintf6 debug "find_existing_app: %a[%a] -> %a" F.pp cst
+        (IArray.pp Node.S.pp) args Node.S.pp nodes;
       let mode =
         if mode.context then
           if Info.Builtin_skipped_for_trigger.skipped d cst.builtin then mode