From cf1a6a09b40fbbe2ce65b7d2012e1303f3b6ec3f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 18 Apr 2022 08:58:05 -0500 Subject: [PATCH] Simplify management of separation logic heap (#8580) 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. --- src/preprocessing/passes/sep_skolem_emp.cpp | 2 +- src/smt/env.cpp | 22 ++++++++++ src/smt/env.h | 16 +++++++ src/smt/set_defaults.cpp | 5 +++ src/smt/solver_engine.cpp | 29 +++++++------ src/theory/sep/theory_sep.cpp | 32 +++++++------- src/theory/sep/theory_sep.h | 48 ++++++--------------- src/theory/theory.h | 9 ---- src/theory/theory_engine.cpp | 36 ---------------- src/theory/theory_engine.h | 13 ------ 10 files changed, 87 insertions(+), 125 deletions(-) diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 783fd0fee..fc974d020 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -109,7 +109,7 @@ PreprocessingPassResult SepSkolemEmp::applyInternal( 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" diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 3060afeee..c454bfc9c 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -256,4 +256,26 @@ theory::TheoryId Env::theoryOf(TNode node) const 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 diff --git a/src/smt/env.h b/src/smt/env.h index 007894752..a501223b3 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -256,6 +256,19 @@ class Env */ 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 ------------------------------------------------- */ @@ -331,6 +344,9 @@ class Env std::unique_ptr 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 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index fb402863d..fca7abee9 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -995,6 +995,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, std::ostream& reason, std::ostream& suggest) const { + if (d_env.hasSepHeap()) + { + reason << "separation logic"; + return true; + } if (opts.smt.ackermann) { reason << "ackermann"; diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 5ae8bd08f..744eb3b42 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1212,31 +1212,34 @@ Env& SolverEngine::getEnv() { return *d_env.get(); } 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; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index d818cb06e..47447ba78 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -58,6 +58,9 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) // indicate we are using the default theory state object d_theoryState = &d_state; d_inferManager = &d_im; + + // initialize the heap types + initializeHeapTypes(); } TheorySep::~TheorySep() { @@ -66,26 +69,21 @@ 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; } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 1dc719a9e..3073c2a44 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -80,15 +80,6 @@ class TheorySep : public Theory { 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; @@ -108,38 +99,26 @@ class TheorySep : public Theory { std::string identify() const override { return std::string("TheorySep"); } - ///////////////////////////////////////////////////////////////////////////// - // PREPROCESSING - ///////////////////////////////////////////////////////////////////////////// - - public: void ppNotifyAssertions(const std::vector& 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: @@ -341,7 +320,6 @@ class TheorySep : public Theory { Node mkUnion( TypeNode tn, std::vector< Node >& locs ); - private: Node getRepresentative( Node t ); bool hasTerm( Node a ); bool areEqual( Node a, Node b ); @@ -351,8 +329,6 @@ class TheorySep : public Theory { void sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer = false ); void doPending(); - public: - void initializeBounds(); };/* class TheorySep */ diff --git a/src/theory/theory.h b/src/theory/theory.h index df7486016..45bd81296 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -203,15 +203,6 @@ class Theory : protected EnvObj */ 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; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f250b053e..7c8f0451e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1076,42 +1076,6 @@ 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 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); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a177a7bc0..7391fd60f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -339,15 +339,6 @@ class TheoryEngine : protected EnvObj } /** 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 @@ -519,10 +510,6 @@ class TheoryEngine : protected EnvObj */ 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; -- 2.30.2