From: Andrew Reynolds Date: Mon, 25 Apr 2022 18:21:57 +0000 (-0500) Subject: Make BVInstantiatorUtil an EnvObj (#8633) X-Git-Tag: cvc5-1.0.1~229 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb6c4c958b8c363c603510672fd8a9e2dc4d832e;p=cvc5.git Make BVInstantiatorUtil an EnvObj (#8633) Eliminates 5 of the remaining 8 static calls to Rewriter::rewrite. --- diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index f5eff833a..156dbc5cc 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -860,8 +860,7 @@ class CVC5_EXPORT SolverEngine std::vector getExpandedAssertions(); /** - * !!!!! temporary, until the environment is passsed to all classes that - * require it. + * Get the enviornment from this solver engine. */ Env& getEnv(); /* ....................................................................... */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 50178ac63..f0be34902 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -19,7 +19,6 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" #include "util/random.h" @@ -55,7 +54,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery }; BvInstantiator::BvInstantiator(Env& env, TypeNode tn, BvInverter* inv) - : Instantiator(env, tn), d_inverter(inv), d_inst_id_counter(0) + : Instantiator(env, tn), d_inverter(inv), d_util(env), d_inst_id_counter(0) { // The inverter utility d_inverter is global to all BvInstantiator classes. // This must be global since we need to: @@ -563,7 +562,7 @@ Node BvInstantiator::rewriteTermForSolvePv( if (options().quantifiers.cegqiBvLinearize && contains_pv[lhs] && contains_pv[rhs]) { - Node result = utils::normalizePvEqual(pv, children, contains_pv); + Node result = d_util.normalizePvEqual(pv, children, contains_pv); if (!result.isNull()) { Trace("cegqi-bv-nl") @@ -584,11 +583,11 @@ Node BvInstantiator::rewriteTermForSolvePv( Node result; if (n.getKind() == BITVECTOR_MULT) { - result = utils::normalizePvMult(pv, children, contains_pv); + result = d_util.normalizePvMult(pv, children, contains_pv); } else { - result = utils::normalizePvPlus(pv, children, contains_pv); + result = d_util.normalizePvPlus(pv, children, contains_pv); } if (!result.isNull()) { diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index fda9aa57c..be990899a 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -19,7 +19,9 @@ #define CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H #include + #include "theory/quantifiers/bv_inverter.h" +#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" namespace cvc5::internal { @@ -104,6 +106,8 @@ class BvInstantiator : public Instantiator private: /** pointer to the bv inverter class */ BvInverter* d_inverter; + /** Utility class */ + BvInstantiatorUtil d_util; //--------------------------------solved forms /** identifier counter, used to allocate ids to each solve form */ unsigned d_inst_id_counter; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index 4e4ee317a..4f68c44d3 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -23,9 +23,10 @@ using namespace cvc5::internal::kind; namespace cvc5::internal { namespace theory { namespace quantifiers { -namespace utils { -Node getPvCoeff(TNode pv, TNode n) +BvInstantiatorUtil::BvInstantiatorUtil(Env& env) : EnvObj(env) {} + +Node BvInstantiatorUtil::getPvCoeff(TNode pv, TNode n) const { bool neg = false; Node coeff; @@ -59,9 +60,10 @@ Node getPvCoeff(TNode pv, TNode n) return coeff; } -Node normalizePvMult(TNode pv, - const std::vector& children, - std::unordered_map& contains_pv) +Node BvInstantiatorUtil::normalizePvMult( + TNode pv, + const std::vector& children, + std::unordered_map& contains_pv) const { bool neg, neg_coeff = false; bool found_pv = false; @@ -111,7 +113,7 @@ Node normalizePvMult(TNode pv, { coeff = nm->mkNode(BITVECTOR_NEG, coeff); } - coeff = Rewriter::rewrite(coeff); + coeff = rewrite(coeff); unsigned size_coeff = bv::utils::getSize(coeff); Node zero = bv::utils::mkZero(size_coeff); if (coeff == zero) @@ -136,11 +138,8 @@ Node normalizePvMult(TNode pv, return result; } -#ifdef CVC5_ASSERTIONS -namespace { -bool isLinearPlus(TNode n, - TNode pv, - std::unordered_map& contains_pv) +bool BvInstantiatorUtil::isLinearPlus( + TNode n, TNode pv, std::unordered_map& contains_pv) const { Node coeff; Assert(n.getAttribute(BvLinearAttribute())); @@ -153,17 +152,16 @@ bool isLinearPlus(TNode n, Assert(!contains_pv[n[0][1]]); } Assert(!contains_pv[n[1]]); - coeff = utils::getPvCoeff(pv, n[0]); + coeff = getPvCoeff(pv, n[0]); Assert(!coeff.isNull()); Assert(!contains_pv[coeff]); return true; } -} // namespace -#endif -Node normalizePvPlus(Node pv, - const std::vector& children, - std::unordered_map& contains_pv) +Node BvInstantiatorUtil::normalizePvPlus( + Node pv, + const std::vector& children, + std::unordered_map& contains_pv) const { NodeManager* nm; NodeBuilder nb_c(BITVECTOR_ADD); @@ -190,7 +188,7 @@ Node normalizePvPlus(Node pv, if (nc == pv || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear))) { - Node coeff = utils::getPvCoeff(pv, nc); + Node coeff = getPvCoeff(pv, nc); Assert(!coeff.isNull()); if (neg) { @@ -202,7 +200,7 @@ Node normalizePvPlus(Node pv, else if (nc.getKind() == BITVECTOR_ADD && nc.getAttribute(is_linear)) { Assert(isLinearPlus(nc, pv, contains_pv)); - Node coeff = utils::getPvCoeff(pv, nc[0]); + Node coeff = getPvCoeff(pv, nc[0]); Assert(!coeff.isNull()); Node leaf = nc[1]; if (neg) @@ -223,15 +221,14 @@ Node normalizePvPlus(Node pv, if (nb_c.getNumChildren() > 0) { Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); - coeffs = Rewriter::rewrite(coeffs); - result = pv_mult_coeffs = - utils::normalizePvMult(pv, {pv, coeffs}, contains_pv); + coeffs = rewrite(coeffs); + result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv); } if (nb_l.getNumChildren() > 0) { Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode(); - leafs = Rewriter::rewrite(leafs); + leafs = rewrite(leafs); Node zero = bv::utils::mkZero(bv::utils::getSize(pv)); /* pv * 0 + t --> t */ if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero) @@ -249,9 +246,10 @@ Node normalizePvPlus(Node pv, return result; } -Node normalizePvEqual(Node pv, - const std::vector& children, - std::unordered_map& contains_pv) +Node BvInstantiatorUtil::normalizePvEqual( + Node pv, + const std::vector& children, + std::unordered_map& contains_pv) const { Assert(children.size() == 2); @@ -275,13 +273,13 @@ Node normalizePvEqual(Node pv, if (child.getKind() == BITVECTOR_ADD) { Assert(isLinearPlus(child, pv, contains_pv)); - coeffs[i] = utils::getPvCoeff(pv, child[0]); + coeffs[i] = getPvCoeff(pv, child[0]); leafs[i] = child[1]; } else { Assert(child.getKind() == BITVECTOR_MULT || child == pv); - coeffs[i] = utils::getPvCoeff(pv, child); + coeffs[i] = getPvCoeff(pv, child); } } if (neg) @@ -303,9 +301,9 @@ Node normalizePvEqual(Node pv, } Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]); - coeff = Rewriter::rewrite(coeff); + coeff = rewrite(coeff); std::vector mult_children = {pv, coeff}; - Node lhs = utils::normalizePvMult(pv, mult_children, contains_pv); + Node lhs = normalizePvMult(pv, mult_children, contains_pv); Node rhs; if (!leafs[0].isNull() && !leafs[1].isNull()) @@ -324,7 +322,7 @@ Node normalizePvEqual(Node pv, { rhs = bv::utils::mkZero(bv::utils::getSize(pv)); } - rhs = Rewriter::rewrite(rhs); + rhs = rewrite(rhs); if (lhs == rhs) { @@ -336,7 +334,6 @@ Node normalizePvEqual(Node pv, return result; } -} // namespace utils } // namespace quantifiers } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 40a25ce87..d17fee50d 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -20,6 +20,7 @@ #include "expr/attribute.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5::internal { namespace theory { @@ -30,76 +31,84 @@ struct BvLinearAttributeId }; using BvLinearAttribute = expr::Attribute; -namespace utils { +class BvInstantiatorUtil : protected EnvObj +{ + public: + BvInstantiatorUtil(Env& env); + /** + * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * + * t, or -pv * t. Extracting the coefficient of multiplications only succeeds + * if the multiplication are normalized with normalizePvMult. + * + * If sucessful it returns + * 1 if n == pv, + * -1 if n == -pv, + * t if n == pv * t, + * -t if n == -pv * t. + * If n is not a linear term, a null node is returned. + */ + Node getPvCoeff(TNode pv, TNode n) const; -/** - * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t, - * or -pv * t. Extracting the coefficient of multiplications only succeeds if - * the multiplication are normalized with normalizePvMult. - * - * If sucessful it returns - * 1 if n == pv, - * -1 if n == -pv, - * t if n == pv * t, - * -t if n == -pv * t. - * If n is not a linear term, a null node is returned. - */ -Node getPvCoeff(TNode pv, TNode n); + /** + * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * -pv * b * c + * + * is rewritten to + * + * pv * -(a * b * c) + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns a + * multiplication over children. + */ + Node normalizePvMult(TNode pv, + const std::vector& children, + std::unordered_map& contains_pv) const; -/** - * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks - * terms in which pv occurs. - * For example, - * - * a * -pv * b * c - * - * is rewritten to - * - * pv * -(a * b * c) - * - * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. If pv does not occur in children it returns a - * multiplication over children. - */ -Node normalizePvMult(TNode pv, - const std::vector& children, - std::unordered_map& contains_pv); + /** + * Normalizes the children of a BITVECTOR_ADD w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * pv + b + c * -pv + * + * is rewritten to + * + * pv * (a - c) + b + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns an + * addition over children. + */ + Node normalizePvPlus(Node pv, + const std::vector& children, + std::unordered_map& contains_pv) const; -/** - * Normalizes the children of a BITVECTOR_ADD w.r.t. pv. contains_pv marks - * terms in which pv occurs. - * For example, - * - * a * pv + b + c * -pv - * - * is rewritten to - * - * pv * (a - c) + b - * - * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. If pv does not occur in children it returns an - * addition over children. - */ -Node normalizePvPlus(Node pv, - const std::vector& children, - std::unordered_map& contains_pv); + /** + * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv + * marks terms in which pv occurs. + * For example, equality + * + * -pv * a + b = c + pv + * + * rewrites to + * + * pv * (-a - 1) = c - b. + */ + Node normalizePvEqual(Node pv, + const std::vector& children, + std::unordered_map& contains_pv) const; -/** - * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv - * marks terms in which pv occurs. - * For example, equality - * - * -pv * a + b = c + pv - * - * rewrites to - * - * pv * (-a - 1) = c - b. - */ -Node normalizePvEqual(Node pv, - const std::vector& children, - std::unordered_map& contains_pv); + private: + /** Checks whether n is a linear plus */ + bool isLinearPlus(TNode n, + TNode pv, + std::unordered_map& contains_pv) const; +}; -} // namespace utils } // namespace quantifiers } // namespace theory } // namespace cvc5::internal diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp index 92f21d31c..f61de869d 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp @@ -29,7 +29,6 @@ using namespace theory; using namespace theory::bv; using namespace theory::bv::utils; using namespace theory::quantifiers; -using namespace theory::quantifiers::utils; namespace test { @@ -60,7 +59,7 @@ class TestTheoryWhiteyQuantifiersBvInstantiator : public TestSmt }; /** - * getPvCoeff(x, n) should return + * util.getPvCoeff(x, n) should return * * 1 if n == x * -1 if n == -x @@ -72,38 +71,45 @@ class TestTheoryWhiteyQuantifiersBvInstantiator : public TestSmt */ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, getPvCoeff) { + Env& env = d_slvEngine->getEnv(); + BvInstantiatorUtil util(env); + Node x = mkVar(32); Node a = mkVar(32); Node one = mkOne(32); BvLinearAttribute is_linear; /* x -> 1 */ - Node coeff_x = getPvCoeff(x, x); + Node coeff_x = util.getPvCoeff(x, x); ASSERT_EQ(coeff_x, one); /* -x -> -1 */ - Node coeff_neg_x = getPvCoeff(x, mkNeg(x)); + Node coeff_neg_x = util.getPvCoeff(x, mkNeg(x)); ASSERT_EQ(coeff_neg_x, mkNeg(one)); /* x * a -> null (since x * a not a normalized) */ Node x_mult_a = mkMult(x, a); - Node coeff_x_mult_a = getPvCoeff(x, x_mult_a); + Node coeff_x_mult_a = util.getPvCoeff(x, x_mult_a); ASSERT_TRUE(coeff_x_mult_a.isNull()); /* x * a -> a */ x_mult_a.setAttribute(is_linear, true); - coeff_x_mult_a = getPvCoeff(x, x_mult_a); + coeff_x_mult_a = util.getPvCoeff(x, x_mult_a); ASSERT_EQ(coeff_x_mult_a, a); /* x * -a -> -a */ Node x_mult_neg_a = mkMult(x, mkNeg(a)); x_mult_neg_a.setAttribute(is_linear, true); - Node coeff_x_mult_neg_a = getPvCoeff(x, x_mult_neg_a); + Node coeff_x_mult_neg_a = util.getPvCoeff(x, x_mult_neg_a); ASSERT_EQ(coeff_x_mult_neg_a, mkNeg(a)); } TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult) { + Env& env = d_slvEngine->getEnv(); + BvInstantiatorUtil util(env); + Rewriter* rr = env.getRewriter(); + Node x = mkVar(32); Node neg_x = mkNeg(x); Node a = mkVar(32); @@ -119,15 +125,15 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult) contains_x[neg_x] = true; /* x * -x -> null (since non linear) */ - Node norm_xx = normalizePvMult(x, {x, neg_x}, contains_x); + Node norm_xx = util.normalizePvMult(x, {x, neg_x}, contains_x); ASSERT_TRUE(norm_xx.isNull()); /* nothing to normalize -> create a * a */ - Node norm_aa = normalizePvMult(x, {a, a}, contains_x); - ASSERT_EQ(norm_aa, Rewriter::rewrite(mkMult(a, a))); + Node norm_aa = util.normalizePvMult(x, {a, a}, contains_x); + ASSERT_EQ(norm_aa, rr->rewrite(mkMult(a, a))); /* normalize x * a -> x * a */ - Node norm_xa = normalizePvMult(x, {x, a}, contains_x); + Node norm_xa = util.normalizePvMult(x, {x, a}, contains_x); ASSERT_TRUE(contains_x[norm_xa]); ASSERT_TRUE(norm_xa.getAttribute(is_linear)); ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_MULT); @@ -136,7 +142,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult) ASSERT_EQ(norm_xa[1], a); /* normalize a * x -> x * a */ - Node norm_ax = normalizePvMult(x, {a, x}, contains_x); + Node norm_ax = util.normalizePvMult(x, {a, x}, contains_x); ASSERT_TRUE(contains_x[norm_ax]); ASSERT_TRUE(norm_ax.getAttribute(is_linear)); ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_MULT); @@ -145,7 +151,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult) ASSERT_EQ(norm_ax[1], a); /* normalize a * -x -> x * -a */ - Node norm_neg_ax = normalizePvMult(x, {a, neg_x}, contains_x); + Node norm_neg_ax = util.normalizePvMult(x, {a, neg_x}, contains_x); ASSERT_TRUE(contains_x[norm_neg_ax]); ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear)); ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_MULT); @@ -154,55 +160,59 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult) ASSERT_EQ(norm_neg_ax[1], mkNeg(a)); /* normalize 0 * x -> 0 */ - Node norm_zx = normalizePvMult(x, {zero, x}, contains_x); + Node norm_zx = util.normalizePvMult(x, {zero, x}, contains_x); ASSERT_EQ(norm_zx, zero); /* normalize 1 * x -> x */ - Node norm_ox = normalizePvMult(x, {one, x}, contains_x); + Node norm_ox = util.normalizePvMult(x, {one, x}, contains_x); ASSERT_EQ(norm_ox, x); /* normalize a * b * c * x * d -> x * (a * b * c * d) */ - Node norm_abcxd = normalizePvMult(x, {a, b, c, x, d}, contains_x); + Node norm_abcxd = util.normalizePvMult(x, {a, b, c, x, d}, contains_x); ASSERT_TRUE(contains_x[norm_abcxd]); ASSERT_TRUE(norm_abcxd.getAttribute(is_linear)); ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_abcxd.getNumChildren(), 2); ASSERT_EQ(norm_abcxd[0], x); - ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkMult({a, b, c, d}))); + ASSERT_EQ(norm_abcxd[1], rr->rewrite(mkMult({a, b, c, d}))); /* normalize a * b * c * -x * d -> x * -(a * b * c * d) */ - Node norm_neg_abcxd = normalizePvMult(x, {a, b, c, neg_x, d}, contains_x); + Node norm_neg_abcxd = + util.normalizePvMult(x, {a, b, c, neg_x, d}, contains_x); ASSERT_TRUE(contains_x[norm_neg_abcxd]); ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear)); ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_neg_abcxd.getNumChildren(), 2); ASSERT_EQ(norm_neg_abcxd[0], x); - ASSERT_TRUE(norm_neg_abcxd[1] - == mkNeg(Rewriter::rewrite(mkMult({a, b, c, d})))); + ASSERT_TRUE(norm_neg_abcxd[1] == mkNeg(rr->rewrite(mkMult({a, b, c, d})))); /* normalize b * (x * a) -> x * (b * a) */ - Node norm_bxa = normalizePvMult(x, {b, norm_ax}, contains_x); + Node norm_bxa = util.normalizePvMult(x, {b, norm_ax}, contains_x); ASSERT_TRUE(contains_x[norm_bxa]); ASSERT_TRUE(norm_bxa.getAttribute(is_linear)); ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_bxa.getNumChildren(), 2); ASSERT_EQ(norm_bxa[0], x); - ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkMult(b, a))); + ASSERT_EQ(norm_bxa[1], rr->rewrite(mkMult(b, a))); /* normalize b * -(x * a) -> x * -(a * b) */ Node neg_norm_ax = mkNeg(norm_ax); contains_x[neg_norm_ax] = true; - Node norm_neg_bxa = normalizePvMult(x, {b, neg_norm_ax}, contains_x); + Node norm_neg_bxa = util.normalizePvMult(x, {b, neg_norm_ax}, contains_x); ASSERT_TRUE(contains_x[norm_neg_bxa]); ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear)); ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_neg_bxa.getNumChildren(), 2); ASSERT_EQ(norm_neg_bxa[0], x); - ASSERT_EQ(norm_neg_bxa[1], mkNeg(Rewriter::rewrite(mkMult(b, a)))); + ASSERT_EQ(norm_neg_bxa[1], mkNeg(rr->rewrite(mkMult(b, a)))); } TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) { + Env& env = d_slvEngine->getEnv(); + BvInstantiatorUtil util(env); + Rewriter* rr = env.getRewriter(); + Node one = mkOne(32); Node x = mkVar(32); Node neg_x = mkNeg(x); @@ -219,15 +229,15 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) /* a + b * x -> null (since b * x not normalized) */ Node mult_bx = mkMult(b, x); contains_x[mult_bx] = true; - Node norm_abx = normalizePvPlus(x, {a, mult_bx}, contains_x); + Node norm_abx = util.normalizePvPlus(x, {a, mult_bx}, contains_x); ASSERT_TRUE(norm_abx.isNull()); /* nothing to normalize -> create a + a */ - Node norm_aa = normalizePvPlus(x, {a, a}, contains_x); - ASSERT_EQ(norm_aa, Rewriter::rewrite(mkPlus(a, a))); + Node norm_aa = util.normalizePvPlus(x, {a, a}, contains_x); + ASSERT_EQ(norm_aa, rr->rewrite(mkPlus(a, a))); /* x + a -> x + a */ - Node norm_xa = normalizePvPlus(x, {x, a}, contains_x); + Node norm_xa = util.normalizePvPlus(x, {x, a}, contains_x); ASSERT_TRUE(contains_x[norm_xa]); ASSERT_TRUE(norm_xa.getAttribute(is_linear)); ASSERT_EQ(norm_xa.getKind(), kind::BITVECTOR_ADD); @@ -236,7 +246,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) ASSERT_EQ(norm_xa[1], a); /* a * x -> x * a */ - Node norm_ax = normalizePvPlus(x, {a, x}, contains_x); + Node norm_ax = util.normalizePvPlus(x, {a, x}, contains_x); ASSERT_TRUE(contains_x[norm_ax]); ASSERT_TRUE(norm_ax.getAttribute(is_linear)); ASSERT_EQ(norm_ax.getKind(), kind::BITVECTOR_ADD); @@ -245,7 +255,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) ASSERT_EQ(norm_ax[1], a); /* a + -x -> (x * -1) + a */ - Node norm_neg_ax = normalizePvPlus(x, {a, neg_x}, contains_x); + Node norm_neg_ax = util.normalizePvPlus(x, {a, neg_x}, contains_x); ASSERT_TRUE(contains_x[norm_neg_ax]); ASSERT_TRUE(norm_neg_ax.getAttribute(is_linear)); ASSERT_EQ(norm_neg_ax.getKind(), kind::BITVECTOR_ADD); @@ -255,30 +265,33 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) ASSERT_TRUE(norm_neg_ax[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_neg_ax[0]]); ASSERT_EQ(norm_neg_ax[0][0], x); - ASSERT_EQ(norm_neg_ax[0][1], Rewriter::rewrite(mkNeg(one))); + ASSERT_EQ(norm_neg_ax[0][1], rr->rewrite(mkNeg(one))); ASSERT_EQ(norm_neg_ax[1], a); /* -x + -a * x -> x * (-1 - a) */ - Node norm_xax = normalizePvPlus( - x, {mkNeg(x), normalizePvMult(x, {mkNeg(a), x}, contains_x)}, contains_x); + Node norm_xax = util.normalizePvPlus( + x, + {mkNeg(x), util.normalizePvMult(x, {mkNeg(a), x}, contains_x)}, + contains_x); ASSERT_TRUE(contains_x[norm_xax]); ASSERT_TRUE(norm_xax.getAttribute(is_linear)); ASSERT_EQ(norm_xax.getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_xax.getNumChildren(), 2); ASSERT_EQ(norm_xax[0], x); - ASSERT_EQ(norm_xax[1], Rewriter::rewrite(mkPlus(mkNeg(one), mkNeg(a)))); + ASSERT_EQ(norm_xax[1], rr->rewrite(mkPlus(mkNeg(one), mkNeg(a)))); /* a + b + c + x + d -> x + (a + b + c + d) */ - Node norm_abcxd = normalizePvPlus(x, {a, b, c, x, d}, contains_x); + Node norm_abcxd = util.normalizePvPlus(x, {a, b, c, x, d}, contains_x); ASSERT_TRUE(contains_x[norm_abcxd]); ASSERT_TRUE(norm_abcxd.getAttribute(is_linear)); ASSERT_EQ(norm_abcxd.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_abcxd.getNumChildren(), 2); ASSERT_EQ(norm_abcxd[0], x); - ASSERT_EQ(norm_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d}))); + ASSERT_EQ(norm_abcxd[1], rr->rewrite(mkPlus({a, b, c, d}))); /* a + b + c + -x + d -> (x * -1) + (a + b + c + d) */ - Node norm_neg_abcxd = normalizePvPlus(x, {a, b, c, neg_x, d}, contains_x); + Node norm_neg_abcxd = + util.normalizePvPlus(x, {a, b, c, neg_x, d}, contains_x); ASSERT_TRUE(contains_x[norm_neg_abcxd]); ASSERT_TRUE(norm_neg_abcxd.getAttribute(is_linear)); ASSERT_EQ(norm_neg_abcxd.getKind(), kind::BITVECTOR_ADD); @@ -288,22 +301,22 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) ASSERT_TRUE(norm_neg_abcxd[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_neg_abcxd[0]]); ASSERT_EQ(norm_neg_abcxd[0][0], x); - ASSERT_EQ(norm_neg_abcxd[0][1], Rewriter::rewrite(mkNeg(one))); - ASSERT_EQ(norm_neg_abcxd[1], Rewriter::rewrite(mkPlus({a, b, c, d}))); + ASSERT_EQ(norm_neg_abcxd[0][1], rr->rewrite(mkNeg(one))); + ASSERT_EQ(norm_neg_abcxd[1], rr->rewrite(mkPlus({a, b, c, d}))); /* b + (x + a) -> x + (b + a) */ - Node norm_bxa = normalizePvPlus(x, {b, norm_ax}, contains_x); + Node norm_bxa = util.normalizePvPlus(x, {b, norm_ax}, contains_x); ASSERT_TRUE(contains_x[norm_bxa]); ASSERT_TRUE(norm_bxa.getAttribute(is_linear)); ASSERT_EQ(norm_bxa.getKind(), kind::BITVECTOR_ADD); ASSERT_EQ(norm_bxa.getNumChildren(), 2); ASSERT_EQ(norm_bxa[0], x); - ASSERT_EQ(norm_bxa[1], Rewriter::rewrite(mkPlus(b, a))); + ASSERT_EQ(norm_bxa[1], rr->rewrite(mkPlus(b, a))); /* b + -(x + a) -> (x * -1) + b - a */ Node neg_norm_ax = mkNeg(norm_ax); contains_x[neg_norm_ax] = true; - Node norm_neg_bxa = normalizePvPlus(x, {b, neg_norm_ax}, contains_x); + Node norm_neg_bxa = util.normalizePvPlus(x, {b, neg_norm_ax}, contains_x); ASSERT_TRUE(contains_x[norm_neg_bxa]); ASSERT_TRUE(norm_neg_bxa.getAttribute(is_linear)); ASSERT_EQ(norm_neg_bxa.getKind(), kind::BITVECTOR_ADD); @@ -313,17 +326,21 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus) ASSERT_TRUE(norm_neg_abcxd[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_neg_abcxd[0]]); ASSERT_EQ(norm_neg_abcxd[0][0], x); - ASSERT_EQ(norm_neg_abcxd[0][1], Rewriter::rewrite(mkNeg(one))); - ASSERT_EQ(norm_neg_bxa[1], Rewriter::rewrite((mkPlus(b, mkNeg(a))))); + ASSERT_EQ(norm_neg_abcxd[0][1], rr->rewrite(mkNeg(one))); + ASSERT_EQ(norm_neg_bxa[1], rr->rewrite((mkPlus(b, mkNeg(a))))); /* -x + x + a -> a */ - Node norm_neg_xxa = normalizePvPlus(x, {neg_x, x, a}, contains_x); + Node norm_neg_xxa = util.normalizePvPlus(x, {neg_x, x, a}, contains_x); ASSERT_FALSE(contains_x[norm_neg_xxa]); ASSERT_EQ(norm_neg_xxa, a); } TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual) { + Env& env = d_slvEngine->getEnv(); + BvInstantiatorUtil util(env); + Rewriter* rr = env.getRewriter(); + Node x = mkVar(32); Node neg_x = mkNeg(x); Node a = mkVar(32); @@ -340,74 +357,75 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual) contains_x[neg_x] = true; /* x = a -> null (nothing to normalize) */ - Node norm_xa = normalizePvEqual(x, {x, a}, contains_x); + Node norm_xa = util.normalizePvEqual(x, {x, a}, contains_x); ASSERT_TRUE(norm_xa.isNull()); /* x = x -> true */ - Node norm_xx = normalizePvEqual(x, {x, x}, contains_x); + Node norm_xx = util.normalizePvEqual(x, {x, x}, contains_x); ASSERT_EQ(norm_xx, ntrue); /* x = -x -> x * 2 = 0 */ - Node norm_neg_xx = normalizePvEqual(x, {x, neg_x}, contains_x); + Node norm_neg_xx = util.normalizePvEqual(x, {x, neg_x}, contains_x); ASSERT_EQ(norm_neg_xx.getKind(), kind::EQUAL); ASSERT_EQ(norm_neg_xx[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_neg_xx[0].getNumChildren(), 2); ASSERT_TRUE(norm_neg_xx[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_neg_xx[0]]); ASSERT_EQ(norm_neg_xx[0][0], x); - ASSERT_EQ(norm_neg_xx[0][1], Rewriter::rewrite(mkConst(32, 2))); + ASSERT_EQ(norm_neg_xx[0][1], rr->rewrite(mkConst(32, 2))); ASSERT_EQ(norm_neg_xx[1], zero); /* a + x = x -> 0 = -a */ - Node norm_axx = normalizePvEqual( - x, {normalizePvPlus(x, {a, x}, contains_x), x}, contains_x); + Node norm_axx = util.normalizePvEqual( + x, {util.normalizePvPlus(x, {a, x}, contains_x), x}, contains_x); ASSERT_EQ(norm_axx.getKind(), kind::EQUAL); ASSERT_EQ(norm_axx[0], zero); ASSERT_EQ(norm_axx[1], mkNeg(a)); /* a + -x = x -> x * -2 = a */ - Node norm_neg_axx = normalizePvEqual( - x, {normalizePvPlus(x, {a, neg_x}, contains_x), x}, contains_x); + Node norm_neg_axx = util.normalizePvEqual( + x, {util.normalizePvPlus(x, {a, neg_x}, contains_x), x}, contains_x); ASSERT_EQ(norm_neg_axx.getKind(), kind::EQUAL); ASSERT_EQ(norm_neg_axx[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_neg_axx[0].getNumChildren(), 2); ASSERT_TRUE(norm_neg_axx[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_neg_axx[0]]); ASSERT_EQ(norm_neg_axx[0][0], x); - ASSERT_EQ(norm_neg_axx[0][1], Rewriter::rewrite(mkNeg(mkConst(32, 2)))); + ASSERT_EQ(norm_neg_axx[0][1], rr->rewrite(mkNeg(mkConst(32, 2)))); ASSERT_EQ(norm_neg_axx[1], mkNeg(a)); /* a * x = x -> x * (a - 1) = 0 */ - Node norm_mult_axx = normalizePvEqual( - x, {normalizePvMult(x, {a, x}, contains_x), x}, contains_x); + Node norm_mult_axx = util.normalizePvEqual( + x, {util.normalizePvMult(x, {a, x}, contains_x), x}, contains_x); ASSERT_EQ(norm_mult_axx.getKind(), kind::EQUAL); ASSERT_EQ(norm_mult_axx[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_mult_axx[0].getNumChildren(), 2); ASSERT_TRUE(norm_mult_axx[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_mult_axx[0]]); ASSERT_EQ(norm_mult_axx[0][0], x); - ASSERT_EQ(norm_mult_axx[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); + ASSERT_EQ(norm_mult_axx[0][1], rr->rewrite(mkPlus(a, mkNeg(one)))); ASSERT_EQ(norm_mult_axx[1], zero); /* a * x = x + b -> x * (a - 1) = b */ - Node norm_axxb = normalizePvEqual(x, - {normalizePvMult(x, {a, x}, contains_x), - normalizePvPlus(x, {b, x}, contains_x)}, - contains_x); + Node norm_axxb = + util.normalizePvEqual(x, + {util.normalizePvMult(x, {a, x}, contains_x), + util.normalizePvPlus(x, {b, x}, contains_x)}, + contains_x); ASSERT_EQ(norm_axxb.getKind(), kind::EQUAL); ASSERT_EQ(norm_axxb[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_axxb[0].getNumChildren(), 2); ASSERT_TRUE(norm_axxb[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_axxb[0]]); ASSERT_EQ(norm_axxb[0][0], x); - ASSERT_EQ(norm_axxb[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); + ASSERT_EQ(norm_axxb[0][1], rr->rewrite(mkPlus(a, mkNeg(one)))); ASSERT_EQ(norm_axxb[1], b); /* a * x + c = x -> x * (a - 1) = -c */ - Node norm_axcx = normalizePvEqual( + Node norm_axcx = util.normalizePvEqual( x, - {normalizePvPlus( - x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x), + {util.normalizePvPlus( + x, {util.normalizePvMult(x, {a, x}, contains_x), c}, contains_x), x}, contains_x); ASSERT_EQ(norm_axcx.getKind(), kind::EQUAL); @@ -416,15 +434,15 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual) ASSERT_TRUE(norm_axcx[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_axcx[0]]); ASSERT_EQ(norm_axcx[0][0], x); - ASSERT_EQ(norm_axcx[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); + ASSERT_EQ(norm_axcx[0][1], rr->rewrite(mkPlus(a, mkNeg(one)))); ASSERT_EQ(norm_axcx[1], mkNeg(c)); /* a * x + c = x + b -> x * (a - 1) = b - c*/ - Node norm_axcxb = normalizePvEqual( + Node norm_axcxb = util.normalizePvEqual( x, - {normalizePvPlus( - x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x), - normalizePvPlus(x, {b, x}, contains_x)}, + {util.normalizePvPlus( + x, {util.normalizePvMult(x, {a, x}, contains_x), c}, contains_x), + util.normalizePvPlus(x, {b, x}, contains_x)}, contains_x); ASSERT_EQ(norm_axcxb.getKind(), kind::EQUAL); ASSERT_EQ(norm_axcxb[0].getKind(), kind::BITVECTOR_MULT); @@ -432,22 +450,22 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual) ASSERT_TRUE(norm_axcxb[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_axcxb[0]]); ASSERT_EQ(norm_axcxb[0][0], x); - ASSERT_EQ(norm_axcxb[0][1], Rewriter::rewrite(mkPlus(a, mkNeg(one)))); - ASSERT_EQ(norm_axcxb[1], Rewriter::rewrite(mkPlus(b, mkNeg(c)))); + ASSERT_EQ(norm_axcxb[0][1], rr->rewrite(mkPlus(a, mkNeg(one)))); + ASSERT_EQ(norm_axcxb[1], rr->rewrite(mkPlus(b, mkNeg(c)))); /* -(a + -x) = a * x -> x * (1 - a) = a */ - Node norm_axax = - normalizePvEqual(x, - {mkNeg(normalizePvPlus(x, {a, neg_x}, contains_x)), - normalizePvMult(x, {a, x}, contains_x)}, - contains_x); + Node norm_axax = util.normalizePvEqual( + x, + {mkNeg(util.normalizePvPlus(x, {a, neg_x}, contains_x)), + util.normalizePvMult(x, {a, x}, contains_x)}, + contains_x); ASSERT_EQ(norm_axax.getKind(), kind::EQUAL); ASSERT_EQ(norm_axax[0].getKind(), kind::BITVECTOR_MULT); ASSERT_EQ(norm_axax[0].getNumChildren(), 2); ASSERT_TRUE(norm_axax[0].getAttribute(is_linear)); ASSERT_TRUE(contains_x[norm_axax[0]]); ASSERT_EQ(norm_axax[0][0], x); - ASSERT_EQ(norm_axax[0][1], Rewriter::rewrite(mkPlus(one, mkNeg(a)))); + ASSERT_EQ(norm_axax[0][1], rr->rewrite(mkPlus(one, mkNeg(a)))); ASSERT_EQ(norm_axax[1], a); } } // namespace test