From 70c0635bf490d237088b6675254408d965468272 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Nov 2020 08:36:28 -0600 Subject: [PATCH] (proof-new) Add datatypes inference to proof constructor (#5408) This adds the module that constructs proofs from inference steps. A followup PR will integrate proof support into the datatypes inference manager. --- src/theory/datatypes/infer_proof_cons.cpp | 275 ++++++++++++++++++++++ src/theory/datatypes/infer_proof_cons.h | 99 ++++++++ 2 files changed, 374 insertions(+) create mode 100644 src/theory/datatypes/infer_proof_cons.cpp create mode 100644 src/theory/datatypes/infer_proof_cons.h diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp new file mode 100644 index 000000000..443218bf4 --- /dev/null +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -0,0 +1,275 @@ +/********************* */ +/*! \file infer_proof_cons.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 inference to proof conversion for datatypes + **/ + +#include "theory/datatypes/infer_proof_cons.h" + +#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace datatypes { + +InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm) + : d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c) +{ + Assert(d_pnm != nullptr); +} + +void InferProofCons::notifyFact(const std::shared_ptr& di) +{ + TNode fact = di->d_conc; + if (d_lazyFactMap.find(fact) != d_lazyFactMap.end()) + { + return; + } + Node symFact = CDProof::getSymmFact(fact); + if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end()) + { + return; + } + d_lazyFactMap.insert(fact, di); +} + +void InferProofCons::convert(InferId infer, TNode conc, TNode exp, CDProof* cdp) +{ + Trace("dt-ipc") << "convert: " << infer << ": " << conc << " by " << exp + << std::endl; + // split into vector + std::vector expv; + if (!exp.isNull() && !exp.isConst()) + { + if (exp.getKind() == AND) + { + for (const Node& ec : exp) + { + expv.push_back(ec); + } + } + else + { + expv.push_back(exp); + } + } + NodeManager* nm = NodeManager::currentNM(); + bool success = false; + switch (infer) + { + case InferId::UNIF: + { + Assert(expv.size() == 1); + Assert(exp.getKind() == EQUAL && exp[0].getKind() == APPLY_CONSTRUCTOR + && exp[1].getKind() == APPLY_CONSTRUCTOR + && exp[0].getOperator() == exp[1].getOperator()); + Node narg; + // we may be asked for a proof of (not P) coming from (= P false) or + // (= false P), or similarly P from (= P true) or (= true P). + bool concPol = conc.getKind() != NOT; + Node concAtom = concPol ? conc : conc[0]; + Node unifConc = conc; + for (size_t i = 0, nchild = exp[0].getNumChildren(); i < nchild; i++) + { + bool argSuccess = false; + if (conc.getKind() == EQUAL) + { + argSuccess = (exp[0][i] == conc[0] && exp[1][i] == conc[1]); + } + else + { + for (size_t j = 0; j < 2; j++) + { + if (exp[j][i] == concAtom && exp[1 - j][i].isConst() + && exp[1 - j][i].getConst() == concPol) + { + argSuccess = true; + unifConc = exp[0][i].eqNode(exp[1][i]); + break; + } + } + } + if (argSuccess) + { + narg = nm->mkConst(Rational(i)); + break; + } + } + if (!narg.isNull()) + { + if (conc.getKind() == EQUAL) + { + // normal case where we conclude an equality + cdp->addStep(conc, PfRule::DT_UNIF, {exp}, {narg}); + } + else + { + // must use true or false elim to prove the final + cdp->addStep(unifConc, PfRule::DT_UNIF, {exp}, {narg}); + // may use symmetry + Node eq = concAtom.eqNode(nm->mkConst(concPol)); + cdp->addStep( + conc, concPol ? PfRule::TRUE_ELIM : PfRule::FALSE_ELIM, {eq}, {}); + } + success = true; + } + } + break; + case InferId::INST: + { + if (expv.size() == 1) + { + Assert(conc.getKind() == EQUAL); + int n = utils::isTester(exp); + if (n >= 0) + { + Node t = exp[0]; + Node nn = nm->mkConst(Rational(n)); + Node eq = exp.eqNode(conc); + cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn}); + cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {}); + success = true; + } + } + } + break; + case InferId::SPLIT: + { + Assert(expv.empty()); + Node t = conc.getKind() == OR ? conc[0][0] : conc[0]; + cdp->addStep(conc, PfRule::DT_SPLIT, {}, {t}); + success = true; + } + break; + case InferId::COLLAPSE_SEL: + { + Assert(exp.getKind() == EQUAL); + Node concEq = conc; + // might be a Boolean conclusion + if (conc.getKind() != EQUAL) + { + bool concPol = conc.getKind() != NOT; + Node concAtom = concPol ? conc : conc[0]; + concEq = concAtom.eqNode(nm->mkConst(concPol)); + } + Assert(concEq.getKind() == EQUAL + && concEq[0].getKind() == APPLY_SELECTOR_TOTAL); + Assert(exp[0].getType().isDatatype()); + Node sop = concEq[0].getOperator(); + Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]); + Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]); + // exp[0] = exp[1] + // --------------------- CONG ----------------- DT_COLLAPSE + // s(exp[0]) = s(exp[1]) s(exp[1]) = r + // --------------------------------------------------- TRANS + // s(exp[0]) = r + Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL); + Node seq = sl.eqNode(sr); + cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop}); + Node sceq = sr.eqNode(concEq[1]); + cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr}); + cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {}); + if (conc.getKind() != EQUAL) + { + PfRule eid = + conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM; + cdp->addStep(conc, eid, {concEq}, {}); + } + success = true; + } + break; + case InferId::CLASH_CONFLICT: + { + cdp->addStep(conc, PfRule::MACRO_SR_PRED_ELIM, {exp}, {}); + success = true; + } + break; + case InferId::TESTER_CONFLICT: + { + // rewrites to false under substitution + Node fn = nm->mkConst(false); + cdp->addStep(fn, PfRule::MACRO_SR_PRED_ELIM, expv, {}); + success = true; + } + break; + case InferId::TESTER_MERGE_CONFLICT: + { + Assert(expv.size() == 3); + Node tester1 = expv[0]; + Node tester1c = + nm->mkNode(APPLY_TESTER, expv[1].getOperator(), expv[0][0]); + cdp->addStep(tester1c, + PfRule::MACRO_SR_PRED_TRANSFORM, + {expv[1], expv[2]}, + {tester1c}); + Node fn = nm->mkConst(false); + cdp->addStep(fn, PfRule::DT_CLASH, {tester1, tester1c}, {}); + success = true; + } + break; + // inferences currently not supported + case InferId::LABEL_EXH: + case InferId::BISIMILAR: + case InferId::CYCLE: + default: + Trace("dt-ipc") << "...no conversion for inference " << infer + << std::endl; + break; + } + + if (!success) + { + // failed to reconstruct, add trust + Trace("dt-ipc") << "...failed " << infer << std::endl; + cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc}); + } + else + { + Trace("dt-ipc") << "...success" << std::endl; + } +} + +std::shared_ptr InferProofCons::getProofFor(Node fact) +{ + Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl; + // temporary proof + CDProof pf(d_pnm); + // get the inference + NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact); + if (it == d_lazyFactMap.end()) + { + Node factSym = CDProof::getSymmFact(fact); + if (!factSym.isNull()) + { + // Use the symmetric fact. There is no need to explictly make a + // SYMM proof, as this is handled by CDProof::getProofFor below. + it = d_lazyFactMap.find(factSym); + } + } + AlwaysAssert(it != d_lazyFactMap.end()); + // now go back and convert it to proof steps and add to proof + std::shared_ptr di = (*it).second; + // run the conversion + convert(di->getInferId(), di->d_conc, di->d_exp, &pf); + return pf.getProofFor(fact); +} + +std::string InferProofCons::identify() const +{ + return "datatypes::InferProofCons"; +} + +} // namespace datatypes +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h new file mode 100644 index 000000000..34e042237 --- /dev/null +++ b/src/theory/datatypes/infer_proof_cons.h @@ -0,0 +1,99 @@ +/********************* */ +/*! \file infer_proof_cons.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Inference to proof conversion for datatypes + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H +#define CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H + +#include + +#include "expr/node.h" +#include "expr/proof_generator.h" +#include "theory/datatypes/inference.h" +#include "theory/theory_proof_step_buffer.h" + +namespace CVC4 { +namespace theory { +namespace datatypes { + +/** + * Converts between the datatype-specific (untrustworthy) DatatypesInference + * class and information about how to construct a trustworthy proof step + * (PfRule, children, args). It acts as a (lazy) proof generator where the + * former is registered via notifyFact and the latter is asked for in + * getProofFor, typically by the proof equality engine. + * + * The main (private) method of this class is convert below, which is + * called when we need to construct a proof node from an InferInfo. + */ +class InferProofCons : public ProofGenerator +{ + typedef context:: + CDHashMap, NodeHashFunction> + NodeDatatypesInferenceMap; + + public: + InferProofCons(context::Context* c, ProofNodeManager* pnm); + ~InferProofCons() {} + /** + * This is called to notify that di is an inference that may need a proof + * in the future. + * + * In detail, this class should be prepared to respond to a call to: + * getProofFor(di.d_conc) + * in the remainder of the SAT context. This method copies di and stores it + * in the context-dependent map d_lazyFactMap below. + * + * This is used for lazy proof construction, where proofs are constructed + * only for facts that are explained. + */ + void notifyFact(const std::shared_ptr& di); + + /** + * This returns the proof for fact. This is required for using this class as + * a lazy proof generator. + * + * It should be the case that a call was made to notifyFact(di) where + * di.d_conc is fact in this SAT context. + */ + std::shared_ptr getProofFor(Node fact) override; + /** Identify this generator (for debugging, etc..) */ + virtual std::string identify() const override; + + private: + /** convert + * + * This method is called when the theory of strings makes an inference + * described by an InferInfo, whose fields are given by the first four + * arguments of this method. + * + * This method converts this call to instructions on what the proof rule + * step(s) are for concluding the conclusion of the inference. This + * information is stored in cdp. + */ + void convert(InferId infer, TNode conc, TNode exp, CDProof* cdp); + /** A dummy context used by this class if none is provided */ + context::Context d_context; + /** the proof node manager */ + ProofNodeManager* d_pnm; + /** The lazy fact map */ + NodeDatatypesInferenceMap d_lazyFactMap; +}; + +} // namespace datatypes +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H */ -- 2.30.2