/********************* */ /*! \file theory_inference_manager.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** ** \brief An inference manager for Theory **/ #include "cvc4_private.h" #ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H #define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H #include #include "context/cdhashset.h" #include "expr/node.h" #include "theory/output_channel.h" #include "theory/theory_state.h" #include "theory/trust_node.h" #include "theory/uf/proof_equality_engine.h" namespace CVC4 { class ProofNodeManager; namespace theory { class Theory; namespace eq { class EqualityEngine; } /** * The base class for inference manager. An inference manager is a wrapper * around the output channel and the official equality engine of a Theory. * It is used for ensuring that the equality engine and output channel * are used properly. This includes the following invariants: * * (1) The state tracks conflicts. * In particular, TheoryState::isInConflict returns true whenever we have * called OutputChannel::conflict in the current context, which we enforce * by always setting d_state.notifyInConflict at the same time we send * conflicts on the output channel. * * (2) The theory is notified of (internal) facts. * In particular, Theory::preNotifyFact and Theory::notifyFact are called * (with isInternal = true) whenever we assert internal facts using * assertFactInernal below, mirroring what is done for facts from the fact * queue (where isInternal = false). * * (3) The proof equality engine is used whenever proofs are enabled (when * the proof node manager provided to this class is non-null). Notice this * class automatically will construct a proof equality engine during * setEqualityEngine, and use it for handling variants of assertInternalFact * below that involve proofs. */ class TheoryInferenceManager { typedef context::CDHashSet NodeSet; public: /** * Constructor, note that state should be the official state of theory t. */ TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm); virtual ~TheoryInferenceManager() {} /** * Set equality engine, ee is a pointer to the official equality engine * of theory. */ void setEqualityEngine(eq::EqualityEngine* ee); /** * Reset, which resets counters regarding the number of added lemmas and * internal facts. This method should be manually called by the theory at * the appropriate time for the purpose of tracking the usage of this * inference manager. * * For example, some theories implement an internal checking loop that * repeats while new facts are added. The theory should call reset at the * beginning of this loop and repeat its strategy while hasAddedFact is true. */ void reset(); //--------------------------------------- propagations /** * T-propagate literal lit, possibly encountered by equality engine, * returns false if we are in conflict. * * Note that this is the preferred method to call on * EqualityEngineNotify::eqNotifyTriggerPredicate and * EqualityEngineNotify::eqNotifyTriggerTermEquality. */ bool propagateLit(TNode lit); /** * Return an explanation for the literal represented by parameter lit * (which was previously propagated by this theory). By default, this * returns the explanation given by the official equality engine of the * Theory, if it exists. */ virtual TrustNode explainLit(TNode lit); //--------------------------------------- conflicts /** * Raise conflict, called when constants a and b merge. Sends the conflict * on the output channel corresponding to the equality engine's explanation * of (= a b). The proof equality engine (if it exists) will be used as the * proof generator. * * Note that this is the preferred method to call on * EqualityEngineNotify::eqNotifyConstantTermMerge. */ void conflictEqConstantMerge(TNode a, TNode b); /** * Raise conflict conf (of any form), without proofs. This method should * only be called if there is not yet proof support in the given theory. */ void conflict(TNode conf); /** * Raise trusted conflict tconf (of any form) where a proof generator has * been provided in a custom way. */ void trustedConflict(TrustNode tconf); //--------------------------------------- lemmas /** * Send (trusted) lemma lem with property p on the output channel. * * @param tlem The trust node containing the lemma and its proof generator. * @param p The property of the lemma * @param doCache If true, we send the lemma only if it has not already been * cached (see cacheLemma), and add it to the cache during this call. * @return true if the lemma was sent on the output channel. */ bool trustedLemma(const TrustNode& tlem, LemmaProperty p = LemmaProperty::NONE, bool doCache = true); /** * Send lemma lem with property p on the output channel. Same as above, with * a node instead of a trust node. */ bool lemma(TNode lem, LemmaProperty p = LemmaProperty::NONE, bool doCache = true); /** * Has this inference manager cached and sent the given lemma (in this user * context)? This method can be overridden by the particular manager. If not, * this returns true if lem is in the cache d_lemmasSent maintained by this * class. Notice that the default cache in this base class is not dependent * on the lemma property. */ virtual bool hasCachedLemma(TNode lem, LemmaProperty p); /** The number of lemmas we have sent since the last call to reset */ uint32_t numAddedLemmas() const; /** Have we added a lemma since the last call to reset? */ bool hasAddedLemma() const; //--------------------------------------- internal facts /** * Assert internal fact. This is recommended method for asserting "internal" * facts into the equality engine of the theory. In particular, this method * should be used for anything the theory infers that is not sent on the * output channel as a propagation or lemma. This method ensures that the * Theory's preNotifyFact and notifyFact method have been called with * isInternal = true. * * @param atom The atom of the fact to assert * @param pol Its polarity * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid. */ void assertInternalFact(TNode atom, bool pol, TNode exp); /** * Assert internal fact, with a proof step justification. Notice that if * proofs are not enabled in this inference manager, then this asserts * a fact to the equality engine in the normal way. * * @param atom The atom of the fact to assert * @param pol Its polarity * @param id The proof rule identifier of the proof step * @param exp Its explanation, interpreted as a conjunction * @param args The arguments of the proof step */ void assertInternalFact(TNode atom, bool pol, PfRule id, const std::vector& exp, const std::vector& args); /** * Assert internal fact, with a proof generator justification. Same as above, * but with a proof generator instead of an explicit step. * * @param atom The atom of the fact to assert * @param pol Its polarity * @param exp Its explanation, interpreted as a conjunction * @param pg The proof generator for this step. It must be the case that pf * can provide a proof concluding (~) atom from free asumptions in exp in * the remainder of the current SAT context. */ void assertInternalFact(TNode atom, bool pol, const std::vector& exp, ProofGenerator* pg); /** The number of internal facts we have added since the last call to reset */ uint32_t numAddedFacts() const; /** Have we added a internal fact since the last call to reset? */ bool hasAddedFact() const; protected: /** * Process internal fact. This is a common helper method for the * assertInternalFact variants above. */ void processInternalFact(TNode atom, bool pol, PfRule id, const std::vector& exp, const std::vector& args, ProofGenerator* pg); /** * Explain conflict from constants merging in the equality engine. This * method is called by conflictEqConstantMerge. By default, it returns * the explanation of the official equality engine of the theory, if it * exists. */ virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b); /** * Explain formula n (which is possibly a conjunction with no nested * conjunctions), add its explanation to assumptions. */ void explain(TNode n, std::vector& assumptions); /** * Explain formula n (which is possibly a conjunction with no nested * conjunctions), return the explanation as a conjunction. */ Node mkExplain(TNode n); /** * Cache that lemma lem is being sent with property p. Return true if it * did not already exist in the cache maintained by this class. If this * method is not overridden, then we use the d_lemmasSent cache maintained * by this class, which notice is not dependent on lemma property. If * the lemma property should be taken into account, the manager should * override this method to take the lemma property into account as needed. */ virtual bool cacheLemma(TNode lem, LemmaProperty p); /** The theory object */ Theory& d_theory; /** Reference to the state of theory */ TheoryState& d_theoryState; /** Reference to the output channel of the theory */ OutputChannel& d_out; /** Pointer to equality engine of the theory. */ eq::EqualityEngine* d_ee; /** A proof equality engine */ std::unique_ptr d_pfee; /** The proof node manager of the theory */ ProofNodeManager* d_pnm; /** * The keep set of this class. This set is maintained to ensure that * facts and their explanations are ref-counted. Since facts and their * explanations are SAT-context-dependent, this set is also * SAT-context-dependent. */ NodeSet d_keep; /** * A cache of all lemmas sent, which is a user-context-dependent set of * nodes. Notice that this cache does not depedent on lemma property. */ NodeSet d_lemmasSent; /** The number of lemmas sent since the last call to reset. */ uint32_t d_numCurrentLemmas; /** The number of internal facts added since the last call to reset. */ uint32_t d_numCurrentFacts; }; } // namespace theory } // namespace CVC4 #endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */