The separation logic heap is conceptually an extension of the logic, which lives in Env. This PR moves the separation logic heap types from TheoryEngine to Env.
It furthermore makes it so that declaring the separation logic heap does not force initialization of the SolverEngine, meaning that further declarations/options may be done after setting the heap.
This is in preparation for making the SmtSolver class easier to deep reset.
AssertionPipeline* assertionsToPreprocess)
{
TypeNode locType, dataType;
- if (!d_preprocContext->getTheoryEngine()->getSepHeapTypes(locType, dataType))
+ if (!d_env.getSepHeapTypes(locType, dataType))
{
warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
"heap types during preprocessing"
node, d_options.theory.theoryOfMode, d_uninterpretedSortOwner);
}
+bool Env::hasSepHeap() const { return !d_sepLocType.isNull(); }
+
+bool Env::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const
+{
+ if (!hasSepHeap())
+ {
+ return false;
+ }
+ locType = d_sepLocType;
+ dataType = d_sepDataType;
+ return true;
+}
+
+void Env::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+ Assert(!locT.isNull());
+ Assert(!dataT.isNull());
+ // remember the types we have set
+ d_sepLocType = locT;
+ d_sepDataType = dataT;
+}
+
} // namespace cvc5::internal
*/
theory::TheoryId theoryOf(TNode node) 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 the theory engine.
+ */
+ void declareSepHeap(TypeNode locT, TypeNode dataT);
+
+ /** Have we called declareSepHeap? */
+ bool hasSepHeap() const;
+
+ /** get the separation logic heap types */
+ bool getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const;
+
private:
/* Private initialization ------------------------------------------------- */
std::unique_ptr<ResourceManager> d_resourceManager;
/** The theory that owns the uninterpreted sort. */
theory::TheoryId d_uninterpretedSortOwner;
+ /** The separation logic location and data types */
+ TypeNode d_sepLocType;
+ TypeNode d_sepDataType;
}; /* class Env */
} // namespace cvc5::internal
std::ostream& reason,
std::ostream& suggest) const
{
+ if (d_env.hasSepHeap())
+ {
+ reason << "separation logic";
+ return true;
+ }
if (opts.smt.ackermann)
{
reason << "ackermann";
void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
{
+ if (d_state->isFullyInited())
+ {
+ throw ModalException(
+ "Cannot set logic in SolverEngine after the engine has "
+ "finished initializing.");
+ }
if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
{
const char* msg =
"Cannot declare heap if not using the separation logic theory.";
throw RecoverableModalException(msg);
}
- SolverEngineScope smts(this);
- finishInit();
- // check whether incremental is enabled, where separation logic is not
- // supported.
- if (d_env->getOptions().base.incrementalSolving)
+ TypeNode locT2, dataT2;
+ if (d_env->getSepHeapTypes(locT2, dataT2))
{
- throw RecoverableModalException(
- "Separation logic not supported in incremental mode");
+ 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 << locT2 << " -> " << dataT2;
+ throw LogicException(ss.str());
}
- TheoryEngine* te = getTheoryEngine();
- te->declareSepHeap(locT, dataT);
+ d_env->declareSepHeap(locT, dataT);
}
bool SolverEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
{
- SolverEngineScope smts(this);
- finishInit();
- TheoryEngine* te = getTheoryEngine();
- return te->getSepHeapTypes(locT, dataT);
+ return d_env->getSepHeapTypes(locT, dataT);
}
Node SolverEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
// indicate we are using the default theory state object
d_theoryState = &d_state;
d_inferManager = &d_im;
+
+ // initialize the heap types
+ initializeHeapTypes();
}
TheorySep::~TheorySep() {
}
}
-void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT)
+void TheorySep::initializeHeapTypes()
{
- if (!d_type_ref.isNull())
+ TypeNode locT;
+ TypeNode dataT;
+ if (d_env.getSepHeapTypes(locT, dataT))
{
- 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());
+ // otherwise set it
+ Trace("sep-type") << "Sep: assume location type " << locT
+ << " is associated with data type " << dataT << std::endl;
+ d_loc_to_data_type[locT] = dataT;
+ // for now, we only allow heap constraints of one type
+ d_type_ref = locT;
+ d_type_data = dataT;
+ d_bound_kind[locT] = bound_default;
}
- // otherwise set it
- Trace("sep-type") << "Sep: assume location type " << locT
- << " is associated with data type " << dataT << std::endl;
- d_loc_to_data_type[locT] = dataT;
- // for now, we only allow heap constraints of one type
- d_type_ref = locT;
- d_type_data = dataT;
- d_bound_kind[locT] = bound_default;
}
TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
TheorySep(Env& env, OutputChannel& out, Valuation valuation);
~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;
std::string identify() const override { return std::string("TheorySep"); }
- /////////////////////////////////////////////////////////////////////////////
- // PREPROCESSING
- /////////////////////////////////////////////////////////////////////////////
-
- public:
void ppNotifyAssertions(const std::vector<Node>& assertions) override;
- /////////////////////////////////////////////////////////////////////////////
- // T-PROPAGATION / REGISTRATION
- /////////////////////////////////////////////////////////////////////////////
- private:
- /** Should be called to propagate the literal. */
- bool propagateLit(TNode literal);
- /** Conflict when merging constants */
- void conflict(TNode a, TNode b);
-
- public:
TrustNode explain(TNode n) override;
- public:
void computeCareGraph() override;
- /////////////////////////////////////////////////////////////////////////////
- // MODEL GENERATION
- /////////////////////////////////////////////////////////////////////////////
-
- public:
void postProcessModel(TheoryModel* m) override;
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
+ private:
+ /**
+ * Initialize heap. For smt2 inputs, this will initialize the heap types
+ * based on if a command (declare-heap (locT datat)) was used. This command
+ * can be executed once only, and must be invoked before solving separation
+ * logic inputs, which is controlled by the solver engine.
+ */
+ void initializeHeapTypes();
+ /** Should be called to propagate the literal. */
+ bool propagateLit(TNode literal);
+ /** Conflict when merging constants */
+ void conflict(TNode a, TNode b);
public:
Node mkUnion( TypeNode tn, std::vector< Node >& locs );
- private:
Node getRepresentative( Node t );
bool hasTerm( Node a );
bool areEqual( Node a, Node b );
void sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer = false );
void doPending();
- public:
-
void initializeBounds();
};/* class TheorySep */
*/
bool proofsEnabled() const;
- /**
- * 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) {}
-
void printFacts(std::ostream& os) const;
void debugPrintFacts() const;
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 CVC5_FOR_EACH_THEORY_STATEMENT
-#undef CVC5_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \
- theoryOf(THEORY)->declareSepHeap(locT, dataT);
-
- // notify each theory using the statement above
- CVC5_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);
}
/** 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
*/
const LogicInfo& d_logicInfo;
- /** The separation logic location and data types */
- TypeNode d_sepLocType;
- TypeNode d_sepDataType;
-
//--------------------------------- new proofs
/** Proof node manager used by this theory engine, if proofs are enabled */
ProofNodeManager* d_pnm;
projects / cvc5.git / commitdiff