From: Andrew Reynolds Date: Thu, 17 Sep 2020 19:43:24 +0000 (-0500) Subject: Reduce recursion in term formula removal (#5052) X-Git-Tag: cvc5-1.0.0~2845 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd6f48ec9ecdd0547b77e9e8a49d3028f4281fe0;p=cvc5.git Reduce recursion in term formula removal (#5052) This reduces the use of recursion in term formula removal module. The recursion depth is now limited to the number of term positions on a path where a formula must be removed, instead of being limited to the overall formula depth. This PR also fixes some documentation. Notice for its main cache d_tfCache, this class uses a CDInsertHashMap (instead of a CDHashMap) which does not allow inserting more than once, hence an auxliary "processedChildren" vector had to be introduced to track whether we have processed children. It's not clear to me whether we should just use the more standard CDHashMap, which would simplify this. One non-linear arithmetic regression went unsat -> unknown, I added --nl-ext-tplanes to fix this. This should fix #4889. It is possible to further reduce the recursion in this pass, which can be done on a followup PR if needed. --- diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index ef21fe399..793b7e9ca 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -43,9 +43,7 @@ theory::TrustNode RemoveTermFormulas::run( std::vector& newSkolems, bool reportDeps) { - TCtxStack ctx(&d_rtfc); - ctx.pushInitial(assertion); - Node itesRemoved = run(ctx, newAsserts, newSkolems); + Node itesRemoved = runInternal(assertion, newAsserts, newSkolems); // In some calling contexts, not necessary to report dependence information. if (reportDeps && options::unsatCores()) { @@ -70,13 +68,116 @@ theory::TrustNode RemoveTermFormulas::run( return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); } -Node RemoveTermFormulas::run(TCtxStack& ctx, - std::vector& output, - std::vector& newSkolems) +Node RemoveTermFormulas::runInternal(Node assertion, + std::vector& output, + std::vector& newSkolems) +{ + NodeManager* nm = NodeManager::currentNM(); + TCtxStack ctx(&d_rtfc); + std::vector processedChildren; + ctx.pushInitial(assertion); + processedChildren.push_back(false); + std::pair initial = ctx.getCurrent(); + std::pair curr; + Node node; + uint32_t nodeVal; + TermFormulaCache::const_iterator itc; + while (!ctx.empty()) + { + curr = ctx.getCurrent(); + itc = d_tfCache.find(curr); + node = curr.first; + nodeVal = curr.second; + Trace("rtf-debug") << "Visit " << node << ", " << nodeVal << std::endl; + if (itc != d_tfCache.end()) + { + Trace("rtf-debug") << "...already computed" << std::endl; + ctx.pop(); + processedChildren.pop_back(); + // already computed + continue; + } + // if we have yet to process children + if (!processedChildren.back()) + { + // check if we should replace the current node + Node currt = runCurrent(curr, output, newSkolems); + // if null, we need to recurse + if (!currt.isNull()) + { + Trace("rtf-debug") << "...replace by skolem" << std::endl; + d_tfCache.insert(curr, currt); + ctx.pop(); + processedChildren.pop_back(); + } + else + { + size_t nchild = node.getNumChildren(); + if (nchild > 0) + { + Trace("rtf-debug") << "...recurse to children" << std::endl; + // recurse if we have children + processedChildren[processedChildren.size() - 1] = true; + for (size_t i = 0; i < nchild; i++) + { + ctx.pushChild(node, nodeVal, i); + processedChildren.push_back(false); + } + } + else + { + Trace("rtf-debug") << "...base case" << std::endl; + d_tfCache.insert(curr, node); + ctx.pop(); + processedChildren.pop_back(); + } + } + continue; + } + Trace("rtf-debug") << "...reconstruct" << std::endl; + // otherwise, we are now finished processing children, pop the current node + // and compute the result + ctx.pop(); + processedChildren.pop_back(); + // if we have not already computed the result + std::vector newChildren; + bool childChanged = false; + if (node.getMetaKind() == kind::metakind::PARAMETERIZED) + { + newChildren.push_back(node.getOperator()); + } + // reconstruct from the children + std::pair currChild; + for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++) + { + // recompute the value of the child + uint32_t val = d_rtfc.computeValue(node, nodeVal, i); + currChild = std::pair(node[i], val); + itc = d_tfCache.find(currChild); + Assert(itc != d_tfCache.end()); + Node newChild = (*itc).second; + Assert(!newChild.isNull()); + childChanged |= (newChild != node[i]); + newChildren.push_back(newChild); + } + // If changes, we reconstruct the node + Node ret = node; + if (childChanged) + { + ret = nm->mkNode(node.getKind(), newChildren); + } + // cache + d_tfCache.insert(curr, ret); + } + itc = d_tfCache.find(initial); + Assert(itc != d_tfCache.end()); + return (*itc).second; +} + +Node RemoveTermFormulas::runCurrent(std::pair& curr, + std::vector& output, + std::vector& newSkolems) { - Assert(!ctx.empty()); - std::pair curr = ctx.getCurrent(); - ctx.pop(); TNode node = curr.first; if (node.getKind() == kind::INST_PATTERN_LIST) { @@ -88,15 +189,7 @@ Node RemoveTermFormulas::run(TCtxStack& ctx, Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << std::endl; - // The result may be cached already NodeManager *nodeManager = NodeManager::currentNM(); - TermFormulaCache::const_iterator itc = d_tfCache.find(curr); - if (itc != d_tfCache.end()) - { - Node cached = (*itc).second; - Debug("ite") << "removeITEs: in-cache: " << cached << endl; - return cached.isNull() ? Node(curr.first) : cached; - } TypeNode nodeType = node.getType(); Node skolem; @@ -288,8 +381,6 @@ Node RemoveTermFormulas::run(TCtxStack& ctx, // if the term should be replaced by a skolem if( !skolem.isNull() ){ - // Attach the 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()) @@ -334,9 +425,7 @@ Node RemoveTermFormulas::run(TCtxStack& ctx, // Remove ITEs from the new assertion, rewrite it and push it to the // output Node newAssertionPre = newAssertion; - TCtxStack cctx(&d_rtfc); - cctx.pushInitial(newAssertion); - newAssertion = run(cctx, output, newSkolems); + newAssertion = runInternal(newAssertion, output, newSkolems); if (isProofEnabled()) { @@ -372,29 +461,8 @@ Node RemoveTermFormulas::run(TCtxStack& ctx, return skolem; } - // If not an ITE, go deep - std::vector newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Remove the ITEs from the children - 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(curr, cached); - return cached; - } - d_tfCache.insert(curr, Node::null()); - return node; + // return null, indicating we will traverse children within runInternal + return Node::null(); } Node RemoveTermFormulas::getSkolemForNode(Node node) const @@ -431,8 +499,7 @@ Node RemoveTermFormulas::replaceInternal(TCtxStack& ctx) const TermFormulaCache::const_iterator itc = d_tfCache.find(curr); if (itc != d_tfCache.end()) { - Node cached = (*itc).second; - return cached.isNull() ? Node(node) : cached; + return (*itc).second; } vector newChildren; diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 00bf74360..7adc51d39 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -178,19 +178,27 @@ class RemoveTermFormulas { RtfTermContext d_rtfc; /** - * Removes terms of the form (1), (2), (3) described above from node. - * All additional assertions are pushed into - * assertions. iteSkolemMap contains a map from introduced skolem - * variables to the index in assertions containing the new Boolean - * ite created in conjunction with that skolem variable. + * Removes terms of the forms described above from formula assertion. + * All additional assertions and skolems are pushed into newAsserts and + * newSkolems, which are always of the same length. * - * inQuant is whether we are processing node in the body of quantified formula - * 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. + * This uses a term-context-sensitive stack to process assertion. It returns + * the version of assertion with all term formulas removed. */ - Node run(TCtxStack& cxt, - std::vector& newAsserts, - std::vector& newSkolems); + Node runInternal(Node assertion, + std::vector& newAsserts, + std::vector& newSkolems); + /** + * This is called on curr of the form (t, val) where t is a term and val is + * a term context identifier computed by RtfTermContext. If curr should be + * replaced by a skolem, this method returns this skolem k, adds k to + * newSkolems and adds the axiom defining that skolem to newAsserts, where + * runInternal is called on that axiom. Otherwise, this method returns the + * null node. + */ + Node runCurrent(std::pair& curr, + std::vector& newAsserts, + std::vector& newSkolems); /** Replace internal */ Node replaceInternal(TCtxStack& ctx) const; diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 9df87e9b5..4a7d977ca 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -35,6 +35,7 @@ cvc4_add_api_test(smt2_compliance) # cvc4_add_api_test(statistics) cvc4_add_api_test(two_solvers) cvc4_add_api_test(issue5074) +cvc4_add_api_test(issue4889) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) diff --git a/test/api/issue4889.cpp b/test/api/issue4889.cpp new file mode 100644 index 000000000..b09b639a9 --- /dev/null +++ b/test/api/issue4889.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \file issue4889.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Test for issue #4889 + **/ + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +int main() +{ +#ifdef CVC4_USE_SYMFPU + Solver slv; + Sort sort_int = slv.getIntegerSort(); + Sort sort_array = slv.mkArraySort(sort_int, sort_int); + Sort sort_fp128 = slv.mkFloatingPointSort(15, 113); + Sort sort_fp32 = slv.mkFloatingPointSort(8, 24); + Sort sort_bool = slv.getBooleanSort(); + Term const0 = slv.mkConst(sort_fp32, "_c0"); + Term const1 = slv.mkConst(sort_fp32, "_c2"); + Term const2 = slv.mkConst(sort_bool, "_c4"); + Term ite = slv.mkTerm(ITE, const2, const1, const0); + Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1); + Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem); + slv.checkSatAssuming(isnan); +#endif + return 0; +} diff --git a/test/regress/regress0/arith/issue3480.smt2 b/test/regress/regress0/arith/issue3480.smt2 index 74ce8d32b..ef4ad7179 100644 --- a/test/regress/regress0/arith/issue3480.smt2 +++ b/test/regress/regress0/arith/issue3480.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --theoryof-mode=type --quiet +; COMMAND-LINE: --theoryof-mode=type --quiet --nl-ext-tplanes (set-logic QF_NIA) (declare-fun a () Int) (declare-fun b () Int)