From c2cf72496097cf94817e171ffa382c69e1da04ba Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 2 Sep 2021 18:27:30 -0700 Subject: [PATCH] theory: Have Theory and TheoryArith* derive from EnvObj. (#7128) Note: the diff in theory.h is only huge because of small changes that caused huge reformat. The effective change is only that it now derives from EnvObj, does not have a member d_env (because it inherits it) and does not need getLogicInfo (because that's in EnvObj). --- src/smt/env_obj.cpp | 2 + src/smt/env_obj.h | 4 + src/theory/arith/theory_arith_private.cpp | 4 +- src/theory/arith/theory_arith_private.h | 10 +- src/theory/theory.cpp | 4 +- src/theory/theory.h | 189 +++++++++++----------- 6 files changed, 112 insertions(+), 101 deletions(-) diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp index 2a9cd285f..04a5050db 100644 --- a/src/smt/env_obj.cpp +++ b/src/smt/env_obj.cpp @@ -26,4 +26,6 @@ EnvObj::EnvObj(Env& env) : d_env(env) {} Node EnvObj::rewrite(TNode node) { return d_env.getRewriter()->rewrite(node); } +const LogicInfo& EnvObj::getLogicInfo() const { return d_env.getLogicInfo(); } + } // namespace cvc5 diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h index bae05874b..ffd5a3915 100644 --- a/src/smt/env_obj.h +++ b/src/smt/env_obj.h @@ -26,6 +26,7 @@ namespace cvc5 { class Env; +class LogicInfo; class NodeManager; class Options; @@ -44,6 +45,9 @@ class EnvObj */ Node rewrite(TNode node); + /** Get the current logic information. */ + const LogicInfo& getLogicInfo() const; + /** The associated environment. */ Env& d_env; }; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 4eff69ef8..070300b3b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -88,8 +88,8 @@ static bool complexityBelow(const DenseMap& row, uint32_t cap); TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, Env& env, BranchAndBound& bab) - : d_containing(containing), - d_env(env), + : EnvObj(env), + d_containing(containing), d_foundNl(false), d_rowTracking(), d_bab(bab), diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 0cdc031e1..389262fed 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -82,13 +82,12 @@ class InferBoundsResult; * Based upon: * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf */ -class TheoryArithPrivate { -private: - +class TheoryArithPrivate : protected EnvObj +{ + private: static const uint32_t RESET_START = 2; TheoryArith& d_containing; - Env& d_env; const Options& options() const { return d_env.getOptions(); } @@ -687,7 +686,6 @@ private: /** Debugging only routine. Prints the model. */ void debugPrintModel(std::ostream& out) const; - inline LogicInfo getLogicInfo() const { return d_containing.getLogicInfo(); } inline bool done() const { return d_containing.done(); } inline TNode get() { return d_containing.get(); } inline bool isLeaf(TNode x) const { return d_containing.isLeaf(x); } @@ -875,7 +873,7 @@ private: Statistics d_statistics; -};/* class TheoryArithPrivate */ +}; /* class TheoryArithPrivate */ } // namespace arith } // namespace theory diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 5ca1979b3..f6513933f 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -64,8 +64,8 @@ Theory::Theory(TheoryId id, OutputChannel& out, Valuation valuation, std::string name) - : d_id(id), - d_env(env), + : EnvObj(env), + d_id(id), d_facts(d_env.getContext()), d_factsHead(d_env.getContext(), 0), d_sharedTermsIndex(d_env.getContext(), 0), diff --git a/src/theory/theory.h b/src/theory/theory.h index 44a0e597b..371d8f76a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -30,6 +30,7 @@ #include "options/theory_options.h" #include "proof/trust_node.h" #include "smt/env.h" +#include "smt/env_obj.h" #include "theory/assertion.h" #include "theory/care_graph.h" #include "theory/logic_info.h" @@ -58,7 +59,7 @@ class TrustSubstitutionMap; namespace eq { class EqualityEngine; - } // namespace eq +} // namespace eq /** * Base class for T-solvers. Abstract DPLL(T). @@ -94,7 +95,8 @@ namespace eq { * Initialization of the second form happens during TheoryEngine::finishInit, * after the quantifiers engine and model objects have been set up. */ -class Theory { +class Theory : protected EnvObj +{ friend class ::cvc5::TheoryEngine; private: @@ -106,9 +108,6 @@ class Theory { /** An integer identifying the type of the theory. */ TheoryId d_id; - /** The environment class */ - Env& d_env; - /** * The assertFact() queue. * @@ -130,9 +129,10 @@ class Theory { DecisionManager* d_decManager; protected: - /** Name of this theory instance. Along with the TheoryId this should provide - * an unique string identifier for each instance of a Theory class. We need - * this to ensure unique statistics names over multiple theory instances. */ + /** Name of this theory instance. Along with the TheoryId this should + * provide an unique string identifier for each instance of a Theory class. + * We need this to ensure unique statistics names over multiple theory + * instances. */ std::string d_instanceName; // === STATISTICS === @@ -178,7 +178,7 @@ class Theory { * you must make an explicit call here to this->Theory::shutdown() * too. */ - virtual void shutdown() { } + virtual void shutdown() {} /** * The output channel for the Theory. @@ -200,8 +200,9 @@ class Theory { */ std::unique_ptr d_allocEqualityEngine; /** - * The theory state, which contains contexts, valuation, and equality engine. - * Notice the theory is responsible for memory management of this class. + * The theory state, which contains contexts, valuation, and equality + * engine. Notice the theory is responsible for memory management of this + * class. */ TheoryState* d_theoryState; /** @@ -233,8 +234,6 @@ class Theory { */ inline Assertion get(); - const LogicInfo& getLogicInfo() const { return d_env.getLogicInfo(); } - /** * Set separation logic heap. This is called when the location and data * types for separation logic are determined. This should be called at @@ -262,10 +261,11 @@ class Theory { * The following criteria imply that x -> val is *not* a legal elimination: * (1) If x is contained in val, * (2) If the type of val is not a subtype of the type of x, - * (3) If val contains an operator that cannot be evaluated, and produceModels - * is true. For example, x -> sqrt(2) is not a legal elimination if we - * are producing models. This is because we care about the value of x, and - * its value must be computed (approximated) by the non-linear solver. + * (3) If val contains an operator that cannot be evaluated, and + * produceModels is true. For example, x -> sqrt(2) is not a legal + * elimination if we are producing models. This is because we care about the + * value of x, and its value must be computed (approximated) by the + * non-linear solver. */ bool isLegalElimination(TNode x, TNode val); //--------------------------------- private initialization @@ -298,9 +298,10 @@ class Theory { */ virtual void notifySharedTerm(TNode n); /** - * Notify in conflict, called when a conflict clause is added to TheoryEngine - * by any theory (not necessarily this one). This signals that the theory - * should suspend what it is currently doing and wait for backtracking. + * Notify in conflict, called when a conflict clause is added to + * TheoryEngine by any theory (not necessarily this one). This signals that + * the theory should suspend what it is currently doing and wait for + * backtracking. */ virtual void notifyInConflict(); @@ -322,10 +323,10 @@ class Theory { * initialize its equality engine field via setEqualityEngine above during * TheoryEngine::finishInit, prior to calling finishInit for this theory. * - * Additionally, if this method returns true, then this method is required to - * update the argument esi with instructions for initializing and setting up - * notifications from its equality engine, which is commonly done with - * a notifications class (eq::EqualityEngineNotify). + * Additionally, if this method returns true, then this method is required + * to update the argument esi with instructions for initializing and setting + * up notifications from its equality engine, which is commonly done with a + * notifications class (eq::EqualityEngineNotify). */ virtual bool needsEqualityEngine(EeSetupInfo& esi); /** @@ -340,16 +341,23 @@ class Theory { /** * Return the ID of the theory responsible for the given type. */ - static inline TheoryId theoryOf(TypeNode typeNode) { + static inline TheoryId theoryOf(TypeNode typeNode) + { Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl; TheoryId id; - if (typeNode.getKind() == kind::TYPE_CONSTANT) { + if (typeNode.getKind() == kind::TYPE_CONSTANT) + { id = typeConstantToTheoryId(typeNode.getConst()); - } else { + } + else + { id = kindToTheoryId(typeNode.getKind()); } - if (id == THEORY_BUILTIN) { - Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl; + if (id == THEORY_BUILTIN) + { + Trace("theory::internal") + << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner + << std::endl; return s_uninterpretedSortOwner; } return id; @@ -363,35 +371,40 @@ class Theory { /** * Returns the ID of the theory responsible for the given node. */ - static inline TheoryId theoryOf(TNode node) { + static inline TheoryId theoryOf(TNode node) + { return theoryOf(options::theoryOfMode(), node); } /** * Set the owner of the uninterpreted sort. */ - static void setUninterpretedSortOwner(TheoryId theory) { + static void setUninterpretedSortOwner(TheoryId theory) + { s_uninterpretedSortOwner = theory; } /** * Get the owner of the uninterpreted sort. */ - static TheoryId getUninterpretedSortOwner() { + static TheoryId getUninterpretedSortOwner() + { return s_uninterpretedSortOwner; } /** * Checks if the node is a leaf node of this theory */ - inline bool isLeaf(TNode node) const { + inline bool isLeaf(TNode node) const + { return node.getNumChildren() == 0 || theoryOf(node) != d_id; } /** * Checks if the node is a leaf node of a theory. */ - inline static bool isLeafOf(TNode node, TheoryId theoryId) { + inline static bool isLeafOf(TNode node, TheoryId theoryId) + { return node.getNumChildren() == 0 || theoryOf(node) != theoryId; } @@ -416,8 +429,8 @@ class Theory { */ EFFORT_STANDARD = 50, /** - * Full effort requires the theory make sure its assertions are satisfiable - * or not + * Full effort requires the theory make sure its assertions are + * satisfiable or not */ EFFORT_FULL = 100, /** @@ -429,20 +442,21 @@ class Theory { static inline bool standardEffortOrMore(Effort e) CVC5_CONST_FUNCTION { - return e >= EFFORT_STANDARD; } + return e >= EFFORT_STANDARD; + } static inline bool standardEffortOnly(Effort e) CVC5_CONST_FUNCTION { - return e >= EFFORT_STANDARD && e < EFFORT_FULL; } + return e >= EFFORT_STANDARD && e < EFFORT_FULL; + } static inline bool fullEffort(Effort e) CVC5_CONST_FUNCTION { - return e == EFFORT_FULL; } + return e == EFFORT_FULL; + } /** * Get the id for this Theory. */ - TheoryId getId() const { - return d_id; - } + TheoryId getId() const { return d_id; } /** * Get a reference to the environment. @@ -462,23 +476,20 @@ class Theory { /** * Get the context associated to this Theory. */ - context::UserContext* getUserContext() const { + context::UserContext* getUserContext() const + { return d_env.getUserContext(); } /** * Get the output channel associated to this theory. */ - OutputChannel& getOutputChannel() { - return *d_out; - } + OutputChannel& getOutputChannel() { return *d_out; } /** * Get the valuation associated to this theory. */ - Valuation& getValuation() { - return d_valuation; - } + Valuation& getValuation() { return d_valuation; } /** Get the equality engine being used by this theory. */ eq::EqualityEngine* getEqualityEngine(); @@ -486,9 +497,7 @@ class Theory { /** * Get the quantifiers engine associated to this theory. */ - QuantifiersEngine* getQuantifiersEngine() { - return d_quantEngine; - } + QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } /** * @return The theory state associated with this theory. @@ -508,7 +517,8 @@ class Theory { /** * Assert a fact in the current context. */ - void assertFact(TNode assertion, bool isPreregistered) { + void assertFact(TNode assertion, bool isPreregistered) + { Trace("theory") << "Theory<" << getId() << ">::assertFact[" << getSatContext()->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl; @@ -532,7 +542,8 @@ class Theory { virtual EqualityStatus getEqualityStatus(TNode a, TNode b); /** - * Return the model value of the give shared term (or null if not available). + * Return the model value of the give shared term (or null if not + * available). * * TODO (project #39): this method is likely to become deprecated. */ @@ -568,11 +579,11 @@ class Theory { * - throw an exception * - or call get() until done() is true. * - * The standard method for check consists of a loop that processes the entire - * fact queue when preCheck returns false. It makes four theory-specific - * callbacks, (preCheck, postCheck, preNotifyFact, notifyFact) as described - * below. It asserts each fact to the official equality engine when - * preNotifyFact returns false. + * The standard method for check consists of a loop that processes the + * entire fact queue when preCheck returns false. It makes four + * theory-specific callbacks, (preCheck, postCheck, preNotifyFact, + * notifyFact) as described below. It asserts each fact to the official + * equality engine when preNotifyFact returns false. * * Theories that use this check method must use an official theory * state object (d_theoryState). @@ -663,8 +674,9 @@ class Theory { */ virtual bool collectModelValues(TheoryModel* m, const std::set& termSet); - /** if theories want to do something with model after building, do it here */ - virtual void postProcessModel( TheoryModel* m ){ } + /** if theories want to do something with model after building, do it here + */ + virtual void postProcessModel(TheoryModel* m) {} //--------------------------------- end collect model info //--------------------------------- preprocessing @@ -677,7 +689,8 @@ class Theory { */ virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {} - enum PPAssertStatus { + enum PPAssertStatus + { /** Atom has been solved */ PP_ASSERT_STATUS_SOLVED, /** Atom has not been solved */ @@ -747,7 +760,7 @@ class Theory { * NOTE: The presolve property must be added to the kinds file for * the theory. */ - virtual void presolve() { } + virtual void presolve() {} /** * A Theory is called with postsolve exactly one time per user @@ -759,7 +772,7 @@ class Theory { * cannot raise conflicts, add lemmas, or propagate literals during * postsolve(). */ - virtual void postsolve() { } + virtual void postsolve() {} /** * Notification sent to the theory wheneven the search restarts. @@ -767,7 +780,7 @@ class Theory { * assume you're at DL 0 for the purposes of Contexts. This function * should not use the output channel. */ - virtual void notifyRestart() { } + virtual void notifyRestart() {} /** * Identify this theory (for debugging, dynamic configuration, @@ -783,9 +796,7 @@ class Theory { * * @return the iterator to the beginning of the fact queue */ - assertions_iterator facts_begin() const { - return d_facts.begin(); - } + assertions_iterator facts_begin() const { return d_facts.begin(); } /** * Provides access to the facts queue, primarily intended for theory @@ -793,9 +804,7 @@ class Theory { * * @return the iterator to the end of the fact queue */ - assertions_iterator facts_end() const { - return d_facts.end(); - } + assertions_iterator facts_end() const { return d_facts.end(); } /** * Whether facts have been asserted to this theory. * @@ -804,9 +813,7 @@ class Theory { bool hasFacts() { return !d_facts.empty(); } /** Return total number of facts asserted to this theory */ - size_t numAssertions() { - return d_facts.size(); - } + size_t numAssertions() { return d_facts.size(); } typedef context::CDList::const_iterator shared_terms_iterator; @@ -816,7 +823,8 @@ class Theory { * * @return the iterator to the beginning of the shared terms list */ - shared_terms_iterator shared_terms_begin() const { + shared_terms_iterator shared_terms_begin() const + { return d_sharedTerms.begin(); } @@ -826,14 +834,11 @@ class Theory { * * @return the iterator to the end of the shared terms list */ - shared_terms_iterator shared_terms_end() const { - return d_sharedTerms.end(); - } - + shared_terms_iterator shared_terms_end() const { return d_sharedTerms.end(); } /** - * This is a utility function for constructing a copy of the currently shared terms - * in a queriable form. As this is + * This is a utility function for constructing a copy of the currently + * shared terms in a queriable form. As this is */ std::unordered_set currentlySharedTerms() const; @@ -841,14 +846,15 @@ class Theory { * This allows the theory to be queried for whether a literal, lit, is * entailed by the theory. This returns a pair of a Boolean and a node E. * - * If the Boolean is true, then E is a formula that entails lit and E is propositionally - * entailed by the assertions to the theory. + * If the Boolean is true, then E is a formula that entails lit and E is + * propositionally entailed by the assertions to the theory. * * If the Boolean is false, it is "unknown" if lit is entailed and E may be * any node. * - * The literal lit is either an atom a or (not a), which must belong to the theory: - * There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId(). + * The literal lit is either an atom a or (not a), which must belong to the + * theory: There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == + * this->getId(). * * There are NO assumptions that a or the subterms of a have been * preprocessed in any form. This includes ppRewrite, rewriting, @@ -856,15 +862,16 @@ class Theory { * * Theories are free to limit the amount of effort they use and so may * always opt to return "unknown". Both "unknown" and "not entailed", - * may return for E a non-boolean Node (e.g. Node::null()). (There is no explicit output - * for the negation of lit is entailed.) + * may return for E a non-boolean Node (e.g. Node::null()). (There is no + * explicit output for the negation of lit is entailed.) * * If lit is theory valid, the return result may be the Boolean constant * true for E. * * If lit is entailed by multiple assertions on the theory's getFact() * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or - * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k) + * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... + * a_k) * * If lit is entailed by a single assertion on the theory's getFact() * queue, say a, this may return E=a. @@ -874,8 +881,8 @@ class Theory { * Theories may not touch their output stream during an entailment check. * * @param lit a literal belonging to the theory. - * @return a pair s.t. if b is true, then a formula E such that - * E |= lit in the theory. + * @return a pair s.t. if b is true, then a formula E such + * that E |= lit in the theory. */ virtual std::pair entailmentCheck(TNode lit); @@ -885,7 +892,7 @@ class Theory { static bool usesCentralEqualityEngine(TheoryId id); /** Explains/propagates via central equality engine only */ static bool expUsingCentralEqualityEngine(TheoryId id); -};/* class Theory */ +}; /* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); -- 2.30.2