Parse standard separation logic inputs (#2257)

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)