From: Aina Niemetz Date: Thu, 9 Sep 2021 21:33:08 +0000 (-0700) Subject: pp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164) X-Git-Tag: cvc5-1.0.0~1244 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44657985f2d52f58803cf64cf9da93e6419ade35;p=cvc5.git pp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164) --- diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index a789a0d0b..f5152f0d2 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -50,7 +50,7 @@ PreprocessingPassResult BoolToBV::applyInternal( for (size_t i = 0; i < size; ++i) { Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true); - assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion)); + assertionsToPreprocess->replace(i, rewrite(newAssertion)); } } else @@ -59,7 +59,7 @@ PreprocessingPassResult BoolToBV::applyInternal( for (size_t i = 0; i < size; ++i) { assertionsToPreprocess->replace( - i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i]))); + i, rewrite(lowerIte((*assertionsToPreprocess)[i]))); } } diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index 597481678..cea5bf37c 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -53,7 +53,7 @@ PreprocessingPassResult BvAbstraction::applyInternal( bv_theory->applyAbstraction(assertions, new_assertions); for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + assertionsToPreprocess->replace(i, rewrite(new_assertions[i])); } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index b3c34087d..e49cc5c44 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -37,28 +37,24 @@ namespace cvc5 { namespace preprocessing { namespace passes { -namespace { - -bool is_bv_const(Node n) +bool BVGauss::is_bv_const(Node n) { if (n.isConst()) { return true; } - return Rewriter::rewrite(n).getKind() == kind::CONST_BITVECTOR; + return rewrite(n).getKind() == kind::CONST_BITVECTOR; } -Node get_bv_const(Node n) +Node BVGauss::get_bv_const(Node n) { Assert(is_bv_const(n)); - return Rewriter::rewrite(n); + return rewrite(n); } -Integer get_bv_const_value(Node n) +Integer BVGauss::get_bv_const_value(Node n) { Assert(is_bv_const(n)); return get_bv_const(n).getConst().getValue(); } -} // namespace - /** * Determines if an overflow may occur in given 'expr'. * @@ -75,7 +71,7 @@ Integer get_bv_const_value(Node n) * will be handled via the default case, which is not incorrect but also not * necessarily the minimum. */ -unsigned BVGauss::getMinBwExpr(Node expr) +uint32_t BVGauss::getMinBwExpr(Node expr) { std::vector visit; /* Maps visited nodes to the determined minimum bit-width required. */ @@ -454,7 +450,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( Assert(is_bv_const(eq[0])); eqrhs = eq[0]; } - if (getMinBwExpr(Rewriter::rewrite(urem[0])) == 0) + if (getMinBwExpr(rewrite(urem[0])) == 0) { Trace("bv-gauss-elim") << "Minimum required bit-width exceeds given bit-width, " @@ -504,7 +500,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( NodeBuilder nb_nonconsts(NodeManager::currentNM(), k); for (const Node& nn : n) { - Node nnrw = Rewriter::rewrite(nn); + Node nnrw = rewrite(nn); if (is_bv_const(nnrw)) { nb_consts << nnrw; @@ -519,7 +515,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( unsigned nc = nb_consts.getNumChildren(); if (nc > 1) { - n0 = Rewriter::rewrite(nb_consts.constructNode()); + n0 = rewrite(nb_consts.constructNode()); } else if (nc == 1) { @@ -532,7 +528,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( /* n1 is a mult with non-const operands */ if (nb_nonconsts.getNumChildren() > 1) { - n1 = Rewriter::rewrite(nb_nonconsts.constructNode()); + n1 = rewrite(nb_nonconsts.constructNode()); } else { diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index 8fafcb741..0078770fb 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -93,14 +93,29 @@ class BVGauss : public PreprocessingPass NONE }; - static Result gaussElim(Integer prime, - std::vector& rhs, - std::vector>& lhs); + Result gaussElim(Integer prime, + std::vector& rhs, + std::vector>& lhs); - static Result gaussElimRewriteForUrem(const std::vector& equations, - std::unordered_map& res); + Result gaussElimRewriteForUrem(const std::vector& equations, + std::unordered_map& res); - static unsigned getMinBwExpr(Node expr); + uint32_t getMinBwExpr(Node expr); + + /** + * Return true if given node is a bit-vector value (after rewriting). + */ + bool is_bv_const(Node n); + /** + * Return the bit-vector value resulting from rewriting node 'n'. + * Asserts that given node can be rewritten to a bit-vector value. + */ + Node get_bv_const(Node n); + /** + * Return the Integer value representing the given bit-vector value. + * Asserts that given node can be rewritten to a bit-vector value. + */ + Integer get_bv_const_value(Node n); }; } // namespace passes diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index 45df7478c..ff0657dcd 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -94,7 +94,7 @@ PreprocessingPassResult BvIntroPow2::applyInternal( Node res = pow2Rewrite(cur, cache); if (res != cur) { - res = Rewriter::rewrite(res); + res = rewrite(res); assertionsToPreprocess->replace(i, res); } } diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index cd58a3faf..0d0131e3e 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -53,7 +53,7 @@ PreprocessingPassResult BVToBool::applyInternal( liftBvToBool(assertionsToPreprocess->ref(), new_assertions); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + assertionsToPreprocess->replace(i, rewrite(new_assertions[i])); } return PreprocessingPassResult::NO_CONFLICT; } @@ -281,7 +281,7 @@ void BVToBool::liftBvToBool(const std::vector& assertions, for (unsigned i = 0; i < assertions.size(); ++i) { Node new_assertion = liftNode(assertions[i]); - new_assertions.push_back(Rewriter::rewrite(new_assertion)); + new_assertions.push_back(rewrite(new_assertion)); Trace("bv-to-bool") << " " << assertions[i] << " => " << new_assertions[i] << "\n"; } diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 65c9bb012..cc631f4bc 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -60,7 +60,7 @@ Node BVToInt::mkRangeConstraint(Node newVar, uint64_t k) Node lower = d_nm->mkNode(kind::LEQ, d_zero, newVar); Node upper = d_nm->mkNode(kind::LT, newVar, pow2(k)); Node result = d_nm->mkNode(kind::AND, lower, upper); - return Rewriter::rewrite(result); + return rewrite(result); } Node BVToInt::maxInt(uint64_t k) @@ -256,7 +256,7 @@ Node BVToInt::eliminationPass(Node n) Node BVToInt::bvToInt(Node n) { // make sure the node is re-written before processing it. - n = Rewriter::rewrite(n); + n = rewrite(n); n = makeBinary(n); n = eliminationPass(n); // binarize again, in case the elimination pass introduced @@ -946,7 +946,7 @@ PreprocessingPassResult BVToInt::applyInternal( { Node bvNode = (*assertionsToPreprocess)[i]; Node intNode = bvToInt(bvNode); - Node rwNode = Rewriter::rewrite(intNode); + Node rwNode = rewrite(intNode); Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl; Trace("bv-to-int-debug") << "int node: " << intNode << std::endl; Trace("bv-to-int-debug") << "rw node: " << rwNode << std::endl; @@ -966,7 +966,7 @@ void BVToInt::addFinalizeRangeAssertions( vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end()); // conjoin all range assertions and add the conjunction // as a new assertion - Node rangeAssertions = Rewriter::rewrite(d_nm->mkAnd(vec_range)); + Node rangeAssertions = rewrite(d_nm->mkAnd(vec_range)); assertionsToPreprocess->push_back(rangeAssertions); Trace("bv-to-int-debug") << "range constraints: " << rangeAssertions.toString() << std::endl; diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp index 6040b3669..24edf1509 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.cpp +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -36,7 +36,7 @@ ForeignTheoryRewrite::ForeignTheoryRewrite( Node ForeignTheoryRewrite::simplify(Node n) { std::vector toVisit; - n = Rewriter::rewrite(n); + n = rewrite(n); toVisit.push_back(n); // traverse n and rewrite until fixpoint while (!toVisit.empty()) @@ -143,7 +143,7 @@ PreprocessingPassResult ForeignTheoryRewrite::applyInternal( for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { assertionsToPreprocess->replace( - i, Rewriter::rewrite(simplify((*assertionsToPreprocess)[i]))); + i, rewrite(simplify((*assertionsToPreprocess)[i]))); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index 2405702b0..7e8f3ffab 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -153,7 +153,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def") << " to " << std::endl; Node new_q = nm->mkNode(FORALL, bvl, bd); - new_q = Rewriter::rewrite(new_q); + new_q = rewrite(new_q); assertionsToPreprocess->replace(i, new_q); Trace("fmf-fun-def") << " " << assertions[i] << std::endl; fd_assertions.push_back(i); @@ -187,7 +187,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) Assert(constraints.empty()); if (n != assertions[i]) { - n = Rewriter::rewrite(n); + n = rewrite(n); Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def-rewrite") << " to " << std::endl; @@ -232,7 +232,7 @@ Node FunDefFmf::simplifyFormula( for (unsigned i = 0; i < constraints.size(); i++) { constraints[i] = nm->mkNode(FORALL, n[0], constraints[i]); - constraints[i] = Rewriter::rewrite(constraints[i]); + constraints[i] = rewrite(constraints[i]); } if (c != n[1]) { @@ -365,7 +365,7 @@ Node FunDefFmf::simplifyFormula( if (constraints.size() > 1) { cons = nm->mkNode(AND, constraints); - cons = Rewriter::rewrite(cons); + cons = rewrite(cons); constraints.clear(); constraints.push_back(cons); } diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index e990f8868..cd8ecc73f 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -94,7 +94,7 @@ Node GlobalNegate::simplify(const std::vector& assertions, } Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; - body = Rewriter::rewrite(body); + body = rewrite(body); Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl; return body; } diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 27dcf651b..515cc4a32 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -315,7 +315,7 @@ PreprocessingPassResult HoElim::applyInternal( Node res = eliminateLambdaComplete(prev, newLambda); if (res != prev) { - res = theory::Rewriter::rewrite(res); + res = rewrite(res); Assert(!expr::hasFreeVar(res)); assertionsToPreprocess->replace(i, res); } @@ -361,7 +361,7 @@ PreprocessingPassResult HoElim::applyInternal( if (!axioms.empty()) { Node conj = nm->mkAnd(axioms); - conj = theory::Rewriter::rewrite(conj); + conj = rewrite(conj); Assert(!expr::hasFreeVar(conj)); assertionsToPreprocess->conjoin(0, conj); } @@ -374,7 +374,7 @@ PreprocessingPassResult HoElim::applyInternal( Node res = eliminateHo(prev); if (res != prev) { - res = theory::Rewriter::rewrite(res); + res = rewrite(res); Assert(!expr::hasFreeVar(res)); assertionsToPreprocess->replace(i, res); } @@ -456,7 +456,7 @@ PreprocessingPassResult HoElim::applyInternal( if (!axioms.empty()) { Node conj = nm->mkAnd(axioms); - conj = theory::Rewriter::rewrite(conj); + conj = rewrite(conj); Assert(!expr::hasFreeVar(conj)); assertionsToPreprocess->conjoin(0, conj); } diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 41d52d1ae..46c75b560 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -203,7 +203,7 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) // Mark the substitution and continue Node result = builder; - result = Rewriter::rewrite(result); + result = rewrite(result); cache[current] = result; } else diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 7578bcad6..97e56c58c 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -64,7 +64,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) } for (unsigned i = 0, size = assertions->size(); i < size; ++i) { - assertions->replace(i, Rewriter::rewrite((*assertions)[i])); + assertions->replace(i, rewrite((*assertions)[i])); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp index 81fbf1ea1..c2693e927 100644 --- a/src/preprocessing/passes/learned_rewrite.cpp +++ b/src/preprocessing/passes/learned_rewrite.cpp @@ -233,7 +233,7 @@ Node LearnedRewrite::rewriteLearned(Node n, { NodeManager* nm = NodeManager::currentNM(); Trace("learned-rewrite-rr-debug") << "Rewrite " << n << std::endl; - Node nr = Rewriter::rewrite(n); + Node nr = rewrite(n); Kind k = nr.getKind(); if (k == INTS_DIVISION || k == INTS_MODULUS || k == DIVISION) { @@ -278,7 +278,7 @@ Node LearnedRewrite::rewriteLearned(Node n, children.insert(children.end(), n.begin(), n.end()); Node ret = nm->mkNode(nk, children); nr = returnRewriteLearned(nr, ret, LearnedRewriteId::NON_ZERO_DEN); - nr = Rewriter::rewrite(nr); + nr = rewrite(nr); k = nr.getKind(); } } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index a5720e758..3ef4b7e9f 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -42,12 +42,59 @@ using namespace cvc5::theory; namespace { +/** + * Trace nodes back to their assertions using CircuitPropagator's + * BackEdgesMap. + */ +void traceBackToAssertions(booleans::CircuitPropagator* propagator, + const std::vector& nodes, + std::vector& assertions) +{ + const booleans::CircuitPropagator::BackEdgesMap& backEdges = + propagator->getBackEdges(); + for (vector::const_iterator i = nodes.begin(); i != nodes.end(); ++i) + { + booleans::CircuitPropagator::BackEdgesMap::const_iterator j = + backEdges.find(*i); + // term must appear in map, otherwise how did we get here?! + Assert(j != backEdges.end()); + // if term maps to empty, that means it's a top-level assertion + if (!(*j).second.empty()) + { + traceBackToAssertions(propagator, (*j).second, assertions); + } + else + { + assertions.push_back(*i); + } + } +} + +} // namespace + +MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "miplib-trick") +{ + if (!options::incrementalSolving()) + { + NodeManager::currentNM()->subscribeEvents(this); + } +} + +MipLibTrick::~MipLibTrick() +{ + if (!options::incrementalSolving()) + { + NodeManager::currentNM()->unsubscribeEvents(this); + } +} + /** * Remove conjuncts in toRemove from conjunction n. Return # of removed * conjuncts. */ -size_t removeFromConjunction(Node& n, - const std::unordered_set& toRemove) +size_t MipLibTrick::removeFromConjunction( + Node& n, const std::unordered_set& toRemove) { Assert(n.getKind() == kind::AND); Node trueNode = NodeManager::currentNM()->mkConst(true); @@ -109,7 +156,7 @@ size_t removeFromConjunction(Node& n, { n = b; } - n = Rewriter::rewrite(n); + n = rewrite(n); return removals; } } @@ -118,53 +165,6 @@ size_t removeFromConjunction(Node& n, return 0; } -/** - * Trace nodes back to their assertions using CircuitPropagator's - * BackEdgesMap. - */ -void traceBackToAssertions(booleans::CircuitPropagator* propagator, - const std::vector& nodes, - std::vector& assertions) -{ - const booleans::CircuitPropagator::BackEdgesMap& backEdges = - propagator->getBackEdges(); - for (vector::const_iterator i = nodes.begin(); i != nodes.end(); ++i) - { - booleans::CircuitPropagator::BackEdgesMap::const_iterator j = - backEdges.find(*i); - // term must appear in map, otherwise how did we get here?! - Assert(j != backEdges.end()); - // if term maps to empty, that means it's a top-level assertion - if (!(*j).second.empty()) - { - traceBackToAssertions(propagator, (*j).second, assertions); - } - else - { - assertions.push_back(*i); - } - } -} - -} // namespace - -MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "miplib-trick") -{ - if (!options::incrementalSolving()) - { - NodeManager::currentNM()->subscribeEvents(this); - } -} - -MipLibTrick::~MipLibTrick() -{ - if (!options::incrementalSolving()) - { - NodeManager::currentNM()->unsubscribeEvents(this); - } -} - void MipLibTrick::nmNotifyNewVar(TNode n) { if (n.getType().isBoolean()) @@ -530,12 +530,12 @@ PreprocessingPassResult MipLibTrick::applyInternal( nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME); - Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); - Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); + Node geq = rewrite(nm->mkNode(kind::GEQ, newVar, zero)); + Node leq = rewrite(nm->mkNode(kind::LEQ, newVar, one)); TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr); TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr); - Node n = Rewriter::rewrite(geq.andNode(leq)); + Node n = rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); TrustSubstitutionMap tnullMap(&fakeContext, nullptr); CVC5_UNUSED SubstitutionMap& nullMap = tnullMap.get(); @@ -575,8 +575,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]); } Debug("miplib") << "vars[] " << var << endl - << " eq " << Rewriter::rewrite(sum) << endl; - Node newAssertion = var.eqNode(Rewriter::rewrite(sum)); + << " eq " << rewrite(sum) << endl; + Node newAssertion = var.eqNode(rewrite(sum)); if (top_level_substs.hasSubstitution(newAssertion[0])) { // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl; @@ -599,7 +599,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl; } - newAssertion = Rewriter::rewrite(newAssertion); + newAssertion = rewrite(newAssertion); Debug("miplib") << " " << newAssertion << endl; assertionsToPreprocess->push_back(newAssertion); @@ -642,7 +642,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( } Debug("miplib") << "had: " << assertion[i] << endl; assertionsToPreprocess->replace( - i, Rewriter::rewrite(top_level_substs.apply(assertion))); + i, rewrite(top_level_substs.apply(assertion))); Debug("miplib") << "now: " << assertion << endl; } } diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index c63885cf0..537d27a0a 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -49,6 +49,9 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener Statistics(); }; + size_t removeFromConjunction( + Node& n, const std::unordered_set& toRemove); + Statistics d_statistics; std::vector d_boolVars; diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index afd21fb7a..27f34f177 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -64,7 +64,7 @@ Node NlExtPurify::purifyNlTerms(TNode n, && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) { // don't do it if it rewrites to a constant - Node nr = Rewriter::rewrite(n); + Node nr = rewrite(n); if (nr.isConst()) { // return the rewritten constant diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index ca61c9197..6c93eba15 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -210,7 +210,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, Node orig) { Assert(assertion.getKind() == kind::GEQ); - Assert(assertion == Rewriter::rewrite(assertion)); + Assert(assertion == rewrite(assertion)); // assume assertion is rewritten Node l = assertion[0]; @@ -264,7 +264,7 @@ void PseudoBooleanProcessor::learnInternal(Node assertion, case kind::LEQ: case kind::LT: { - Node rw = Rewriter::rewrite(assertion); + Node rw = rewrite(assertion); if (assertion == rw) { if (assertion.getKind() == kind::GEQ) @@ -320,7 +320,7 @@ void PseudoBooleanProcessor::addSub(Node from, Node to) { if (!d_subCache.hasSubstitution(from)) { - Node rw_to = Rewriter::rewrite(to); + Node rw_to = rewrite(to); d_subCache.addSubstitution(from, rw_to); } } @@ -386,7 +386,7 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq) Node PseudoBooleanProcessor::applyReplacements(Node pre) { - Node assertion = Rewriter::rewrite(pre); + Node assertion = rewrite(pre); Node result = d_subCache.apply(assertion); if (Debug.isOn("pbs::rewrites") && result != assertion) diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index c0bb0ea7f..f80c4383c 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -45,7 +45,7 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal( if (!trn.isNull()) { Node next = trn.getNode(); - assertionsToPreprocess->replace(i, Rewriter::rewrite(next)); + assertionsToPreprocess->replace(i, rewrite(next)); Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-preprocess") << " ...got " << (*assertionsToPreprocess)[i] << endl; diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 3cfc29ed6..9e2170ffd 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -57,7 +57,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va || n.getKind() == kind::GEQ || n.getKind() == kind::LT || n.getKind() == kind::GT || n.getKind() == kind::LEQ) { - ret = Rewriter::rewrite(n); + ret = rewrite(n); Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl; if (!ret.isConst()) { @@ -81,13 +81,12 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va Rational(c.getConst().getDenominator()))); } } - Node cc = - coeffs.empty() - ? Node::null() - : (coeffs.size() == 1 - ? coeffs[0] - : Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::MULT, coeffs))); + Node cc = coeffs.empty() + ? Node::null() + : (coeffs.size() == 1 + ? coeffs[0] + : rewrite(NodeManager::currentNM()->mkNode( + kind::MULT, coeffs))); std::vector sum; for (std::map::iterator itm = msum.begin(); itm != msum.end(); @@ -105,7 +104,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va { if (!cc.isNull()) { - c = Rewriter::rewrite( + c = rewrite( NodeManager::currentNM()->mkNode(kind::MULT, c, cc)); } } diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index 4704f1cb5..0e7aafcc3 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -34,7 +34,7 @@ PreprocessingPassResult Rewrite::applyInternal( AssertionPipeline* assertionsToPreprocess) { for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i])); + assertionsToPreprocess->replace(i, rewrite((*assertionsToPreprocess)[i])); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 4322e60d5..37bf0fd8b 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -113,7 +113,7 @@ PreprocessingPassResult SepSkolemEmp::applyInternal( Node next = preSkolemEmp(prev, pol, visited); if (next != prev) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(next)); + assertionsToPreprocess->replace(i, rewrite(next)); Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl; Trace("sep-preprocess") << " ...got " << (*assertionsToPreprocess)[i] << endl; diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 7b93f43cf..c139f0a86 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -52,7 +52,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( Node next = si->simplify(prev, model_replace_f, visited); if (next != prev) { - next = theory::Rewriter::rewrite(next); + next = rewrite(next); assertionsToPreprocess->replace(i, next); Trace("sort-infer-preprocess") << "*** Preprocess SortInferencePass " << prev << endl; @@ -64,7 +64,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( si->getNewAssertions(newAsserts); for (const Node& na : newAsserts) { - Node nar = theory::Rewriter::rewrite(na); + Node nar = rewrite(na); Trace("sort-infer-preprocess") << "*** Preprocess SortInferencePass : new constraint " << nar << endl; diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 09d24d900..24d25e354 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -47,8 +47,7 @@ PreprocessingPassResult StaticLearning::applyInternal( } else { - assertionsToPreprocess->replace( - i, theory::Rewriter::rewrite(learned.constructNode())); + assertionsToPreprocess->replace(i, rewrite(learned.constructNode())); } } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp index 6ab3a9bd2..80d6dd0e8 100644 --- a/src/preprocessing/passes/strings_eager_pp.cpp +++ b/src/preprocessing/passes/strings_eager_pp.cpp @@ -49,7 +49,7 @@ PreprocessingPassResult StringsEagerPp::applyInternal( } if (prev != rew) { - assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew)); + assertionsToPreprocess->replace(i, rewrite(rew)); } } diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 8194f9f52..8abd77a27 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -65,7 +65,7 @@ PreprocessingPassResult SygusInference::applyInternal( prev.substitute(funs.begin(), funs.end(), sols.begin(), sols.end()); if (curr != prev) { - curr = theory::Rewriter::rewrite(curr); + curr = rewrite(curr); Trace("sygus-infer-debug") << "...rewrote " << prev << " to " << curr << std::endl; assertionsToPreprocess->replace(i, curr); @@ -127,7 +127,7 @@ bool SygusInference::solveSygus(const std::vector& assertions, std::map type_count; Node pas = as; // rewrite - pas = theory::Rewriter::rewrite(pas); + pas = rewrite(pas); Trace("sygus-infer") << "assertion : " << pas << std::endl; if (pas.getKind() == FORALL) { diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index c8ddfc2fa..c59aa86ef 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -231,7 +231,7 @@ void UnconstrainedSimplifier::processUnconstrained() // Special case: condition is unconstrained, then and else are // different, and total cardinality of the type is 2, then the // result is unconstrained - Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); + Node test = rewrite(parent[1].eqNode(parent[2])); if (test == nm->mkConst(false)) { ++d_numUnconstrainedElim; @@ -530,7 +530,7 @@ void UnconstrainedSimplifier::processUnconstrained() { // TODO(#2377): could build ITE here Node test = other.eqNode(nm->mkConst(0)); - if (Rewriter::rewrite(test) != nm->mkConst(false)) + if (rewrite(test) != nm->mkConst(false)) { break; } @@ -573,7 +573,7 @@ void UnconstrainedSimplifier::processUnconstrained() Node test = nm->mkNode(extractOp, children); BitVector one(1, unsigned(1)); test = test.eqNode(nm->mkConst(one)); - if (Rewriter::rewrite(test) != nm->mkConst(true)) + if (rewrite(test) != nm->mkConst(true)) { done = true; break; @@ -753,8 +753,7 @@ void UnconstrainedSimplifier::processUnconstrained() } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - Node test = - Rewriter::rewrite(other.eqNode(nm->mkConst(bv))); + Node test = rewrite(other.eqNode(nm->mkConst(bv))); if (test == nm->mkConst(false)) { break; @@ -861,7 +860,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal( for (size_t i = 0, asize = assertions.size(); i < asize; ++i) { Node a = assertions[i]; - Node as = Rewriter::rewrite(d_substitutions.apply(a)); + Node as = rewrite(d_substitutions.apply(a)); // replace the assertion assertionsToPreprocess->replace(i, as); } diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 8f6fa7b14..68758f766 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -48,6 +48,8 @@ class TestPPWhiteBVGauss : public TestSmt d_preprocContext.reset(new preprocessing::PreprocessingPassContext( d_smtEngine.get(), d_smtEngine->getEnv(), nullptr)); + d_bv_gauss.reset(new BVGauss(d_preprocContext.get())); + d_zero = bv::utils::mkZero(16); d_p = bv::utils::mkConcat( @@ -147,7 +149,7 @@ class TestPPWhiteBVGauss : public TestSmt std::cout << "Input: " << std::endl; print_matrix_dbg(rhs, lhs); - ret = BVGauss::gaussElim(prime, resrhs, reslhs); + ret = d_bv_gauss->gaussElim(prime, resrhs, reslhs); std::cout << "BVGauss::Result: " << (ret == BVGauss::Result::INVALID @@ -199,6 +201,7 @@ class TestPPWhiteBVGauss : public TestSmt } std::unique_ptr d_preprocContext; + std::unique_ptr d_bv_gauss; Node d_p; Node d_x; @@ -262,7 +265,7 @@ TEST_F(TestPPWhiteBVGauss, elim_mod) {Integer(2), Integer(3), Integer(5)}, {Integer(4), Integer(0), Integer(5)}}; std::cout << "matrix 0, modulo 0" << std::endl; // throws - ASSERT_DEATH(BVGauss::gaussElim(Integer(0), rhs, lhs), "prime > 0"); + ASSERT_DEATH(d_bv_gauss->gaussElim(Integer(0), rhs, lhs), "prime > 0"); std::cout << "matrix 0, modulo 1" << std::endl; testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE); std::cout << "matrix 0, modulo 2" << std::endl; @@ -931,7 +934,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1) std::vector eqs = {eq1, eq2, eq3}; std::unordered_map res; - BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + BVGauss::Result ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::UNIQUE); ASSERT_EQ(res.size(), 3); ASSERT_EQ(res[d_x], d_three32); @@ -1037,7 +1040,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2) std::vector eqs = {eq1, eq2, eq3}; std::unordered_map res; - BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + BVGauss::Result ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::UNIQUE); ASSERT_EQ(res.size(), 3); ASSERT_EQ(res[d_x], d_three32); @@ -1075,7 +1078,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a) d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); @@ -1199,7 +1202,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b) d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); @@ -1321,7 +1324,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2) d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); @@ -1419,7 +1422,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3) d_eight); std::vector eqs = {eq1, eq2}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); @@ -1562,7 +1565,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4) d_thirty); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); @@ -1713,7 +1716,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5) d_thirty); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 1); @@ -1820,7 +1823,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6) kind::EQUAL, d_nodeManager->mkNode(kind::BITVECTOR_UREM, w, d_p), d_two); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 3); @@ -1915,7 +1918,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial) d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); @@ -2086,7 +2089,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::PARTIAL); ASSERT_EQ(res.size(), 2); @@ -2224,7 +2227,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1) d_five); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::UNIQUE); ASSERT_EQ(res.size(), 3); @@ -2285,7 +2288,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2) bv::utils::mkConcat(d_zero, d_nine)); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::UNIQUE); ASSERT_EQ(res.size(), 3); @@ -2353,7 +2356,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_invalid) bv::utils::mkConcat(d_zero, d_nine)); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGauss::gaussElimRewriteForUrem(eqs, res); + ret = d_bv_gauss->gaussElimRewriteForUrem(eqs, res); ASSERT_EQ(ret, BVGauss::Result::INVALID); } @@ -2627,15 +2630,15 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial) TEST_F(TestPPWhiteBVGauss, get_min_bw1) { - ASSERT_EQ(BVGauss::getMinBwExpr(bv::utils::mkConst(32, 11)), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(bv::utils::mkConst(32, 11)), 4); - ASSERT_EQ(BVGauss::getMinBwExpr(d_p), 4); - ASSERT_EQ(BVGauss::getMinBwExpr(d_x), 16); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_p), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(d_x), 16); Node extp = bv::utils::mkExtract(d_p, 4, 0); - ASSERT_EQ(BVGauss::getMinBwExpr(extp), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(extp), 4); Node extx = bv::utils::mkExtract(d_x, 4, 0); - ASSERT_EQ(BVGauss::getMinBwExpr(extx), 5); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(extx), 5); Node zextop8 = d_nodeManager->mkConst(BitVectorZeroExtend(8)); @@ -2647,132 +2650,132 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1) d_nodeManager->mkConst(BitVectorZeroExtend(40)); Node zext40p = d_nodeManager->mkNode(zextop8, d_p); - ASSERT_EQ(BVGauss::getMinBwExpr(zext40p), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40p), 4); Node zext40x = d_nodeManager->mkNode(zextop8, d_x); - ASSERT_EQ(BVGauss::getMinBwExpr(zext40x), 16); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext40x), 16); Node zext48p = d_nodeManager->mkNode(zextop16, d_p); - ASSERT_EQ(BVGauss::getMinBwExpr(zext48p), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p), 4); Node zext48x = d_nodeManager->mkNode(zextop16, d_x); - ASSERT_EQ(BVGauss::getMinBwExpr(zext48x), 16); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x), 16); Node p8 = d_nodeManager->mkConst(BitVector(8, 11u)); Node x8 = d_nodeManager->mkVar("x8", d_nodeManager->mkBitVectorType(8)); Node zext48p8 = d_nodeManager->mkNode(zextop40, p8); - ASSERT_EQ(BVGauss::getMinBwExpr(zext48p8), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48p8), 4); Node zext48x8 = d_nodeManager->mkNode(zextop40, x8); - ASSERT_EQ(BVGauss::getMinBwExpr(zext48x8), 8); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext48x8), 8); Node mult1p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extp, extp); - ASSERT_EQ(BVGauss::getMinBwExpr(mult1p), 5); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1p), 5); Node mult1x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, extx, extx); - ASSERT_EQ(BVGauss::getMinBwExpr(mult1x), 0); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult1x), 0); Node mult2p = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p); - ASSERT_EQ(BVGauss::getMinBwExpr(mult2p), 7); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2p), 7); Node mult2x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x); - ASSERT_EQ(BVGauss::getMinBwExpr(mult2x), 32); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult2x), 32); NodeBuilder nbmult3p(kind::BITVECTOR_MULT); nbmult3p << zext48p << zext48p << zext48p; Node mult3p = nbmult3p; - ASSERT_EQ(BVGauss::getMinBwExpr(mult3p), 11); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3p), 11); NodeBuilder nbmult3x(kind::BITVECTOR_MULT); nbmult3x << zext48x << zext48x << zext48x; Node mult3x = nbmult3x; - ASSERT_EQ(BVGauss::getMinBwExpr(mult3x), 48); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult3x), 48); NodeBuilder nbmult4p(kind::BITVECTOR_MULT); nbmult4p << zext48p << zext48p8 << zext48p; Node mult4p = nbmult4p; - ASSERT_EQ(BVGauss::getMinBwExpr(mult4p), 11); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4p), 11); NodeBuilder nbmult4x(kind::BITVECTOR_MULT); nbmult4x << zext48x << zext48x8 << zext48x; Node mult4x = nbmult4x; - ASSERT_EQ(BVGauss::getMinBwExpr(mult4x), 40); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(mult4x), 40); Node concat1p = bv::utils::mkConcat(d_p, zext48p); - ASSERT_EQ(BVGauss::getMinBwExpr(concat1p), 52); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1p), 52); Node concat1x = bv::utils::mkConcat(d_x, zext48x); - ASSERT_EQ(BVGauss::getMinBwExpr(concat1x), 64); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat1x), 64); Node concat2p = bv::utils::mkConcat(bv::utils::mkZero(16), zext48p); - ASSERT_EQ(BVGauss::getMinBwExpr(concat2p), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2p), 4); Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x); - ASSERT_EQ(BVGauss::getMinBwExpr(concat2x), 16); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(concat2x), 16); Node udiv1p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p); - ASSERT_EQ(BVGauss::getMinBwExpr(udiv1p), 1); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1p), 1); Node udiv1x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x); - ASSERT_EQ(BVGauss::getMinBwExpr(udiv1x), 48); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv1x), 48); Node udiv2p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p8); - ASSERT_EQ(BVGauss::getMinBwExpr(udiv2p), 1); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2p), 1); Node udiv2x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x8); - ASSERT_EQ(BVGauss::getMinBwExpr(udiv2x), 48); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(udiv2x), 48); Node urem1p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p); - ASSERT_EQ(BVGauss::getMinBwExpr(urem1p), 1); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1p), 1); Node urem1x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x); - ASSERT_EQ(BVGauss::getMinBwExpr(urem1x), 1); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem1x), 1); Node urem2p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p8); - ASSERT_EQ(BVGauss::getMinBwExpr(urem2p), 1); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2p), 1); Node urem2x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x8); - ASSERT_EQ(BVGauss::getMinBwExpr(urem2x), 16); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem2x), 16); Node urem3p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p8, zext48p); - ASSERT_EQ(BVGauss::getMinBwExpr(urem3p), 1); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3p), 1); Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x); - ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(urem3x), 8); Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extp, extp); - ASSERT_EQ(BVGauss::getMinBwExpr(add1p), 5); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1p), 5); Node add1x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, extx, extx); - ASSERT_EQ(BVGauss::getMinBwExpr(add1x), 0); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add1x), 0); Node add2p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40p, zext40p); - ASSERT_EQ(BVGauss::getMinBwExpr(add2p), 5); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2p), 5); Node add2x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext40x, zext40x); - ASSERT_EQ(BVGauss::getMinBwExpr(add2x), 17); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add2x), 17); Node add3p = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48p8, zext48p); - ASSERT_EQ(BVGauss::getMinBwExpr(add3p), 5); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3p), 5); Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext48x8, zext48x); - ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add3x), 17); NodeBuilder nbadd4p(kind::BITVECTOR_ADD); nbadd4p << zext48p << zext48p << zext48p; Node add4p = nbadd4p; - ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4p), 6); NodeBuilder nbadd4x(kind::BITVECTOR_ADD); nbadd4x << zext48x << zext48x << zext48x; Node add4x = nbadd4x; - ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add4x), 18); NodeBuilder nbadd5p(kind::BITVECTOR_ADD); nbadd5p << zext48p << zext48p8 << zext48p; Node add5p = nbadd5p; - ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5p), 6); NodeBuilder nbadd5x(kind::BITVECTOR_ADD); nbadd5x << zext48x << zext48x8 << zext48x; Node add5x = nbadd5x; - ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add5x), 18); NodeBuilder nbadd6p(kind::BITVECTOR_ADD); nbadd6p << zext48p << zext48p << zext48p << zext48p; Node add6p = nbadd6p; - ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6p), 6); NodeBuilder nbadd6x(kind::BITVECTOR_ADD); nbadd6x << zext48x << zext48x << zext48x << zext48x; Node add6x = nbadd6x; - ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(add6x), 18); Node not1p = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40p); - ASSERT_EQ(BVGauss::getMinBwExpr(not1p), 40); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1p), 40); Node not1x = d_nodeManager->mkNode(kind::BITVECTOR_NOT, zext40x); - ASSERT_EQ(BVGauss::getMinBwExpr(not1x), 40); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(not1x), 40); } TEST_F(TestPPWhiteBVGauss, get_min_bw2) @@ -2786,7 +2789,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw2) Node zext1 = d_nodeManager->mkNode(zextop15, d_p); Node ext = bv::utils::mkExtract(zext1, 7, 0); Node zext2 = d_nodeManager->mkNode(zextop5, ext); - ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 4); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 4); } TEST_F(TestPPWhiteBVGauss, get_min_bw3a) @@ -2805,7 +2808,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3a) Node ext2 = bv::utils::mkExtract(z, 4, 0); Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2); Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); - ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5); } TEST_F(TestPPWhiteBVGauss, get_min_bw3b) @@ -2821,7 +2824,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3b) Node ext2 = bv::utils::mkExtract(d_z, 4, 0); Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2); Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); - ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(zext2), 5); } TEST_F(TestPPWhiteBVGauss, get_min_bw4a) @@ -2856,7 +2859,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4a) Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2); - ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6); } TEST_F(TestPPWhiteBVGauss, get_min_bw4b) @@ -2888,7 +2891,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4b) Node plus = d_nodeManager->mkNode(kind::BITVECTOR_ADD, zext2_1, zext2_2); - ASSERT_EQ(BVGauss::getMinBwExpr(plus), 6); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus), 6); } TEST_F(TestPPWhiteBVGauss, get_min_bw5a) @@ -2994,7 +2997,7 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5a) d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww)); - ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 0); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 0); } TEST_F(TestPPWhiteBVGauss, get_min_bw5b) @@ -3098,8 +3101,8 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b) d_nodeManager->mkNode( kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww)); - ASSERT_EQ(BVGauss::getMinBwExpr(plus7), 19); - ASSERT_EQ(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)), 17); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(plus7), 19); + ASSERT_EQ(d_bv_gauss->getMinBwExpr(Rewriter::rewrite(plus7)), 17); } } // namespace test } // namespace cvc5