From: Andrew Reynolds Date: Wed, 2 Sep 2020 19:01:39 +0000 (-0500) Subject: (proof-new) Add proof support in TheoryUF (#5002) X-Git-Tag: cvc5-1.0.0~2913 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c17f9b25cac7c0d2941ef136466cb750cf4c3e7b;p=cvc5.git (proof-new) Add proof support in TheoryUF (#5002) This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled. This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct. Co-authored-by: Haniel Barbosa --- diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 0a45c6790..bd58fc787 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -94,6 +94,8 @@ const char* toString(PfRule id) case PfRule::TRUE_ELIM: return "TRUE_ELIM"; case PfRule::FALSE_INTRO: return "FALSE_INTRO"; case PfRule::FALSE_ELIM: return "FALSE_ELIM"; + case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; + case PfRule::HO_CONG: return "HO_CONG"; //================================================= Quantifiers rules case PfRule::WITNESS_INTRO: return "WITNESS_INTRO"; case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 59c406d28..b6b9f1ea8 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -520,6 +520,20 @@ enum class PfRule : uint32_t // ---------------------------------------- // Conclusion: (not F) FALSE_ELIM, + // ======== HO trust + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t)) + // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y) + HO_APP_ENCODE, + // ======== Congruence + // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn)) + // Arguments: () + // --------------------------------------------- + // Conclusion: (= (f t1 ... tn) (g s1 ... sn)) + // Notice that this rule is only used when the application kinds are APPLY_UF. + HO_CONG, //================================================= Quantifiers rules // ======== Witness intro diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 11b872e72..2a57cde5e 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -18,7 +18,6 @@ #include "expr/node_algorithm.h" #include "options/uf_options.h" #include "theory/theory_model.h" -#include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_rewriter.h" using namespace std; @@ -28,9 +27,9 @@ namespace CVC4 { namespace theory { namespace uf { -HoExtension::HoExtension(TheoryUF& p, TheoryState& state) - : d_parent(p), - d_state(state), +HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im) + : d_state(state), + d_im(im), d_extensionality(state.getUserContext()), d_uf_std_skolem(state.getUserContext()) { @@ -108,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq) Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc); Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl; - d_parent.getOutputChannel().lemma(lem); + d_im.lemma(lem); return 1; } return 0; @@ -168,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) Trace("uf-ho-lemma") << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem << std::endl; - d_parent.getOutputChannel().lemma(lem); + d_im.lemma(lem); d_uf_std_skolem[f] = new_f; } else @@ -257,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) Node lem = nm->mkNode(OR, deq.negate(), eq); Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem << std::endl; - d_parent.getOutputChannel().lemma(lem); + d_im.lemma(lem); return 1; } } @@ -282,10 +281,10 @@ unsigned HoExtension::applyAppCompletion(TNode n) Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n); if (!ee->hasTerm(ret) || !ee->areEqual(ret, n)) { - Node eq = ret.eqNode(n); + Node eq = n.eqNode(ret); Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq << std::endl; - ee->assertEquality(eq, true, d_true); + d_im.assertInternalFact(eq, true, PfRule::HO_APP_ENCODE, {}, {n}); return 1; } Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." @@ -442,7 +441,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) Node eq = n.eqNode(hn); Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq << std::endl; - d_parent.getOutputChannel().lemma(eq); + d_im.lemma(eq); return false; } } diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index 25cb3623b..ceb8e9c12 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -21,6 +21,7 @@ #include "context/cdhashset.h" #include "context/cdo.h" #include "expr/node.h" +#include "theory/theory_inference_manager.h" #include "theory/theory_model.h" #include "theory/theory_state.h" @@ -51,7 +52,7 @@ class HoExtension typedef context::CDHashMap NodeNodeMap; public: - HoExtension(TheoryUF& p, TheoryState& state); + HoExtension(TheoryState& state, TheoryInferenceManager& im); /** expand definition * @@ -181,10 +182,10 @@ class HoExtension private: /** common constants */ Node d_true; - /** the parent of this extension */ - TheoryUF& d_parent; /** Reference to the state object */ TheoryState& d_state; + /** Reference to the inference manager */ + TheoryInferenceManager& d_im; /** extensionality has been applied to these disequalities */ NodeSet d_extensionality; diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp index b010b6d17..ea95c1f24 100644 --- a/src/theory/uf/proof_checker.cpp +++ b/src/theory/uf/proof_checker.cpp @@ -14,6 +14,8 @@ #include "theory/uf/proof_checker.h" +#include "theory/uf/theory_uf_rewriter.h" + using namespace CVC4::kind; namespace CVC4 { @@ -31,6 +33,8 @@ void UfProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::TRUE_ELIM, this); pc->registerChecker(PfRule::FALSE_INTRO, this); pc->registerChecker(PfRule::FALSE_ELIM, this); + pc->registerChecker(PfRule::HO_CONG, this); + pc->registerChecker(PfRule::HO_APP_ENCODE, this); } Node UfProofRuleChecker::checkInternal(PfRule id, @@ -171,6 +175,32 @@ Node UfProofRuleChecker::checkInternal(PfRule id, } return children[0][0].notNode(); } + if (id == PfRule::HO_CONG) + { + Assert(children.size() > 0); + std::vector lchildren; + std::vector rchildren; + for (size_t i = 0, nchild = children.size(); i < nchild; ++i) + { + Node eqp = children[i]; + if (eqp.getKind() != EQUAL) + { + return Node::null(); + } + lchildren.push_back(eqp[0]); + rchildren.push_back(eqp[1]); + } + NodeManager* nm = NodeManager::currentNM(); + Node l = nm->mkNode(kind::APPLY_UF, lchildren); + Node r = nm->mkNode(kind::APPLY_UF, rchildren); + return l.eqNode(r); + } + else if (id == PfRule::HO_APP_ENCODE) + { + Assert(args.size() == 1); + Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]); + return args[0].eqNode(ret); + } // no rule return Node::null(); } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3d90637e2..a58834891 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -53,7 +53,8 @@ TheoryUF::TheoryUF(context::Context* c, d_ho(nullptr), d_functionsTerms(c), d_symb(u, instanceName), - d_state(c, u, valuation) + d_state(c, u, valuation), + d_im(*this, d_state, pnm) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -62,8 +63,9 @@ TheoryUF::TheoryUF(context::Context* c, { d_ufProofChecker.registerTo(pc); } - // indicate we are using the default theory state object + // indicate we are using the default theory state and inference managers d_theoryState = &d_state; + d_inferManager = &d_im; } TheoryUF::~TheoryUF() { @@ -96,7 +98,7 @@ void TheoryUF::finishInit() { if (options::ufHo()) { d_equalityEngine->addFunctionKind(kind::HO_APPLY); - d_ho.reset(new HoExtension(*this, d_state)); + d_ho.reset(new HoExtension(d_state, d_im)); } } @@ -304,12 +306,7 @@ void TheoryUF::explain(TNode literal, Node& exp) exp = mkAnd(assumptions); } -TrustNode TheoryUF::explain(TNode literal) -{ - Node explanation; - explain(literal, explanation); - return TrustNode::mkTrustPropExp(literal, explanation, nullptr); -} +TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); } bool TheoryUF::collectModelValues(TheoryModel* m, const std::set& termSet) { @@ -338,7 +335,8 @@ void TheoryUF::presolve() { i != newClauses.end(); ++i) { Debug("uf") << "uf: generating a lemma: " << *i << std::endl; - d_out->lemma(*i); + // no proof generator provided + d_im.lemma(*i); } } if( d_thss ){ @@ -652,10 +650,10 @@ void TheoryUF::computeCareGraph() { void TheoryUF::conflict(TNode a, TNode b) { - Node conf; - explain(a.eqNode(b), conf); - d_out->conflict(conf); - d_state.notifyInConflict(); + // call the inference manager, which will construct the conflict (possibly + // with proofs from the underlying proof equality engine), and notify the + // state object. + d_im.conflictEqConstantMerge(a, b); } void TheoryUF::eqNotifyNewClass(TNode t) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 41f2ba9d5..4a8369483 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -26,6 +26,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_checker.h" +#include "theory/uf/proof_equality_engine.h" #include "theory/uf/symmetry_breaker.h" #include "theory/uf/theory_uf_rewriter.h" @@ -205,6 +206,8 @@ private: UfProofRuleChecker d_ufProofChecker; /** A (default) theory state object */ TheoryState d_state; + /** A (default) inference manager */ + TheoryInferenceManager d_im; };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index e651edb51..5d301cf9e 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -22,6 +22,7 @@ #include "expr/node_algorithm.h" #include "options/uf_options.h" +#include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/theory_rewriter.h"