This introduces a TheoryInference base class, which is a generalization and cleaner version of the former Lemma object. This changes the name of Lemma -> SimpleTheoryLemma, and makes the callback responsible for calling the inference manager.
This PR also updates the datatypes inference manager to use the new style. This required adding some additional interfaces to TheoryInferenceManager.
theory/theory_engine_proof_generator.h
theory/theory_id.cpp
theory/theory_id.h
+ theory/theory_inference.cpp
+ theory/theory_inference.h
theory/theory_inference_manager.cpp
theory/theory_inference_manager.h
theory/theory_model.cpp
namespace theory {
namespace datatypes {
-InferenceManager::InferenceManager(Theory& t,
- TheoryState& state,
- ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, state, pnm)
+DatatypesInference::DatatypesInference(Node conc, Node exp, ProofGenerator* pg)
+ : SimpleTheoryInternalFact(conc, exp, pg)
{
- d_true = NodeManager::currentNM()->mkConst(true);
+ // false is not a valid explanation
+ Assert(d_exp.isNull() || !d_exp.isConst() || d_exp.getConst<bool>());
}
-bool InferenceManager::mustCommunicateFact(Node n, Node exp) const
+bool DatatypesInference::mustCommunicateFact(Node n, Node exp)
{
Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
bool addLemma = false;
- if (options::dtInferAsLemmas() && exp != d_true)
+ if (options::dtInferAsLemmas() && !exp.isConst())
{
+ // all units are lemmas
addLemma = true;
}
else if (n.getKind() == EQUAL)
return false;
}
-void InferenceManager::process()
+bool DatatypesInference::process(TheoryInferenceManager* im)
{
- // process pending lemmas, used infrequently, only for definitional lemmas
- doPendingLemmas();
- // now process the pending facts
- size_t i = 0;
- NodeManager* nm = NodeManager::currentNM();
- while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
+ // check to see if we have to communicate it to the rest of the system
+ if (mustCommunicateFact(d_conc, d_exp))
{
- std::pair<Node, Node>& pfact = d_pendingFact[i];
- const Node& fact = pfact.first;
- const Node& exp = pfact.second;
- Trace("datatypes-debug")
- << "Assert fact (#" << (i + 1) << "/" << d_pendingFact.size() << ") "
- << fact << " with explanation " << exp << std::endl;
- // check to see if we have to communicate it to the rest of the system
- if (mustCommunicateFact(fact, exp))
- {
- Node lem = fact;
- if (exp.isNull() || exp == d_true)
- {
- Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
- }
- else
- {
- Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
- std::vector<TNode> assumptions;
- explain(exp, assumptions);
- if (!assumptions.empty())
- {
- std::vector<Node> children;
- for (const TNode& assumption : assumptions)
- {
- children.push_back(assumption.negate());
- }
- children.push_back(fact);
- lem = nm->mkNode(OR, children);
- }
- }
- Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
- lemma(lem);
- }
- else
+ // send it as an (explained) lemma
+ std::vector<Node> exp;
+ if (!d_exp.isNull() && !d_exp.isConst())
{
- // assert the internal fact
- bool polarity = fact.getKind() != NOT;
- TNode atom = polarity ? fact : fact[0];
- assertInternalFact(atom, polarity, exp);
+ exp.push_back(d_exp);
}
- Trace("datatypes-debug") << "Finished fact " << fact
- << ", now = " << d_theoryState.isInConflict()
- << " " << d_pendingFact.size() << std::endl;
- i++;
+ return im->lemmaExp(d_conc, exp, {});
}
- d_pendingFact.clear();
+ // assert the internal fact
+ bool polarity = d_conc.getKind() != NOT;
+ TNode atom = polarity ? d_conc : d_conc[0];
+ im->assertInternalFact(atom, polarity, d_exp);
+ return true;
+}
+
+InferenceManager::InferenceManager(Theory& t,
+ TheoryState& state,
+ ProofNodeManager* pnm)
+ : InferenceManagerBuffered(t, state, pnm)
+{
+}
+
+void InferenceManager::addPendingInference(Node conc,
+ Node exp,
+ ProofGenerator* pg)
+{
+ d_pendingFact.push_back(std::make_shared<DatatypesInference>(conc, exp, pg));
+}
+
+void InferenceManager::process()
+{
+ // process pending lemmas, used infrequently, only for definitional lemmas
+ doPendingLemmas();
+ // now process the pending facts
+ doPendingFacts();
}
} // namespace datatypes
namespace datatypes {
/**
- * The datatypes inference manager. The main unique features of this inference
- * manager are:
- * (1) Explicit caching of lemmas,
- * (2) A custom process() method with relies on a policy determining which
- * facts must be sent as lemmas (mustCommunicateFact).
- * (3) Methods for tracking when lemmas and facts have been processed.
+ * A custom inference class. The main feature of this class is that it
+ * dynamically decides whether to process itself as a fact or as a lemma,
+ * based on the mustCommunicateFact method below.
*/
-class InferenceManager : public InferenceManagerBuffered
+class DatatypesInference : public SimpleTheoryInternalFact
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-
public:
- InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
- ~InferenceManager() {}
- /**
- * Process the current lemmas and facts. This is a custom method that can
- * be seen as overriding the behavior of calling both doPendingLemmas and
- * doPendingFacts. It determines whether facts should be sent as lemmas
- * or processed internally.
- */
- void process();
-
- protected:
+ DatatypesInference(Node conc, Node exp, ProofGenerator* pg);
/**
* Must communicate fact method.
* The datatypes decision procedure makes "internal" inferences :
* communicate outwards if the conclusions involve other theories. Also
* communicate (6) and OR conclusions.
*/
- bool mustCommunicateFact(Node n, Node exp) const;
- /** Common node */
- Node d_true;
+ static bool mustCommunicateFact(Node n, Node exp);
+ /**
+ * Process this fact, possibly as a fact or as a lemma, depending on the
+ * above method.
+ */
+ bool process(TheoryInferenceManager* im) override;
+};
+
+/**
+ * The datatypes inference manager, which uses the above class for
+ * inferences.
+ */
+class InferenceManager : public InferenceManagerBuffered
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+ InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
+ ~InferenceManager() {}
+ /**
+ * Add pending inference, which may be processed as either a fact or
+ * a lemma based on mustCommunicateFact in DatatypesInference above.
+ */
+ void addPendingInference(Node conc, Node exp, ProofGenerator* pg = nullptr);
+ /**
+ * Process the current lemmas and facts. This is a custom method that can
+ * be seen as overriding the behavior of calling both doPendingLemmas and
+ * doPendingFacts. It determines whether facts should be sent as lemmas
+ * or processed internally.
+ */
+ void process();
};
} // namespace datatypes
LemmaProperty p,
ProofGenerator* pg)
{
- d_pendingLem.push_back(std::make_shared<Lemma>(lem, p, pg));
+ // make the simple theory lemma
+ d_pendingLem.push_back(std::make_shared<SimpleTheoryLemma>(lem, p, pg));
}
-void InferenceManagerBuffered::addPendingLemma(std::shared_ptr<Lemma> lemma)
+void InferenceManagerBuffered::addPendingLemma(
+ std::shared_ptr<TheoryInference> lemma)
{
d_pendingLem.emplace_back(std::move(lemma));
}
-void InferenceManagerBuffered::addPendingFact(Node fact, Node exp)
+void InferenceManagerBuffered::addPendingFact(Node conc,
+ Node exp,
+ ProofGenerator* pg)
{
- Assert(fact.getKind() != AND && fact.getKind() != OR);
- d_pendingFact.push_back(std::pair<Node, Node>(fact, exp));
+ // make a simple theory internal fact
+ Assert(conc.getKind() != AND && conc.getKind() != OR);
+ d_pendingFact.push_back(
+ std::make_shared<SimpleTheoryInternalFact>(conc, exp, pg));
+}
+
+void InferenceManagerBuffered::addPendingFact(
+ std::shared_ptr<TheoryInference> fact)
+{
+ d_pendingFact.emplace_back(std::move(fact));
}
void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
size_t i = 0;
while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
{
- std::pair<Node, Node>& pfact = d_pendingFact[i];
- Node fact = pfact.first;
- Node exp = pfact.second;
- bool polarity = fact.getKind() != NOT;
- TNode atom = polarity ? fact : fact[0];
- // no double negation or conjunctive conclusions
- Assert(atom.getKind() != NOT && atom.getKind() != AND);
- assertInternalFact(atom, polarity, exp);
+ // process this fact, which notice may enqueue more pending facts in this
+ // loop.
+ d_pendingFact[i]->process(this);
i++;
}
d_pendingFact.clear();
void InferenceManagerBuffered::doPendingLemmas()
{
- // process all the pending lemmas
- for (const std::shared_ptr<Lemma>& plem : d_pendingLem)
+ for (const std::shared_ptr<TheoryInference>& plem : d_pendingLem)
{
- if (!plem->notifySend())
- {
- // the lemma indicated that it should not be sent after all
- continue;
- }
- Node lem = plem->d_node;
- LemmaProperty p = plem->d_property;
- ProofGenerator* pg = plem->d_pg;
- Assert(!lem.isNull());
- // send (trusted) lemma on the output channel with property p
- trustedLemma(TrustNode::mkTrustLemma(lem, pg), p);
+ // process this lemma
+ plem->process(this);
}
d_pendingLem.clear();
}
#include "context/cdhashmap.h"
#include "expr/node.h"
+#include "theory/theory_inference.h"
#include "theory/theory_inference_manager.h"
namespace CVC4 {
namespace theory {
-/**
- * A lemma base class. This class is an abstract data structure for storing
- * pending lemmas in the inference manager below.
- */
-class Lemma
-{
- public:
- Lemma(Node n, LemmaProperty p, ProofGenerator* pg)
- : d_node(n), d_property(p), d_pg(pg)
- {
- }
- virtual ~Lemma() {}
- /**
- * Called just before this lemma is sent on the output channel. The purpose
- * of this callback is to do any specific process of the lemma, e.g. take
- * debug statistics, cache, etc.
- *
- * @return true if the lemma should be sent on the output channel.
- */
- virtual bool notifySend() { return true; }
- /** The lemma to send */
- Node d_node;
- /** The lemma property (see OutputChannel::lemma) */
- LemmaProperty d_property;
- /**
- * The proof generator for this lemma, which if non-null, is wrapped in a
- * TrustNode to be set on the output channel via trustedLemma at the time
- * the lemma is sent. This proof generator must be able to provide a proof
- * for d_node in the remainder of the user context.
- */
- ProofGenerator* d_pg;
-};
-
/**
* The buffered inference manager. This class implements standard methods
* for buffering facts, lemmas and phase requirements.
ProofGenerator* pg = nullptr);
/**
* Add pending lemma, where lemma can be a (derived) class of the
- * above one. Pending lemmas are sent to the output channel using
- * doPendingLemmas.
+ * theory inference base class.
*/
- void addPendingLemma(std::shared_ptr<Lemma> lemma);
+ void addPendingLemma(std::shared_ptr<TheoryInference> lemma);
/**
* Add pending fact, which adds a fact on the pending fact queue. It must
* be the case that:
- * (1) exp => fact is valid,
+ * (1) exp => conc is valid,
* (2) exp is a literal (or conjunction of literals) that holds in the
* equality engine of the theory.
*
* Pending facts are sent to the equality engine of this class using
* doPendingFacts.
*/
- void addPendingFact(Node fact, Node exp);
+ void addPendingFact(Node conc, Node exp, ProofGenerator* pg = nullptr);
+ /**
+ * Add pending fact, where fact can be a (derived) class of the
+ * theory inference base class.
+ */
+ void addPendingFact(std::shared_ptr<TheoryInference> fact);
/** Add pending phase requirement
*
* This method is called to indicate this class should send a phase
void clearPendingPhaseRequirements();
protected:
- /** A set of pending lemmas */
- std::vector<std::shared_ptr<Lemma>> d_pendingLem;
- /** A set of pending facts, paired with their explanations */
- std::vector<std::pair<Node, Node>> d_pendingFact;
+ /** A set of pending inferences to be processed as lemmas */
+ std::vector<std::shared_ptr<TheoryInference>> d_pendingLem;
+ /** A set of pending inferences to be processed as facts */
+ std::vector<std::shared_ptr<TheoryInference>> d_pendingFact;
/** A map from literals to their pending phase requirement */
std::map<Node, bool> d_pendingReqPhase;
};
--- /dev/null
+/********************* */
+/*! \file theory_inference.cpp
+ ** \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 The theory inference utility
+ **/
+
+#include "theory/theory_inference.h"
+
+#include "theory/theory_inference_manager.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+SimpleTheoryLemma::SimpleTheoryLemma(Node n,
+ LemmaProperty p,
+ ProofGenerator* pg)
+ : d_node(n), d_property(p), d_pg(pg)
+{
+}
+
+bool SimpleTheoryLemma::process(TheoryInferenceManager* im)
+{
+ Assert(!d_node.isNull());
+ // send (trusted) lemma on the output channel with property p
+ return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property);
+}
+
+SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc,
+ Node exp,
+ ProofGenerator* pg)
+ : d_conc(conc), d_exp(exp), d_pg(pg)
+{
+}
+
+bool SimpleTheoryInternalFact::process(TheoryInferenceManager* im)
+{
+ bool polarity = d_conc.getKind() != NOT;
+ TNode atom = polarity ? d_conc : d_conc[0];
+ // no double negation or conjunctive conclusions
+ Assert(atom.getKind() != NOT && atom.getKind() != AND);
+ if (d_pg != nullptr)
+ {
+ im->assertInternalFact(atom, polarity, {d_exp}, d_pg);
+ }
+ else
+ {
+ im->assertInternalFact(atom, polarity, d_exp);
+ }
+ return true;
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file theory_inference.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 The theory inference utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__THEORY_INFERENCE_H
+#define CVC4__THEORY__THEORY_INFERENCE_H
+
+#include "expr/node.h"
+#include "theory/output_channel.h"
+
+namespace CVC4 {
+namespace theory {
+
+class TheoryInferenceManager;
+
+/**
+ * A theory inference base class. This class is an abstract data structure for
+ * storing pending lemmas or facts in the buffered inference manager. It can
+ * be seen a single use object capturing instructions for making a single
+ * call to TheoryInferenceManager for lemmas or facts.
+ */
+class TheoryInference
+{
+ public:
+ virtual ~TheoryInference() {}
+ /**
+ * Called by the provided inference manager to process this inference. This
+ * method should make call(s) to inference manager to process this
+ * inference, as well as processing any specific side effects. This method
+ * typically makes a single call to the provided inference manager e.g.
+ * d_im->trustedLemma or d_im->assertFactInternal. Notice it is the sole
+ * responsibility of this class to make this call; the inference manager
+ * does not call itself otherwise when processing pending inferences.
+ *
+ * @return true if the inference was successfully processed by the inference
+ * manager. This method for instance returns false if it corresponds to a
+ * lemma that was already cached by im and hence was discarded.
+ */
+ virtual bool process(TheoryInferenceManager* im) = 0;
+};
+
+/**
+ * A simple theory lemma with no side effects. Makes a single call to
+ * trustedLemma in its process method.
+ */
+class SimpleTheoryLemma : public TheoryInference
+{
+ public:
+ SimpleTheoryLemma(Node n, LemmaProperty p, ProofGenerator* pg);
+ virtual ~SimpleTheoryLemma() {}
+ /**
+ * Send the lemma using inference manager im, return true if the lemma was
+ * sent.
+ */
+ virtual bool process(TheoryInferenceManager* im) override;
+ /** The lemma to send */
+ Node d_node;
+ /** The lemma property (see OutputChannel::lemma) */
+ LemmaProperty d_property;
+ /**
+ * The proof generator for this lemma, which if non-null, is wrapped in a
+ * TrustNode to be set on the output channel via trustedLemma at the time
+ * the lemma is sent. This proof generator must be able to provide a proof
+ * for d_node in the remainder of the user context.
+ */
+ ProofGenerator* d_pg;
+};
+
+/**
+ * A simple internal fact with no side effects. Makes a single call to
+ * assertFactInternal in its process method.
+ */
+class SimpleTheoryInternalFact : public TheoryInference
+{
+ public:
+ SimpleTheoryInternalFact(Node conc, Node exp, ProofGenerator* pg);
+ virtual ~SimpleTheoryInternalFact() {}
+ /**
+ * Send the lemma using inference manager im, return true if the lemma was
+ * sent.
+ */
+ virtual bool process(TheoryInferenceManager* im) override;
+ /** The lemma to send */
+ Node d_conc;
+ /** The explanation */
+ Node d_exp;
+ /** The proof generator */
+ ProofGenerator* d_pg;
+};
+
+} // namespace theory
+} // namespace CVC4
+
+#endif
}
}
+void TheoryInferenceManager::conflictExp(PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args)
+{
+ if (!d_theoryState.isInConflict())
+ {
+ if (d_pfee != nullptr)
+ {
+ // use proof equality engine to construct the trust node
+ TrustNode tconf = d_pfee->assertConflict(id, exp, args);
+ d_out.trustedConflict(tconf);
+ }
+ else
+ {
+ // version without proofs
+ Node conf = mkExplainPartial(exp, {});
+ conflict(conf);
+ }
+ }
+}
+
bool TheoryInferenceManager::propagateLit(TNode lit)
{
// If already in conflict, no more propagation
Node lit = a.eqNode(b);
if (d_pfee != nullptr)
{
- return d_pfee->explain(lit);
+ return d_pfee->assertConflict(lit);
}
if (d_ee != nullptr)
{
return true;
}
+bool TheoryInferenceManager::lemmaExp(Node conc,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ const std::vector<Node>& args,
+ LemmaProperty p,
+ bool doCache)
+{
+ if (d_pfee != nullptr)
+ {
+ // make the trust node from the proof equality engine
+ TrustNode trn = d_pfee->assertLemma(conc, id, exp, noExplain, args);
+ return trustedLemma(trn, p, doCache);
+ }
+ // otherwise, not using proofs, explain and send lemma
+ Node ant = mkExplainPartial(exp, noExplain);
+ Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
+ return lemma(lem, p, doCache);
+}
+
+bool TheoryInferenceManager::lemmaExp(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofGenerator* pg,
+ LemmaProperty p,
+ bool doCache)
+{
+ if (d_pfee != nullptr)
+ {
+ // make the trust node from the proof equality engine
+ TrustNode trn = d_pfee->assertLemma(conc, exp, noExplain, pg);
+ return trustedLemma(trn, p, doCache);
+ }
+ // otherwise, not using proofs, explain and send lemma
+ Node ant = mkExplainPartial(exp, noExplain);
+ Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
+ return lemma(lem, p, doCache);
+}
+
bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
{
return d_lemmasSent.find(lem) != d_lemmasSent.end();
return NodeManager::currentNM()->mkAnd(assumptions);
}
+Node TheoryInferenceManager::mkExplainPartial(
+ const std::vector<Node>& exp, const std::vector<Node>& noExplain)
+{
+ std::vector<TNode> assumps;
+ for (const Node& e : exp)
+ {
+ if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
+ {
+ if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
+ {
+ // a non-explained literal
+ assumps.push_back(e);
+ }
+ continue;
+ }
+ // otherwise, explain it
+ explain(e, assumps);
+ }
+ return NodeManager::currentNM()->mkAnd(assumps);
+}
+
uint32_t TheoryInferenceManager::numAddedFacts() const
{
return d_numCurrentFacts;
* been provided 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);
//--------------------------------------- lemmas
/**
* Send (trusted) lemma lem with property p on the output channel.
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);
+ /**
+ * Same as above, but where pg can provide a proof of conc from free
+ * assumptions in exp. It is required to do so in the remainder of the user
+ * context when this method returns true.
+ *
+ * @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);
/**
* 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,
* @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
+ * @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.
*/
void assertInternalFact(TNode atom,
* 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
projects / cvc5.git / commitdiff