From c2757f0440c5d5b841e05c60d1fd93dc9ee3763a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 10 Nov 2020 07:43:19 -0600 Subject: [PATCH] Add proper support for the declare-heap command for separation logic (#5405) This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic. This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred. Fixes #5343, fixes #4926. Work towards CVC4/cvc4-wishues#22. --- src/api/cvc4cpp.cpp | 11 +++ src/api/cvc4cpp.h | 9 ++ src/api/python/cvc4.pxd | 1 + src/api/python/cvc4.pxi | 3 + src/parser/smt2/Smt2.g | 7 +- src/printer/printer.cpp | 7 ++ src/printer/printer.h | 4 + src/printer/smt2/smt2_printer.cpp | 7 ++ src/printer/smt2/smt2_printer.h | 5 ++ src/smt/command.cpp | 36 +++++++- src/smt/command.h | 29 +++++- src/smt/smt_engine.cpp | 42 +++++++-- src/smt/smt_engine.h | 17 ++++ src/theory/sep/theory_sep.cpp | 90 ++++++++++--------- src/theory/sep/theory_sep.h | 18 +++- src/theory/smt_engine_subsolver.cpp | 2 +- src/theory/smt_engine_subsolver.h | 11 ++- src/theory/theory.h | 9 ++ src/theory/theory_engine.cpp | 36 ++++++++ src/theory/theory_engine.h | 13 +++ test/api/sep_log_api.cpp | 5 ++ test/regress/regress0/sep/dispose-1.smt2 | 2 + test/regress/regress0/sep/dup-nemp.smt2 | 1 + .../regress0/sep/issue3720-check-model.smt2 | 1 + test/regress/regress0/sep/nemp.smt2 | 1 + test/regress/regress0/sep/nil-no-elim.smt2 | 1 + test/regress/regress0/sep/nspatial-simp.smt2 | 1 + test/regress/regress0/sep/pto-01.smt2 | 1 + test/regress/regress0/sep/pto-02.smt2 | 1 + test/regress/regress0/sep/sep-01.smt2 | 1 + test/regress/regress0/sep/sep-plus1.smt2 | 1 + .../regress0/sep/sep-simp-unsat-emp.smt2 | 3 +- .../sep/simple-080420-const-sets.smt2 | 1 + test/regress/regress0/sep/skolem_emp.smt2 | 1 + test/regress/regress0/sep/trees-1.smt2 | 1 + test/regress/regress0/sep/wand-crash.smt2 | 1 + test/regress/regress1/sep/chain-int.smt2 | 1 + test/regress/regress1/sep/crash1220.smt2 | 1 + .../regress1/sep/dispose-list-4-init.smt2 | 1 + .../regress1/sep/emp2-quant-unsat.smt2 | 1 + .../regress1/sep/finite-witness-sat.smt2 | 1 + test/regress/regress1/sep/fmf-nemp-2.smt2 | 1 + test/regress/regress1/sep/loop-1220.smt2 | 1 + test/regress/regress1/sep/pto-04.smt2 | 1 + test/regress/regress1/sep/quant_wand.smt2 | 1 + test/regress/regress1/sep/sep-02.smt2 | 1 + test/regress/regress1/sep/sep-03.smt2 | 1 + test/regress/regress1/sep/sep-find2.smt2 | 1 + .../regress1/sep/sep-fmf-priority.smt2 | 1 + .../regress/regress1/sep/sep-neg-1refine.smt2 | 1 + .../regress/regress1/sep/sep-neg-nstrict.smt2 | 1 + .../regress1/sep/sep-neg-nstrict2.smt2 | 1 + test/regress/regress1/sep/sep-neg-simple.smt2 | 1 + test/regress/regress1/sep/sep-neg-swap.smt2 | 1 + .../regress/regress1/sep/sep-nterm-again.smt2 | 1 + .../regress1/sep/sep-nterm-val-model.smt2 | 1 + test/regress/regress1/sep/sep-simp-unc.smt2 | 1 + test/regress/regress1/sep/simple-neg-sat.smt2 | 1 + .../regress1/sep/split-find-unsat-w-emp.smt2 | 1 + .../regress1/sep/split-find-unsat.smt2 | 1 + test/regress/regress1/sep/wand-0526-sat.smt2 | 1 + test/regress/regress1/sep/wand-false.smt2 | 1 + .../regress/regress1/sep/wand-nterm-simp.smt2 | 1 + .../regress1/sep/wand-nterm-simp2.smt2 | 1 + test/regress/regress1/sep/wand-simp-sat.smt2 | 1 + test/regress/regress1/sep/wand-simp-sat2.smt2 | 1 + .../regress/regress1/sep/wand-simp-unsat.smt2 | 1 + test/unit/api/solver_black.h | 13 +++ 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 @@ -3157,6 +3157,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* cmd] @declarations { std::vector dts; CVC4::api::Term e, e2; - CVC4::api::Sort t; + CVC4::api::Sort t, s; std::string name; std::vector names; std::vector terms; @@ -1073,9 +1073,8 @@ extendedCommand[std::unique_ptr* 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& 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& 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 */ @@ -561,6 +560,34 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command bool d_global; }; /* 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 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 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& 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& 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& 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 @@ -248,6 +248,15 @@ class Theory { return d_logicInfo; } + /** + * 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. */ 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); -- 2.30.2