namespace theory {
namespace quantifiers {
+struct BvLinearAttributeId {};
+using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>;
+
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;
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);
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)
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<TNode> trace_visit;
+ std::unordered_set<TNode, TNodeHashFunction> 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<Node>& children,
+ std::unordered_map<TNode, bool, TNodeHashFunction>& 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<TNode, bool, TNodeHashFunction>& 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<Node>& children,
+ std::unordered_map<TNode, bool, TNodeHashFunction>& 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<Node> 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<Node>& children,
+ std::unordered_map<TNode, bool, TNodeHashFunction>& 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<Node> 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(
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
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+#include <iostream>
+#include <vector>
+
+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<Node>& children);
+ Node mkPlus(TNode a, TNode b);
+ Node mkPlus(const std::vector<Node>& 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<Node>& 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<Node>& 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<TNode, bool, TNodeHashFunction> 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<TNode, bool, TNodeHashFunction> 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<TNode, bool, TNodeHashFunction> 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);
+}
projects / cvc5.git / commitdiff