--- /dev/null
+/********************* */
+/*! \file proof_equality_engine.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 Implementation of the proof-producing equality engine
+ **/
+
+#include "theory/uf/proof_equality_engine.h"
+
+#include "theory/rewriter.h"
+#include "theory/uf/proof_checker.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace eq {
+
+ProofEqEngine::ProofEqEngine(context::Context* c,
+ context::UserContext* u,
+ EqualityEngine& ee,
+ ProofNodeManager* pnm)
+ : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()),
+ d_ee(ee),
+ d_factPg(c, pnm),
+ d_pnm(pnm),
+ d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()),
+ d_keep(c),
+ d_pfEnabled(pnm != nullptr)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ d_true = nm->mkConst(true);
+ d_false = nm->mkConst(false);
+}
+
+bool ProofEqEngine::assertAssume(TNode lit)
+{
+ Trace("pfee") << "pfee::assertAssume " << lit << std::endl;
+ // don't need to explicitly add anything to the proof here, since ASSUME
+ // nodes are constructed lazily
+ TNode atom = lit.getKind() == NOT ? lit[0] : lit;
+ bool polarity = lit.getKind() != NOT;
+
+ // Second, assert it directly to the equality engine, where it is its own
+ // explanation. Notice we do not reference count atom/lit.
+ if (atom.getKind() == EQUAL)
+ {
+ if (d_pfEnabled)
+ {
+ // If proofs are enabled, we check if lit is an assertion of the form
+ // (= P true), (= P false), (= false P) or (= true P).
+ // Such literals must be handled as a special case here, since equality
+ // with Boolean constants have a special status internally within equality
+ // engine. In particular, the proofs constructed by EqProof conversion
+ // always produce proofs involving equalities with Boolean constants, and
+ // whose assumptions are only of the form P or (not P). However, in the
+ // case that (= P true) (resp (= P false)) is itself an input to the
+ // equality engine, we will explain in terms of P (resp. (not P)), which
+ // leads to a bogus proof, typically encountered in
+ // ProofNodeManager::mkScope.
+ //
+ // To correct this, we add an explicit *fact* that P holds by (= P true)
+ // here. This means that EqProof conversion may generate a proof where
+ // the internal equality (= P true) is justified by assumption P, and that
+ // afterwards, P is explained in terms of the original (external) equality
+ // (= P true) by the step provided here. This means that the proof may end
+ // up using (= P true) in a roundabout way (through two redundant steps),
+ // but regardless this allows the core proof utilities (EqProof
+ // conversion, proof equality engine, lazy proof, etc.) to be unconcerned
+ // with this case. Multiple users of the proof equality engine
+ // (SharedTermDatabase and TheoryArrays) require this special case.
+ if (atom[0].getKind() == kind::CONST_BOOLEAN
+ || atom[1].getKind() == kind::CONST_BOOLEAN)
+ {
+ Node nlit = Rewriter::rewrite(lit);
+ if (!CDProof::isSame(lit, nlit))
+ {
+ // use a rewrite step as a fact
+ std::vector<Node> pfChildren;
+ pfChildren.push_back(lit);
+ return assertFact(nlit, PfRule::MACRO_SR_PRED_ELIM, pfChildren, {});
+ }
+ }
+ }
+ return d_ee.assertEquality(atom, polarity, lit);
+ }
+ return d_ee.assertPredicate(atom, polarity, lit);
+}
+
+bool ProofEqEngine::assertFact(Node lit,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args)
+{
+ Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
+ << ", args = " << args << std::endl;
+
+ Node atom = lit.getKind() == NOT ? lit[0] : lit;
+ bool polarity = lit.getKind() != NOT;
+ // register the step in the proof
+ if (d_pfEnabled)
+ {
+ if (holds(atom, polarity))
+ {
+ // we do not process this fact if it already holds
+ return false;
+ }
+ // Buffer the step in the fact proof generator. We do this instead of
+ // adding explict steps to the lazy proof d_proof since CDProof has
+ // (at most) one proof for each formula. Thus, we "claim" only the
+ // formula that is proved by this fact. Otherwise, aliasing may occur,
+ // which leads to cyclic or bogus proofs.
+ ProofStep ps;
+ ps.d_rule = id;
+ ps.d_children = exp;
+ ps.d_args = args;
+ d_factPg.addStep(lit, ps);
+ // add lazy step to proof
+ d_proof.addLazyStep(lit, &d_factPg, false);
+ }
+ // second, assert it to the equality engine
+ Node reason = mkAnd(exp);
+ return assertFactInternal(atom, polarity, reason);
+}
+
+bool ProofEqEngine::assertFact(Node lit,
+ PfRule id,
+ Node exp,
+ const std::vector<Node>& args)
+{
+ Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
+ << ", args = " << args << std::endl;
+ Node atom = lit.getKind() == NOT ? lit[0] : lit;
+ bool polarity = lit.getKind() != NOT;
+ // register the step in the proof
+ if (d_pfEnabled)
+ {
+ if (holds(atom, polarity))
+ {
+ // we do not process this fact if it already holds
+ return false;
+ }
+ // must extract the explanation as a vector
+ std::vector<Node> expv;
+ // Flatten (single occurrences) of AND. We do not allow nested AND, it is
+ // the responsibilty of the caller to ensure these do not occur.
+ if (exp != d_true)
+ {
+ if (exp.getKind() == AND)
+ {
+ for (const Node& expc : exp)
+ {
+ // should not have doubly nested AND
+ Assert(expc.getKind() != AND);
+ expv.push_back(expc);
+ }
+ }
+ else
+ {
+ expv.push_back(exp);
+ }
+ }
+ // buffer the step in the fact proof generator
+ ProofStep ps;
+ ps.d_rule = id;
+ ps.d_children = expv;
+ ps.d_args = args;
+ d_factPg.addStep(lit, ps);
+ // add lazy step to proof
+ d_proof.addLazyStep(lit, &d_factPg, false);
+ }
+ // second, assert it to the equality engine
+ return assertFactInternal(atom, polarity, exp);
+}
+
+bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
+{
+ Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
+ << " via buffer with " << psb.getNumSteps() << " steps"
+ << std::endl;
+ Node atom = lit.getKind() == NOT ? lit[0] : lit;
+ bool polarity = lit.getKind() != NOT;
+ if (d_pfEnabled)
+ {
+ if (holds(atom, polarity))
+ {
+ // we do not process this fact if it already holds
+ return false;
+ }
+ // buffer the steps in the fact proof generator
+ const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
+ for (const std::pair<Node, ProofStep>& step : steps)
+ {
+ d_factPg.addStep(step.first, step.second);
+ }
+ // add lazy step to proof
+ d_proof.addLazyStep(lit, &d_factPg, false);
+ }
+ // second, assert it to the equality engine
+ return assertFactInternal(atom, polarity, exp);
+}
+
+bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
+{
+ Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
+ << " via generator" << std::endl;
+ Node atom = lit.getKind() == NOT ? lit[0] : lit;
+ bool polarity = lit.getKind() != NOT;
+ if (d_pfEnabled)
+ {
+ if (holds(atom, polarity))
+ {
+ // we do not process this fact if it already holds
+ return false;
+ }
+ // note the proof generator is responsible for remembering the explanation
+ d_proof.addLazyStep(lit, pg, false);
+ }
+ // second, assert it to the equality engine
+ return assertFactInternal(atom, polarity, exp);
+}
+
+TrustNode ProofEqEngine::assertConflict(Node lit)
+{
+ Trace("pfee") << "pfee::assertConflict " << lit << std::endl;
+ std::vector<TNode> assumps;
+ explainWithProof(lit, assumps, &d_proof);
+ if (d_pfEnabled)
+ {
+ // lit may not be equivalent to false, but should rewrite to false
+ if (lit != d_false)
+ {
+ Assert(Rewriter::rewrite(lit) == d_false)
+ << "pfee::assertConflict: conflict literal is not rewritable to "
+ "false";
+ std::vector<Node> exp;
+ exp.push_back(lit);
+ std::vector<Node> args;
+ if (!d_proof.addStep(d_false, PfRule::MACRO_SR_PRED_ELIM, exp, args))
+ {
+ Assert(false) << "pfee::assertConflict: failed conflict step";
+ return TrustNode::null();
+ }
+ }
+ }
+ return ensureProofForFact(
+ d_false, assumps, TrustNodeKind::CONFLICT, &d_proof);
+}
+
+TrustNode ProofEqEngine::assertConflict(PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args)
+{
+ Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp
+ << ", args = " << args << std::endl;
+ // conflict is same as proof of false
+ std::vector<Node> empVec;
+ return assertLemma(d_false, id, exp, empVec, args);
+}
+
+TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
+ ProofStepBuffer& psb)
+{
+ Trace("pfee") << "pfee::assertConflict " << exp << " via buffer with "
+ << psb.getNumSteps() << " steps" << std::endl;
+ if (d_pfEnabled)
+ {
+ if (!d_proof.addSteps(psb))
+ {
+ return TrustNode::null();
+ }
+ }
+ std::vector<Node> empVec;
+ return assertLemmaInternal(d_false, exp, empVec, &d_proof);
+}
+
+TrustNode ProofEqEngine::assertLemma(Node conc,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ const std::vector<Node>& args)
+{
+ Trace("pfee") << "pfee::assertLemma " << conc << " " << id
+ << ", exp = " << exp << ", noExplain = " << noExplain
+ << ", args = " << args << std::endl;
+ Assert(conc != d_true);
+ if (d_pfEnabled)
+ {
+ LazyCDProof tmpProof(d_pnm, &d_proof);
+ LazyCDProof* curr;
+ if (conc == d_false)
+ {
+ // optimization: we can use the main lazy proof directly, because we
+ // know we will backtrack immediately after this call.
+ curr = &d_proof;
+ }
+ else
+ {
+ // use a lazy proof that always links to d_proof
+ curr = &tmpProof;
+ }
+ // Register the proof step.
+ if (!curr->addStep(conc, id, exp, args))
+ {
+ // a step went wrong, e.g. during checking
+ Assert(false) << "pfee::assertConflict: register proof step";
+ return TrustNode::null();
+ }
+ // We've now decided which lazy proof to use (curr), now get the proof
+ // for conc.
+ return assertLemmaInternal(conc, exp, noExplain, curr);
+ }
+ // not using a proof
+ return assertLemmaInternal(conc, exp, noExplain, nullptr);
+}
+
+TrustNode ProofEqEngine::assertLemma(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofStepBuffer& psb)
+{
+ Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
+ << ", noExplain = " << noExplain << " via buffer with "
+ << psb.getNumSteps() << " steps" << std::endl;
+ if (d_pfEnabled)
+ {
+ LazyCDProof tmpProof(d_pnm, &d_proof);
+ LazyCDProof* curr;
+ // same policy as above: for conflicts, use existing lazy proof
+ if (conc == d_false)
+ {
+ curr = &d_proof;
+ }
+ else
+ {
+ curr = &tmpProof;
+ }
+ // add all steps to the proof
+ const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
+ for (const std::pair<Node, ProofStep>& ps : steps)
+ {
+ if (!curr->addStep(ps.first, ps.second))
+ {
+ return TrustNode::null();
+ }
+ }
+ return assertLemmaInternal(conc, exp, noExplain, curr);
+ }
+ return assertLemmaInternal(conc, exp, noExplain, nullptr);
+}
+
+TrustNode ProofEqEngine::assertLemma(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofGenerator* pg)
+{
+ Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
+ << ", noExplain = " << noExplain << " via buffer with generator"
+ << std::endl;
+ if (d_pfEnabled)
+ {
+ LazyCDProof tmpProof(d_pnm, &d_proof);
+ LazyCDProof* curr;
+ // same policy as above: for conflicts, use existing lazy proof
+ if (conc == d_false)
+ {
+ curr = &d_proof;
+ }
+ else
+ {
+ curr = &tmpProof;
+ }
+ // Register the proof step.
+ if (!pg->addProofTo(conc, curr))
+ {
+ // a step went wrong, e.g. during checking
+ Assert(false) << "pfee::assertConflict: register proof step";
+ return TrustNode::null();
+ }
+ return assertLemmaInternal(conc, exp, noExplain, curr);
+ }
+ return assertLemmaInternal(conc, exp, noExplain, nullptr);
+}
+
+TrustNode ProofEqEngine::explain(Node conc)
+{
+ Trace("pfee") << "pfee::explain " << conc << std::endl;
+ if (d_pfEnabled)
+ {
+ LazyCDProof tmpProof(d_pnm, &d_proof);
+ std::vector<TNode> assumps;
+ explainWithProof(conc, assumps, &tmpProof);
+ return ensureProofForFact(
+ conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
+ }
+ std::vector<TNode> assumps;
+ explainWithProof(conc, assumps, nullptr);
+ return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, nullptr);
+}
+
+TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ LazyCDProof* curr)
+{
+ // We are a conflict if the conclusion is false and all literals are
+ // explained.
+ TrustNodeKind tnk =
+ conc == d_false ? TrustNodeKind::CONFLICT : TrustNodeKind::LEMMA;
+
+ // get the explanation, with proofs
+ std::vector<TNode> assumps;
+ std::vector<Node> expn;
+ for (const Node& e : exp)
+ {
+ if (std::find(noExplain.begin(), noExplain.end(), e) == noExplain.end())
+ {
+ explainWithProof(e, assumps, curr);
+ }
+ else
+ {
+ // it did not have a proof; it was an assumption of the previous rule
+ assumps.push_back(e);
+ // it is not a conflict, since it may involve new literals
+ tnk = TrustNodeKind::LEMMA;
+ }
+ }
+ return ensureProofForFact(conc, assumps, tnk, curr);
+}
+
+TrustNode ProofEqEngine::ensureProofForFact(Node conc,
+ const std::vector<TNode>& assumps,
+ TrustNodeKind tnk,
+ LazyCDProof* curr)
+{
+ Trace("pfee-proof") << std::endl;
+ Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
+ << assumps << ", TrustNodeKind=" << tnk << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ // The proof
+ std::shared_ptr<ProofNode> pf;
+ ProofGenerator* pfg = nullptr;
+ // the explanation is the conjunction of assumptions
+ Node exp;
+ // If proofs are enabled, generate the proof and possibly modify the
+ // assumptions to match SCOPE.
+ if (d_pfEnabled)
+ {
+ Assert(curr != nullptr);
+ Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
+ << std::endl;
+ // get the proof for conc
+ std::shared_ptr<ProofNode> pfBody = curr->getProofFor(conc);
+ if (pfBody == nullptr)
+ {
+ Trace("pfee-proof")
+ << "pfee::ensureProofForFact: failed to make proof for fact"
+ << std::endl
+ << std::endl;
+ // should have existed
+ Assert(false) << "pfee::assertConflict: failed to get proof for " << conc;
+ return TrustNode::null();
+ }
+ // clone it so that we have a fresh copy
+ pfBody = pfBody->clone();
+ Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl;
+ // The free assumptions must be closed by assumps, which should be passed
+ // as arguments of SCOPE. However, some of the free assumptions may not
+ // literally be equal to assumps, for instance, due to symmetry. In other
+ // words, the SCOPE could be closing (= x y) in a proof with free
+ // assumption (= y x). We modify the proof leaves to account for this
+ // below.
+
+ std::vector<Node> scopeAssumps;
+ // we first ensure the assumptions are flattened
+ for (const TNode& a : assumps)
+ {
+ if (a.getKind() == AND)
+ {
+ scopeAssumps.insert(scopeAssumps.end(), a.begin(), a.end());
+ }
+ else
+ {
+ scopeAssumps.push_back(a);
+ }
+ }
+ // 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);
+ }
+ else
+ {
+ exp = mkAnd(assumps);
+ }
+ // Make the lemma or conflict node. This must exactly match the conclusion
+ // of SCOPE below.
+ Node formula;
+ if (tnk == TrustNodeKind::CONFLICT)
+ {
+ // conflict is negated
+ Assert(conc == d_false);
+ formula = exp;
+ }
+ else
+ {
+ formula =
+ exp == d_true
+ ? conc
+ : (conc == d_false ? exp.negate() : nm->mkNode(IMPLIES, exp, conc));
+ }
+ Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula
+ << std::endl;
+ if (d_pfEnabled)
+ {
+ // should always be non-null
+ Assert(pf != nullptr);
+ if (Trace.isOn("pfee-proof") || Trace.isOn("pfee-proof-final"))
+ {
+ Trace("pfee-proof") << "pfee::ensureProofForFact: printing proof"
+ << std::endl;
+ std::stringstream ss;
+ pf->printDebug(ss);
+ Trace("pfee-proof") << "pfee::ensureProofForFact: Proof is " << ss.str()
+ << std::endl;
+ }
+ // Should be a closed proof now. If it is not, then the overall proof
+ // is malformed.
+ Assert(pf->isClosed());
+ pfg = this;
+ // set the proof for the conflict or lemma, which can be queried later
+ switch (tnk)
+ {
+ case TrustNodeKind::CONFLICT: setProofForConflict(formula, pf); break;
+ case TrustNodeKind::LEMMA: setProofForLemma(formula, pf); break;
+ case TrustNodeKind::PROP_EXP: setProofForPropExp(conc, exp, pf); break;
+ default:
+ pfg = nullptr;
+ Unhandled() << "Unhandled trust node kind " << tnk;
+ break;
+ }
+ }
+ Trace("pfee-proof") << "pfee::ensureProofForFact: finish" << std::endl
+ << std::endl;
+ // we can provide a proof for conflict, lemma or explained propagation
+ switch (tnk)
+ {
+ case TrustNodeKind::CONFLICT:
+ return TrustNode::mkTrustConflict(formula, pfg);
+ case TrustNodeKind::LEMMA: return TrustNode::mkTrustLemma(formula, pfg);
+ case TrustNodeKind::PROP_EXP:
+ return TrustNode::mkTrustPropExp(conc, exp, pfg);
+ default: Unhandled() << "Unhandled trust node kind " << tnk; break;
+ }
+ return TrustNode::null();
+}
+
+bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
+{
+ Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity
+ << " " << reason << std::endl;
+ bool ret;
+ if (atom.getKind() == EQUAL)
+ {
+ ret = d_ee.assertEquality(atom, polarity, reason);
+ }
+ else
+ {
+ ret = d_ee.assertPredicate(atom, polarity, reason);
+ }
+ if (ret)
+ {
+ // must reference count the new atom and explanation
+ d_keep.insert(atom);
+ d_keep.insert(reason);
+ }
+ return ret;
+}
+
+bool ProofEqEngine::holds(TNode atom, bool polarity)
+{
+ if (atom.getKind() == EQUAL)
+ {
+ if (!d_ee.hasTerm(atom[0]) || !d_ee.hasTerm(atom[1]))
+ {
+ return false;
+ }
+ return polarity ? d_ee.areEqual(atom[0], atom[1])
+ : d_ee.areDisequal(atom[0], atom[1], false);
+ }
+ if (!d_ee.hasTerm(atom))
+ {
+ return false;
+ }
+ TNode b = polarity ? d_true : d_false;
+ return d_ee.areEqual(atom, b);
+}
+
+void ProofEqEngine::explainWithProof(Node lit,
+ std::vector<TNode>& assumps,
+ LazyCDProof* curr)
+{
+ if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
+ {
+ return;
+ }
+ std::shared_ptr<eq::EqProof> pf =
+ d_pfEnabled ? std::make_shared<eq::EqProof>() : nullptr;
+ Trace("pfee-proof") << "pfee::explainWithProof: " << lit << std::endl;
+ bool polarity = lit.getKind() != NOT;
+ TNode atom = polarity ? lit : lit[0];
+ Assert(atom.getKind() != AND);
+ std::vector<TNode> tassumps;
+ if (atom.getKind() == EQUAL)
+ {
+ if (atom[0] == atom[1])
+ {
+ return;
+ }
+ Assert(d_ee.hasTerm(atom[0]));
+ Assert(d_ee.hasTerm(atom[1]));
+ if (!polarity)
+ {
+ // ensure the explanation exists
+ AlwaysAssert(d_ee.areDisequal(atom[0], atom[1], true));
+ }
+ d_ee.explainEquality(atom[0], atom[1], polarity, tassumps, pf.get());
+ }
+ else
+ {
+ Assert(d_ee.hasTerm(atom));
+ d_ee.explainPredicate(atom, polarity, tassumps, pf.get());
+ }
+ Trace("pfee-proof") << "...got " << tassumps << std::endl;
+ // avoid duplicates
+ for (const TNode a : tassumps)
+ {
+ if (a == lit)
+ {
+ assumps.push_back(a);
+ }
+ else if (std::find(assumps.begin(), assumps.end(), a) == assumps.end())
+ {
+ assumps.push_back(a);
+ }
+ }
+ if (d_pfEnabled)
+ {
+ if (Trace.isOn("pfee-proof"))
+ {
+ Trace("pfee-proof") << "pfee::explainWithProof: add to proof ---"
+ << std::endl;
+ std::stringstream sse;
+ pf->debug_print(sse);
+ Trace("pfee-proof") << sse.str() << std::endl;
+ Trace("pfee-proof") << "---" << std::endl;
+ }
+ // add the steps in the equality engine proof to the Proof
+ pf->addToProof(curr);
+ }
+ 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)
+{
+}
+
+bool ProofEqEngine::FactProofGenerator::addStep(Node fact, ProofStep ps)
+{
+ if (d_facts.find(fact) != d_facts.end())
+ {
+ // duplicate
+ return false;
+ }
+ Node symFact = CDProof::getSymmFact(fact);
+ if (!symFact.isNull())
+ {
+ if (d_facts.find(symFact) != d_facts.end())
+ {
+ // duplicate due to symmetry
+ return false;
+ }
+ }
+ d_facts.insert(fact, std::make_shared<ProofStep>(ps));
+ return true;
+}
+
+std::shared_ptr<ProofNode> ProofEqEngine::FactProofGenerator::getProofFor(
+ Node fact)
+{
+ Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact
+ << std::endl;
+ NodeProofStepMap::iterator it = d_facts.find(fact);
+ if (it == d_facts.end())
+ {
+ Node symFact = CDProof::getSymmFact(fact);
+ if (symFact.isNull())
+ {
+ Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
+ Assert(false);
+ return nullptr;
+ }
+ it = d_facts.find(symFact);
+ if (it == d_facts.end())
+ {
+ Assert(false);
+ Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
+ return nullptr;
+ }
+ }
+ Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
+ CDProof cdp(d_pnm);
+ cdp.addStep(fact, *(*it).second);
+ return cdp.getProofFor(fact);
+}
+
+} // namespace eq
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file proof_equality_engine.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 proof-producing equality engine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
+#define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "expr/lazy_proof.h"
+#include "expr/node.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
+#include "expr/proof_step_buffer.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace eq {
+
+/**
+ * A layer on top of an EqualityEngine. The goal of this class is manage the
+ * use of an EqualityEngine object in such a way that the proper proofs are
+ * internally constructed, and can be retrieved from this class when
+ * necessary.
+ *
+ * Notice that this class is intended to be a *partial layer* on top of
+ * equality engine. A user of this class should still issue low-level calls
+ * (getRepresentative, areEqual, areDisequal, etc.) on the underlying equality
+ * engine directly. The methods that should *not* be called directly on the
+ * underlying equality engine are:
+ * - assertEquality/assertPredicate [*]
+ * - explain
+ * Instead, the user should use variants of the above methods provided by
+ * the public interface of this class.
+ *
+ * [*] the exception is that assertions from the fact queue (who are their own
+ * explanation) should be sent directly to the underlying equality engine. This
+ * is for the sake of efficiency.
+ *
+ * This class tracks the reason for why all facts are added to an EqualityEngine
+ * in a SAT-context dependent manner in a context-dependent (CDProof) object.
+ * It furthermore maintains an internal FactProofGenerator class for managing
+ * proofs of facts whose steps are explicitly provided (those that are given
+ * concrete PfRule, children, and args). Call these "simple facts".
+ *
+ * Overall, this class is an eager proof generator (theory/proof_generator.h),
+ * in that it stores (copies) of proofs for lemmas at the moment they are sent
+ * out.
+ *
+ * A theory that is proof producing and uses the equality engine may use this
+ * class to manage proofs that are justified by its underlying equality engine.
+ * In particular, the following interfaces are available for constructing
+ * a TrustNode:
+ * - assertConflict, when the user of the equality engine has discovered that
+ * false can be derived from the current state,
+ * - assertLemma, for lemmas/conflicts that can be (partially) explained in the
+ * current state,
+ * - explain, for explaining why a literal is true in the current state.
+ * Details on these methods can be found below.
+ */
+class ProofEqEngine : public EagerProofGenerator
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
+ NodeProofMap;
+
+ public:
+ ProofEqEngine(context::Context* c,
+ context::UserContext* u,
+ EqualityEngine& ee,
+ ProofNodeManager* pnm);
+ ~ProofEqEngine() {}
+ //-------------------------- assert assumption
+ /**
+ * Assert literal lit by assumption to the underlying equality engine. It is
+ * its own explanation.
+ *
+ * @param lit The literal to assert to the equality engine
+ * @return true if this fact was processed by this method. If lit already
+ * holds in the equality engine, this method returns false.
+ */
+ bool assertAssume(TNode lit);
+ //-------------------------- assert fact
+ /**
+ * Assert the literal lit by proof step id, given explanation exp and
+ * arguments args. This fact is
+ *
+ * @param lit The literal to assert to the equality engine
+ * @param id The proof rule of the proof step concluding lit
+ * @param exp The premises of the proof step concluding lit. These are also
+ * the premises that are used when calling explain(lit).
+ * @param args The arguments to the proof step concluding lit.
+ * @return true if this fact was processed by this method. If lit already
+ * holds in the equality engine, this method returns false.
+ */
+ bool assertFact(Node lit,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args);
+ /** Same as above but where exp is (conjunctive) node */
+ bool assertFact(Node lit, PfRule id, Node exp, const std::vector<Node>& args);
+ /**
+ * Multi-step version of assert fact via a proof step buffer. This method
+ * is similar to above, but the justification for lit may have multiple steps.
+ * In particular, we assume that psb has a list of proof steps where the
+ * proof step concluding lit has free assumptions exp.
+ *
+ * For example, a legal call to this method is such that:
+ * lit: A
+ * exp: B
+ * psb.d_steps: { A by (step id1 {B,C} {}), C by (step id2 {} {}) )
+ * In other words, A holds by a proof step with rule id1 and premises
+ * B and C, and C holds by proof step with rule id2 and no premises.
+ *
+ * @param lit The literal to assert to the equality engine.
+ * @param exp The premises of the proof steps concluding lit. These are also
+ * the premises that are used when calling explain(lit).
+ * @param psb The proof step buffer containing the proof steps.
+ * @return true if this fact was processed by this method. If lit already
+ * holds in the equality engine, this method returns false.
+ */
+ bool assertFact(Node lit, Node exp, ProofStepBuffer& psb);
+ /**
+ * Assert fact via generator pg. This method asserts lit with explanation exp
+ * to the equality engine of this class. It must be the case that pg can
+ * provide a proof for lit in terms of exp. More precisely, pg should be
+ * prepared in the remainder of the SAT context to respond to a call to
+ * ProofGenerator::getProofFor(lit), and return a proof whose free
+ * assumptions are a subset of the conjuncts of exp.
+ *
+ * @param lit The literal to assert to the equality engine.
+ * @param exp The premises of the proof concluding lit. These are also
+ * the premises that are used when calling explain(lit).
+ * @param pg The proof generator that can provide a proof concluding lit
+ * from free asumptions in exp.
+ * @return true if this fact was processed by this method. If lit already
+ * holds in the equality engine, this method returns false.
+ */
+ bool assertFact(Node lit, Node exp, ProofGenerator* pg);
+ //-------------------------- assert conflicts
+ /**
+ * This method is called when the equality engine of this class is
+ * inconsistent (false has been proven) by a contradictory literal lit. This
+ * returns the trust node corresponding to the current conflict.
+ *
+ * @param lit The conflicting literal, which must rewrite to false.
+ * @return The trust node capturing the fact that this class can provide a
+ * proof for this conflict.
+ */
+ TrustNode assertConflict(Node lit);
+ /**
+ * Get proven conflict from contradictory facts. This method is called when
+ * the proof rule with premises exp and arguments args implies a contradiction
+ * by proof rule id.
+ *
+ * This method returns the TrustNode containing the corresponding conflict
+ * resulting from adding this step, and ensures that a proof has been stored
+ * internally so that this class may respond to a call to
+ * ProofGenerator::getProof(...).
+ */
+ TrustNode assertConflict(PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& args);
+ /** Multi-step version */
+ TrustNode assertConflict(const std::vector<Node>& exp, ProofStepBuffer& psb);
+ //-------------------------- assert lemma
+ /**
+ * Called when we have concluded conc, typically via theory specific
+ * reasoning. The purpose of this method is to construct a TrustNode of
+ * kind TrustNodeKind::LEMMA or TrustNodeKind::CONFLICT corresponding to the
+ * lemma or conflict to be sent on the output channel of the Theory.
+ *
+ * The user provides the explanation of conc in two parts:
+ * (1) (exp \ noExplain), which are literals that hold in the equality engine
+ * of this class,
+ * (2) noExplain, which do not necessarily hold in the equality engine of this
+ * class.
+ * Notice that noExplain is a subset of exp.
+ *
+ * The proof for conc follows from exp by proof rule with the given
+ * id and arguments.
+ *
+ * This call corresponds to a conflict if conc is false and noExplain is
+ * empty.
+ *
+ * This returns the TrustNode corresponding to the formula corresonding to
+ * the call to this method [*], for which a proof can be provided by this
+ * generator in the remainder of the user context.
+ *
+ * [*]
+ * a. If this call does not correspond to a conflict, then this formula is:
+ * ( ^_{e in exp \ noExplain} <explain>(e) ^ noExplain ) => conc
+ * where <explain>(e) is a conjunction of literals L1 ^ ... ^ Ln such that
+ * L1 ^ ... ^ Ln entail e, and each Li was passed as an explanation to a
+ * call to assertFact in the current SAT context. This explanation method
+ * always succeeds, provided that e is a literal that currently holds in
+ * the equality engine of this class. Notice that if the antecedant is empty,
+ * the formula above is assumed to be conc itself. The above formula is
+ * intended to be valid in Theory that owns this class.
+ * b. If this call is a conflict, then this formula is:
+ * ^_{e in exp} <explain>(e)
+ * The formula can be queried via TrustNode::getProven in the standard way.
+ */
+ TrustNode assertLemma(Node conc,
+ PfRule id,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ const std::vector<Node>& args);
+ /** Multi-step version */
+ TrustNode assertLemma(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofStepBuffer& psb);
+ /** Generator version, where pg has a proof of conc */
+ TrustNode assertLemma(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ ProofGenerator* pg);
+ //-------------------------- explain
+ /**
+ * Explain literal conc. This calls the appropriate methods in the underlying
+ * equality engine of this class to construct the explanation of why conc
+ * currently holds.
+ *
+ * It returns a trust node of kind TrustNodeKind::PROP_EXP whose node
+ * is the explanation of conc (a conjunction of literals that implies it).
+ * The proof that can be proven by this generator is then (=> exp conc), see
+ * TrustNode::getPropExpProven(conc,exp);
+ *
+ * @param conc The conclusion to explain
+ * @return The trust node indicating the explanation of conc and the generator
+ * (this class) that can prove the implication.
+ */
+ TrustNode explain(Node conc);
+
+ private:
+ /**
+ * The default proof generator (for simple facts). This class is a context
+ * dependent mapping from formulas to proof steps. It does not generate
+ * ProofNode until it is asked to provide a proof for a given fact.
+ */
+ class FactProofGenerator : public ProofGenerator
+ {
+ typedef context::
+ CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
+ NodeProofStepMap;
+
+ public:
+ FactProofGenerator(context::Context* c, ProofNodeManager* pnm);
+ ~FactProofGenerator() {}
+ /** add step */
+ bool addStep(Node fact, ProofStep ps);
+ /** Get proof for */
+ std::shared_ptr<ProofNode> getProofFor(Node f) override;
+ /** identify */
+ std::string identify() const override { return "FactProofGenerator"; }
+
+ private:
+ /** maps expected to ProofStep */
+ NodeProofStepMap d_facts;
+ /** the proof node manager */
+ ProofNodeManager* d_pnm;
+ };
+ /** Assert internal */
+ bool assertFactInternal(TNode pred, bool polarity, TNode reason);
+ /** holds */
+ bool holds(TNode pred, bool polarity);
+ /**
+ * Assert lemma internal. This method is called for ensuring the proof of
+ * conc exists in curr, where exp / noExplain are the its explanation (see
+ * assertLemma). This method is used for conflicts as well, where noExplain
+ * must be empty and conc = d_false.
+ *
+ * If curr is null, no proof is constructed.
+ *
+ * This method returns the trust node of the lemma or conflict with this
+ * class as the proof generator.
+ */
+ TrustNode assertLemmaInternal(Node conc,
+ const std::vector<Node>& exp,
+ const std::vector<Node>& noExplain,
+ LazyCDProof* curr);
+ /**
+ * Ensure proof for fact. This is called by the above method after we have
+ * determined the final set of assumptions used for showing conc. This
+ * method is used for lemmas, conflicts, and explanations for propagations.
+ * The argument tnk is the kind of trust node to return.
+ */
+ TrustNode ensureProofForFact(Node conc,
+ 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) */
+ FactProofGenerator d_factPg;
+ /** common nodes */
+ Node d_true;
+ Node d_false;
+ /** the proof node manager */
+ ProofNodeManager* d_pnm;
+ /** The SAT-context-dependent proof object */
+ LazyCDProof d_proof;
+ /**
+ * The keep set of this class. This set is maintained to ensure that
+ * facts and their explanations are reference counted. Since facts and their
+ * explanations are SAT-context-dependent, this set is also
+ * SAT-context-dependent.
+ */
+ NodeSet d_keep;
+ /**
+ * Whether proofs are enabled. If this flag is false, then this class acts
+ * as a simplified interface to the EqualityEngine, without proofs.
+ */
+ bool d_pfEnabled;
+ /** Explain
+ *
+ * This adds to assumps the set of facts that were asserted to this
+ * class in the current SAT context by calls to assertAssume that are
+ * required for showing lit.
+ *
+ * This additionally registers the equality proof steps required to
+ * regress the explanation of lit.
+ */
+ void explainWithProof(Node lit,
+ std::vector<TNode>& assumps,
+ LazyCDProof* curr);
+};
+
+} // namespace eq
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */
projects / cvc5.git / commitdiff