diff options
68 files changed, 368 insertions, 56 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index c0e6bad5f..566bcc3c7 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5194,6 +5194,17 @@ Term Solver::getQuantifierEliminationDisjunct(api::Term q) const CVC4_API_SOLVER_TRY_CATCH_END; } +void Solver::declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK( + d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) + << "Cannot obtain separation logic expressions if not using the " + "separation logic theory."; + d_smtEngine->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode()); + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::getSeparationHeap() const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 13d4f6e23..db57af121 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3158,6 +3158,15 @@ class CVC4_PUBLIC Solver Term getQuantifierEliminationDisjunct(api::Term q) const; /** + * When using separation logic, this sets the location sort and the + * datatype sort to the given ones. This method should be invoked exactly + * once, before any separation logic constraints are provided. + * @param locSort The location sort of the heap + * @param dataSort The data sort of the heap + */ + void declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const; + + /** * When using separation logic, obtain the term for the heap. * @return The term for the heap */ diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 13f4606da..29f997394 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -235,6 +235,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": vector[Term] getUnsatCore() except + Term getValue(Term term) except + vector[Term] getValue(const vector[Term]& terms) except + + void declareSeparationHeap(Sort locSort, Sort dataSort) except + Term getSeparationHeap() except + Term getSeparationNilTerm() except + void pop(uint32_t nscopes) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 16f454311..f945228dd 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -1122,6 +1122,9 @@ cdef class Solver: term.cterm = self.csolver.getSeparationHeap() return term + def declareSeparationHeap(self, Sort locType, Sort dataType): + self.csolver.declareSeparationHeap(locType.csort, dataType.csort) + def getSeparationNilTerm(self): cdef Term term = Term(self) term.cterm = self.csolver.getSeparationNilTerm() diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index fe051f036..40c66eaa5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -895,7 +895,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<api::DatatypeDecl> dts; CVC4::api::Term e, e2; - CVC4::api::Sort t; + CVC4::api::Sort t, s; std::string name; std::vector<std::string> names; std::vector<CVC4::api::Term> terms; @@ -1073,9 +1073,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] } | 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()); } + sortSymbol[s, CHECK_DECLARED] + { cmd->reset(new DeclareHeapCommand(t, s)); } RPAREN_TOK | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new BlockModelCommand()); } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 195247df7..21eb88c8c 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -415,6 +415,13 @@ void Printer::toStreamCmdComment(std::ostream& out, printUnknownCommand(out, "comment"); } +void Printer::toStreamCmdDeclareHeap(std::ostream& out, + TypeNode locType, + TypeNode dataType) const +{ + printUnknownCommand(out, "declare-heap"); +} + void Printer::toStreamCmdCommandSequence( std::ostream& out, const std::vector<Command*>& sequence) const { diff --git a/src/printer/printer.h b/src/printer/printer.h index 84262d992..ffacaa5d8 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -256,6 +256,10 @@ class Printer /** Print comment command */ virtual void toStreamCmdComment(std::ostream& out, const std::string& comment) const; + /** Declare heap command */ + virtual void toStreamCmdDeclareHeap(std::ostream& out, + TypeNode locType, + TypeNode dataType) const; /** Print command sequence command */ virtual void toStreamCmdCommandSequence( diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index bc6902305..032d26511 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1938,6 +1938,13 @@ void Smt2Printer::toStreamCmdComment(std::ostream& out, out << "(set-info :notes \"" << s << "\")" << std::endl; } +void Smt2Printer::toStreamCmdDeclareHeap(std::ostream& out, + TypeNode locType, + TypeNode dataType) const +{ + out << "(declare-heap (" << locType << " " << dataType << "))" << std::endl; +} + void Smt2Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index f4783c955..3fc144d46 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -217,6 +217,11 @@ class Smt2Printer : public CVC4::Printer void toStreamCmdComment(std::ostream& out, const std::string& comment) const override; + /** Print declare-heap command */ + void toStreamCmdDeclareHeap(std::ostream& out, + TypeNode locType, + TypeNode dataType) const override; + /** Print command sequence command */ void toStreamCmdCommandSequence( std::ostream& out, const std::vector<Command*>& sequence) const override; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 58ac57cc9..b33fe5ad9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1425,9 +1425,43 @@ void DefineFunctionRecCommand::toStream(std::ostream& out, formals, api::termVectorToNodes(d_formulas)); } +/* -------------------------------------------------------------------------- */ +/* class DeclareHeapCommand */ +/* -------------------------------------------------------------------------- */ +DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort) + : d_locSort(locSort), d_dataSort(dataSort) +{ +} + +api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; } +api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; } + +void DeclareHeapCommand::invoke(api::Solver* solver) +{ + solver->declareSeparationHeap(d_locSort, d_dataSort); +} + +Command* DeclareHeapCommand::clone() const +{ + return new DeclareHeapCommand(d_locSort, d_dataSort); +} + +std::string DeclareHeapCommand::getCommandName() const +{ + return "declare-heap"; +} + +void DeclareHeapCommand::toStream(std::ostream& out, + int toDepth, + size_t dag, + OutputLanguage language) const +{ + Printer::getPrinter(language)->toStreamCmdDeclareHeap( + out, d_locSort.getTypeNode(), d_dataSort.getTypeNode()); +} /* -------------------------------------------------------------------------- */ -/* class SetUserAttribute */ +/* class SetUserAttributeCommand */ /* -------------------------------------------------------------------------- */ SetUserAttributeCommand::SetUserAttributeCommand( diff --git a/src/smt/command.h b/src/smt/command.h index d2ce99f2f..438f9febb 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -511,7 +511,6 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DefineNamedFunctionCommand */ @@ -562,6 +561,34 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command }; /* class DefineFunctionRecCommand */ /** + * In separation logic inputs, which is an extension of smt2 inputs, this + * corresponds to the command: + * (declare-heap (T U)) + * where T is the location sort and U is the data sort. + */ +class CVC4_PUBLIC DeclareHeapCommand : public Command +{ + public: + DeclareHeapCommand(api::Sort locSort, api::Sort dataSort); + api::Sort getLocationSort() const; + api::Sort getDataSort() const; + void invoke(api::Solver* solver) override; + Command* clone() const override; + std::string getCommandName() const override; + void toStream( + std::ostream& out, + int toDepth = -1, + size_t dag = 1, + OutputLanguage language = language::output::LANG_AUTO) const override; + + protected: + /** The location sort */ + api::Sort d_locSort; + /** The data sort */ + api::Sort d_dataSort; +}; + +/** * The command when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! expr :attr) */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index dc5338199..a5861c6b0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -65,6 +65,7 @@ #include "theory/logic_info.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/rewriter.h" +#include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" #include "util/hash.h" #include "util/random.h" @@ -1448,6 +1449,28 @@ std::vector<Node> SmtEngine::getExpandedAssertions() return eassertsProc; } +void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) +{ + if (!d_logic.isTheoryEnabled(THEORY_SEP)) + { + const char* msg = + "Cannot declare heap if not using the separation logic theory."; + throw RecoverableModalException(msg); + } + SmtScope smts(this); + finishInit(); + TheoryEngine* te = getTheoryEngine(); + te->declareSepHeap(locT, dataT); +} + +bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) +{ + SmtScope smts(this); + finishInit(); + TheoryEngine* te = getTheoryEngine(); + return te->getSepHeapTypes(locT, dataT); +} + Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; } Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } @@ -1483,21 +1506,28 @@ void SmtEngine::checkUnsatCore() { Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; UnsatCore core = getUnsatCore(); - SmtEngine coreChecker(d_exprManager, &d_options); - coreChecker.setIsInternalSubsolver(); - coreChecker.setLogic(getLogicInfo()); - coreChecker.getOptions().set(options::checkUnsatCores, false); + // initialize the core checker + std::unique_ptr<SmtEngine> coreChecker; + initializeSubsolver(coreChecker); + coreChecker->getOptions().set(options::checkUnsatCores, false); + + // set up separation logic heap if necessary + TypeNode sepLocType, sepDataType; + if (getSepHeapTypes(sepLocType, sepDataType)) + { + coreChecker->declareSepHeap(sepLocType, sepDataType); + } Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl; for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { Node assertionAfterExpansion = expandDefinitions(*i); Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << ", expanded to " << assertionAfterExpansion << "\n"; - coreChecker.assertFormula(assertionAfterExpansion); + coreChecker->assertFormula(assertionAfterExpansion); } Result r; try { - r = coreChecker.checkSat(); + r = coreChecker->checkSat(); } catch(...) { throw; } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index de0daffd0..0661ae918 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -309,6 +309,23 @@ class CVC4_PUBLIC SmtEngine */ Result blockModelValues(const std::vector<Node>& exprs); + /** + * Declare heap. For smt2 inputs, this is called when the command + * (declare-heap (locT datat)) is invoked by the user. This sets locT as the + * location type and dataT is the data type for the heap. This command should + * be executed only once, and must be invoked before solving separation logic + * inputs. + */ + void declareSepHeap(TypeNode locT, TypeNode dataT); + + /** + * Get the separation heap types, which extracts which types were passed to + * the method above. + * + * @return true if the separation logic heap types have been declared. + */ + bool getSepHeapTypes(TypeNode& locT, TypeNode& dataT); + /** When using separation logic, obtain the expression for the heap. */ Node getSepHeapExpr(); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 013c61e52..1b25bb0f4 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -69,6 +69,22 @@ TheorySep::~TheorySep() { } } +void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT) +{ + if (!d_type_ref.isNull()) + { + TypeNode te1 = d_loc_to_data_type.begin()->first; + std::stringstream ss; + ss << "ERROR: cannot declare heap types for separation logic more than " + "once. We are declaring heap of type "; + ss << locT << " -> " << dataT << ", but we already have "; + ss << d_type_ref << " -> " << d_type_data; + throw LogicException(ss.str()); + } + Node nullAtom; + registerRefDataTypes(locT, dataT, nullAtom); +} + TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; } bool TheorySep::needsEqualityEngine(EeSetupInfo& esi) @@ -239,7 +255,6 @@ void TheorySep::postProcessModel( TheoryModel* m ){ void TheorySep::presolve() { Trace("sep-pp") << "Presolving" << std::endl; - //TODO: cleanup if incremental? } @@ -1119,48 +1134,43 @@ int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& } void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){ - //separation logic is effectively enabled when we find at least one spatial constraint occurs in the input - if( options::incrementalSolving() ){ - std::stringstream ss; - ss << "ERROR: cannot use separation logic in incremental mode." << std::endl; - throw LogicException(ss.str()); - } - std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 ); - if( itt==d_loc_to_data_type.end() ){ - if( !d_loc_to_data_type.empty() ){ - TypeNode te1 = d_loc_to_data_type.begin()->first; + if (!d_type_ref.isNull()) + { + Assert(!atom.isNull()); + // already declared, ensure compatible + if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref)) + || (!tn2.isNull() && !tn2.isComparableTo(d_type_data))) + { std::stringstream ss; - ss << "ERROR: specifying heap constraints for two different types : " << tn1 << " -> " << tn2 << " and " << te1 << " -> " << d_loc_to_data_type[te1] << std::endl; - throw LogicException(ss.str()); - Assert(false); - } - if( tn2.isNull() ){ - Trace("sep-type") << "Sep: assume location type " << tn1 << " (from " << atom << ")" << std::endl; - }else{ - Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << 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; - }else{ - if( !tn2.isNull() ){ - if( itt->second!=tn2 ){ - if( itt->second.isNull() ){ - Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl; - //now we know data type - d_loc_to_data_type[tn1] = tn2; - d_type_data = tn2; - }else{ - std::stringstream ss; - ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl; - throw LogicException(ss.str()); - Assert(false); - } - } + 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()) + { + std::stringstream ss; + // error, heap not declared + ss << "ERROR: the type of the separation logic heap has not been declared " + "(e.g. via a declare-heap command), and we have a separation logic " + "constraint " + << 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() { diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index ac87ebe67..2cd7aba91 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -79,6 +79,15 @@ class TheorySep : public Theory { ProofNodeManager* pnm = nullptr); ~TheorySep(); + /** + * Declare heap. For smt2 inputs, this is called when the command + * (declare-heap (locT datat)) is invoked by the user. This sets locT as the + * location type and dataT is the data type for the heap. This command can be + * executed once only, and must be invoked before solving separation logic + * inputs. + */ + void declareSepHeap(TypeNode locT, TypeNode dataT) override; + //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; @@ -274,7 +283,14 @@ class TheorySep : public Theory { //get global reference/data type TypeNode getReferenceType( Node n ); TypeNode getDataType( Node n ); - void registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ); + /** + * This is called either when: + * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or + * (B) an atom specifying the heap type tn1/tn2 is registered to this theory. + * We set the heap type if we are are case (A), and check whether the + * heap type is consistent in the case of (B). + */ + void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom); //get location/data type //get the base label for the spatial assertion Node getBaseLabel( TypeNode tn ); diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index cedb838af..ed10e85ae 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -51,11 +51,11 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions())); smte->setIsInternalSubsolver(); smte->setLogic(smtCurr->getLogicInfo()); + // set the options if (needsTimeout) { smte->setTimeLimit(timeout); } - smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); } Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index d34729dec..f68900ccc 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -31,7 +31,16 @@ namespace theory { /** * This function initializes the smt engine smte to check the satisfiability - * of the argument "query". + * of the argument "query". It takes the logic and options of the current + * SMT engine in scope. + * + * Notice this method intentionally does not fully initialize smte. This means + * that the options of smte can still be modified after it is returned by + * this method. + * + * Notice that some aspects of subsolvers are not incoporated by this call. + * For example, the type of separation logic heaps is not set on smte, even + * if the current SMT engine has declared a separation logic heap. * * @param smte The smt engine pointer to initialize * @param needsTimeout Whether we would like to set a timeout diff --git a/src/theory/theory.h b/src/theory/theory.h index 9519624b7..6256360e4 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -249,6 +249,15 @@ class Theory { } /** + * Set separation logic heap. This is called when the location and data + * types for separation logic are determined. This should be called at + * most once, before solving. + * + * This currently should be overridden by the separation logic theory only. + */ + virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {} + + /** * The theory that owns the uninterpreted sort. */ static TheoryId s_uninterpretedSortOwner; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 706149d86..3a155b9ad 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1116,6 +1116,42 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; } +bool TheoryEngine::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const +{ + if (d_sepLocType.isNull()) + { + return false; + } + locType = d_sepLocType; + dataType = d_sepDataType; + return true; +} + +void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT) +{ + Theory* tsep = theoryOf(THEORY_SEP); + if (tsep == nullptr) + { + Assert(false) << "TheoryEngine::declareSepHeap called without the " + "separation logic theory enabled"; + return; + } + + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + theoryOf(THEORY)->declareSepHeap(locT, dataT); + + // notify each theory using the statement above + CVC4_FOR_EACH_THEORY; + + // remember the types we have set + d_sepLocType = locT; + d_sepDataType = dataT; +} + theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { Assert(a.getType().isComparableTo(b.getType())); return d_sharedSolver->getEqualityStatus(a, b); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e47dbbc6f..088e413bb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -139,6 +139,9 @@ class TheoryEngine { * the cost of walking the DAG on registration, etc. */ const LogicInfo& d_logicInfo; + /** The separation logic location and data types */ + TypeNode d_sepLocType; + TypeNode d_sepDataType; /** Reference to the output manager of the smt engine */ OutputManager& d_outMgr; @@ -637,6 +640,16 @@ class TheoryEngine { } /** get the logic info used by this theory engine */ const LogicInfo& getLogicInfo() const; + /** get the separation logic heap types */ + bool getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const; + + /** + * Declare heap. This is used for separation logics to set the location + * and data types. It should be called only once, and before any separation + * logic constraints are asserted to this theory engine. + */ + void declareSepHeap(TypeNode locT, TypeNode dataT); + /** * Returns the equality status of the two terms, from the theory * that owns the domain type. The types of a and b must be the same. diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp index 1b1efb07e..cc20f1ed1 100644 --- a/test/api/sep_log_api.cpp +++ b/test/api/sep_log_api.cpp @@ -46,6 +46,8 @@ int validate_exception(void) /* Our integer type */ Sort integer = slv.getIntegerSort(); + /** we intentionally do not set the separation logic heap */ + /* Our SMT constants */ Term x = slv.mkConst(integer, "x"); Term y = slv.mkConst(integer, "y"); @@ -134,6 +136,9 @@ int validate_getters(void) /* Our integer type */ Sort integer = slv.getIntegerSort(); + /** Declare the separation logic heap types */ + slv.declareSeparationHeap(integer, integer); + /* A "random" constant */ Term random_constant = slv.mkInteger(0xDEADBEEF); diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 index 25a38b018..aff32e241 100644 --- a/test/regress/regress0/sep/dispose-1.smt2 +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -1,6 +1,8 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) + (declare-const w Int) (declare-const w1 Int) (declare-const w2 Int) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 20421e735..454b73f64 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -2,6 +2,7 @@ (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) +(declare-heap (Loc Loc)) (assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc)))) (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 6130c0ca8..7e9c73cb8 100644 --- a/test/regress/regress0/sep/issue3720-check-model.smt2 +++ b/test/regress/regress0/sep/issue3720-check-model.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --quiet ; EXPECT: sat (set-logic ALL) +(declare-heap (Int Int)) (assert (_ emp Int Int)) (check-sat) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index 2eaf664cd..583457e48 100644 --- a/test/regress/regress0/sep/nemp.smt2 +++ b/test/regress/regress0/sep/nemp.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_SEP_LIA) +(declare-heap (Int Int)) (assert (not (_ emp Int Int))) (check-sat) diff --git a/test/regress/regress0/sep/nil-no-elim.smt2 b/test/regress/regress0/sep/nil-no-elim.smt2 index e9aa3807a..6e6656865 100644 --- a/test/regress/regress0/sep/nil-no-elim.smt2 +++ b/test/regress/regress0/sep/nil-no-elim.smt2 @@ -3,6 +3,7 @@ (declare-sort U 0) (declare-fun f (U) U) (declare-fun a () U) +(declare-heap (U Int)) (assert (= (as sep.nil U) (f a))) diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2 index c807757d1..e57e50ea2 100644 --- a/test/regress/regress0/sep/nspatial-simp.smt2 +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -3,6 +3,7 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) +(declare-heap (Int Int)) (assert (sep (= x 0) (not (= x 5)))) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 index 28ed5c47b..f980ac13f 100644 --- a/test/regress/regress0/sep/pto-01.smt2 +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 index ab1cea0c8..111048c70 100644 --- a/test/regress/regress0/sep/pto-02.smt2 +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 index a93fc4db8..8e577d5b7 100644 --- a/test/regress/regress0/sep/sep-01.smt2 +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 index 9522e2420..b843c1eda 100644 --- a/test/regress/regress0/sep/sep-plus1.smt2 +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index f620e9360..fc7bd0a51 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -1,7 +1,8 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) - (declare-sort U 0) +(declare-heap (U U)) + (declare-fun x () U) (declare-fun y () U) (declare-fun a () U) diff --git a/test/regress/regress0/sep/simple-080420-const-sets.smt2 b/test/regress/regress0/sep/simple-080420-const-sets.smt2 index 1d85fb133..785017d5c 100644 --- a/test/regress/regress0/sep/simple-080420-const-sets.smt2 +++ b/test/regress/regress0/sep/simple-080420-const-sets.smt2 @@ -3,6 +3,7 @@ (set-logic QF_ALL_SUPPORTED) (set-option :produce-models true) (set-info :status sat) +(declare-heap (Int Int)) (declare-fun x () Int) ; works diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2 index 7798f6bed..aac8382a7 100644 --- a/test/regress/regress0/sep/skolem_emp.smt2 +++ b/test/regress/regress0/sep/skolem_emp.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) +(declare-heap (Int Int)) (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 7daf012e2..46d96e84c 100644 --- a/test/regress/regress0/sep/trees-1.smt2 +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -5,6 +5,7 @@ (declare-const loc0 Loc) (declare-datatypes ((Node 0)) (((node (data Int) (left Loc) (right Loc))))) +(declare-heap (Loc Node)) (declare-fun data0 () Node) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 4828646cb..95156a20c 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) +(declare-heap (Int Int)) (assert (wand (_ emp Int Int) (_ emp Int Int))) (check-sat) diff --git a/test/regress/regress1/sep/chain-int.smt2 b/test/regress/regress1/sep/chain-int.smt2 index ebe52fa46..6aaca31c5 100644 --- a/test/regress/regress1/sep/chain-int.smt2 +++ b/test/regress/regress1/sep/chain-int.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/crash1220.smt2 b/test/regress/regress1/sep/crash1220.smt2 index f68434f33..4df23fd80 100644 --- a/test/regress/regress1/sep/crash1220.smt2 +++ b/test/regress/regress1/sep/crash1220.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const a Int) diff --git a/test/regress/regress1/sep/dispose-list-4-init.smt2 b/test/regress/regress1/sep/dispose-list-4-init.smt2 index b3e2088b1..0ee63cc8a 100644 --- a/test/regress/regress1/sep/dispose-list-4-init.smt2 +++ b/test/regress/regress1/sep/dispose-list-4-init.smt2 @@ -3,6 +3,7 @@ (set-logic QF_ALL_SUPPORTED) (declare-sort Loc 0) +(declare-heap (Loc Loc)) (declare-const w Loc) (declare-const u1 Loc) diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2 index 118e63f07..a0921aa31 100644 --- a/test/regress/regress1/sep/emp2-quant-unsat.smt2 +++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2 @@ -4,6 +4,7 @@ (set-info :status unsat) (declare-sort U 0) (declare-fun u () U) +(declare-heap (U U)) (assert (sep (not (_ emp U U)) (not (_ emp U U)))) diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2 index 1f3338ed7..fac9d6b9d 100644 --- a/test/regress/regress1/sep/finite-witness-sat.smt2 +++ b/test/regress/regress1/sep/finite-witness-sat.smt2 @@ -3,6 +3,7 @@ (set-logic ALL_SUPPORTED) (declare-sort Loc 0) (declare-const l Loc) +(declare-heap (Loc Loc)) (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 356405869..49420145e 100644 --- a/test/regress/regress1/sep/fmf-nemp-2.smt2 +++ b/test/regress/regress1/sep/fmf-nemp-2.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic ALL_SUPPORTED) (declare-sort U 0) +(declare-heap (U Int)) (declare-fun u1 () U) (declare-fun u2 () U) (assert (not (= u1 u2))) diff --git a/test/regress/regress1/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2 index b857aec2a..41078391a 100644 --- a/test/regress/regress1/sep/loop-1220.smt2 +++ b/test/regress/regress1/sep/loop-1220.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const a Int) diff --git a/test/regress/regress1/sep/pto-04.smt2 b/test/regress/regress1/sep/pto-04.smt2 index 9b0afda7a..e3d3ea7a1 100644 --- a/test/regress/regress1/sep/pto-04.smt2 +++ b/test/regress/regress1/sep/pto-04.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x1 Int) (declare-const x2 Int) diff --git a/test/regress/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2 index 662682ec3..bb4e40308 100644 --- a/test/regress/regress1/sep/quant_wand.smt2 +++ b/test/regress/regress1/sep/quant_wand.smt2 @@ -2,6 +2,7 @@ ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const u Int) diff --git a/test/regress/regress1/sep/sep-02.smt2 b/test/regress/regress1/sep/sep-02.smt2 index 6f190d964..a67394d90 100644 --- a/test/regress/regress1/sep/sep-02.smt2 +++ b/test/regress/regress1/sep/sep-02.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-03.smt2 b/test/regress/regress1/sep/sep-03.smt2 index 8dce5acc7..f29d081fc 100644 --- a/test/regress/regress1/sep/sep-03.smt2 +++ b/test/regress/regress1/sep/sep-03.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-find2.smt2 b/test/regress/regress1/sep/sep-find2.smt2 index 3d6188894..412caee9b 100644 --- a/test/regress/regress1/sep/sep-find2.smt2 +++ b/test/regress/regress1/sep/sep-find2.smt2 @@ -1,5 +1,6 @@ (set-logic QF_SEP_LIA) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x1 Int) (declare-const x2 Int) diff --git a/test/regress/regress1/sep/sep-fmf-priority.smt2 b/test/regress/regress1/sep/sep-fmf-priority.smt2 index fe3af1b35..8aed93119 100644 --- a/test/regress/regress1/sep/sep-fmf-priority.smt2 +++ b/test/regress/regress1/sep/sep-fmf-priority.smt2 @@ -5,6 +5,7 @@ (declare-sort Loc 0) (declare-const l Loc) (declare-const x Loc) +(declare-heap (Loc Loc)) (assert (wand (pto x x) false)) (assert (forall ((x Loc) (y Loc)) (not (pto x y)))) diff --git a/test/regress/regress1/sep/sep-neg-1refine.smt2 b/test/regress/regress1/sep/sep-neg-1refine.smt2 index ab12c6461..81b107ab5 100644 --- a/test/regress/regress1/sep/sep-neg-1refine.smt2 +++ b/test/regress/regress1/sep/sep-neg-1refine.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-neg-nstrict.smt2 b/test/regress/regress1/sep/sep-neg-nstrict.smt2 index 425e5ce3c..6594a1075 100644 --- a/test/regress/regress1/sep/sep-neg-nstrict.smt2 +++ b/test/regress/regress1/sep/sep-neg-nstrict.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-neg-nstrict2.smt2 b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 index 7ada6ff06..0243282a3 100644 --- a/test/regress/regress1/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-neg-simple.smt2 b/test/regress/regress1/sep/sep-neg-simple.smt2 index 7b6fc69e9..8b23a6da8 100644 --- a/test/regress/regress1/sep/sep-neg-simple.smt2 +++ b/test/regress/regress1/sep/sep-neg-simple.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-neg-swap.smt2 b/test/regress/regress1/sep/sep-neg-swap.smt2 index 53f890b0d..ba83f2575 100644 --- a/test/regress/regress1/sep/sep-neg-swap.smt2 +++ b/test/regress/regress1/sep/sep-neg-swap.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-nterm-again.smt2 b/test/regress/regress1/sep/sep-nterm-again.smt2 index 3e595b5e9..43fb7b00d 100644 --- a/test/regress/regress1/sep/sep-nterm-again.smt2 +++ b/test/regress/regress1/sep/sep-nterm-again.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-nterm-val-model.smt2 b/test/regress/regress1/sep/sep-nterm-val-model.smt2 index d4fb0fd52..635f0895a 100644 --- a/test/regress/regress1/sep/sep-nterm-val-model.smt2 +++ b/test/regress/regress1/sep/sep-nterm-val-model.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/sep-simp-unc.smt2 b/test/regress/regress1/sep/sep-simp-unc.smt2 index cedbb53eb..88950d655 100644 --- a/test/regress/regress1/sep/sep-simp-unc.smt2 +++ b/test/regress/regress1/sep/sep-simp-unc.smt2 @@ -3,6 +3,7 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-sort U 0) +(declare-heap (U U)) (declare-fun x () U) (declare-fun y () U) (declare-fun a () U) diff --git a/test/regress/regress1/sep/simple-neg-sat.smt2 b/test/regress/regress1/sep/simple-neg-sat.smt2 index 70927ad82..929a8e66f 100644 --- a/test/regress/regress1/sep/simple-neg-sat.smt2 +++ b/test/regress/regress1/sep/simple-neg-sat.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const 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 91b07093c..1b7932dc4 100644 --- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 @@ -1,5 +1,6 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/split-find-unsat.smt2 b/test/regress/regress1/sep/split-find-unsat.smt2 index 1a9e76a8a..60ab5d038 100644 --- a/test/regress/regress1/sep/split-find-unsat.smt2 +++ b/test/regress/regress1/sep/split-find-unsat.smt2 @@ -2,6 +2,7 @@ ; EXPECT: unsat (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) +(declare-heap (Int Int)) (declare-const x Int) (declare-const y Int) diff --git a/test/regress/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2 index 99116c9d1..556be6c18 100644 --- a/test/regress/regress1/sep/wand-0526-sat.smt2 +++ b/test/regress/regress1/sep/wand-0526-sat.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) +(declare-heap (Int Int)) (declare-fun x () Int) (declare-fun y () Int) (declare-fun u () Int) diff --git a/test/regress/regress1/sep/wand-false.smt2 b/test/regress/regress1/sep/wand-false.smt2 index 65500f775..9f95c06b7 100644 --- a/test/regress/regress1/sep/wand-false.smt2 +++ b/test/regress/regress1/sep/wand-false.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (pto x x) false)) (check-sat) diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2 index 702f03a02..4ecc8ad1e 100644 --- a/test/regress/regress1/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) +(declare-heap (Int Int)) (declare-fun x () Int) (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 352be5777..5b7c92a4a 100644 --- a/test/regress/regress1/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (pto x 1) (_ emp Int Int))) (check-sat) diff --git a/test/regress/regress1/sep/wand-simp-sat.smt2 b/test/regress/regress1/sep/wand-simp-sat.smt2 index 120683f74..ec63a762e 100644 --- a/test/regress/regress1/sep/wand-simp-sat.smt2 +++ b/test/regress/regress1/sep/wand-simp-sat.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) +(declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 1))) (check-sat) diff --git a/test/regress/regress1/sep/wand-simp-sat2.smt2 b/test/regress/regress1/sep/wand-simp-sat2.smt2 index c684d16ad..315071c05 100644 --- a/test/regress/regress1/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress1/sep/wand-simp-sat2.smt2 @@ -2,6 +2,7 @@ ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) +(declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) (check-sat) diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2 index 8c038e3d7..da1d8bd51 100644 --- a/test/regress/regress1/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress1/sep/wand-simp-unsat.smt2 @@ -2,6 +2,7 @@ ; EXPECT: unsat (set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) +(declare-heap (Int Int)) (assert (wand (pto x 1) (pto x 3))) (assert (_ emp Int Int)) (check-sat) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 1324e3890..f292acc88 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -118,6 +118,7 @@ class SolverBlack : public CxxTest::TestSuite void testGetValue3(); void testGetQuantifierElimination(); void testGetQuantifierEliminationDisjunct(); + void testDeclareSeparationHeap(); void testGetSeparationHeapTerm1(); void testGetSeparationHeapTerm2(); void testGetSeparationHeapTerm3(); @@ -1697,6 +1698,16 @@ void SolverBlack::testGetQuantifierEliminationDisjunct() TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierEliminationDisjunct(forall)); } +void SolverBlack::testDeclareSeparationHeap() +{ + d_solver->setLogic("ALL_SUPPORTED"); + Sort integer = d_solver->getIntegerSort(); + TS_ASSERT_THROWS_NOTHING(d_solver->declareSeparationHeap(integer, integer)); + // cannot declare separation logic heap more than once + TS_ASSERT_THROWS(d_solver->declareSeparationHeap(integer, integer), + CVC4ApiException&); +} + namespace { /** * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks @@ -1705,6 +1716,8 @@ namespace { void checkSimpleSeparationConstraints(Solver* solver) { Sort integer = solver->getIntegerSort(); + // declare the separation heap + solver->declareSeparationHeap(integer, integer); Term x = solver->mkConst(integer, "x"); Term p = solver->mkConst(integer, "p"); Term heap = solver->mkTerm(Kind::SEP_PTO, p, x); |