From 99fb7d9e0b963222574c01e0362d3720c62b825f Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 8 Dec 2017 17:36:15 -0800 Subject: [PATCH] Add CEGQI BV linearization of additions and equalities over additions. (#1417) Adds support for linearizing additions w.r.t. to a variable. For example, a * x + b + c * d * -x = e + x is rewritten to x * (a - c * d - 1) = e - b. This also adds an additional rewriting rule x * x = x --> x < 2. --- src/options/quantifiers_options | 2 + src/theory/bv/theory_bv_utils.cpp | 15 + src/theory/bv/theory_bv_utils.h | 2 +- src/theory/quantifiers/ceg_t_instantiator.cpp | 469 ++++++++++++++++- test/unit/Makefile.am | 1 + ...theory_quantifiers_bv_instantiator_white.h | 484 ++++++++++++++++++ 6 files changed, 961 insertions(+), 12 deletions(-) create mode 100644 test/unit/theory/theory_quantifiers_bv_instantiator_white.h diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index ef20881db..c3091a131 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -349,6 +349,8 @@ option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqM choose mode for handling bit-vector inequalities with counterexample-guided instantiation option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true replaces extract terms with variables for counterexample-guided instantiation for bit-vectors +option cbqiBvLinearize --cbqi-bv-linear bool :read-write :default true + linearize adder chains for variables ### local theory extensions options diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 089989e19..783d04492 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -26,6 +26,21 @@ namespace theory { namespace bv { namespace utils { +Node mkSum(std::vector& children, unsigned width) +{ + std::size_t nchildren = children.size(); + + if (nchildren == 0) + { + return mkZero(width); + } + else if (nchildren == 1) + { + return children[0]; + } + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, children); +} + Node mkInc(TNode t) { return NodeManager::currentNM()->mkNode( diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index fca0a3a47..ea2dd4fc8 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -156,9 +156,9 @@ inline Node mkExtract(TNode node, unsigned high, unsigned low) { inline Node mkBitOf(TNode node, unsigned index) { Node bitOfOp = NodeManager::currentNM()->mkConst(BitVectorBitOf(index)); return NodeManager::currentNM()->mkNode(bitOfOp, node); - } +Node mkSum(std::vector& children, unsigned width); inline Node mkConcat(TNode node, unsigned repeat) { Assert (repeat); diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 18086cbd5..55cc59c51 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -40,6 +40,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { +struct BvLinearAttributeId {}; +using BvLinearAttribute = expr::Attribute; + Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { Node val = t; Trace("cegqi-arith-bound2") << "Value : " << val << std::endl; @@ -1317,6 +1320,8 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, children.push_back(it->second); contains_pv = contains_pv || visited_contains_pv[cur[i]]; } + // careful that rewrites above do not affect whether this term contains pv + visited_contains_pv[cur] = contains_pv; // rewrite the term ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv); @@ -1329,8 +1334,19 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, ret = cur; } } - // careful that rewrites above do not affect whether this term contains pv - visited_contains_pv[cur] = contains_pv; + + /* We need to update contains_pv also for rewritten nodes, since + * the normalizePv* functions rely on the information if pv occurs in a + * rewritten node or not. */ + if (ret != cur) + { + contains_pv = (ret == pv); + for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i) + { + contains_pv = contains_pv || visited_contains_pv[ret[i]]; + } + visited_contains_pv[ret] = contains_pv; + } // if was choice, pop context if (cur.getKind() == CHOICE) @@ -1345,19 +1361,391 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, visited.top()[cur] = ret; } - else if (Trace.isOn("cegqi-bv-nl")) - { - if (cur == pv) - { - Trace("cegqi-bv-nl") << "NONLINEAR LITERAL for " << pv << " : " << lit - << std::endl; - } - } } while (!visit.top().empty()); Assert(visited.size() == 1); Assert(visited.top().find(lit) != visited.top().end()); Assert(!visited.top().find(lit)->second.isNull()); - return visited.top()[lit]; + + Node result = visited.top()[lit]; + + if (Trace.isOn("cegqi-bv-nl")) + { + std::vector trace_visit; + std::unordered_set trace_visited; + + trace_visit.push_back(result); + do + { + cur = trace_visit.back(); + trace_visit.pop_back(); + + if (trace_visited.find(cur) == trace_visited.end()) + { + trace_visited.insert(cur); + trace_visit.insert(trace_visit.end(), cur.begin(), cur.end()); + } + else if (cur == pv) + { + Trace("cegqi-bv-nl") + << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl; + } + } while (!trace_visit.empty()); + } + + return result; +} + +/** + * 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. + */ +static Node getPvCoeff(TNode pv, TNode n) +{ + bool neg = false; + Node coeff; + + if (n.getKind() == BITVECTOR_NEG) + { + neg = true; + n = n[0]; + } + + if (n == pv) + { + coeff = bv::utils::mkOne(bv::utils::getSize(pv)); + } + /* All multiplications are normalized to pv * (t1 * t2). */ + else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute())) + { + Assert(n.getNumChildren() == 2); + Assert(n[0] == pv); + coeff = n[1]; + } + else /* n is in no form to extract the coefficient for pv */ + { + Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in " + << n << std::endl; + return Node::null(); + } + Assert(!coeff.isNull()); + + if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff); + return coeff; +} + +/** + * 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. + */ +static Node normalizePvMult( + TNode pv, + const std::vector& children, + std::unordered_map& contains_pv) +{ + bool neg, neg_coeff = false; + bool found_pv = false; + NodeManager* nm; + NodeBuilder<> nb(BITVECTOR_MULT); + BvLinearAttribute is_linear; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (!found_pv && nc == pv) + { + found_pv = true; + neg_coeff = neg; + continue; + } + else if (!found_pv && nc.getKind() == BITVECTOR_MULT + && nc.getAttribute(is_linear)) + { + Assert(nc.getNumChildren() == 2); + Assert(nc[0] == pv); + Assert(!contains_pv[nc[1]]); + found_pv = true; + neg_coeff = neg; + nb << nc[1]; + continue; + } + return Node::null(); /* non-linear */ + } + Assert(nb.getNumChildren() > 0); + + Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode(); + if (neg_coeff) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + coeff = Rewriter::rewrite(coeff); + unsigned size_coeff = bv::utils::getSize(coeff); + Node zero = bv::utils::mkZero(size_coeff); + if (coeff == zero) + { + return zero; + } + else if (coeff == bv::utils::mkOne(size_coeff)) + { + return pv; + } + Node result = nm->mkNode(BITVECTOR_MULT, pv, coeff); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + return result; +} + +#ifdef CVC4_ASSERTIONS +static bool isLinearPlus( + TNode n, + TNode pv, + std::unordered_map& contains_pv) +{ + Node coeff; + Assert(n.getAttribute(BvLinearAttribute())); + Assert(n.getNumChildren() == 2); + if (n[0] != pv) + { + Assert(n[0].getKind() == BITVECTOR_MULT); + Assert(n[0].getNumChildren() == 2); + Assert(n[0][0] == pv); + Assert(!contains_pv[n[0][1]]); + } + Assert(!contains_pv[n[1]]); + coeff = getPvCoeff(pv, n[0]); + Assert(!coeff.isNull()); + Assert(!contains_pv[coeff]); + return true; +} +#endif + +/** + * Normalizes the children of a BITVECTOR_PLUS 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. + */ +static Node normalizePvPlus( + Node pv, + const std::vector& children, + std::unordered_map& contains_pv) +{ + NodeManager* nm; + NodeBuilder<> nb_c(BITVECTOR_PLUS); + NodeBuilder<> nb_l(BITVECTOR_PLUS); + BvLinearAttribute is_linear; + bool neg; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb_l << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (nc == pv + || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear))) + { + Node coeff = getPvCoeff(pv, nc); + Assert(!coeff.isNull()); + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + nb_c << coeff; + continue; + } + else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear)) + { + Assert(isLinearPlus(nc, pv, contains_pv)); + Node coeff = getPvCoeff(pv, nc[0]); + Node leaf = nc[1]; + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + leaf = nm->mkNode(BITVECTOR_NEG, leaf); + } + nb_c << coeff; + nb_l << leaf; + continue; + } + /* can't collect coefficients of 'pv' in 'cur' -> non-linear */ + return Node::null(); + } + Assert(nb_c.getNumChildren() > 0); + + Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); + coeffs = Rewriter::rewrite(coeffs); + + std::vector mult_children = {pv, coeffs}; + Node pv_mult_coeffs = normalizePvMult(pv, mult_children, contains_pv); + + if (nb_l.getNumChildren() > 0) + { + Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode(); + leafs = Rewriter::rewrite(leafs); + Node zero = bv::utils::mkZero(bv::utils::getSize(pv)); + Node result; + /* pv * 0 + t --> t */ + if (pv_mult_coeffs == zero) + { + result = leafs; + } + else + { + result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + } + return result; + } + return pv_mult_coeffs; +} + +/** + * 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. + */ +static Node normalizePvEqual( + Node pv, + const std::vector& children, + std::unordered_map& contains_pv) +{ + Assert(children.size() == 2); + + NodeManager* nm = NodeManager::currentNM(); + BvLinearAttribute is_linear; + Node coeffs[2], leafs[2]; + bool neg; + TNode child; + + for (unsigned i = 0; i < 2; ++i) + { + child = children[i]; + neg = false; + if (child.getKind() == BITVECTOR_NEG) + { + neg = true; + child = child[0]; + } + if (child.getAttribute(is_linear) || child == pv) + { + if (child.getKind() == BITVECTOR_PLUS) + { + Assert(isLinearPlus(child, pv, contains_pv)); + coeffs[i] = getPvCoeff(pv, child[0]); + leafs[i] = child[1]; + } + else + { + Assert(child.getKind() == BITVECTOR_MULT || child == pv); + coeffs[i] = getPvCoeff(pv, child); + } + } + if (neg) + { + if (!coeffs[i].isNull()) + { + coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]); + } + if (!leafs[i].isNull()) + { + leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]); + } + } + } + + if (coeffs[0].isNull() || coeffs[1].isNull()) + { + return Node::null(); + } + + Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]); + coeff = Rewriter::rewrite(coeff); + std::vector mult_children = {pv, coeff}; + Node lhs = normalizePvMult(pv, mult_children, contains_pv); + + Node rhs; + if (!leafs[0].isNull() && !leafs[1].isNull()) + { + rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]); + } + else if (!leafs[0].isNull()) + { + rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]); + } + else if (!leafs[1].isNull()) + { + rhs = leafs[1]; + } + else + { + rhs = bv::utils::mkZero(bv::utils::getSize(pv)); + } + rhs = Rewriter::rewrite(rhs); + + if (lhs == rhs) + { + return bv::utils::mkTrue(); + } + + Node result = lhs.eqNode(rhs); + contains_pv[result] = true; + return result; } Node BvInstantiator::rewriteTermForSolvePv( @@ -1384,6 +1772,65 @@ Node BvInstantiator::rewriteTermForSolvePv( children[1])); } } + else if (n.getKind() == EQUAL) + { + TNode lhs = children[0]; + TNode rhs = children[1]; + + /* rewrite: x * x = x -> x < 2 */ + if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv + && rhs[1] == pv) + || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv + && lhs[1] == pv)) + { + return nm->mkNode( + BITVECTOR_ULT, + pv, + bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2)))); + } + + if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) + { + Node result = normalizePvEqual(pv, children, contains_pv); + if (!result.isNull()) + { + Trace("cegqi-bv-nl") + << "Normalize " << n << " to " << result << std::endl; + } + else + { + Trace("cegqi-bv-nl") + << "Nonlinear " << n.getKind() << " " << n << std::endl; + } + return result; + } + } + else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS) + { + if (options::cbqiBvLinearize() && contains_pv[n]) + { + Node result; + if (n.getKind() == BITVECTOR_MULT) + { + result = normalizePvMult(pv, children, contains_pv); + } + else + { + result = normalizePvPlus(pv, children, contains_pv); + } + if (!result.isNull()) + { + Trace("cegqi-bv-nl") + << "Normalize " << n << " to " << result << std::endl; + return result; + } + else + { + Trace("cegqi-bv-nl") + << "Nonlinear " << n.getKind() << " " << n << std::endl; + } + } + } // [2] try to rewrite non-linear literals -> linear literals diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index dfa3c79b6..9f61ef031 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -13,6 +13,7 @@ UNIT_TESTS += \ theory/theory_arith_white \ theory/theory_bv_white \ theory/theory_bv_bvgauss_white \ + theory/theory_quantifiers_bv_instantiator_white \ theory/theory_quantifiers_bv_inverter_white \ theory/type_enumerator_white \ expr/node_white \ diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h new file mode 100644 index 000000000..1f3932be0 --- /dev/null +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -0,0 +1,484 @@ +/********************* */ +/*! \file theory_bv_bvgauss_white.h + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Unit tests for BvInstantiator. + ** + ** Unit tests for BvInstantiator. + **/ + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" +#include "util/bitvector.h" + +#include "theory/quantifiers/ceg_t_instantiator.cpp" + +#include +#include +#include + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::smt; + +class BvInstantiatorWhite : public CxxTest::TestSuite +{ + public: + void setUp(); + void tearDown(); + + void testGetPvCoeff(); + void testNormalizePvMult(); + void testNormalizePvPlus(); + void testNormalizePvEqual(); + + private: + ExprManager* d_em; + NodeManager* d_nm; + SmtEngine* d_smt; + SmtScope* d_scope; + + Node mkNeg(TNode n); + Node mkMult(TNode a, TNode b); + Node mkMult(const std::vector& children); + Node mkPlus(TNode a, TNode b); + Node mkPlus(const std::vector& children); +}; + +void BvInstantiatorWhite::setUp() +{ + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_scope = new SmtScope(d_smt); +} + +void BvInstantiatorWhite::tearDown() +{ + delete d_scope; + delete d_smt; + delete d_em; +} + +Node BvInstantiatorWhite::mkNeg(TNode n) +{ + return d_nm->mkNode(kind::BITVECTOR_NEG, n); +} + +Node BvInstantiatorWhite::mkMult(TNode a, TNode b) +{ + return d_nm->mkNode(kind::BITVECTOR_MULT, a, b); +} + +Node BvInstantiatorWhite::mkMult(const std::vector& children) +{ + return d_nm->mkNode(kind::BITVECTOR_MULT, children); +} + +Node BvInstantiatorWhite::mkPlus(TNode a, TNode b) +{ + return d_nm->mkNode(kind::BITVECTOR_PLUS, a, b); +} + +Node BvInstantiatorWhite::mkPlus(const std::vector& children) +{ + return d_nm->mkNode(kind::BITVECTOR_PLUS, children); +} + +/** + * getPvCoeff(x, n) should return + * + * 1 if n == x + * -1 if n == -x + * a if n == x * a + * -a if n == x * -a + * Node::null() otherwise. + * + * Note that x * a and x * -a have to be normalized. + */ +void BvInstantiatorWhite::testGetPvCoeff() +{ + Node x = mkVar(32); + Node a = mkVar(32); + Node one = mkOne(32); + BvLinearAttribute is_linear; + + /* x -> 1 */ + Node coeff_x = getPvCoeff(x, x); + TS_ASSERT(coeff_x == one); + + /* -x -> -1 */ + Node coeff_neg_x = getPvCoeff(x, mkNeg(x)); + TS_ASSERT(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); + TS_ASSERT(coeff_x_mult_a.isNull()); + + /* x * a -> a */ + x_mult_a.setAttribute(is_linear, true); + coeff_x_mult_a = getPvCoeff(x, x_mult_a); + TS_ASSERT(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); + TS_ASSERT(coeff_x_mult_neg_a == mkNeg(a)); +} + +void BvInstantiatorWhite::testNormalizePvMult() +{ + Node x = mkVar(32); + Node neg_x = mkNeg(x); + Node a = mkVar(32); + Node b = mkVar(32); + Node c = mkVar(32); + Node d = mkVar(32); + Node zero = mkZero(32); + Node one = mkOne(32); + BvLinearAttribute is_linear; + std::unordered_map contains_x; + + contains_x[x] = true; + contains_x[neg_x] = true; + + /* x * -x -> null (since non linear) */ + Node norm_xx = normalizePvMult(x, {x, neg_x}, contains_x); + TS_ASSERT(norm_xx.isNull()); + + /* normalize x * a -> x * a */ + Node norm_xa = normalizePvMult(x, {x, a}, contains_x); + TS_ASSERT(contains_x[norm_xa]); + TS_ASSERT(norm_xa.getAttribute(is_linear)); + TS_ASSERT(norm_xa.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_xa.getNumChildren() == 2); + TS_ASSERT(norm_xa[0] == x); + TS_ASSERT(norm_xa[1] == a); + + /* normalize a * x -> x * a */ + Node norm_ax = normalizePvMult(x, {a, x}, contains_x); + TS_ASSERT(contains_x[norm_ax]); + TS_ASSERT(norm_ax.getAttribute(is_linear)); + TS_ASSERT(norm_ax.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_ax.getNumChildren() == 2); + TS_ASSERT(norm_ax[0] == x); + TS_ASSERT(norm_ax[1] == a); + + /* normalize a * -x -> x * -a */ + Node norm_neg_ax = normalizePvMult(x, {a, neg_x}, contains_x); + TS_ASSERT(contains_x[norm_neg_ax]); + TS_ASSERT(norm_neg_ax.getAttribute(is_linear)); + TS_ASSERT(norm_neg_ax.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_ax.getNumChildren() == 2); + TS_ASSERT(norm_neg_ax[0] == x); + TS_ASSERT(norm_neg_ax[1] == mkNeg(a)); + + /* normalize 0 * x -> 0 */ + Node norm_zx = normalizePvMult(x, {zero, x}, contains_x); + TS_ASSERT(norm_zx == zero); + + /* normalize 1 * x -> x */ + Node norm_ox = normalizePvMult(x, {one, x}, contains_x); + TS_ASSERT(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); + TS_ASSERT(contains_x[norm_abcxd]); + TS_ASSERT(norm_abcxd.getAttribute(is_linear)); + TS_ASSERT(norm_abcxd.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_abcxd.getNumChildren() == 2); + TS_ASSERT(norm_abcxd[0] == x); + TS_ASSERT(norm_abcxd[1] == Rewriter::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); + TS_ASSERT(contains_x[norm_neg_abcxd]); + TS_ASSERT(norm_neg_abcxd.getAttribute(is_linear)); + TS_ASSERT(norm_neg_abcxd.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_abcxd.getNumChildren() == 2); + TS_ASSERT(norm_neg_abcxd[0] == x); + TS_ASSERT(norm_neg_abcxd[1] + == mkNeg(Rewriter::rewrite(mkMult({a, b, c, d})))); + + /* normalize b * (x * a) -> x * (b * a) */ + Node norm_bxa = normalizePvMult(x, {b, norm_ax}, contains_x); + TS_ASSERT(contains_x[norm_bxa]); + TS_ASSERT(norm_bxa.getAttribute(is_linear)); + TS_ASSERT(norm_bxa.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_bxa.getNumChildren() == 2); + TS_ASSERT(norm_bxa[0] == x); + TS_ASSERT(norm_bxa[1] == Rewriter::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); + TS_ASSERT(contains_x[norm_neg_bxa]); + TS_ASSERT(norm_neg_bxa.getAttribute(is_linear)); + TS_ASSERT(norm_neg_bxa.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_bxa.getNumChildren() == 2); + TS_ASSERT(norm_neg_bxa[0] == x); + TS_ASSERT(norm_neg_bxa[1] == mkNeg(Rewriter::rewrite(mkMult(b, a)))); +} + +void BvInstantiatorWhite::testNormalizePvPlus() +{ + Node one = mkOne(32); + Node x = mkVar(32); + Node neg_x = mkNeg(x); + Node a = mkVar(32); + Node b = mkVar(32); + Node c = mkVar(32); + Node d = mkVar(32); + BvLinearAttribute is_linear; + std::unordered_map contains_x; + + contains_x[x] = true; + contains_x[neg_x] = true; + + /* 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); + TS_ASSERT(norm_abx.isNull()); + + /* x + a -> x + a */ + Node norm_xa = normalizePvPlus(x, {x, a}, contains_x); + TS_ASSERT(contains_x[norm_xa]); + TS_ASSERT(norm_xa.getAttribute(is_linear)); + TS_ASSERT(norm_xa.getKind() == kind::BITVECTOR_PLUS); + TS_ASSERT(norm_xa.getNumChildren() == 2); + TS_ASSERT(norm_xa[0] == x); + TS_ASSERT(norm_xa[1] == a); + + /* a * x -> x * a */ + Node norm_ax = normalizePvPlus(x, {a, x}, contains_x); + TS_ASSERT(contains_x[norm_ax]); + TS_ASSERT(norm_ax.getAttribute(is_linear)); + TS_ASSERT(norm_ax.getKind() == kind::BITVECTOR_PLUS); + TS_ASSERT(norm_ax.getNumChildren() == 2); + TS_ASSERT(norm_ax[0] == x); + TS_ASSERT(norm_ax[1] == a); + + /* a + -x -> (x * -1) + a */ + Node norm_neg_ax = normalizePvPlus(x, {a, neg_x}, contains_x); + TS_ASSERT(contains_x[norm_neg_ax]); + TS_ASSERT(norm_neg_ax.getAttribute(is_linear)); + TS_ASSERT(norm_neg_ax.getKind() == kind::BITVECTOR_PLUS); + TS_ASSERT(norm_neg_ax.getNumChildren() == 2); + TS_ASSERT(norm_neg_ax[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_ax[0].getNumChildren() == 2); + TS_ASSERT(norm_neg_ax[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_neg_ax[0]]); + TS_ASSERT(norm_neg_ax[0][0] == x); + TS_ASSERT(norm_neg_ax[0][1] == Rewriter::rewrite(mkNeg(one))); + TS_ASSERT(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); + TS_ASSERT(contains_x[norm_xax]); + TS_ASSERT(norm_xax.getAttribute(is_linear)); + TS_ASSERT(norm_xax.getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_xax.getNumChildren() == 2); + TS_ASSERT(norm_xax[0] == x); + TS_ASSERT(norm_xax[1] == Rewriter::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); + TS_ASSERT(contains_x[norm_abcxd]); + TS_ASSERT(norm_abcxd.getAttribute(is_linear)); + TS_ASSERT(norm_abcxd.getKind() == kind::BITVECTOR_PLUS); + TS_ASSERT(norm_abcxd.getNumChildren() == 2); + TS_ASSERT(norm_abcxd[0] == x); + TS_ASSERT(norm_abcxd[1] == Rewriter::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); + TS_ASSERT(contains_x[norm_neg_abcxd]); + TS_ASSERT(norm_neg_abcxd.getAttribute(is_linear)); + TS_ASSERT(norm_neg_abcxd.getKind() == kind::BITVECTOR_PLUS); + TS_ASSERT(norm_neg_abcxd.getNumChildren() == 2); + TS_ASSERT(norm_neg_abcxd[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_abcxd[0].getNumChildren() == 2); + TS_ASSERT(norm_neg_abcxd[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_neg_abcxd[0]]); + TS_ASSERT(norm_neg_abcxd[0][0] == x); + TS_ASSERT(norm_neg_abcxd[0][1] == Rewriter::rewrite(mkNeg(one))); + TS_ASSERT(norm_neg_abcxd[1] == Rewriter::rewrite(mkPlus({a, b, c, d}))); + + /* b + (x + a) -> x + (b + a) */ + Node norm_bxa = normalizePvPlus(x, {b, norm_ax}, contains_x); + TS_ASSERT(contains_x[norm_bxa]); + TS_ASSERT(norm_bxa.getAttribute(is_linear)); + TS_ASSERT(norm_bxa.getKind() == kind::BITVECTOR_PLUS); + TS_ASSERT(norm_bxa.getNumChildren() == 2); + TS_ASSERT(norm_bxa[0] == x); + TS_ASSERT(norm_bxa[1] == Rewriter::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); + TS_ASSERT(contains_x[norm_neg_bxa]); + TS_ASSERT(norm_neg_bxa.getAttribute(is_linear)); + TS_ASSERT(norm_neg_bxa.getKind() == kind::BITVECTOR_PLUS); + TS_ASSERT(norm_neg_bxa.getNumChildren() == 2); + TS_ASSERT(norm_neg_abcxd[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_abcxd[0].getNumChildren() == 2); + TS_ASSERT(norm_neg_abcxd[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_neg_abcxd[0]]); + TS_ASSERT(norm_neg_abcxd[0][0] == x); + TS_ASSERT(norm_neg_abcxd[0][1] == Rewriter::rewrite(mkNeg(one))); + TS_ASSERT(norm_neg_bxa[1] == Rewriter::rewrite((mkPlus(b, mkNeg(a))))); + + /* -x + x + a -> a */ + Node norm_neg_xxa = normalizePvPlus(x, {neg_x, x, a}, contains_x); + TS_ASSERT(!contains_x[norm_neg_xxa]); + TS_ASSERT(norm_neg_xxa == a); +} + +void BvInstantiatorWhite::testNormalizePvEqual() +{ + Node x = mkVar(32); + Node neg_x = mkNeg(x); + Node a = mkVar(32); + Node b = mkVar(32); + Node c = mkVar(32); + Node d = mkVar(32); + Node zero = mkZero(32); + Node one = mkOne(32); + Node ntrue = mkTrue(); + BvLinearAttribute is_linear; + std::unordered_map contains_x; + + contains_x[x] = true; + contains_x[neg_x] = true; + + /* x = a -> null (nothing to normalize) */ + Node norm_xa = normalizePvEqual(x, {x, a}, contains_x); + TS_ASSERT(norm_xa.isNull()); + + /* x = x -> true */ + Node norm_xx = normalizePvEqual(x, {x, x}, contains_x); + TS_ASSERT(norm_xx == ntrue); + + /* x = -x -> x * 2 = 0 */ + Node norm_neg_xx = normalizePvEqual(x, {x, neg_x}, contains_x); + TS_ASSERT(norm_neg_xx.getKind() == kind::EQUAL); + TS_ASSERT(norm_neg_xx[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_xx[0].getNumChildren() == 2); + TS_ASSERT(norm_neg_xx[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_neg_xx[0]]); + TS_ASSERT(norm_neg_xx[0][0] == x); + TS_ASSERT(norm_neg_xx[0][1] == Rewriter::rewrite(mkConst(32, 2))); + TS_ASSERT(norm_neg_xx[1] == zero); + + /* a + x = x -> 0 = -a */ + Node norm_axx = normalizePvEqual( + x, {normalizePvPlus(x, {a, x}, contains_x), x}, contains_x); + TS_ASSERT(norm_axx.getKind() == kind::EQUAL); + TS_ASSERT(norm_axx[0] == zero); + TS_ASSERT(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); + TS_ASSERT(norm_neg_axx.getKind() == kind::EQUAL); + TS_ASSERT(norm_neg_axx[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_neg_axx[0].getNumChildren() == 2); + TS_ASSERT(norm_neg_axx[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_neg_axx[0]]); + TS_ASSERT(norm_neg_axx[0][0] == x); + TS_ASSERT(norm_neg_axx[0][1] == Rewriter::rewrite(mkNeg(mkConst(32, 2)))); + TS_ASSERT(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); + TS_ASSERT(norm_mult_axx.getKind() == kind::EQUAL); + TS_ASSERT(norm_mult_axx[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_mult_axx[0].getNumChildren() == 2); + TS_ASSERT(norm_mult_axx[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_mult_axx[0]]); + TS_ASSERT(norm_mult_axx[0][0] == x); + TS_ASSERT(norm_mult_axx[0][1] == Rewriter::rewrite(mkPlus(a, mkNeg(one)))); + TS_ASSERT(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); + TS_ASSERT(norm_axxb.getKind() == kind::EQUAL); + TS_ASSERT(norm_axxb[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_axxb[0].getNumChildren() == 2); + TS_ASSERT(norm_axxb[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_axxb[0]]); + TS_ASSERT(norm_axxb[0][0] == x); + TS_ASSERT(norm_axxb[0][1] == Rewriter::rewrite(mkPlus(a, mkNeg(one)))); + TS_ASSERT(norm_axxb[1] == b); + + /* a * x + c = x -> x * (a - 1) = -c */ + Node norm_axcx = normalizePvEqual( + x, + {normalizePvPlus( + x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x), + x}, + contains_x); + TS_ASSERT(norm_axcx.getKind() == kind::EQUAL); + TS_ASSERT(norm_axcx[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_axcx[0].getNumChildren() == 2); + TS_ASSERT(norm_axcx[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_axcx[0]]); + TS_ASSERT(norm_axcx[0][0] == x); + TS_ASSERT(norm_axcx[0][1] == Rewriter::rewrite(mkPlus(a, mkNeg(one)))); + TS_ASSERT(norm_axcx[1] == mkNeg(c)); + + /* a * x + c = x + b -> x * (a - 1) = b - c*/ + Node norm_axcxb = normalizePvEqual( + x, + {normalizePvPlus( + x, {normalizePvMult(x, {a, x}, contains_x), c}, contains_x), + normalizePvPlus(x, {b, x}, contains_x)}, + contains_x); + TS_ASSERT(norm_axcxb.getKind() == kind::EQUAL); + TS_ASSERT(norm_axcxb[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_axcxb[0].getNumChildren() == 2); + TS_ASSERT(norm_axcxb[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_axcxb[0]]); + TS_ASSERT(norm_axcxb[0][0] == x); + TS_ASSERT(norm_axcxb[0][1] == Rewriter::rewrite(mkPlus(a, mkNeg(one)))); + TS_ASSERT(norm_axcxb[1] == Rewriter::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); + TS_ASSERT(norm_axax.getKind() == kind::EQUAL); + TS_ASSERT(norm_axax[0].getKind() == kind::BITVECTOR_MULT); + TS_ASSERT(norm_axax[0].getNumChildren() == 2); + TS_ASSERT(norm_axax[0].getAttribute(is_linear)); + TS_ASSERT(contains_x[norm_axax[0]]); + TS_ASSERT(norm_axax[0][0] == x); + TS_ASSERT(norm_axax[0][1] == Rewriter::rewrite(mkPlus(one, mkNeg(a)))); + TS_ASSERT(norm_axax[1] == a); +} -- 2.30.2