From: Andrew Reynolds Date: Thu, 27 Aug 2020 20:04:03 +0000 (-0500) Subject: (proof-new) Add the proof equality engine (#4881) X-Git-Tag: cvc5-1.0.0~2950 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4adff162770a841d136ec44146928c2296eaf1b2;p=cvc5.git (proof-new) Add the proof equality engine (#4881) This is a (partial) layer on top of EqualityEngine that is a universal black box proof generator for users of the equality engine. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index df981db2d..e86f3e491 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -856,6 +856,8 @@ libcvc4_add_sources( theory/uf/eq_proof.h theory/uf/proof_checker.cpp theory/uf/proof_checker.h + theory/uf/proof_equality_engine.cpp + theory/uf/proof_equality_engine.h theory/uf/ho_extension.cpp theory/uf/ho_extension.h theory/uf/symmetry_breaker.cpp diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp new file mode 100644 index 000000000..274a46b26 --- /dev/null +++ b/src/theory/uf/proof_equality_engine.cpp @@ -0,0 +1,754 @@ +/********************* */ +/*! \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 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& exp, + const std::vector& 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& 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 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>& steps = psb.getSteps(); + for (const std::pair& 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 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 exp; + exp.push_back(lit); + std::vector 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& exp, + const std::vector& args) +{ + Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp + << ", args = " << args << std::endl; + // conflict is same as proof of false + std::vector empVec; + return assertLemma(d_false, id, exp, empVec, args); +} + +TrustNode ProofEqEngine::assertConflict(const std::vector& 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 empVec; + return assertLemmaInternal(d_false, exp, empVec, &d_proof); +} + +TrustNode ProofEqEngine::assertLemma(Node conc, + PfRule id, + const std::vector& exp, + const std::vector& noExplain, + const std::vector& 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& exp, + const std::vector& 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>& steps = psb.getSteps(); + for (const std::pair& 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& exp, + const std::vector& 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 assumps; + explainWithProof(conc, assumps, &tmpProof); + return ensureProofForFact( + conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof); + } + std::vector assumps; + explainWithProof(conc, assumps, nullptr); + return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, nullptr); +} + +TrustNode ProofEqEngine::assertLemmaInternal(Node conc, + const std::vector& exp, + const std::vector& 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 assumps; + std::vector 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& 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 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 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 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& assumps, + LazyCDProof* curr) +{ + if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end()) + { + return; + } + std::shared_ptr pf = + d_pfEnabled ? std::make_shared() : 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 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& 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& 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(ps)); + return true; +} + +std::shared_ptr 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 diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h new file mode 100644 index 000000000..2ee379509 --- /dev/null +++ b/src/theory/uf/proof_equality_engine.h @@ -0,0 +1,356 @@ +/********************* */ +/*! \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 +#include + +#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 NodeSet; + typedef context::CDHashMap, 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& exp, + const std::vector& args); + /** Same as above but where exp is (conjunctive) node */ + bool assertFact(Node lit, PfRule id, Node exp, const std::vector& 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& exp, + const std::vector& args); + /** Multi-step version */ + TrustNode assertConflict(const std::vector& 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} (e) ^ noExplain ) => conc + * where (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} (e) + * The formula can be queried via TrustNode::getProven in the standard way. + */ + TrustNode assertLemma(Node conc, + PfRule id, + const std::vector& exp, + const std::vector& noExplain, + const std::vector& args); + /** Multi-step version */ + TrustNode assertLemma(Node conc, + const std::vector& exp, + const std::vector& noExplain, + ProofStepBuffer& psb); + /** Generator version, where pg has a proof of conc */ + TrustNode assertLemma(Node conc, + const std::vector& exp, + const std::vector& 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, NodeHashFunction> + NodeProofStepMap; + + public: + FactProofGenerator(context::Context* c, ProofNodeManager* pnm); + ~FactProofGenerator() {} + /** add step */ + bool addStep(Node fact, ProofStep ps); + /** Get proof for */ + std::shared_ptr 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& exp, + const std::vector& 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& 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& a); + Node mkAnd(const std::vector& 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& assumps, + LazyCDProof* curr); +}; + +} // namespace eq +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */