From dcc1a5ff44ed83bdc1e2abcac3aebb299a376b08 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Feb 2021 18:21:56 -0600 Subject: [PATCH] Do not traverse quantifiers in term formula removal (#5859) Our current policy for term formula removal leaves quantifier bodies unchanged. This simplifies the code based on this observation. --- src/smt/term_formula_removal.cpp | 92 ++++++++++++++++---------------- 1 file changed, 47 insertions(+), 45 deletions(-) diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 0df521c0b..0b9d2d9c9 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -180,6 +180,11 @@ Node RemoveTermFormulas::runInternal(TNode assertion, ctx.pop(); processedChildren.pop_back(); } + else if (node.isClosure()) + { + // currently, we never do any term formula removal in quantifier bodies + d_tfCache.insert(curr, node); + } else { size_t nchild = node.getNumChildren(); @@ -253,6 +258,7 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, RtfTermContext::getFlags(curr.second, inQuant, inTerm); Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << std::endl; + Assert(!inQuant); NodeManager *nodeManager = NodeManager::currentNM(); @@ -269,57 +275,54 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, // not in a quantified formula. This policy should be in sync with // the policy for when to apply theory preprocessing to terms, see PR // #5497. - if (!inQuant) + skolem = getSkolemForNode(node); + if (skolem.isNull()) { - 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( - node, - "termITE", - "a variable introduced due to term-level ITE removal"); - d_skolem_cache.insert(node, skolem); + 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( + node, + "termITE", + "a variable introduced due to term-level ITE removal"); + d_skolem_cache.insert(node, skolem); - // The new assertion - newAssertion = nodeManager->mkNode( - kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); + // The new assertion + newAssertion = nodeManager->mkNode( + kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); - // 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 - // (= node node[2])) node = skolem - // ------------------------------------------ MACRO_SR_PRED_TRANSFORM - // (ite node[0] (= skolem node[1]) (= skolem node[2])) - // - // Note that the MACRO_SR_PRED_INTRO step holds due to conversion - // of skolem into its witness form, which is node. - Node axiom = getAxiomFor(node); - d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node}); - Node eq = node.eqNode(skolem); - d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq}); - d_lp->addStep(newAssertion, - PfRule::MACRO_SR_PRED_TRANSFORM, - {axiom, eq}, - {newAssertion}); - newAssertionPg = d_lp.get(); - } + // 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 + // (= node node[2])) node = skolem + // ------------------------------------------ MACRO_SR_PRED_TRANSFORM + // (ite node[0] (= skolem node[1]) (= skolem node[2])) + // + // Note that the MACRO_SR_PRED_INTRO step holds due to conversion + // of skolem into its witness form, which is node. + Node axiom = getAxiomFor(node); + d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node}); + Node eq = node.eqNode(skolem); + d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq}); + d_lp->addStep(newAssertion, + PfRule::MACRO_SR_PRED_TRANSFORM, + {axiom, eq}, + {newAssertion}); + newAssertionPg = d_lp.get(); } } } else if (node.getKind() == kind::LAMBDA) { // if a lambda, do lambda-lifting - if (!inQuant || !expr::hasFreeVar(node)) + if (!expr::hasFreeVar(node)) { skolem = getSkolemForNode(node); if (skolem.isNull()) @@ -363,7 +366,7 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, // If a witness choice // For details on this operator, see // http://planetmath.org/hilbertsvarepsilonoperator. - if (!inQuant || !expr::hasFreeVar(node)) + if (!expr::hasFreeVar(node)) { // NOTE: we can replace by t if body is of the form (and (= z t) ...) skolem = getSkolemForNode(node); @@ -411,8 +414,7 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, } } else if (node.getKind() != kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() - && inTerm - && !inQuant) + && inTerm) { // if a non-variable Boolean term within another term, replace it skolem = getSkolemForNode(node); -- 2.30.2