From 46ad5bddc9bc0e03ea702f29c56c22e917aeb06b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Sep 2021 10:38:44 -0500 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 13 ++- src/api/cpp/cvc5_kind.h | 11 +- src/parser/smt2/Smt2.g | 12 +- src/parser/smt2/smt2.cpp | 1 + src/preprocessing/passes/sep_skolem_emp.cpp | 29 +++-- src/theory/sep/kinds | 2 +- src/theory/sep/theory_sep.cpp | 107 ++++++++---------- src/theory/sep/theory_sep.h | 12 +- test/regress/regress0/sep/dispose-1.smt2 | 2 +- test/regress/regress0/sep/dup-nemp.smt2 | 2 +- .../regress0/sep/issue3720-check-model.smt2 | 4 +- test/regress/regress0/sep/nemp.smt2 | 2 +- .../regress0/sep/sep-simp-unsat-emp.smt2 | 2 +- test/regress/regress0/sep/skolem_emp.smt2 | 2 +- test/regress/regress0/sep/trees-1.smt2 | 4 +- test/regress/regress0/sep/wand-crash.smt2 | 2 +- .../regress1/sep/emp2-quant-unsat.smt2 | 2 +- .../regress1/sep/finite-witness-sat.smt2 | 2 +- test/regress/regress1/sep/fmf-nemp-2.smt2 | 2 +- test/regress/regress1/sep/quant_wand.smt2 | 2 +- .../regress1/sep/split-find-unsat-w-emp.smt2 | 2 +- test/regress/regress1/sep/wand-0526-sat.smt2 | 2 +- .../regress/regress1/sep/wand-nterm-simp.smt2 | 2 +- .../regress1/sep/wand-nterm-simp2.smt2 | 2 +- .../regress/regress1/sep/wand-simp-unsat.smt2 | 2 +- 25 files changed, 107 insertions(+), 118 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d33ef5b42..42690586a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5079,21 +5079,26 @@ Sort Solver::mkTupleSortHelper(const std::vector& sorts) const Term Solver::mkTermFromKind(Kind kind) const { - CVC5_API_KIND_CHECK_EXPECTED( - kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind) + CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY + || kind == REGEXP_SIGMA || kind == SEP_EMP, + kind) << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; //////// all checks before this line Node res; + cvc5::Kind k = extToIntKind(kind); if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) { - cvc5::Kind k = extToIntKind(kind); Assert(isDefinedIntKind(k)); res = d_nodeMgr->mkNode(k, std::vector()); } + else if (kind == SEP_EMP) + { + res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->booleanType(), k); + } else { Assert(kind == PI); - res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), cvc5::kind::PI); + res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), k); } (void)res.getType(true); /* kick off type checking */ increment_term_stats(kind); diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 94a8a6f92..0ff05022f 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2064,17 +2064,10 @@ enum CVC5_EXPORT Kind : int32_t */ SEP_NIL, /** - * Separation logic empty heap. - * - * Parameters: - * - 1: Term of the same sort as the sort of the location of the heap - * that is constrained to be empty - * - 2: Term of the same sort as the data sort of the heap that is - * that is constrained to be empty + * Separation logic empty heap constraint * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(Kind kind, const std::vector& children) const` + * - `Solver::mkTerm(Kind kind) const` */ SEP_EMP, /** diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 68499ad0d..982063b6e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1756,16 +1756,7 @@ termAtomic[cvc5::api::Term& atomTerm] // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity // as a 32-bit floating-point constant) | LPAREN_TOK INDEX_TOK - ( EMP_TOK - sortSymbol[type,CHECK_DECLARED] - sortSymbol[type2,CHECK_DECLARED] - { - // Empty heap constant in seperation logic - api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1"); - api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2"); - atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); - } - | CHAR_TOK HEX_LITERAL + ( CHAR_TOK HEX_LITERAL { std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); atomTerm = PARSER_STATE->mkCharConstant(hexStr); @@ -2321,7 +2312,6 @@ ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid'; EXISTS_TOK : 'exists'; FORALL_TOK : 'forall'; -EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp'; CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index fc75ac552..0daddea40 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -676,6 +676,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) // the Boolean sort is a placeholder here since we don't have type info // without type annotation defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); + defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP)); addSepOperators(); } diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 37bf0fd8b..dd85bec69 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -22,9 +22,11 @@ #include "expr/node.h" #include "expr/skolem_manager.h" #include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/quantifiers/quant_util.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_engine.h" namespace cvc5 { namespace preprocessing { @@ -35,9 +37,11 @@ using namespace cvc5::theory; namespace { -Node preSkolemEmp(Node n, - bool pol, - std::map>& visited) +Node preSkolemEmp(TypeNode locType, + TypeNode dataType, + Node n, + bool pol, + std::map>& visited) { std::map::iterator it = visited[pol].find(n); if (it == visited[pol].end()) @@ -51,11 +55,10 @@ Node preSkolemEmp(Node n, { if (!pol) { - TypeNode tnx = n[0].getType(); - TypeNode tny = n[1].getType(); Node x = - sm->mkDummySkolem("ex", tnx, "skolem location for negated emp"); - Node y = sm->mkDummySkolem("ey", tny, "skolem data for negated emp"); + sm->mkDummySkolem("ex", locType, "skolem location for negated emp"); + Node y = + sm->mkDummySkolem("ey", dataType, "skolem data for negated emp"); return nm ->mkNode(kind::SEP_STAR, nm->mkNode(kind::SEP_PTO, x, y), @@ -78,7 +81,7 @@ Node preSkolemEmp(Node n, Node nc = n[i]; if (newHasPol) { - nc = preSkolemEmp(n[i], newPol, visited); + nc = preSkolemEmp(locType, dataType, n[i], newPol, visited); childChanged = childChanged || nc != n[i]; } children.push_back(nc); @@ -105,12 +108,20 @@ SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext) PreprocessingPassResult SepSkolemEmp::applyInternal( AssertionPipeline* assertionsToPreprocess) { + TypeNode locType, dataType; + if (!d_preprocContext->getTheoryEngine()->getSepHeapTypes(locType, dataType)) + { + Warning() << "SepSkolemEmp::applyInternal: failed to get separation logic " + "heap types during preprocessing" + << std::endl; + return PreprocessingPassResult::NO_CONFLICT; + } std::map> visited; for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { Node prev = (*assertionsToPreprocess)[i]; bool pol = true; - Node next = preSkolemEmp(prev, pol, visited); + Node next = preSkolemEmp(locType, dataType, prev, pol, visited); if (next != prev) { assertionsToPreprocess->replace(i, rewrite(next)); diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 17dfed893..598bec636 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -14,7 +14,7 @@ rewriter ::cvc5::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter. nullaryoperator SEP_NIL "separation nil" -operator SEP_EMP 2 "separation empty heap" +nullaryoperator SEP_EMP "separation logic empty heap constraint" operator SEP_PTO 2 "points to relation" operator SEP_STAR 2: "separation star" operator SEP_WAND 2 "separation magic wand" diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index dc72783c0..bcf5c78f7 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -78,8 +78,14 @@ void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT) ss << d_type_ref << " -> " << d_type_data; throw LogicException(ss.str()); } - Node nullAtom; - registerRefDataTypes(locT, dataT, nullAtom); + // otherwise set it + Trace("sep-type") << "Sep: assume location type " << locT + << " is associated with data type " << dataT << std::endl; + d_loc_to_data_type[locT] = dataT; + // for now, we only allow heap constraints of one type + d_type_ref = locT; + d_type_data = dataT; + d_bound_kind[locT] = bound_default; } TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; } @@ -107,7 +113,7 @@ void TheorySep::preRegisterTerm(TNode n) Kind k = n.getKind(); if (k == SEP_PTO || k == SEP_EMP || k == SEP_STAR || k == SEP_WAND) { - registerRefDataTypesAtom(n); + ensureHeapTypesFor(n); } } @@ -175,6 +181,7 @@ void TheorySep::computeCareGraph() { void TheorySep::postProcessModel( TheoryModel* m ){ Trace("sep-model") << "Printing model for TheorySep..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); std::vector< Node > sep_children; Node m_neq; Node m_heap; @@ -228,17 +235,18 @@ void TheorySep::postProcessModel( TheoryModel* m ){ } Node nil = getNilRef( it->first ); Node vnil = d_valuation.getModel()->getRepresentative( nil ); - m_neq = NodeManager::currentNM()->mkNode( kind::EQUAL, nil, vnil ); + m_neq = nm->mkNode(kind::EQUAL, nil, vnil); Trace("sep-model") << "sep.nil = " << vnil << std::endl; Trace("sep-model") << std::endl; if( sep_children.empty() ){ TypeEnumerator te_domain( it->first ); TypeEnumerator te_range( d_loc_to_data_type[it->first] ); - m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range ); + TypeNode boolType = nm->booleanType(); + m_heap = nm->mkNullaryOperator(boolType, kind::SEP_EMP); }else if( sep_children.size()==1 ){ m_heap = sep_children[0]; }else{ - m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children ); + m_heap = nm->mkNode(kind::SEP_STAR, sep_children); } m->setHeapModel( m_heap, m_neq ); } @@ -317,7 +325,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl; // introduce top-level label, add iff - TypeNode refType = getReferenceType(satom); + TypeNode refType = getReferenceType(); Trace("sep-lemma-debug") << "...reference type is : " << refType << std::endl; Node b_lbl = getBaseLabel(refType); @@ -350,7 +358,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) { std::vector children; std::vector c_lems; - TypeNode tn = getReferenceType(satom); + TypeNode tn = getReferenceType(); if (d_reference_bound_max.find(tn) != d_reference_bound_max.end()) { c_lems.push_back(nm->mkNode(SUBSET, slbl, d_reference_bound_max[tn])); @@ -433,8 +441,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) } else { - Node kl = sm->mkDummySkolem("loc", getReferenceType(satom)); - Node kd = sm->mkDummySkolem("data", getDataType(satom)); + Node kl = sm->mkDummySkolem("loc", getReferenceType()); + Node kd = sm->mkDummySkolem("data", getDataType()); Node econc = nm->mkNode( SEP_LABEL, nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true), @@ -718,7 +726,7 @@ void TheorySep::postCheck(Effort level) continue; } needAddLemma = true; - TypeNode tn = getReferenceType(satom); + TypeNode tn = getReferenceType(); tn = nm->mkSetType(tn); // tn = nm->mkSetType(nm->mkRefType(tn)); Node o_b_lbl_mval = d_label_model[slbl].getValue(tn); @@ -933,12 +941,14 @@ TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) { } //for now, assume all constraints are for the same heap type (ensured by logic exceptions thrown in computeReferenceType2) -TypeNode TheorySep::getReferenceType( Node n ) { +TypeNode TheorySep::getReferenceType() const +{ Assert(!d_type_ref.isNull()); return d_type_ref; } -TypeNode TheorySep::getDataType( Node n ) { +TypeNode TheorySep::getDataType() const +{ Assert(!d_type_data.isNull()); return d_type_data; } @@ -980,7 +990,7 @@ int TheorySep::processAssertion( if( it==visited[index].end() ){ Trace("sep-pp-debug") << "process assertion : " << n << ", index = " << index << std::endl; if( n.getKind()==kind::SEP_EMP ){ - registerRefDataTypesAtom(n); + ensureHeapTypesFor(n); if( hasPol && pol ){ references[index][n].clear(); references_strict[index][n] = true; @@ -988,7 +998,7 @@ int TheorySep::processAssertion( card = 1; } }else if( n.getKind()==kind::SEP_PTO ){ - registerRefDataTypesAtom(n); + ensureHeapTypesFor(n); if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){ TypeNode tn1 = n[0].getType(); if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){ @@ -1065,7 +1075,7 @@ int TheorySep::processAssertion( } if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){ - TypeNode tn = getReferenceType( n ); + TypeNode tn = getReferenceType(); Assert(!tn.isNull()); // add references to overall type unsigned bt = d_bound_kind[tn]; @@ -1098,46 +1108,33 @@ int TheorySep::processAssertion( return card; } -void TheorySep::registerRefDataTypesAtom(Node atom) -{ - TypeNode tn1; - TypeNode tn2; - Kind k = atom.getKind(); - if (k == SEP_PTO || k == SEP_EMP) - { - tn1 = atom[0].getType(); - tn2 = atom[1].getType(); - } - else - { - Assert(k == SEP_STAR || k == SEP_WAND); - } - registerRefDataTypes(tn1, tn2, atom); -} - -void TheorySep::registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom) +void TheorySep::ensureHeapTypesFor(Node atom) const { - if (!d_type_ref.isNull()) + Assert(!atom.isNull()); + if (!d_type_ref.isNull() && !d_type_data.isNull()) { - Assert(!atom.isNull()); - // already declared, ensure compatible - if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref)) - || (!tn2.isNull() && !tn2.isComparableTo(d_type_data))) + if (atom.getKind() == SEP_PTO) { - std::stringstream ss; - ss << "ERROR: the separation logic heap type has already been set to " - << d_type_ref << " -> " << d_type_data - << " but we have a constraint that uses different heap types, " - "offending atom is " - << atom << " with associated heap type " << tn1 << " -> " << tn2 - << std::endl; + TypeNode tn1 = atom[0].getType(); + TypeNode tn2 = atom[1].getType(); + // already declared, ensure compatible + if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref)) + || (!tn2.isNull() && !tn2.isComparableTo(d_type_data))) + { + std::stringstream ss; + ss << "ERROR: the separation logic heap type has already been set to " + << d_type_ref << " -> " << d_type_data + << " but we have a constraint that uses different heap types, " + "offending atom is " + << atom << " with associated heap type " << tn1 << " -> " << tn2 + << std::endl; + } } - return; } - // if not declared yet, and we have a separation logic constraint, throw - // an error. - if (!atom.isNull()) + else { + // if not declared yet, and we have a separation logic constraint, throw + // an error. std::stringstream ss; // error, heap not declared ss << "ERROR: the type of the separation logic heap has not been declared " @@ -1146,14 +1143,6 @@ void TheorySep::registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom) << atom << std::endl; throw LogicException(ss.str()); } - // otherwise set it - Trace("sep-type") << "Sep: assume location type " << tn1 - << " is associated with data type " << tn2 << std::endl; - d_loc_to_data_type[tn1] = tn2; - // for now, we only allow heap constraints of one type - d_type_ref = tn1; - d_type_data = tn2; - d_bound_kind[tn1] = bound_default; } void TheorySep::initializeBounds() { @@ -1314,7 +1303,7 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) { if( it==d_label_map[atom][lbl].end() ){ NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - TypeNode refType = getReferenceType( atom ); + TypeNode refType = getReferenceType(); std::stringstream ss; ss << "__Lc" << child; TypeNode ltn = NodeManager::currentNM()->mkSetType(refType); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 985513fd8..b4439c104 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -284,14 +284,14 @@ class TheorySep : public Theory { std::map< Node, HeapAssertInfo * > d_eqc_info; HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false ); - //get global reference/data type - TypeNode getReferenceType( Node n ); - TypeNode getDataType( Node n ); /** - * Register reference data types for atom. Calls the method below for - * the appropriate types. + * Ensure that reference and data types have been set to something that is + * non-null, and compatible with separation logic constraint atom. */ - void registerRefDataTypesAtom(Node atom); + void ensureHeapTypesFor(Node atom) const; + // get global reference/data type + TypeNode getReferenceType() const; + TypeNode getDataType() const; /** * This is called either when: * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 index 45dd29459..5191ecd5b 100644 --- a/test/regress/regress0/sep/dispose-1.smt2 +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -13,7 +13,7 @@ ;----------------- (assert (pto w (as sep.nil Int))) -(assert (not (and (sep (and (_ emp Int Int) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true)))) +(assert (not (and (sep (and sep.emp (= 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 5682a0a02..3f792a4fb 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -3,6 +3,6 @@ (declare-sort Loc 0) (declare-const l Loc) (declare-heap (Loc Loc)) -(assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc)))) +(assert (sep (not sep.emp) (not sep.emp))) (assert (pto l l)) (check-sat) diff --git a/test/regress/regress0/sep/issue3720-check-model.smt2 b/test/regress/regress0/sep/issue3720-check-model.smt2 index 7e9c73cb8..488c558b0 100644 --- a/test/regress/regress0/sep/issue3720-check-model.smt2 +++ b/test/regress/regress0/sep/issue3720-check-model.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --quiet +; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic ALL) (declare-heap (Int Int)) -(assert (_ emp Int Int)) +(assert sep.emp) (check-sat) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index 583457e48..2d35a43d8 100644 --- a/test/regress/regress0/sep/nemp.smt2 +++ b/test/regress/regress0/sep/nemp.smt2 @@ -2,5 +2,5 @@ ; EXPECT: sat (set-logic QF_SEP_LIA) (declare-heap (Int Int)) -(assert (not (_ emp Int Int))) +(assert (not sep.emp)) (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 312c97542..c83e98b66 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -8,6 +8,6 @@ (declare-fun a () U) (declare-fun b () U) -(assert (_ emp U U)) +(assert sep.emp) (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 2a836bef9..1c690cc75 100644 --- a/test/regress/regress0/sep/skolem_emp.smt2 +++ b/test/regress/regress0/sep/skolem_emp.smt2 @@ -2,5 +2,5 @@ ; EXPECT: sat (set-logic QF_ALL) (declare-heap (Int Int)) -(assert (not (_ emp Int Int))) +(assert (not sep.emp)) (check-sat) diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 index 2c742c60f..31c85d62d 100644 --- a/test/regress/regress0/sep/trees-1.smt2 +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -18,7 +18,7 @@ (declare-const r Loc) (define-fun ten-tree0 ((x Loc) (d Int)) Bool -(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))))) +(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and sep.emp (= l (as sep.nil Loc))) (and sep.emp (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10))))) (declare-const dy Int) (declare-const y Loc) @@ -26,7 +26,7 @@ (declare-const z Loc) (define-fun ord-tree0 ((x Loc) (d Int)) Bool -(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)))) +(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and sep.emp (= y (as sep.nil Loc))) (and sep.emp (= 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 02511bbae..d84d900f3 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -2,5 +2,5 @@ ; EXPECT: sat (set-logic QF_ALL) (declare-heap (Int Int)) -(assert (wand (_ emp Int Int) (_ emp Int Int))) +(assert (wand sep.emp sep.emp)) (check-sat) 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) -- 2.30.2