/*! \file theory_inference_manager.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Mathias Preiner, Gereon Kremer
** 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.
+ ** 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
**
#ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
#define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
+#include <memory>
+
#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 {
* (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
{
*/
TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
virtual ~TheoryInferenceManager() {}
- //--------------------------------------- initialization
/**
* Set equality engine, ee is a pointer to the official equality engine
* of theory.
*/
void setEqualityEngine(eq::EqualityEngine* ee);
- //--------------------------------------- end initialization
+ /**
+ * Are proofs enabled in this inference manager? Returns true if the proof
+ * node manager pnm provided to the constructor of this class was non-null.
+ */
+ bool isProofEnabled() const;
+ /**
+ * 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();
+ /**
+ * Returns true if we are in conflict, or if we have sent a lemma or fact
+ * since the last call to reset.
+ */
+ bool hasSent() const;
+ /** Get the underlying proof equality engine */
+ eq::ProofEqEngine* getProofEqEngine();
+ //--------------------------------------- propagations
/**
* T-propagate literal lit, possibly encountered by equality engine,
* returns false if we are in conflict.
* 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
void conflict(TNode conf);
/**
* Raise trusted conflict tconf (of any form) where a proof generator has
- * been provided in a custom way.
+ * been provided (as part of the trust node) in a custom way.
*/
void trustedConflict(TrustNode tconf);
+ /**
+ * Explain and send conflict from contradictory facts. This method is called
+ * when the proof rule id with premises exp and arguments args concludes
+ * false. This method sends a trusted conflict corresponding to the official
+ * equality engine's explanation of literals in exp, with the proof equality
+ * engine as the proof generator (if it exists).
+ */
+ void conflictExp(PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args);
+ /**
+ * Make the trust node corresponding to the conflict of the above form. It is
+ * the responsibility of the caller to subsequently call trustedConflict with
+ * the returned trust node.
+ */
+ TrustNode mkConflictExp(PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args);
+ /**
+ * Explain and send conflict from contradictory facts. This method is called
+ * when proof generator pg has a proof of false from free assumptions exp.
+ * This method sends a trusted conflict corresponding to the official
+ * equality engine's explanation of literals in exp, with the proof equality
+ * engine as the proof generator (if it exists), where pg provides the
+ * final step(s) of this proof during this call.
+ */
+ void conflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
+ /**
+ * Make the trust node corresponding to the conflict of the above form. It is
+ * the responsibility of the caller to subsequently call trustedConflict with
+ * the returned trust node.
+ */
+ TrustNode mkConflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
+ //--------------------------------------- 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);
+ /**
+ * Explained lemma. This should be called when
+ * ( exp => conc )
+ * is a valid theory lemma. This method adds a lemma where part of exp
+ * is replaced by its explanation according to the official equality engine
+ * of the theory.
+ *
+ * In particular, this method adds a lemma on the output channel of the form
+ * ( ^_{e in exp \ noExplain} EXPLAIN(e) ^ noExplain ) => conc
+ * where EXPLAIN(e) returns the explanation of literal e according to the
+ * official equality engine of the theory. Note that noExplain is the *subset*
+ * of exp that should not be explained.
+ *
+ * @param conc The conclusion of the lemma
+ * @param id The proof rule concluding conc
+ * @param exp The set of (all) literals that imply conc
+ * @param noExplain The subset of exp that should not be explained by the
+ * equality engine
+ * @param args The arguments to the proof step concluding conc
+ * @param p The property of the lemma
+ * @param doCache Whether to check and add the lemma to the cache
+ * @return true if the lemma was sent on the output channel.
+ */
+ bool lemmaExp(Node conc,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ const std::vector<Node>& args,
+ LemmaProperty p = LemmaProperty::NONE,
+ bool doCache = true);
+ /**
+ * Make the trust node for the above method. It is responsibility of the
+ * caller to subsequently call trustedLemma with the returned trust node.
+ */
+ TrustNode mkLemmaExp(Node conc,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ const std::vector<Node>& args);
+ /**
+ * Same as above, but where pg can provide a proof of conc from free
+ * assumptions in exp. This sends a trusted lemma on the output channel where
+ * the proof equality engine is the proof generator. The generator pg
+ * is asked to provide the final step(s) of this proof during this call.
+ *
+ * @param conc The conclusion of the lemma
+ * @param exp The set of (all) literals that imply conc
+ * @param noExplain The subset of exp that should not be explained by the
+ * equality engine
+ * @param pg If non-null, the proof generator who can provide a proof of conc.
+ * @param p The property of the lemma
+ * @param doCache Whether to check and add the lemma to the cache
+ * @return true if the lemma was sent on the output channel.
+ */
+ bool lemmaExp(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofGenerator* pg = nullptr,
+ LemmaProperty p = LemmaProperty::NONE,
+ bool doCache = true);
+ /**
+ * Make the trust node for the above method. It is responsibility of the
+ * caller to subsequently call trustedLemma with the returned trust node.
+ */
+ TrustNode mkLemmaExp(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofGenerator* pg = nullptr);
+ /**
+ * 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 numSentLemmas() const;
+ /** Have we added a lemma since the last call to reset? */
+ bool hasSentLemma() 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
* 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.
+ * @return true if the fact was processed, i.e. it was asserted to the
+ * equality engine or preNotifyFact returned true.
+ */
+ bool 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
+ * @return true if the fact was processed, i.e. it was asserted to the
+ * equality engine or preNotifyFact returned true.
+ */
+ bool assertInternalFact(TNode atom,
+ bool pol,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& 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. If non-null, pg must be able
+ * to provide a proof concluding (~) atom from free asumptions in exp in
+ * the remainder of the current SAT context.
+ * @return true if the fact was processed, i.e. it was asserted to the
+ * equality engine or preNotifyFact returned true.
+ */
+ bool assertInternalFact(TNode atom,
+ bool pol,
+ const std::vector<Node>& exp,
+ ProofGenerator* pg);
+ /** The number of internal facts we have added since the last call to reset */
+ uint32_t numSentFacts() const;
+ /** Have we added a internal fact since the last call to reset? */
+ bool hasSentFact() const;
+ //--------------------------------------- phase requirements
+ /**
+ * Set that literal n has SAT phase requirement pol, that is, it should be
+ * decided with polarity pol, for details see OutputChannel::requirePhase.
+ */
+ void requirePhase(TNode n, bool pol);
+
+ /**
+ * Forward to OutputChannel::spendResource() to spend resources.
*/
- void assertInternalFact(TNode atom, bool pol, TNode fact);
+ void spendResource(ResourceManager::Resource r);
+
+ /**
+ * Forward to OutputChannel::safePoint() to spend resources.
+ */
+ void safePoint(ResourceManager::Resource r);
+ /**
+ * Notification from a theory that it realizes it is incomplete at
+ * this context level.
+ */
+ void setIncomplete();
protected:
+ /**
+ * Process internal fact. This is a common helper method for the
+ * assertInternalFact variants above. Returns true if the fact was processed.
+ */
+ bool processInternalFact(TNode atom,
+ bool pol,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args,
+ ProofGenerator* pg);
/**
* Explain conflict from constants merging in the equality engine. This
* method is called by conflictEqConstantMerge. By default, it returns
* 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<TNode>& assumptions);
+ /**
+ * Explain formula n (which is possibly a conjunction with no nested
+ * conjunctions), return the explanation as a conjunction.
+ */
+ Node mkExplain(TNode n);
+ /**
+ * Explain the set of formulas in exp using the official equality engine of
+ * the theory. We ask the equality engine to explain literals in exp
+ * that do not occur in noExplain, and return unchanged those that occur in
+ * noExplain. Note the vector noExplain should be a subset of exp.
+ */
+ Node mkExplainPartial(const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain);
+ /**
+ * 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 */
OutputChannel& d_out;
/** Pointer to equality engine of the theory. */
eq::EqualityEngine* d_ee;
+ /** A proof equality engine */
+ std::unique_ptr<eq::ProofEqEngine> d_pfee;
/** The proof node manager of the theory */
ProofNodeManager* d_pnm;
/**
* 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 conflicts sent since the last call to reset. */
+ uint32_t d_numConflicts;
+ /** 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
projects / cvc5.git / blobdiff