From f358a4250d1f7ef00d8bd78b29342c7576f8e3e6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 5 Oct 2021 00:10:52 +0200
Subject: [PATCH] Use new define-fun-rec
instantiate more rapidly reccursive definition.
---
src_colibri2/tests/solve/all/unsat/dune.inc | 3 +
.../union-Union-is_singletonqtvc_2.psmt2 | 71 +++++++++++++++++++
src_common/union/why3session.xml | 42 ++++-------
3 files changed, 87 insertions(+), 29 deletions(-)
create mode 100644 src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_2.psmt2
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index bfd765ada..5b1982eb9 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -20,6 +20,9 @@
--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_2.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_2.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
diff --git a/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_2.psmt2 b/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_2.psmt2
new file mode 100644
index 000000000..97317daa2
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_2.psmt2
@@ -0,0 +1,71 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+
+(declare-sort t 0)
+
+(declare-fun make (Int Int) t)
+
+(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-rec nth0 ((i Int)
+ (l t0)) t (ite ((_ is Singleton) l) (let ((x2 (Singleton_proj_1 l))
+ (x3 (Singleton_proj_2 l))) (ite (= i 0)
+ x2
+ (nth0
+ (- i 1) x3)))
+ (ite ((_ is Inter) l) (let ((x4 (Inter_proj_1 l))
+ (x5 (Inter_proj_3 l))
+ (x6 (Inter_proj_5 l))) (ite (= i 0) x4
+ (ite (= i 1) x5
+ (nth0 (- i 2) x6))))
+ (ite ((_ is FiniteInf) l) (let ((x7 (FiniteInf_proj_1 l))
+ ) (ite (= i 0) x7 (make 0 1)))
+ (make 0 1)))))
+
+(define-fun-rec nth ((i Int)
+ (l t3)) t (ite ((_ is InfFinite) l) (let ((x10 (InfFinite_proj_1 l))
+ (x11 (InfFinite_proj_3 l))) (ite (= i 0)
+ x10
+ (nth0
+ (- i 1)
+ x11)))
+ (ite ((_ is Finite) l) (let ((x12 (Finite_proj_1 l))) (nth0 i
+ x12))
+ (make 0 1))))
+(declare-sort tqt 0)
+
+(declare-fun a12 (tqt) t3)
+
+(declare-fun u () tqt)
+
+(declare-fun x28 () t)
+
+(declare-fun x29 () t2)
+
+(declare-fun x30 () t)
+
+(declare-fun x31 () t2)
+
+(declare-fun x32 () t0)
+
+;; H
+ (assert
+ (= (a12 u) (Finite (Singleton x28 (Inter (nth 1 (a12 u)) x29 x30 x31 x32)))))
+
+(assert
+;; is_singletonqtvc
+ ;; File "src_common/union.mlw", line 126, characters 8-20
+ (not (= (nth 2 (a12 u)) x30)))
+(check-sat)
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index eaab74097..061b91a2b 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -12,7 +12,7 @@
<goal name="t''vc" expl="VC for t'" proved="true">
<transf name="split_vc" proved="true" >
<goal name="t''vc.0" expl="type invariant" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="t''vc.1" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -20,58 +20,42 @@
</transf>
</goal>
<goal name="singleton'vc" expl="VC for singleton" proved="true">
- <proof prover="3"><result status="valid" time="0.80"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<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="valid" time="0.23"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="is_singleton'vc.1" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="1.59"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="is_singleton'vc.2" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.94"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="is_singleton'vc.3" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.54"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="is_singleton'vc.4" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="2.23"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="is_singleton'vc.5" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="1.39"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="is_singleton'vc.6" expl="unreachable point" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="is_singleton'vc.7" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="is_singleton'vc.8" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.88"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="is_singleton'vc.9" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.55"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<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.10.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.08"/></proof>
- </goal>
- <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.10.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.05"/></proof>
- </goal>
- <goal name="is_singleton'vc.10.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.28"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.89"/></proof>
</goal>
</transf>
</goal>
--
GitLab