From: Andrew Reynolds Date: Fri, 13 Nov 2020 21:12:35 +0000 (-0600) Subject: (proof-new) Enable proofs for datatypes (#5436) X-Git-Tag: cvc5-1.0.0~2599 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=117b00689149c20bf7106fd0ac931eb3dee57d89;p=cvc5.git (proof-new) Enable proofs for datatypes (#5436) This enables initial proof support in datatypes, which includes connecting the inference-to-proof constructor to the inference manager and making the proper calls to the inference manager using TheoryDatatypes. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c1e39f47e..b505871a3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -537,6 +537,10 @@ libcvc4_add_sources( theory/datatypes/inference.h theory/datatypes/inference_manager.cpp theory/datatypes/inference_manager.h + theory/datatypes/infer_proof_cons.cpp + theory/datatypes/infer_proof_cons.h + theory/datatypes/proof_checker.cpp + theory/datatypes/proof_checker.h theory/datatypes/sygus_datatype_utils.cpp theory/datatypes/sygus_datatype_utils.h theory/datatypes/sygus_extension.cpp diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp index 9c49b2a4e..806dfd418 100644 --- a/src/theory/datatypes/inference.cpp +++ b/src/theory/datatypes/inference.cpp @@ -93,9 +93,9 @@ bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma) // sent as a lemma in addPendingInference below. if (asLemma || mustCommunicateFact(d_conc, d_exp)) { - return d_im->processDtInference(d_conc, d_exp, d_id, true); + return d_im->processDtLemma(d_conc, d_exp, d_id); } - return d_im->processDtInference(d_conc, d_exp, d_id, false); + return d_im->processDtFact(d_conc, d_exp, d_id); } InferId DatatypesInference::getInferId() const { return d_id; } diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h index 6923d8a1e..1cf135a7b 100644 --- a/src/theory/datatypes/inference.h +++ b/src/theory/datatypes/inference.h @@ -34,7 +34,7 @@ enum class InferId : uint32_t INST, // (or ((_ is C1) t) V ... V ((_ is Cn) t)) SPLIT, - // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Ci) t) + // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Cj) t) LABEL_EXH, // (= t (Ci t1 ... tn)) => (= (sel_j t) rewrite((sel_j (Ci t1 ... tn)))) COLLAPSE_SEL, @@ -42,7 +42,7 @@ enum class InferId : uint32_t CLASH_CONFLICT, // ((_ is Ci) t) ^ (= t (Cj t1 ... tn)) => false TESTER_CONFLICT, - // ((_ is Ci) t) ^ (= t s) ^ ((_ is Cj) s) => false + // ((_ is Ci) t) ^ ((_ is Cj) s) ^ (= t s) => false TESTER_MERGE_CONFLICT, // bisimilarity for codatatypes BISIMILAR, diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index ddff97283..f391cacd9 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -28,18 +28,29 @@ namespace datatypes { InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, nullptr), + : InferenceManagerBuffered(t, state, pnm), d_inferenceLemmas("theory::datatypes::inferenceLemmas"), - d_inferenceFacts("theory::datatypes::inferenceFacts") + d_inferenceFacts("theory::datatypes::inferenceFacts"), + d_inferenceConflicts("theory::datatypes::inferenceConflicts"), + d_pnm(pnm), + d_ipc(pnm == nullptr ? nullptr + : new InferProofCons(state.getSatContext(), pnm)), + d_lemPg(pnm == nullptr + ? nullptr + : new EagerProofGenerator( + pnm, state.getUserContext(), "datatypes::lemPg")) { + d_false = NodeManager::currentNM()->mkConst(false); smtStatisticsRegistry()->registerStat(&d_inferenceLemmas); smtStatisticsRegistry()->registerStat(&d_inferenceFacts); + smtStatisticsRegistry()->registerStat(&d_inferenceConflicts); } InferenceManager::~InferenceManager() { smtStatisticsRegistry()->unregisterStat(&d_inferenceLemmas); smtStatisticsRegistry()->unregisterStat(&d_inferenceFacts); + smtStatisticsRegistry()->unregisterStat(&d_inferenceConflicts); } void InferenceManager::addPendingInference(Node conc, @@ -65,6 +76,34 @@ void InferenceManager::process() doPendingFacts(); } +void InferenceManager::sendDtLemma(Node lem, + InferId id, + LemmaProperty p, + bool doCache) +{ + if (isProofEnabled()) + { + processDtLemma(lem, Node::null(), id); + return; + } + // otherwise send as a normal lemma + if (lemma(lem, p, doCache)) + { + d_inferenceLemmas << id; + } +} + +void InferenceManager::sendDtConflict(const std::vector& conf, InferId id) +{ + if (isProofEnabled()) + { + Node exp = NodeManager::currentNM()->mkAnd(conf); + prepareDtInference(d_false, exp, id, d_ipc.get()); + } + conflictExp(conf, d_ipc.get()); + d_inferenceConflicts << id; +} + bool InferenceManager::sendLemmas(const std::vector& lemmas) { bool ret = false; @@ -78,44 +117,103 @@ bool InferenceManager::sendLemmas(const std::vector& lemmas) return ret; } -bool InferenceManager::processDtInference(Node conc, - Node exp, - InferId id, - bool asLemma) +bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; } + +bool InferenceManager::processDtLemma( + Node conc, Node exp, InferId id, LemmaProperty p, bool doCache) { - Trace("dt-lemma-debug") << "processDtInference : " << conc << " via " << exp - << " by " << id << ", asLemma = " << asLemma - << std::endl; - if (asLemma) + // set up a proof constructor + std::shared_ptr ipcl; + if (isProofEnabled()) + { + ipcl = std::make_shared(nullptr, d_pnm); + } + conc = prepareDtInference(conc, exp, id, ipcl.get()); + // send it as a lemma + Node lem; + if (!exp.isNull() && !exp.isConst()) + { + lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc); + } + else + { + lem = conc; + } + if (isProofEnabled()) { - // send it as a lemma - Node lem; + // store its proof + std::shared_ptr pbody = ipcl->getProofFor(conc); + std::shared_ptr pn = pbody; if (!exp.isNull() && !exp.isConst()) { - lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc); - } - else - { - lem = conc; + std::vector expv; + expv.push_back(exp); + pn = d_pnm->mkScope(pbody, expv); } - if (!lemma(lem)) + d_lemPg->setProofFor(lem, pn); + } + // use trusted lemma + TrustNode tlem = TrustNode::mkTrustLemma(lem, d_lemPg.get()); + if (!trustedLemma(tlem)) + { + Trace("dt-lemma-debug") << "...duplicate lemma" << std::endl; + return false; + } + d_inferenceLemmas << id; + return true; +} + +bool InferenceManager::processDtFact(Node conc, Node exp, InferId id) +{ + conc = prepareDtInference(conc, exp, id, d_ipc.get()); + // assert the internal fact, which has the same issue as above + bool polarity = conc.getKind() != NOT; + TNode atom = polarity ? conc : conc[0]; + if (isProofEnabled()) + { + std::vector expv; + if (!exp.isNull() && !exp.isConst()) { - Trace("dt-lemma-debug") << "...duplicate lemma" << std::endl; - return false; + expv.push_back(exp); } - d_inferenceLemmas << id; + assertInternalFact(atom, polarity, expv, d_ipc.get()); } else { - // assert the internal fact, which has the same issue as above - bool polarity = conc.getKind() != NOT; - TNode atom = polarity ? conc : conc[0]; + // use version without proofs assertInternalFact(atom, polarity, exp); - d_inferenceFacts << id; } + d_inferenceFacts << id; return true; } +Node InferenceManager::prepareDtInference(Node conc, + Node exp, + InferId id, + InferProofCons* ipc) +{ + Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp + << " by " << id << std::endl; + if (conc.getKind() == EQUAL && conc[0].getType().isBoolean()) + { + // must turn (= conc false) into (not conc) + conc = Rewriter::rewrite(conc); + } + if (isProofEnabled()) + { + Assert(ipc != nullptr); + // If proofs are enabled, notify the proof constructor. + // Notice that we have to reconstruct a datatypes inference here. This is + // because the inference in the pending vector may be destroyed as we are + // processing this inference, if we triggered to backtrack based on the + // call below, since it is a unique pointer. + std::shared_ptr di = + std::make_shared(this, conc, exp, id); + ipc->notifyFact(di); + } + return conc; +} + } // namespace datatypes } // namespace theory } // namespace CVC4 diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 163a736c4..88b2befd7 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -19,6 +19,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" +#include "theory/datatypes/infer_proof_cons.h" #include "theory/datatypes/inference.h" #include "theory/inference_manager_buffered.h" #include "util/statistics_registry.h" @@ -61,6 +62,17 @@ class InferenceManager : public InferenceManagerBuffered * or processed internally. */ void process(); + /** + * Send lemma immediately on the output channel + */ + void sendDtLemma(Node lem, + InferId i = InferId::NONE, + LemmaProperty p = LemmaProperty::NONE, + bool doCache = true); + /** + * Send conflict immediately on the output channel + */ + void sendDtConflict(const std::vector& conf, InferId i = InferId::NONE); /** * Send lemmas with property NONE on the output channel immediately. * Returns true if any lemma was sent. @@ -68,17 +80,48 @@ class InferenceManager : public InferenceManagerBuffered bool sendLemmas(const std::vector& lemmas); private: + /** Are proofs enabled? */ + bool isProofEnabled() const; /** - * Process datatype inference. We send a lemma if asLemma is true, and - * send an internal fact if asLemma is false. + * Process datatype inference as a lemma + */ + bool processDtLemma(Node conc, + Node exp, + InferId id, + LemmaProperty p = LemmaProperty::NONE, + bool doCache = true); + /** + * Process datatype inference as a fact + */ + bool processDtFact(Node conc, Node exp, InferId id); + /** + * Helper function for the above methods. Returns the conclusion, which + * may be modified so that it is compatible with proofs. If proofs are + * enabled, it ensures the proof constructor is ready to provide a proof + * of (=> exp conc). + * + * In particular, if conc is a Boolean equality, it is rewritten. This is + * to ensure that we do not assert equalities of the form (= t true) + * or (= t false) to the equality engine, which have a reserved internal + * status for proof generation. If this is not done, then it is possible + * to have proofs with missing connections and hence free assumptions. */ - bool processDtInference(Node conc, Node exp, InferId id, bool asLemma); + Node prepareDtInference(Node conc, Node exp, InferId id, InferProofCons* ipc); + /** The false node */ + Node d_false; /** * Counts the number of applications of each type of inference processed by - * the above method as facts and lemmas. + * the above method as facts, lemmas and conflicts. */ HistogramStat d_inferenceLemmas; HistogramStat d_inferenceFacts; + HistogramStat d_inferenceConflicts; + /** Pointer to the proof node manager */ + ProofNodeManager* d_pnm; + /** The inference to proof converter */ + std::unique_ptr d_ipc; + /** An eager proof generator for lemmas */ + std::unique_ptr d_lemPg; }; } // namespace datatypes diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index d60d8af32..6bfe136ce 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -68,6 +68,13 @@ TheoryDatatypes::TheoryDatatypes(Context* c, // indicate we are using the default theory state object d_theoryState = &d_state; d_inferManager = &d_im; + + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add checkers + d_pchecker.registerTo(pc); + } } TheoryDatatypes::~TheoryDatatypes() { @@ -317,7 +324,10 @@ void TheoryDatatypes::postCheck(Effort level) Trace("dt-split") << "*************Split for constructors on " << n << endl; Node lemma = utils::mkSplit(n, dt); Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; - d_im.lemma(lemma, LemmaProperty::SEND_ATOMS, false); + d_im.sendDtLemma(lemma, + InferId::SPLIT, + LemmaProperty::SEND_ATOMS, + false); } if( !options::dtBlastSplits() ){ break; @@ -662,7 +672,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ conf.push_back(unifEq); Trace("dt-conflict") << "CONFLICT: Clash conflict : " << conf << std::endl; - d_im.conflictExp(conf, nullptr); + d_im.sendDtConflict(conf, InferId::CLASH_CONFLICT); return; } else @@ -863,10 +873,10 @@ void TheoryDatatypes::addTester( //conflict because equivalence class contains a constructor std::vector conf; conf.push_back(t); - conf.push_back(eqc->d_constructor.get().eqNode(t_arg)); + conf.push_back(t_arg.eqNode(eqc->d_constructor.get())); Trace("dt-conflict") << "CONFLICT: Tester eq conflict " << conf << std::endl; - d_im.conflictExp(conf, nullptr); + d_im.sendDtConflict(conf, InferId::TESTER_CONFLICT); return; }else{ makeConflict = true; @@ -972,7 +982,7 @@ void TheoryDatatypes::addTester( conf.push_back(t); conf.push_back(jt[0].eqNode(t_arg)); Trace("dt-conflict") << "CONFLICT: Tester conflict : " << conf << std::endl; - d_im.conflictExp(conf, nullptr); + d_im.sendDtConflict(conf, InferId::TESTER_MERGE_CONFLICT); } } @@ -1030,7 +1040,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ conf.push_back(c.eqNode(t[0][0])); Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << conf << std::endl; - d_im.conflictExp(conf, nullptr); + d_im.sendDtConflict(conf, InferId::TESTER_CONFLICT); return; } } @@ -1055,7 +1065,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl; Node r; bool wrong = false; - Node eq_exp = c.eqNode(s[0]); + Node eq_exp = s[0].eqNode(c); if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){ Node selector = s.getOperator(); size_t constructorIndex = utils::indexOf(c.getOperator()); @@ -1087,15 +1097,14 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { if (s != rrs) { Node eq = s.eqNode(rrs); - Node peq = c.eqNode(s[0]); // Since collapsing selectors may generate new terms, we must send // this out as a lemma if it is of an external type, or otherwise we // may ask for the equality status of terms that only datatypes knows // about, see issue #5344. bool forceLemma = !s.getType().isDatatype(); Trace("datatypes-infer") << "DtInfer : collapse sel"; - Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl; - d_im.addPendingInference(eq, peq, forceLemma, InferId::COLLAPSE_SEL); + Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl; + d_im.addPendingInference(eq, eq_exp, forceLemma, InferId::COLLAPSE_SEL); } } } @@ -1587,7 +1596,7 @@ void TheoryDatatypes::checkCycles() { Assert(expl.size() > 0); Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << expl << std::endl; - d_im.conflictExp(expl, nullptr); + d_im.sendDtConflict(expl, InferId::CYCLE); return; } } @@ -1680,7 +1689,8 @@ void TheoryDatatypes::separateBisimilar( if( ncons.getKind()==APPLY_CONSTRUCTOR ) { Node cc = ncons.getOperator(); cn_cons[part[j]] = ncons; - if( mkExp ){ + if (mkExp && c != ncons) + { exp.push_back(c.eqNode(ncons)); } new_part[cc].push_back( part[j] ); @@ -1739,9 +1749,12 @@ void TheoryDatatypes::separateBisimilar( //set current node for( unsigned k=0; k > c_part_out; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 97fa9600a..45ce76504 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -27,6 +27,7 @@ #include "expr/node_trie.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/inference_manager.h" +#include "theory/datatypes/proof_checker.h" #include "theory/datatypes/sygus_extension.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" @@ -308,6 +309,8 @@ private: InferenceManager d_im; /** The notify class */ NotifyClass d_notify; + /** Proof checker for datatypes */ + DatatypesProofRuleChecker d_pchecker; };/* class TheoryDatatypes */ }/* CVC4::theory::datatypes namespace */