diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 11 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 9 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 1 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 7 | ||||
-rw-r--r-- | src/printer/printer.cpp | 7 | ||||
-rw-r--r-- | src/printer/printer.h | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 7 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 5 | ||||
-rw-r--r-- | src/smt/command.cpp | 36 | ||||
-rw-r--r-- | src/smt/command.h | 29 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 42 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 17 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 90 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 18 | ||||
-rw-r--r-- | src/theory/smt_engine_subsolver.cpp | 2 | ||||
-rw-r--r-- | src/theory/smt_engine_subsolver.h | 11 | ||||
-rw-r--r-- | src/theory/theory.h | 9 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 36 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 13 |
20 files changed, 302 insertions, 55 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. |