Parse standard separation logic inputs (#2257)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d3bec9d42a2c029969458dbe8f3ef7f1c09bfd41..31d8b1a807325861c242a6d4717b8147e73b92f7 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1463,6 +1463,12 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
   | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[e,e2]
     { cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
+  | DECLARE_HEAP LPAREN_TOK 
+    sortSymbol[t,CHECK_DECLARED] 
+    sortSymbol[t, CHECK_DECLARED]
+    // We currently do nothing with the type information declared for the heap.
+    { cmd->reset(new EmptyCommand()); }
+    RPAREN_TOK
   ;
 
 
@@ -1804,7 +1810,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
   std::vector<Expr> patconds;
   std::unordered_set<std::string> names;
   std::vector< std::pair<std::string, Expr> > binders;
-  Type type;
+  Type type, type2;
   std::string s;
   bool isBuiltinOperator = false;
   bool isOverloadedFunction = false;
@@ -1995,7 +2001,6 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-
   | LPAREN_TOK
     ( /* An indexed function application */
       indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK { 
@@ -2340,6 +2345,14 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb),
                                                                 AntlrInput::tokenToUnsigned($sb)),
                                               true)); }
+    | EMP_TOK
+      sortSymbol[type,CHECK_DECLARED]
+      sortSymbol[type2,CHECK_DECLARED]
+      {
+        Expr v1 = PARSER_STATE->mkVar("_emp1", type);
+        Expr v2 = PARSER_STATE->mkVar("_emp2", type2);
+        expr = MK_EXPR(kind::SEP_EMP,v1,v2);
+      }
     // NOTE: Theory parametric constants go here
 
     )
@@ -3144,6 +3157,8 @@ SIMPLIFY_TOK : 'simplify';
 INCLUDE_TOK : 'include';
 GET_QE_TOK : 'get-qe';
 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
+DECLARE_HEAP : 'declare-heap';
+EMP_TOK : 'emp';
 
 // SyGuS commands
 SYNTH_FUN_TOK : 'synth-fun';

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 017e4f9bdc2ac0ed7e88151a630c91972a073d1e..6cbdfee267538a6dc28ad6a2c4ff04e092f1eb2f 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1392,6 +1392,7 @@ REG1_TESTS = \
        regress1/sep/sep-nterm-val-model.smt2 \
        regress1/sep/sep-simp-unc.smt2 \
        regress1/sep/simple-neg-sat.smt2 \
+       regress1/sep/sl-standard.smt2 \
        regress1/sep/split-find-unsat-w-emp.smt2 \
        regress1/sep/split-find-unsat.smt2 \
        regress1/sep/wand-0526-sat.smt2 \

diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2
index 3f908c3be3d3b25fdeabddf922655b7a2d14ebe9..25a38b0187319b84abd2331d9bc1104b0f633766 100644 (file)
--- a/test/regress/regress0/sep/dispose-1.smt2
+++ b/test/regress/regress0/sep/dispose-1.smt2
@@ -11,7 +11,7 @@
 ;-----------------
 
 (assert (pto w (as sep.nil Int)))
-(assert (not (and (sep (and (emp 0 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
+(assert (not (and (sep (and (_ emp Int Int) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
 
 (check-sat)
 ;(get-model)

diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
index 17750eaa344f472df9dd19f257834b9c7ee5cda0..20421e7353f45db39fc82532c43632e3ff9e7c0f 100644 (file)
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -2,6 +2,6 @@
 (set-info :status unsat)
 (declare-sort Loc 0)
 (declare-const l Loc)
-(assert (sep (not (emp l l)) (not (emp l l))))
+(assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc))))
 (assert (pto l l))
 (check-sat)

diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 99d7f9c91d210599f50e0d844f3557b568d6cd0e..27e2aa2c35b0ec3530139ee93bdb28d006c1f0b1 100644 (file)
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
-(assert (not (emp 0 0)))
+(assert (not (_ emp Int Int)))
 (check-sat)

diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index 42efae553b91874d0b02d4092bfc5adefa26329c..f620e9360361ad88b5a5eec3af3ce4a2a3df0ccf 100644 (file)
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -7,6 +7,6 @@
 (declare-fun a () U)
 (declare-fun b () U)
 
-(assert (emp x x))
+(assert (_ emp U U))
 (assert (sep (pto x a) (pto y b)))
 (check-sat)

diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2
index d17f98ac3db6951e42717ef07a7a0e298672375a..7798f6bed80745a045fd6edf2892c32a3c6b2e6e 100644 (file)
--- a/test/regress/regress0/sep/skolem_emp.smt2
+++ b/test/regress/regress0/sep/skolem_emp.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
-(assert (not (emp 0 0)))
+(assert (not (_ emp Int Int)))
 (check-sat)

diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index e0ccee04919d7f746c2684073326a15b615af435..7daf012e2c3a51ae4aff08d63a4a32caef5c9411 100644 (file)
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -17,7 +17,7 @@
 (declare-const r Loc)
 
 (define-fun ten-tree0 ((x Loc) (d Int)) Bool 
-(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0 data0) (= l (as sep.nil Loc))) (and (emp loc0 data0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (_ emp Loc Node) (= l (as sep.nil Loc))) (and (_ emp Loc Node) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
 
 (declare-const dy Int)
 (declare-const y Loc)
@@ -25,7 +25,7 @@
 (declare-const z Loc)
 
 (define-fun ord-tree0 ((x Loc) (d Int)) Bool 
-(or (and (emp loc0 data0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0 data0) (= y (as sep.nil Loc))) (and (emp loc0 data0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (_ emp Loc Node) (= y (as sep.nil Loc))) (and (_ emp Loc Node) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
 
 ;------- f -------
 (assert (= y (as sep.nil Loc)))

diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index dad089f8b8b6bbce07aef73f5bf188f671f792f5..4828646cb45863f614b052e051af16445c77cf7a 100644 (file)
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
-(assert (wand (emp 0 0) (emp 0 0)))
+(assert (wand (_ emp Int Int) (_ emp Int Int)))
 (check-sat)

diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2
index e89c0fd30fe31d5ca41062a96ec6950353d53d64..118e63f074e6a9c95e42176b65ff3f0788737769 100644 (file)
--- 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 8aedbfd259e3395bc7c015adea050f39918af16d..1f3338ed782fbdb5113434f50128c70225fe0248 100644 (file)
--- 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 679b1e363a6213c8245997a663cf417c77db61fc..35640586933fb8f0cd07466e03d4bfb936260d00 100644 (file)
--- 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 8a69c10c47c72c8fb0c0ed903f25116373ebd96f..662682ec3d8c86764837f81530bf18ccb5b0cb64 100644 (file)
--- 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 (file)
index 0000000..16d3165
--- /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 c606d0ab6d2e85c9b63cbe8add48a9db53472110..91b07093c9c1d2e243942347c772b60158175828 100644 (file)
--- 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 12aa0a67e647d058e8cb16de84166cbd817a1d92..99116c9d14de9919abc92f90eb8e02a851de5ef4 100644 (file)
--- 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 b59b53b58efaa05233a661400b63d617d022c44e..702f03a02cbdc3c62fde7404099476a60c4ff12a 100644 (file)
--- 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 fa6a831436ade5b3ac75bdabf0f74a46b16fcd63..352be577721aeed482a732722a531805cda61de9 100644 (file)
--- 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 850be7b9757dc00996aad91f635ceb64084281ef..8c038e3d7f580536cb847c00ff91746f500ceb9c 100644 (file)
--- 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)