diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-30 10:38:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-30 15:38:44 +0000 |
commit | 46ad5bddc9bc0e03ea702f29c56c22e917aeb06b (patch) | |
tree | f5401a4a35643d25b6e3c43403018cf57ec5c0b4 /test/regress/regress1/sep | |
parent | 0a15133a7de2289fdfb10ccf65e9b753f5064ba7 (diff) |
Simplify the syntax and representation of the separation logic empty heap constraint (#7268)
Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.
This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.
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/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 |
9 files changed, 9 insertions, 9 deletions
diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2 index cdca1a909..acdd5f6c6 100644 --- a/test/regress/regress1/sep/emp2-quant-unsat.smt2 +++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2 @@ -6,7 +6,7 @@ (declare-fun u () U) (declare-heap (U U)) -(assert (sep (not (_ emp U U)) (not (_ emp U U)))) +(assert (sep (not sep.emp) (not sep.emp))) (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 479dbe2b2..1d5488296 100644 --- a/test/regress/regress1/sep/finite-witness-sat.smt2 +++ b/test/regress/regress1/sep/finite-witness-sat.smt2 @@ -5,7 +5,7 @@ (declare-const l Loc) (declare-heap (Loc Loc)) -(assert (not (_ emp Loc Loc))) +(assert (not sep.emp)) (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 e6e2aca98..c40106c48 100644 --- a/test/regress/regress1/sep/fmf-nemp-2.smt2 +++ b/test/regress/regress1/sep/fmf-nemp-2.smt2 @@ -6,6 +6,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 U Int)) (pto x 0))))) +(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not sep.emp) (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 87f0a974b..63dcebfda 100644 --- a/test/regress/regress1/sep/quant_wand.smt2 +++ b/test/regress/regress1/sep/quant_wand.smt2 @@ -6,7 +6,7 @@ (declare-const u Int) -(assert (_ emp Int Int)) +(assert sep.emp) (assert (forall ((y Int)) 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 c6fa301f0..7935ccdc1 100644 --- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 @@ -11,7 +11,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 Int Int)) )) + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not sep.emp) )) (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 a07d0b8ae..334908e64 100644 --- a/test/regress/regress1/sep/wand-0526-sat.smt2 +++ b/test/regress/regress1/sep/wand-0526-sat.smt2 @@ -7,5 +7,5 @@ (declare-fun u () Int) (declare-fun v () Int) (assert (wand (pto x u) (pto y v))) -(assert (_ emp Int Int)) +(assert sep.emp) (check-sat) diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2 index 47d39eb0b..4239a415e 100644 --- a/test/regress/regress1/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp.smt2 @@ -3,6 +3,6 @@ (set-logic QF_ALL) (declare-heap (Int Int)) (declare-fun x () Int) -(assert (wand (_ emp Int Int) (pto x 3))) +(assert (wand sep.emp (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 647421665..15362f227 100644 --- a/test/regress/regress1/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2 @@ -4,5 +4,5 @@ (set-info :status sat) (declare-heap (Int Int)) (declare-fun x () Int) -(assert (wand (pto x 1) (_ emp Int Int))) +(assert (wand (pto x 1) sep.emp)) (check-sat) diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2 index 2e90dfb26..b974b9a32 100644 --- a/test/regress/regress1/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress1/sep/wand-simp-unsat.smt2 @@ -4,5 +4,5 @@ (declare-fun x () Int) (declare-heap (Int Int)) (assert (wand (pto x 1) (pto x 3))) -(assert (_ emp Int Int)) +(assert sep.emp) (check-sat) |