summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/theory_inference_manager.cpp120
-rw-r--r--src/theory/theory_inference_manager.h68
-rw-r--r--src/theory/uf/proof_equality_engine.cpp32
-rw-r--r--src/theory/uf/proof_equality_engine.h6
4 files changed, 175 insertions, 51 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index b2da91e16..a42c33814 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -37,6 +37,14 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t,
void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
{
d_ee = ee;
+ // if proofs are enabled, also make a proof equality engine to wrap ee
+ if (d_pnm != nullptr)
+ {
+ d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
+ d_theoryState.getUserContext(),
+ *d_ee,
+ d_pnm));
+ }
}
void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
@@ -85,7 +93,10 @@ bool TheoryInferenceManager::propagateLit(TNode lit)
TrustNode TheoryInferenceManager::explainLit(TNode lit)
{
- // TODO (project #37): use proof equality engine if it exists
+ if (d_pfee != nullptr)
+ {
+ return d_pfee->explain(lit);
+ }
if (d_ee != nullptr)
{
Node exp = d_ee->mkExplainLit(lit);
@@ -100,10 +111,13 @@ TrustNode TheoryInferenceManager::explainLit(TNode lit)
TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
TNode b)
{
- // TODO (project #37): use proof equality engine if it exists
+ Node lit = a.eqNode(b);
+ if (d_pfee != nullptr)
+ {
+ return d_pfee->explain(lit);
+ }
if (d_ee != nullptr)
{
- Node lit = a.eqNode(b);
Node conf = d_ee->mkExplainLit(lit);
return TrustNode::mkTrustConflict(conf, nullptr);
}
@@ -122,36 +136,112 @@ LemmaStatus TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
return d_out.trustedLemma(tlem, p);
}
+void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp)
+{
+ processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
+}
+
+void TheoryInferenceManager::assertInternalFact(TNode atom,
+ bool pol,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args)
+{
+ Assert(id != PfRule::UNKNOWN);
+ processInternalFact(atom, pol, id, exp, args, nullptr);
+}
+
void TheoryInferenceManager::assertInternalFact(TNode atom,
bool pol,
- TNode fact)
+ const std::vector<Node>& exp,
+ ProofGenerator* pg)
{
+ Assert(pg != nullptr);
+ processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg);
+}
+
+void TheoryInferenceManager::processInternalFact(TNode atom,
+ bool pol,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args,
+ ProofGenerator* pg)
+{
+ // make the node corresponding to the explanation
+ Node expn = NodeManager::currentNM()->mkAnd(exp);
// call the pre-notify fact method with preReg = false, isInternal = true
- if (d_theory.preNotifyFact(atom, pol, fact, false, true))
+ if (d_theory.preNotifyFact(atom, pol, expn, false, true))
{
// handled in a theory-specific way that doesn't require equality engine
return;
}
Assert(d_ee != nullptr);
Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
- << fact << std::endl;
- if (atom.getKind() == kind::EQUAL)
+ << expn << std::endl;
+ // Now, assert the fact. How to do so depends on whether proofs are enabled.
+ // If no proof production, or no proof rule was given
+ if (d_pfee == nullptr || id == PfRule::UNKNOWN)
{
- d_ee->assertEquality(atom, pol, fact);
+ if (atom.getKind() == kind::EQUAL)
+ {
+ d_ee->assertEquality(atom, pol, expn);
+ }
+ else
+ {
+ d_ee->assertPredicate(atom, pol, expn);
+ }
+ // Must reference count the equality and its explanation, which is not done
+ // by the equality engine. Notice that we do *not* need to do this for
+ // external assertions, which enter as facts in theory check. This is also
+ // not done if we are asserting to the proof equality engine, which does
+ // this caching itself within ProofEqEngine::assertFact.
+ d_keep.insert(atom);
+ d_keep.insert(expn);
}
else
{
- d_ee->assertPredicate(atom, pol, fact);
+ // Note that we reconstruct the original literal lit here, since both the
+ // original literal is needed for bookkeeping proofs. It is possible to
+ // optimize this so that a few less nodes are created, but at the cost
+ // of a more verbose interface to proof equality engine.
+ Node lit = pol ? Node(atom) : atom.notNode();
+ if (pg != nullptr)
+ {
+ // use the proof generator interface
+ d_pfee->assertFact(lit, expn, pg);
+ }
+ else
+ {
+ // use the explict proof step interface
+ d_pfee->assertFact(lit, id, expn, args);
+ }
}
// call the notify fact method with isInternal = true
- d_theory.notifyFact(atom, pol, fact, true);
+ d_theory.notifyFact(atom, pol, expn, true);
Trace("infer-manager")
<< "TheoryInferenceManager::finished assertInternalFact" << std::endl;
- // Must reference count the equality and its explanation, which is not done
- // by the equality engine. Notice that we do *not* need to do this for
- // external assertions, which enter as facts in theory check.
- d_keep.insert(atom);
- d_keep.insert(fact);
+}
+
+void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
+{
+ if (n.getKind() == kind::AND)
+ {
+ for (const Node& nc : n)
+ {
+ d_ee->explainLit(nc, assumptions);
+ }
+ }
+ else
+ {
+ d_ee->explainLit(n, assumptions);
+ }
+}
+
+Node TheoryInferenceManager::mkExplain(TNode n)
+{
+ std::vector<TNode> assumptions;
+ explain(n, assumptions);
+ return NodeManager::currentNM()->mkAnd(assumptions);
}
} // namespace theory
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index e52afe124..af8e817b4 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -17,11 +17,14 @@
#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 {
@@ -51,6 +54,12 @@ class EqualityEngine;
* (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
{
@@ -117,17 +126,72 @@ class TheoryInferenceManager
* 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, TNode fact);
+ void 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. 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<Node>& exp,
+ ProofGenerator* pg);
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<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
* 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<TNode>& assumptions);
+ /**
+ * Explain formula n (which is possibly a conjunction with no nested
+ * conjunctions), return the explanation as a conjunction.
+ */
+ Node mkExplain(TNode n);
/** The theory object */
Theory& d_theory;
/** Reference to the state of theory */
@@ -136,6 +200,8 @@ class TheoryInferenceManager
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;
/**
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 274a46b26..021a737c0 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -126,7 +126,7 @@ bool ProofEqEngine::assertFact(Node lit,
d_proof.addLazyStep(lit, &d_factPg, false);
}
// second, assert it to the equality engine
- Node reason = mkAnd(exp);
+ Node reason = NodeManager::currentNM()->mkAnd(exp);
return assertFactInternal(atom, polarity, reason);
}
@@ -494,11 +494,11 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
// scope the proof constructed above, and connect the formula with the proof
// minimize the assumptions
pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
- exp = mkAnd(scopeAssumps);
+ exp = nm->mkAnd(scopeAssumps);
}
else
{
- exp = mkAnd(assumps);
+ exp = nm->mkAnd(assumps);
}
// Make the lemma or conflict node. This must exactly match the conclusion
// of SCOPE below.
@@ -668,32 +668,6 @@ void ProofEqEngine::explainWithProof(Node lit,
Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
}
-Node ProofEqEngine::mkAnd(const std::vector<Node>& a)
-{
- if (a.empty())
- {
- return d_true;
- }
- else if (a.size() == 1)
- {
- return a[0];
- }
- return NodeManager::currentNM()->mkNode(AND, a);
-}
-
-Node ProofEqEngine::mkAnd(const std::vector<TNode>& a)
-{
- if (a.empty())
- {
- return d_true;
- }
- else if (a.size() == 1)
- {
- return a[0];
- }
- return NodeManager::currentNM()->mkNode(AND, a);
-}
-
ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c,
ProofNodeManager* pnm)
: ProofGenerator(), d_facts(c), d_pnm(pnm)
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index b71f72c53..314353131 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -307,12 +307,6 @@ class ProofEqEngine : public EagerProofGenerator
const std::vector<TNode>& assumps,
TrustNodeKind tnk,
LazyCDProof* curr);
- /**
- * Make the conjunction of nodes in a. Returns true if a is empty, and a
- * single literal if a has size 1.
- */
- Node mkAnd(const std::vector<Node>& a);
- Node mkAnd(const std::vector<TNode>& a);
/** Reference to the equality engine */
eq::EqualityEngine& d_ee;
/** The default proof generator (for simple facts) */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback