summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp11
-rw-r--r--src/api/cvc4cpp.h9
-rw-r--r--src/api/python/cvc4.pxd1
-rw-r--r--src/api/python/cvc4.pxi3
-rw-r--r--src/parser/smt2/Smt2.g7
-rw-r--r--src/printer/printer.cpp7
-rw-r--r--src/printer/printer.h4
-rw-r--r--src/printer/smt2/smt2_printer.cpp7
-rw-r--r--src/printer/smt2/smt2_printer.h5
-rw-r--r--src/smt/command.cpp36
-rw-r--r--src/smt/command.h29
-rw-r--r--src/smt/smt_engine.cpp42
-rw-r--r--src/smt/smt_engine.h17
-rw-r--r--src/theory/sep/theory_sep.cpp90
-rw-r--r--src/theory/sep/theory_sep.h18
-rw-r--r--src/theory/smt_engine_subsolver.cpp2
-rw-r--r--src/theory/smt_engine_subsolver.h11
-rw-r--r--src/theory/theory.h9
-rw-r--r--src/theory/theory_engine.cpp36
-rw-r--r--src/theory/theory_engine.h13
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback