diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-02 17:17:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-02 17:17:09 -0500 |
commit | df0d51e1541034656fd503dbf5561399b9a3db9f (patch) | |
tree | 72c2ca07c8ae4e79e25c53a16c3510bc3f3715d0 /test/regress/regress1/sep | |
parent | 5d9fa2555c67e0d6661a69ee93d384f717b6858b (diff) |
Parse standard separation logic inputs (#2257)
Diffstat (limited to 'test/regress/regress1/sep')
-rw-r--r-- | test/regress/regress1/sep/emp2-quant-unsat.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/finite-witness-sat.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/fmf-nemp-2.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/quant_wand.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/sl-standard.smt2 | 35 | ||||
-rw-r--r-- | test/regress/regress1/sep/split-find-unsat-w-emp.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/wand-0526-sat.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/wand-nterm-simp.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/wand-nterm-simp2.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress1/sep/wand-simp-unsat.smt2 | 2 |
10 files changed, 44 insertions, 9 deletions
diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2 index e89c0fd30..118e63f07 100644 --- a/test/regress/regress1/sep/emp2-quant-unsat.smt2 +++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2 @@ -5,7 +5,7 @@ (declare-sort U 0) (declare-fun u () U) -(assert (sep (not (emp u u)) (not (emp u u)))) +(assert (sep (not (_ emp U U)) (not (_ emp U U)))) (assert (forall ((x U) (y U)) (= x y))) diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2 index 8aedbfd25..1f3338ed7 100644 --- a/test/regress/regress1/sep/finite-witness-sat.smt2 +++ b/test/regress/regress1/sep/finite-witness-sat.smt2 @@ -4,7 +4,7 @@ (declare-sort Loc 0) (declare-const l Loc) -(assert (not (emp l l))) +(assert (not (_ emp Loc Loc))) (assert (forall ((x Loc) (y Loc)) (not (pto x y)))) diff --git a/test/regress/regress1/sep/fmf-nemp-2.smt2 b/test/regress/regress1/sep/fmf-nemp-2.smt2 index 679b1e363..356405869 100644 --- a/test/regress/regress1/sep/fmf-nemp-2.smt2 +++ b/test/regress/regress1/sep/fmf-nemp-2.smt2 @@ -5,6 +5,6 @@ (declare-fun u1 () U) (declare-fun u2 () U) (assert (not (= u1 u2))) -(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (emp u1 0)) (pto x 0))))) +(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (_ emp U Int)) (pto x 0))))) ; satisfiable with heap of size 2, model of U of size 3 (check-sat) diff --git a/test/regress/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2 index 8a69c10c4..662682ec3 100644 --- a/test/regress/regress1/sep/quant_wand.smt2 +++ b/test/regress/regress1/sep/quant_wand.smt2 @@ -5,7 +5,7 @@ (declare-const u Int) -(assert (emp 0 0)) +(assert (_ emp Int Int)) (assert (forall ((y Int)) diff --git a/test/regress/regress1/sep/sl-standard.smt2 b/test/regress/regress1/sep/sl-standard.smt2 new file mode 100644 index 000000000..16d3165c1 --- /dev/null +++ b/test/regress/regress1/sep/sl-standard.smt2 @@ -0,0 +1,35 @@ +(set-logic QF_ALL) +(set-info :source | CVC4 - Andrew Reynolds |) +(set-info :smt-lib-version 2.6) +(set-info :category "crafted") +(set-info :status unsat) + +(declare-sort Loc 0) + +(declare-heap (Loc Loc)) + +(declare-const loc0 Loc) + +(declare-const u Loc) +(declare-const v Loc) +(declare-const y Loc) +(declare-const y0 Loc) +(declare-const y00 Loc) +(declare-const t Loc) +(declare-const t0 Loc) +(declare-const t00 Loc) + +(define-fun pos2 ((x Loc) (a Loc) (i Int)) Bool (or (and (pto x a) (= i 0)) (sep (pto x a) (or (and (pto a y) (= (- i 1) 0)) (sep (pto a y) (or (and (pto y y0) (= (- (- i 1) 1) 0)) (sep (pto y y0) (and (pto y0 y00) (= (- (- (- i 1) 1) 1) 0))))))))) + +(define-fun neg2 ((z Loc) (b Loc) (j Int)) Bool (or (and (not (pto z b)) (= j 0)) (sep (pto z b) (or (and (not (pto b t)) (= (- j 1) 0)) (sep (pto b t) (or (and (not (pto t t0)) (= (- (- j 1) 1) 0)) (sep (pto t t0) (and (not (pto t0 t00)) (= (- (- (- j 1) 1) 1) 0))))))))) + +;------- f ------- +(assert (= t y)) +(assert (= t0 y0)) +(assert (not (= t00 y00))) +;----------------- + +(assert (pos2 u v 3)) +(assert (not (neg2 u v 3))) + +(check-sat) diff --git a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 index c606d0ab6..91b07093c 100644 --- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 @@ -10,7 +10,7 @@ (declare-const c Int) (assert (and - (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (emp x x)) )) + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (_ emp Int Int)) )) (sep (pto x a) (pto y b)) ) ) diff --git a/test/regress/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2 index 12aa0a67e..99116c9d1 100644 --- a/test/regress/regress1/sep/wand-0526-sat.smt2 +++ b/test/regress/regress1/sep/wand-0526-sat.smt2 @@ -6,5 +6,5 @@ (declare-fun u () Int) (declare-fun v () Int) (assert (wand (pto x u) (pto y v))) -(assert (emp 0 0)) +(assert (_ emp Int Int)) (check-sat) diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2 index b59b53b58..702f03a02 100644 --- a/test/regress/regress1/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp.smt2 @@ -2,6 +2,6 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) -(assert (wand (emp x x) (pto x 3))) +(assert (wand (_ emp Int Int) (pto x 3))) (check-sat) diff --git a/test/regress/regress1/sep/wand-nterm-simp2.smt2 b/test/regress/regress1/sep/wand-nterm-simp2.smt2 index fa6a83143..352be5777 100644 --- a/test/regress/regress1/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2 @@ -3,5 +3,5 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) -(assert (wand (pto x 1) (emp x x))) +(assert (wand (pto x 1) (_ emp Int Int))) (check-sat) diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2 index 850be7b97..8c038e3d7 100644 --- a/test/regress/regress1/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress1/sep/wand-simp-unsat.smt2 @@ -3,5 +3,5 @@ (set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) -(assert (emp x x)) +(assert (_ emp Int Int)) (check-sat) |