diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 6ecfee75469ac55e3028628eefe5ffd6a90e76e0..bfd765ada649235048ac2c3b0d2d25f821d374ed 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -20,5 +20,8 @@
--dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:union-Union-is_singletonqtvc_5.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_5.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
diff --git a/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_5.psmt2 b/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_5.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..5cb00766cfb1aaebecc1899965a4be474c274e37
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_5.psmt2
@@ -0,0 +1,61 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(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))))
+
+(declare-datatypes ((t2 0))
+(((Strict) (Large))))
+(declare-datatypes ((t0 0))
+(((Singleton (Singleton_proj_1 t)(Singleton_proj_2 t0))
+ (Inter
+ (Inter_proj_1 t)(Inter_proj_2 t2)(Inter_proj_3 t)(Inter_proj_4 t2)(Inter_proj_5 t0))
+ (FiniteInf (FiniteInf_proj_1 t)(FiniteInf_proj_2 t2)) (End))))
+(declare-datatypes ((t3 0))
+(((InfFinite (InfFinite_proj_1 t)(InfFinite_proj_2 t2)(InfFinite_proj_3 t0))
+ (Finite (Finite_proj_1 t0)) (Inf))))
+
+(define-fun cmp ((x4 Real) (b1 t2)
+ (y Real)) Bool (ite ((_ is Large) b1) (<= x4 y) (< x4 y)))
+
+(declare-fun mem0 (Real t0) Bool)
+
+;; mem0'def
+ (assert
+ (forall ((x13 Real) (l t0))
+ (ite ((_ is Singleton) l) (let ((x14 (Singleton_proj_1 l))
+ (x15 (Singleton_proj_2 l))) (= (mem0 x13 l)
+ (or
+ (= x13 (real x14))
+ (mem0 x13 x15))))
+ (ite ((_ is Inter) l) (let ((x16 (Inter_proj_1 l)) (x17 (Inter_proj_2 l))
+ (x18 (Inter_proj_3 l)) (x19 (Inter_proj_4 l))
+ (x20 (Inter_proj_5 l))) (= (mem0 x13 l)
+ (or
+ (and (cmp (real x16) x17 x13)
+ (cmp x13 x19 (real x18)))
+ (mem0 x13 x20)))) (ite ((_ is FiniteInf) l)
+ (let ((x21 (FiniteInf_proj_1 l))
+ (x22 (FiniteInf_proj_2 l)))
+ (= (mem0
+ x13 l) (cmp
+ (real x21)
+ x22 x13)))
+ (not (mem0
+ x13 l)))))))
+(declare-sort tqt 0)
+
+(declare-fun u () tqt)
+
+(declare-fun x29 () Real)
+
+;; H
+ (assert (mem0 x29 End))
+
+(check-sat)
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 5a9a95d3f6ad0676e3f4ac1771007e4883932c64..62dd5b8c003c4ffd77c2a113d8d9a22bee59ff46 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -349,5 +349,5 @@ let init env =
let () =
Colibri2_theories_quantifiers.Trigger.register_builtin_skipped_for_trigger
(function
- | Expr.Leq | Expr.Geq | Expr.Lt | Expr.Gt -> true
+ | Expr.Leq | Expr.Geq | Expr.Lt | Expr.Gt | Expr.Equal -> true
| _ -> false)
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index 255166ef538be16722fe78478402f9e1edb64540..0fce499a73b3a3099c555dcc507a35606c812d4b 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -56,6 +56,24 @@ let compute_top_triggers (cq : Ground.ClosedQuantifier.t) =
let t = cq'.body in
let rec aux pats (t : Expr.Term.t) =
match t.term_descr with
+ | Expr.Binder (Let_seq l, f) ->
+ (* could be both optimized with Let inside pattern; and efficient handling in
+ match and invertedpath *)
+ let subst =
+ List.fold_left
+ (fun subst (v, t) ->
+ let t = Expr.Term.subst Expr.Subst.empty subst t in
+ Expr.Subst.Var.bind subst v t)
+ Expr.Subst.empty l
+ in
+ aux pats (Expr.Term.subst Expr.Subst.empty subst f)
+ | Expr.Binder (Let_par l, f) ->
+ let subst =
+ List.fold_left
+ (fun subst (v, t) -> Expr.Subst.Var.bind subst v t)
+ Expr.Subst.empty l
+ in
+ aux pats (Expr.Term.subst Expr.Subst.empty subst f)
| Expr.Binder (_, _) -> pats (* todo *)
| Expr.Match (_, _) -> pats (* todo *)
| Expr.App
@@ -65,7 +83,7 @@ let compute_top_triggers (cq : Ground.ClosedQuantifier.t) =
{
builtin =
( Expr.And | Expr.Equal | Expr.Equiv | Expr.Or | Expr.Xor
- | Expr.Imply | Expr.Ite );
+ | Expr.Imply | Expr.Ite | Expr.Neg );
_;
};
_;
diff --git a/src_common/union.mlw b/src_common/union.mlw
index 2cfd4dcb5ac50dee4f9b99ac9a4c392eabab7468..153a03032e86e211cb44ab50d661dddd5f56fa8e 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -134,12 +134,7 @@ module Union
match u.a with
| Inf -> (None, ghost 0., ghost 1.)
| InfFinite q _ _ -> (None, ghost (Q.real q)-.1., ghost (Q.real q)-.2.)
- | Finite (Singleton q End) ->
-
- assert { forall x:real. mem x u.a -> mem0 x (Singleton q End) };
- assert { forall x:real. mem x u.a -> (x = q \/ mem0 x End) };
- assert { forall x:real. mem0 x End -> false };
- (Some q,0., 1.)
+ | Finite (Singleton q End) -> (Some q,0., 1.)
| Finite End -> absurd
| Finite (Inter q b q' b' _) ->
assert { nth 0 u.a = q };
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index b20a311776eafbb51036e5477ba91030a42dfa84..eaab740972c638860bb92345d4cfb5a90679c4d8 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="3" name="Colibri2" version="n/a" timelimit="5" steplimit="0" memlimit="1000"/>
-<file format="whyml">
+<file format="whyml" proved="true">
<path name=".."/><path name="union.mlw"/>
-<theory name="Union">
+<theory name="Union" proved="true">
<goal name="length0_positive'vc" expl="VC for length0_positive" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
@@ -20,156 +20,56 @@
</transf>
</goal>
<goal name="singleton'vc" expl="VC for singleton" proved="true">
- <proof prover="3"><result status="valid" time="2.82"/></proof>
+ <proof prover="3"><result status="valid" time="0.80"/></proof>
</goal>
- <goal name="is_singleton'vc" expl="VC for is_singleton">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
+ <goal name="is_singleton'vc" expl="VC for is_singleton" proved="true">
+ <transf name="split_vc" proved="true" >
<goal name="is_singleton'vc.0" expl="assertion" proved="true">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- <transf name="instantiate" proved="true" arg1="t''invariant" arg2="u">
- <goal name="is_singleton'vc.0.0" expl="assertion" proved="true">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- <transf name="destruct" proved="true" arg1="Hinst">
- <goal name="is_singleton'vc.0.0.0" expl="assertion" proved="true">
- <proof prover="3" obsolete="true"><path name="union-Union-is_singletonqtvc_3.psmt2"/><result status="timeout" time="5.00"/></proof>
- <transf name="instantiate" proved="true" arg1="Hinst1" arg2="0,1">
- <goal name="is_singleton'vc.0.0.0.0" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.97"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="is_singleton'vc.1" expl="assertion">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="is_singleton'vc.1" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="1.59"/></proof>
</goal>
- <goal name="is_singleton'vc.2" expl="unreachable point" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="is_singleton'vc.2" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.94"/></proof>
</goal>
<goal name="is_singleton'vc.3" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="is_singleton'vc.4" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="2.23"/></proof>
</goal>
<goal name="is_singleton'vc.5" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="1.39"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.6" expl="unreachable point" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="is_singleton'vc.6" expl="assertion" proved="true">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- <transf name="instantiate" proved="true" arg1="t''invariant" arg2="u">
- <goal name="is_singleton'vc.6.0" expl="assertion" proved="true">
- <transf name="destruct" proved="true" arg1="Hinst">
- <goal name="is_singleton'vc.6.0.0" expl="assertion" proved="true">
- <proof prover="3" obsolete="true"><path name="union-Union-is_singletonqtvc_4.psmt2"/><result status="timeout" time="5.00"/></proof>
- <transf name="instantiate" proved="true" arg1="Hinst1" arg2="0,1">
- <goal name="is_singleton'vc.6.0.0.0" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
+ <goal name="is_singleton'vc.7" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.8" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.88"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.9" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.55"/></proof>
</goal>
- <goal name="is_singleton'vc.7" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="highfailure" time="0.05"/></proof>
- <transf name="split_vc" >
- <goal name="is_singleton'vc.7.0" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="is_singleton'vc.10" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_singleton'vc.10.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.28"/></proof>
</goal>
- <goal name="is_singleton'vc.7.1" expl="postcondition" proved="true">
+ <goal name="is_singleton'vc.10.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="is_singleton'vc.7.2" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" proved="true" >
- <goal name="is_singleton'vc.7.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.2.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.2.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.2.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.2.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
+ <goal name="is_singleton'vc.10.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="is_singleton'vc.7.3" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="unknown" time="0.01"/></proof>
- <transf name="split_vc" >
- <goal name="is_singleton'vc.7.3.0" expl="postcondition">
- <proof prover="3"><result status="unknown" time="0.31"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.05"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.3.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.3.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.13"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.3.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.60"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.3.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.05"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.3.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- </transf>
+ <goal name="is_singleton'vc.10.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.05"/></proof>
</goal>
- <goal name="is_singleton'vc.7.4" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="unknown" time="0.01"/></proof>
- <transf name="split_vc" >
- <goal name="is_singleton'vc.7.4.0" expl="postcondition">
- <proof prover="3"><result status="unknown" time="0.30"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.4.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.4.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.10"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.4.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.12"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.4.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.67"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.4.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.06"/></proof>
- </goal>
- <goal name="is_singleton'vc.7.4.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- </transf>
+ <goal name="is_singleton'vc.10.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.28"/></proof>
</goal>
</transf>
</goal>