From 24c4e9d5612fd7549a8ff7acaf76ce95acaca0d9 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 1 Sep 2021 07:24:02 -0700 Subject: rewriter: Make registerTheoryRewriter non-static. (#7101) More work towards getting rid of SmtEngine::currentSmtEngine and closing #3468. --- src/theory/theory_engine.h | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'src/theory/theory_engine.h') diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e610adcf7..81769254f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -78,11 +78,13 @@ struct NodeTheoryPairHashFunction { /* Forward declarations */ namespace theory { -class TheoryModel; + class CombinationEngine; -class SharedSolver; class DecisionManager; class RelevanceManager; +class Rewriter; +class SharedSolver; +class TheoryModel; } // namespace theory @@ -316,7 +318,7 @@ class TheoryEngine { d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); d_theoryTable[theoryId] = new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this)); - theory::Rewriter::registerTheoryRewriter( + getRewriter()->registerTheoryRewriter( theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } @@ -372,6 +374,11 @@ class TheoryEngine { } private: + /** + * Get a pointer to the rewriter owned by the associated Env. + */ + theory::Rewriter* getRewriter(); + /** * Queue of nodes for pre-registration. */ -- cgit v1.2.3 From 847ce3697de4a26e085049496ae1efb7cfb85a99 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 1 Sep 2021 12:24:03 -0700 Subject: Clean up TheoryEngine header according to code style guidelines. (#7107) --- src/theory/theory_engine.h | 561 +++++++++++++++++++++++---------------------- 1 file changed, 285 insertions(+), 276 deletions(-) (limited to 'src/theory/theory_engine.h') diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 81769254f..5c44f8968 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -98,203 +98,14 @@ class PropEngine; * T-solvers look like a single unit to the propositional part of * cvc5. */ -class TheoryEngine { - +class TheoryEngine +{ /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; friend class theory::EngineOutputChannel; friend class theory::CombinationEngine; friend class theory::SharedSolver; - /** Associated PropEngine engine */ - prop::PropEngine* d_propEngine; - - /** - * Reference to the environment. - */ - Env& d_env; - - /** - * A table of from theory IDs to theory pointers. Never use this table - * directly, use theoryOf() instead. - */ - theory::Theory* d_theoryTable[theory::THEORY_LAST]; - - /** - * A collection of theories that are "active" for the current run. - * This set is provided by the user (as a logic string, say, in SMT-LIBv2 - * format input), or else by default it's all-inclusive. This is important - * because we can optimize for single-theory runs (no sharing), can reduce - * 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; - - //--------------------------------- new proofs - /** Proof node manager used by this theory engine, if proofs are enabled */ - ProofNodeManager* d_pnm; - /** The lazy proof object - * - * This stores instructions for how to construct proofs for all theory lemmas. - */ - std::shared_ptr d_lazyProof; - /** The proof generator */ - std::shared_ptr d_tepg; - //--------------------------------- end new proofs - /** The combination manager we are using */ - std::unique_ptr d_tc; - /** The shared solver of the above combination engine. */ - theory::SharedSolver* d_sharedSolver; - /** The quantifiers engine, which is owned by the quantifiers theory */ - theory::QuantifiersEngine* d_quantEngine; - /** - * The decision manager - */ - std::unique_ptr d_decManager; - /** The relevance manager */ - std::unique_ptr d_relManager; - /** - * An empty set of relevant assertions, which is returned as a dummy value for - * getRelevantAssertions when relevance is disabled. - */ - std::unordered_set d_emptyRelevantSet; - - /** are we in eager model building mode? (see setEagerModelBuilding). */ - bool d_eager_model_building; - - /** - * Output channels for individual theories. - */ - theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; - - /** - * Are we in conflict. - */ - context::CDO d_inConflict; - - /** - * Are we in "SAT mode"? In this state, the user can query for the model. - * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB - * standard, version 2.6. - */ - bool d_inSatMode; - - /** - * Called by the theories to notify of a conflict. - * - * @param conflict The trust node containing the conflict and its proof - * generator (if it exists), - * @param theoryId The theory that sent the conflict - */ - void conflict(TrustNode conflict, theory::TheoryId theoryId); - - /** set in conflict */ - void markInConflict(); - - /** - * Debugging flag to ensure that shutdown() is called before the - * destructor. - */ - bool d_hasShutDown; - - /** - * True if a theory has notified us of incompleteness (at this - * context level or below). - */ - context::CDO d_incomplete; - /** The theory and identifier that (most recently) set incomplete */ - context::CDO d_incompleteTheory; - context::CDO d_incompleteId; - - /** - * Called by the theories to notify that the current branch is incomplete. - */ - void setIncomplete(theory::TheoryId theory, theory::IncompleteId id); - - /** - * Mapping of propagations from recievers to senders. - */ - typedef context::CDHashMap PropagationMap; - PropagationMap d_propagationMap; - - /** - * Timestamp of propagations - */ - context::CDO d_propagationMapTimestamp; - - /** - * Literals that are propagated by the theory. Note that these are TNodes. - * The theory can only propagate nodes that have an assigned literal in the - * SAT solver and are hence referenced in the SAT solver. - */ - context::CDList d_propagatedLiterals; - - /** - * The index of the next literal to be propagated by a theory. - */ - context::CDO d_propagatedLiteralsIndex; - - /** - * Called by the output channel to propagate literals and facts - * @return false if immediate conflict - */ - bool propagate(TNode literal, theory::TheoryId theory); - - /** - * Internal method to call the propagation routines and collect the - * propagated literals. - */ - void propagate(theory::Theory::Effort effort); - - /** - * A variable to mark if we added any lemmas. - */ - bool d_lemmasAdded; - - /** - * A variable to mark if the OutputChannel was "used" by any theory - * since the start of the last check. If it has been, we require - * a FULL_EFFORT check before exiting and reporting SAT. - * - * See the documentation for the needCheck() function, below. - */ - bool d_outputChannelUsed; - - /** Atom requests from lemmas */ - AtomRequests d_atomRequests; - - /** - * Adds a new lemma, returning its status. - * @param node the lemma - * @param p the properties of the lemma. - * @param atomsTo the theory that atoms of the lemma should be sent to - * @param from the theory that sent the lemma - */ - void lemma(TrustNode node, - theory::LemmaProperty p, - theory::TheoryId from = theory::THEORY_LAST); - - /** Ensure atoms from the given node are sent to the given theory */ - void ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo); - /** Ensure that the given atoms are sent to the given theory */ - void ensureLemmaAtoms(const std::vector& atoms, - theory::TheoryId atomsTo); - - /** sort inference module */ - std::unique_ptr d_sortInfer; - - /** Time spent in theory combination */ - TimerStat d_combineTheoriesTime; - - Node d_true; - Node d_false; - - /** Whether we were just interrupted (or not) */ - bool d_interrupted; - public: /** Constructs a theory engine */ TheoryEngine(Env& env); @@ -312,7 +123,7 @@ class TheoryEngine { * there is another theory it will be deleted. */ template - inline void addTheory(theory::TheoryId theoryId) + void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); @@ -342,9 +153,7 @@ class TheoryEngine { /** * Get a pointer to the underlying propositional engine. */ - inline prop::PropEngine* getPropEngine() const { - return d_propEngine; - } + prop::PropEngine* getPropEngine() const { return d_propEngine; } /** Get the proof node manager */ ProofNodeManager* getProofNodeManager() const; @@ -362,7 +171,8 @@ class TheoryEngine { /** * Get a pointer to the underlying quantifiers engine. */ - theory::QuantifiersEngine* getQuantifiersEngine() const { + theory::QuantifiersEngine* getQuantifiersEngine() const + { return d_quantEngine; } /** @@ -373,65 +183,6 @@ class TheoryEngine { return d_decManager.get(); } - private: - /** - * Get a pointer to the rewriter owned by the associated Env. - */ - theory::Rewriter* getRewriter(); - - /** - * Queue of nodes for pre-registration. - */ - std::queue d_preregisterQueue; - - /** - * Boolean flag denoting we are in pre-registration. - */ - bool d_inPreregister; - - /** - * Did the theories get any new facts since the last time we called - * check() - */ - context::CDO d_factsAsserted; - - /** - * Assert the formula to the given theory. - * @param assertion the assertion to send (not necesserily normalized) - * @param original the assertion as it was sent in from the propagating theory - * @param toTheoryId the theory to assert to - * @param fromTheoryId the theory that sent it - */ - void assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); - - /** - * Marks a theory propagation from a theory to a theory where a - * theory could be the THEORY_SAT_SOLVER for literals coming from - * or being propagated to the SAT solver. If the receiving theory - * already recieved the literal, the method returns false, otherwise - * it returns true. - * - * @param assertion the normalized assertion being sent - * @param originalAssertion the actual assertion that was sent - * @param toTheoryId the theory that is on the receiving end - * @param fromTheoryId the theory that sent the assertion - * @return true if a new assertion, false if theory already got it - */ - bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); - - /** - * Computes the explanation by traversing the propagation graph and - * asking relevant theories to explain the propagations. Initially - * the explanation vector should contain only the element (node, theory) - * where the node is the one to be explained, and the theory is the - * theory that sent the literal. - */ - TrustNode getExplanation(std::vector& explanationVector); - - /** Are proofs enabled? */ - bool isProofEnabled() const; - - public: /** * Preprocess rewrite equality, called by the preprocessor to rewrite * equalities appearing in the input. @@ -441,7 +192,7 @@ class TheoryEngine { void notifyPreprocessedAssertions(const std::vector& assertions); /** Return whether or not we are incomplete (in the current context). */ - inline bool isIncomplete() const { return d_incomplete; } + bool isIncomplete() const { return d_incomplete; } /** * Returns true if we need another round of checking. If this @@ -458,9 +209,7 @@ class TheoryEngine { * as it might decide to further instantiate some lemmas, precluding * a SAT response. */ - inline bool needCheck() const { - return d_outputChannelUsed || d_lemmasAdded; - } + bool needCheck() const { return d_outputChannelUsed || d_lemmasAdded; } /** * Is the literal lit (possibly) critical for satisfying the input formula in * the current context? This call is applicable only during collectModelInfo @@ -512,7 +261,7 @@ class TheoryEngine { */ bool presolve(); - /** + /** * Calls postsolve() on all theories. */ void postsolve(); @@ -522,9 +271,14 @@ class TheoryEngine { */ void notifyRestart(); - void getPropagatedLiterals(std::vector& literals) { - for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) { - Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl; + void getPropagatedLiterals(std::vector& literals) + { + for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); + d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) + { + Debug("getPropagatedLiterals") + << "TheoryEngine::getPropagatedLiterals: propagating: " + << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl; literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]); } } @@ -576,7 +330,8 @@ class TheoryEngine { * @returns the theory, or NULL if the TNode is * of built-in type. */ - inline theory::Theory* theoryOf(TNode node) const { + theory::Theory* theoryOf(TNode node) const + { return d_theoryTable[theory::Theory::theoryOf(node)]; } @@ -585,12 +340,14 @@ class TheoryEngine { * * @returns the theory */ - inline theory::Theory* theoryOf(theory::TheoryId theoryId) const { + theory::Theory* theoryOf(theory::TheoryId theoryId) const + { Assert(theoryId < theory::THEORY_LAST); return d_theoryTable[theoryId]; } - inline bool isTheoryEnabled(theory::TheoryId theoryId) const { + bool isTheoryEnabled(theory::TheoryId theoryId) const + { return d_logicInfo.isTheoryEnabled(theoryId); } /** get the logic info used by this theory engine */ @@ -655,26 +412,278 @@ class TheoryEngine { */ bool isFiniteType(TypeNode tn) const; //---------------------- end information about cardinality of types + + theory::SortInference* getSortInference() { return d_sortInfer.get(); } + + /** Prints the assertions to the debug stream */ + void printAssertions(const char* tag); + + /** + * Check that the theory assertions are satisfied in the model. + * This function is called from the smt engine's checkModel routine. + */ + void checkTheoryAssertionsWithModel(bool hardFailure); + private: + typedef context:: + CDHashMap + PropagationMap; + + /** + * Called by the theories to notify of a conflict. + * + * @param conflict The trust node containing the conflict and its proof + * generator (if it exists), + * @param theoryId The theory that sent the conflict + */ + void conflict(TrustNode conflict, theory::TheoryId theoryId); + + /** set in conflict */ + void markInConflict(); + + /** + * Called by the theories to notify that the current branch is incomplete. + */ + void setIncomplete(theory::TheoryId theory, theory::IncompleteId id); + + /** + * Called by the output channel to propagate literals and facts + * @return false if immediate conflict + */ + bool propagate(TNode literal, theory::TheoryId theory); + + /** + * Internal method to call the propagation routines and collect the + * propagated literals. + */ + void propagate(theory::Theory::Effort effort); + + /** + * Assert the formula to the given theory. + * @param assertion the assertion to send (not necesserily normalized) + * @param original the assertion as it was sent in from the propagating theory + * @param toTheoryId the theory to assert to + * @param fromTheoryId the theory that sent it + */ + void assertToTheory(TNode assertion, + TNode originalAssertion, + theory::TheoryId toTheoryId, + theory::TheoryId fromTheoryId); + + /** + * Marks a theory propagation from a theory to a theory where a + * theory could be the THEORY_SAT_SOLVER for literals coming from + * or being propagated to the SAT solver. If the receiving theory + * already recieved the literal, the method returns false, otherwise + * it returns true. + * + * @param assertion the normalized assertion being sent + * @param originalAssertion the actual assertion that was sent + * @param toTheoryId the theory that is on the receiving end + * @param fromTheoryId the theory that sent the assertion + * @return true if a new assertion, false if theory already got it + */ + bool markPropagation(TNode assertion, + TNode originalAssertions, + theory::TheoryId toTheoryId, + theory::TheoryId fromTheoryId); + + /** + * Computes the explanation by traversing the propagation graph and + * asking relevant theories to explain the propagations. Initially + * the explanation vector should contain only the element (node, theory) + * where the node is the one to be explained, and the theory is the + * theory that sent the literal. + */ + TrustNode getExplanation(std::vector& explanationVector); + + /** Are proofs enabled? */ + bool isProofEnabled() const; + + /** + * Get a pointer to the rewriter owned by the associated Env. + */ + theory::Rewriter* getRewriter(); + + /** + * Adds a new lemma, returning its status. + * @param node the lemma + * @param p the properties of the lemma. + * @param atomsTo the theory that atoms of the lemma should be sent to + * @param from the theory that sent the lemma + */ + void lemma(TrustNode node, + theory::LemmaProperty p, + theory::TheoryId from = theory::THEORY_LAST); + + /** Ensure atoms from the given node are sent to the given theory */ + void ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo); + /** Ensure that the given atoms are sent to the given theory */ + void ensureLemmaAtoms(const std::vector& atoms, + theory::TheoryId atomsTo); /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ -public: - theory::SortInference* getSortInference() { return d_sortInfer.get(); } + /** Associated PropEngine engine */ + prop::PropEngine* d_propEngine; - /** Prints the assertions to the debug stream */ - void printAssertions(const char* tag); + /** + * Reference to the environment. + */ + Env& d_env; - public: + /** + * A table of from theory IDs to theory pointers. Never use this table + * directly, use theoryOf() instead. + */ + theory::Theory* d_theoryTable[theory::THEORY_LAST]; /** - * Check that the theory assertions are satisfied in the model. - * This function is called from the smt engine's checkModel routine. + * A collection of theories that are "active" for the current run. + * This set is provided by the user (as a logic string, say, in SMT-LIBv2 + * format input), or else by default it's all-inclusive. This is important + * because we can optimize for single-theory runs (no sharing), can reduce + * the cost of walking the DAG on registration, etc. */ - void checkTheoryAssertionsWithModel(bool hardFailure); -};/* class TheoryEngine */ + 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; + /** The lazy proof object + * + * This stores instructions for how to construct proofs for all theory lemmas. + */ + std::shared_ptr d_lazyProof; + /** The proof generator */ + std::shared_ptr d_tepg; + //--------------------------------- end new proofs + /** The combination manager we are using */ + std::unique_ptr d_tc; + /** The shared solver of the above combination engine. */ + theory::SharedSolver* d_sharedSolver; + /** The quantifiers engine, which is owned by the quantifiers theory */ + theory::QuantifiersEngine* d_quantEngine; + /** + * The decision manager + */ + std::unique_ptr d_decManager; + /** The relevance manager */ + std::unique_ptr d_relManager; + /** + * An empty set of relevant assertions, which is returned as a dummy value for + * getRelevantAssertions when relevance is disabled. + */ + std::unordered_set d_emptyRelevantSet; + + /** are we in eager model building mode? (see setEagerModelBuilding). */ + bool d_eager_model_building; + + /** + * Output channels for individual theories. + */ + theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; + + /** + * Are we in conflict. + */ + context::CDO d_inConflict; + + /** + * Are we in "SAT mode"? In this state, the user can query for the model. + * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB + * standard, version 2.6. + */ + bool d_inSatMode; + + /** + * Debugging flag to ensure that shutdown() is called before the + * destructor. + */ + bool d_hasShutDown; + + /** + * True if a theory has notified us of incompleteness (at this + * context level or below). + */ + context::CDO d_incomplete; + /** The theory and identifier that (most recently) set incomplete */ + context::CDO d_incompleteTheory; + context::CDO d_incompleteId; + + /** + * Mapping of propagations from recievers to senders. + */ + PropagationMap d_propagationMap; + + /** + * Timestamp of propagations + */ + context::CDO d_propagationMapTimestamp; + + /** + * Literals that are propagated by the theory. Note that these are TNodes. + * The theory can only propagate nodes that have an assigned literal in the + * SAT solver and are hence referenced in the SAT solver. + */ + context::CDList d_propagatedLiterals; + + /** + * The index of the next literal to be propagated by a theory. + */ + context::CDO d_propagatedLiteralsIndex; + + /** + * A variable to mark if we added any lemmas. + */ + bool d_lemmasAdded; + + /** + * A variable to mark if the OutputChannel was "used" by any theory + * since the start of the last check. If it has been, we require + * a FULL_EFFORT check before exiting and reporting SAT. + * + * See the documentation for the needCheck() function, below. + */ + bool d_outputChannelUsed; + + /** Atom requests from lemmas */ + AtomRequests d_atomRequests; + + /** sort inference module */ + std::unique_ptr d_sortInfer; + + /** Time spent in theory combination */ + TimerStat d_combineTheoriesTime; + + Node d_true; + Node d_false; + + /** Whether we were just interrupted (or not) */ + bool d_interrupted; + + /** + * Queue of nodes for pre-registration. + */ + std::queue d_preregisterQueue; + + /** + * Boolean flag denoting we are in pre-registration. + */ + bool d_inPreregister; + + /** + * Did the theories get any new facts since the last time we called + * check() + */ + context::CDO d_factsAsserted; + +}; /* class TheoryEngine */ } // namespace cvc5 -- cgit v1.2.3