[Trigger] remove variable as possible triggers

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

@@ -8,6 +8,9 @@
 --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})) (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:fact-FactRecursive-fact_recqtvc.psmt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:float_interval-GenericFloat-add_special_1.psmt2})) (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:float_interval-GenericFloat-add_special_1.psmt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})) (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:interval-Convexe-exists_memqtvc_1.psmt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 

src_common/float_interval/float_interval-GenericFloat-add_special_1.psmt2 → src_colibri2/tests/solve/all/unsat/float_interval-GenericFloat-add_special_1.psmt2

 ;; produced by local colibri2.drv ;;
 (set-logic ALL)
 (set-info :smt-lib-version 2.6)
+(set-option :max-steps-colibri2 8000)
 ;;; SMT-LIB2: integer arithmetic
 ;;; SMT-LIB2: real arithmetic
 (declare-sort string 0)
@@ -317,7 +318,7 @@
 (declare-fun truncate (Real) Int)
 
 ;; Truncate_int
-;;(assert (forall ((i Int)) (= (truncate (to_real i)) i)))
+(assert (forall ((i Int)) (= (truncate (to_real i)) i)))
 
 ;; Truncate_down_pos
 (assert
@@ -327,57 +328,57 @@
       (and (<= (to_real (truncate x)) x) (< x (to_real (+ (truncate x) 1)))))))
 
 ;; Truncate_up_neg
-;; (assert
-;;   (forall ((x Real))
-;;     (=>
-;;       (<= x 0.0)
-;;       (and (< (to_real (- (truncate x) 1)) x) (<= x (to_real (truncate x)))))))
-
-;; ;; Real_of_truncate
-;; (assert
-;;   (forall ((x Real))
-;;     (and
-;;       (<= (- x 1.0) (to_real (truncate x)))
-;;       (<= (to_real (truncate x)) (+ x 1.0)))))
-
-;; ;; Truncate_monotonic
-;; ;;(assert
-;; ;;  (forall ((x Real) (y Real)) (=> (<= x y) (<= (truncate x) (truncate y)))))
-
-;; ;; Truncate_monotonic_int1
-;; (assert
-;;   (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (truncate x) i))))
-
-;; ;; Truncate_monotonic_int2
-;; (assert
-;;   (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (truncate x)))))
+(assert
+  (forall ((x Real))
+    (=>
+      (<= x 0.0)
+      (and (< (to_real (- (truncate x) 1)) x) (<= x (to_real (truncate x)))))))
+
+;; Real_of_truncate
+(assert
+  (forall ((x Real))
+    (and
+      (<= (- x 1.0) (to_real (truncate x)))
+      (<= (to_real (truncate x)) (+ x 1.0)))))
+
+;; Truncate_monotonic
+;;(assert
+;;  (forall ((x Real) (y Real)) (=> (<= x y) (<= (truncate x) (truncate y)))))
+
+;; Truncate_monotonic_int1
+(assert
+  (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (truncate x) i))))
+
+;; Truncate_monotonic_int2
+(assert
+  (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (truncate x)))))
 
 ;;Floor_int
 (assert (forall ((i Int)) (= (to_int (to_real i)) i)))
 
-;; Ceil_int
-;;(assert (forall ((i Int)) (= (- (to_int (- (to_real i)))) i)))
+;;Ceil_int
+(assert (forall ((i Int)) (= (- (to_int (- (to_real i)))) i)))
 
-;; ;; Floor_down
-;; (assert
-;;   (forall ((x Real))
-;;     (and (<= (to_real (to_int x)) x) (< x (to_real (+ (to_int x) 1))))))
+;; Floor_down
+(assert
+  (forall ((x Real))
+    (and (<= (to_real (to_int x)) x) (< x (to_real (+ (to_int x) 1))))))
 
-;; ;; Ceil_up
-;; (assert
-;;   (forall ((x Real))
-;;     (and
-;;       (< (to_real (- (- (to_int (- x))) 1)) x)
-;;       (<= x (to_real (- (to_int (- x))))))))
+;; Ceil_up
+(assert
+  (forall ((x Real))
+    (and
+      (< (to_real (- (- (to_int (- x))) 1)) x)
+      (<= x (to_real (- (to_int (- x))))))))
 
 ;; Floor_monotonic
 (assert
   (forall ((x Real) (y Real)) (=> (<= x y) (<= (to_int x) (to_int y)))))
 
-;; ;; Ceil_monotonic
-;; (assert
-;;   (forall ((x Real) (y Real))
-;;     (=> (<= x y) (<= (- (to_int (- x))) (- (to_int (- y)))))))
+;; Ceil_monotonic
+(assert
+  (forall ((x Real) (y Real))
+    (=> (<= x y) (<= (- (to_int (- x))) (- (to_int (- y)))))))
 
 ;; infix +.
 (define-fun infix_pldt ((x Real) (y Real)) Real

src_colibri2/theories/quantifier/InvertedPath.ml

@@ -72,7 +72,7 @@ let create =
           };
     }
 
-let stat = Debug.register_stats_int "InvertedPath.exec"
+let stat = Debug.register_stats_int "Quantifier.InvertedPath.exec"
 
 let rec exec d acc substs n ip =
   Debug.dprintf5 debug_full "[Quant] Exec: %a, %a[%i]" Node.pp n

src_colibri2/theories/quantifier/trigger.ml

@@ -178,6 +178,9 @@ let compute_top_triggers d (cq : Ground.ClosedQuantifier.t) =
     | Expr.App ({ term_descr = Cst { builtin; _ }; _ }, _, tl)
       when Info.Builtin_skipped_for_trigger.skipped d builtin ->
         List.fold_left aux pats tl
+    | Expr.Var _ ->
+        (* variable alone are bad pattern *)
+        pats
     | _ -> t :: pats
   in
   let pats = CCList.sort_uniq ~cmp:Expr.Term.compare (aux [] t) in
@@ -406,9 +409,10 @@ module Delayed_instantiation = struct
 
   let run d (tri, subst) =
     let instantiate d =
-      Debug.dprintf8 debug_instantiation
-        "[Quant] %a delayed instantiation %a, pat %a, checks:%a" Ground.Subst.pp
-        subst Ground.ClosedQuantifier.pp tri.form
+      Debug.dprintf10 debug_instantiation
+        "[Quant] %a delayed instantiation %a, pat %a %a, checks:%a"
+        Ground.Subst.pp subst Ground.ClosedQuantifier.pp tri.form Pattern.pp
+        tri.pat
         Fmt.(list ~sep:comma Pattern.pp)
         tri.pats
         Fmt.(list ~sep:comma Pattern.pp)