diff options
19 files changed, 70 insertions, 19 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d3bec9d42..31d8b1a80 100644 --- 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 017e4f9bd..6cbdfee26 100644 --- 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 3f908c3be..25a38b018 100644 --- 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 17750eaa3..20421e735 100644 --- 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 99d7f9c91..27e2aa2c3 100644 --- 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 42efae553..f620e9360 100644 --- 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 d17f98ac3..7798f6bed 100644 --- 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 e0ccee049..7daf012e2 100644 --- 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 dad089f8b..4828646cb 100644 --- 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 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) |