From: Andrew Reynolds Date: Wed, 9 Sep 2020 20:53:30 +0000 (-0500) Subject: (proof-new) Make proofs in term formula removal term context sensitive (#5008) X-Git-Tag: cvc5-1.0.0~2882 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ed06a895c7e2c5b83c8fd470c1ee4cf42827a7f;p=cvc5.git (proof-new) Make proofs in term formula removal term context sensitive (#5008) Previously term formula removal proofs didnt not take the term context into account. This updates it to make use of the term context sensitive support in TConvProofGenerator. More generally, it uses the term context computation as the standard way of caching the results of rewrites in this class (regardless of proofs). --- diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 74fcda668..ef21fe399 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -43,7 +43,9 @@ theory::TrustNode RemoveTermFormulas::run( std::vector& newSkolems, bool reportDeps) { - Node itesRemoved = run(assertion, newAsserts, newSkolems, false, false); + TCtxStack ctx(&d_rtfc); + ctx.pushInitial(assertion); + Node itesRemoved = run(ctx, newAsserts, newSkolems); // In some calling contexts, not necessary to report dependence information. if (reportDeps && options::unsatCores()) { @@ -68,32 +70,34 @@ theory::TrustNode RemoveTermFormulas::run( return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); } -Node RemoveTermFormulas::run(TNode node, +Node RemoveTermFormulas::run(TCtxStack& ctx, std::vector& output, - std::vector& newSkolems, - bool inQuant, - bool inTerm) + std::vector& newSkolems) { - // Current node - Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl; - - if( node.getKind()==kind::INST_PATTERN_LIST ){ + Assert(!ctx.empty()); + std::pair curr = ctx.getCurrent(); + ctx.pop(); + TNode node = curr.first; + if (node.getKind() == kind::INST_PATTERN_LIST) + { return Node(node); } + uint32_t cval = curr.second; + bool inQuant, inTerm; + RtfTermContext::getFlags(curr.second, inQuant, inTerm); + Debug("ite") << "removeITEs(" << node << ")" + << " " << inQuant << " " << inTerm << std::endl; // The result may be cached already - int cv = cacheVal( inQuant, inTerm ); - std::pair cacheKey(node, cv); NodeManager *nodeManager = NodeManager::currentNM(); - TermFormulaCache::const_iterator i = d_tfCache.find(cacheKey); - if (i != d_tfCache.end()) + TermFormulaCache::const_iterator itc = d_tfCache.find(curr); + if (itc != d_tfCache.end()) { - Node cached = (*i).second; + Node cached = (*itc).second; Debug("ite") << "removeITEs: in-cache: " << cached << endl; - return cached.isNull() ? Node(node) : cached; + return cached.isNull() ? Node(curr.first) : cached; } - TypeNode nodeType = node.getType(); Node skolem; Node newAssertion; @@ -110,6 +114,8 @@ Node RemoveTermFormulas::run(TNode node, skolem = getSkolemForNode(node); if (skolem.isNull()) { + Trace("rtf-proof-debug") + << "RemoveTermFormulas::run: make ITE skolem" << std::endl; // Make the skolem to represent the ITE SkolemManager* sm = nodeManager->getSkolemManager(); skolem = sm->mkPurifySkolem( @@ -125,6 +131,9 @@ Node RemoveTermFormulas::run(TNode node, // we justify it internally if (isProofEnabled()) { + Trace("rtf-proof-debug") + << "RemoveTermFormulas::run: justify " << newAssertion + << " with ITE axiom" << std::endl; // ---------------------- REMOVE_TERM_FORMULA_AXIOM // (ite node[0] // (= node node[1]) ------------- MACRO_SR_PRED_INTRO @@ -155,6 +164,8 @@ Node RemoveTermFormulas::run(TNode node, skolem = getSkolemForNode(node); if (skolem.isNull()) { + Trace("rtf-proof-debug") + << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl; // Make the skolem to represent the lambda SkolemManager* sm = nodeManager->getSkolemManager(); skolem = sm->mkPurifySkolem( @@ -194,9 +205,12 @@ Node RemoveTermFormulas::run(TNode node, // http://planetmath.org/hilbertsvarepsilonoperator. if (!inQuant || !expr::hasFreeVar(node)) { + // NOTE: we can replace by t if body is of the form (and (= z t) ...) skolem = getSkolemForNode(node); if (skolem.isNull()) { + Trace("rtf-proof-debug") + << "RemoveTermFormulas::run: make WITNESS skolem" << std::endl; // Make the skolem to witness the choice, which notice is handled // as a special case within SkolemManager::mkPurifySkolem. SkolemManager* sm = nodeManager->getSkolemManager(); @@ -225,10 +239,12 @@ Node RemoveTermFormulas::run(TNode node, // -------------------- SKOLEMIZE // node[1] * { x -> skolem } ProofGenerator* expg = sm->getProofGenerator(existsAssertion); - if (expg != nullptr) - { - d_lp->addLazyStep(existsAssertion, expg); - } + d_lp->addLazyStep(existsAssertion, + expg, + true, + "RemoveTermFormulas::run:skolem_pf", + false, + PfRule::WITNESS_AXIOM); d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {}); newAssertionPg = d_lp.get(); } @@ -243,6 +259,9 @@ Node RemoveTermFormulas::run(TNode node, skolem = getSkolemForNode(node); if (skolem.isNull()) { + Trace("rtf-proof-debug") + << "RemoveTermFormulas::run: make BOOLEAN_TERM_VARIABLE skolem" + << std::endl; // Make the skolem to represent the Boolean term // Skolems introduced for Boolean formulas appearing in terms have a // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled @@ -270,25 +289,34 @@ Node RemoveTermFormulas::run(TNode node, // if the term should be replaced by a skolem if( !skolem.isNull() ){ // Attach the skolem - d_tfCache.insert(cacheKey, skolem); + d_tfCache.insert(curr, skolem); + // this must be done regardless of whether the assertion was new below, + // since a formula-term may rewrite to the same skolem in multiple contexts. + if (isProofEnabled()) + { + // justify the introduction of the skolem + // ------------------- MACRO_SR_PRED_INTRO + // t = witness x. x=t + // The above step is trivial, since the skolems introduced above are + // all purification skolems. We record this equality in the term + // conversion proof generator. + d_tpg->addRewriteStep(node, + skolem, + PfRule::MACRO_SR_PRED_INTRO, + {}, + {node.eqNode(skolem)}, + cval); + } // if the skolem was introduced in this call if (!newAssertion.isNull()) { + Trace("rtf-proof-debug") + << "RemoveTermFormulas::run: setup proof for new assertion " + << newAssertion << std::endl; // if proofs are enabled if (isProofEnabled()) { - // justify the introduction of the skolem - // ------------------- MACRO_SR_PRED_INTRO - // t = witness x. x=t - // The above step is trivial, since the skolems introduced above are - // all purification skolems. We record this equality in the term - // conversion proof generator. - d_tpg->addRewriteStep(node, - skolem, - PfRule::MACRO_SR_PRED_INTRO, - {}, - {node.eqNode(skolem)}); // justify the axiom that defines the skolem, if not already done so if (newAssertionPg == nullptr) { @@ -300,16 +328,42 @@ Node RemoveTermFormulas::run(TNode node, newAssertion, PfRule::MACRO_SR_PRED_INTRO, {}, {newAssertion}); } } - Debug("ite") << "*** term formula removal introduced " << skolem - << " for " << node << std::endl; + Trace("rtf-debug") << "*** term formula removal introduced " << skolem + << " for " << node << std::endl; // Remove ITEs from the new assertion, rewrite it and push it to the // output - newAssertion = run(newAssertion, output, newSkolems, false, false); + Node newAssertionPre = newAssertion; + TCtxStack cctx(&d_rtfc); + cctx.pushInitial(newAssertion); + newAssertion = run(cctx, output, newSkolems); + + if (isProofEnabled()) + { + if (newAssertionPre != newAssertion) + { + Trace("rtf-proof-debug") + << "RemoveTermFormulas::run: setup proof for processed new lemma" + << std::endl; + // for new assertions that rewrite recursively + Node naEq = newAssertionPre.eqNode(newAssertion); + d_lp->addLazyStep(naEq, d_tpg.get()); + // ---------------- from lp ------------------------------- from tpg + // newAssertionPre newAssertionPre = newAssertion + // ------------------------------------------------------- EQ_RESOLVE + // newAssertion + d_lp->addStep( + newAssertion, PfRule::EQ_RESOLVE, {newAssertionPre, naEq}, {}); + } + } theory::TrustNode trna = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); + Trace("rtf-proof-debug") << "Checking closed..." << std::endl; + trna.debugCheckClosed("rtf-proof-debug", + "RemoveTermFormulas::run:new_assert"); + output.push_back(trna); newSkolems.push_back(skolem); } @@ -318,38 +372,29 @@ Node RemoveTermFormulas::run(TNode node, return skolem; } - if (node.isClosure()) - { - // Remember if we're inside a quantifier - inQuant = true; - }else if( !inTerm && hasNestedTermChildren( node ) ){ - // Remember if we're inside a term - Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; - inTerm = true; - } - // If not an ITE, go deep - vector newChildren; + std::vector newChildren; bool somethingChanged = false; if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { newChildren.push_back(node.getOperator()); } // Remove the ITEs from the children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, newSkolems, inQuant, inTerm); - somethingChanged |= (newChild != *it); + for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++) + { + ctx.pushChild(node, cval, i); + Node newChild = run(ctx, output, newSkolems); + somethingChanged |= (newChild != node[i]); newChildren.push_back(newChild); } // If changes, we rewrite if(somethingChanged) { Node cached = nodeManager->mkNode(node.getKind(), newChildren); - d_tfCache.insert(cacheKey, cached); + d_tfCache.insert(curr, cached); return cached; - } else { - d_tfCache.insert(cacheKey, Node::null()); - return node; } + d_tfCache.insert(curr, Node::null()); + return node; } Node RemoveTermFormulas::getSkolemForNode(Node node) const @@ -363,58 +408,53 @@ Node RemoveTermFormulas::getSkolemForNode(Node node) const return Node::null(); } -Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { +Node RemoveTermFormulas::replace(TNode node) const +{ + TCtxStack ctx(&d_rtfc); + ctx.pushInitial(node); + return replaceInternal(ctx); +} + +Node RemoveTermFormulas::replaceInternal(TCtxStack& ctx) const +{ + // get the current node, tagged with a term context identifier + Assert(!ctx.empty()); + std::pair curr = ctx.getCurrent(); + ctx.pop(); + TNode node = curr.first; + if( node.getKind()==kind::INST_PATTERN_LIST ){ return Node(node); } // Check the cache - NodeManager *nodeManager = NodeManager::currentNM(); - int cv = cacheVal( inQuant, inTerm ); - TermFormulaCache::const_iterator i = d_tfCache.find(make_pair(node, cv)); - if (i != d_tfCache.end()) + TermFormulaCache::const_iterator itc = d_tfCache.find(curr); + if (itc != d_tfCache.end()) { - Node cached = (*i).second; + Node cached = (*itc).second; return cached.isNull() ? Node(node) : cached; } - if (node.isClosure()) - { - // Remember if we're inside a quantifier - inQuant = true; - }else if( !inTerm && hasNestedTermChildren( node ) ){ - // Remember if we're inside a term - inTerm = true; - } - vector newChildren; bool somethingChanged = false; if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { newChildren.push_back(node.getOperator()); } // Replace in children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = replace(*it, inQuant, inTerm); - somethingChanged |= (newChild != *it); + uint32_t cval = curr.second; + for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++) + { + ctx.pushChild(node, cval, i); + Node newChild = replaceInternal(ctx); + somethingChanged |= (newChild != node[i]); newChildren.push_back(newChild); } // If changes, we rewrite if(somethingChanged) { - return nodeManager->mkNode(node.getKind(), newChildren); - } else { - return node; + return NodeManager::currentNM()->mkNode(node.getKind(), newChildren); } -} - -// returns true if the children of node should be considered nested terms -bool RemoveTermFormulas::hasNestedTermChildren( TNode node ) { - return theory::kindToTheoryId(node.getKind()) != theory::THEORY_BOOL - && node.getKind() != kind::EQUAL && node.getKind() != kind::SEP_STAR - && node.getKind() != kind::SEP_WAND - && node.getKind() != kind::SEP_LABEL - && node.getKind() != kind::BITVECTOR_EAGER_ATOM; - // dont' worry about FORALL or EXISTS (handled separately) + return node; } Node RemoveTermFormulas::getAxiomFor(Node n) @@ -438,7 +478,8 @@ void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm) nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, - "RemoveTermFormulas::TConvProofGenerator")); + "RemoveTermFormulas::TConvProofGenerator", + &d_rtfc)); d_lp.reset(new LazyCDProof( d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); } diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 78d5899d0..85f0c30d7 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -25,6 +25,7 @@ #include "context/context.h" #include "expr/lazy_proof.h" #include "expr/node.h" +#include "expr/term_context_stack.h" #include "expr/term_conversion_proof_generator.h" #include "smt/dump.h" #include "theory/eager_proof_generator.h" @@ -97,7 +98,7 @@ class RemoveTermFormulas { * Substitute under node using pre-existing cache. Do not remove * any ITEs not seen during previous runs. */ - Node replace(TNode node, bool inQuant = false, bool inTerm = false) const; + Node replace(TNode node) const; /** Returns true if e contains a term ite. */ bool containsTermITE(TNode e) const; @@ -120,11 +121,11 @@ class RemoveTermFormulas { static Node getAxiomFor(Node n); private: - typedef context:: - CDInsertHashMap, - Node, - PairHashFunction > - TermFormulaCache; + typedef context::CDInsertHashMap< + std::pair, + Node, + PairHashFunction > + TermFormulaCache; /** term formula removal cache * * This stores the results of term formula removal for inputs to the run(...) @@ -133,9 +134,6 @@ class RemoveTermFormulas { */ TermFormulaCache d_tfCache; - /** return the integer cache value for the input flags to run(...) */ - static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } - /** skolem cache * * This is a cache that maps terms to the skolem we use to replace them. @@ -163,9 +161,7 @@ class RemoveTermFormulas { */ inline Node getSkolemForNode(Node node) const; - static bool hasNestedTermChildren( TNode node ); - - /** A proof node manager */ + /** Pointer to a proof node manager */ ProofNodeManager* d_pnm; /** * A proof generator for the term conversion. @@ -176,6 +172,11 @@ class RemoveTermFormulas { * this class is responsible for. */ std::unique_ptr d_lp; + /** + * The remove term formula context, which computes hash values for term + * contexts. + */ + RtfTermContext d_rtfc; /** * Removes terms of the form (1), (2), (3) described above from node. @@ -188,11 +189,11 @@ class RemoveTermFormulas { * inTerm is whether we are are processing node in a "term" position, that is, it is a subterm * of a parent term that is not a Boolean connective. */ - Node run(TNode node, + Node run(TCtxStack& cxt, std::vector& newAsserts, - std::vector& newSkolems, - bool inQuant, - bool inTerm); + std::vector& newSkolems); + /** Replace internal */ + Node replaceInternal(TCtxStack& ctx) const; /** Whether proofs are enabled */ bool isProofEnabled() const;