From: Aina Niemetz Date: Wed, 11 Apr 2018 01:52:54 +0000 (-0700) Subject: Refactored BVGauss preprocessing pass. (#1766) X-Git-Tag: cvc5-1.0.0~5159 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b5b926f28b66c3812d77fd234e93b9eee03f71f;p=cvc5.git Refactored BVGauss preprocessing pass. (#1766) --- diff --git a/src/Makefile.am b/src/Makefile.am index b33c0586f..67e105089 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -64,6 +64,8 @@ libcvc4_la_SOURCES = \ decision/justification_heuristic.h \ preprocessing/passes/int_to_bv.cpp \ preprocessing/passes/int_to_bv.h \ + preprocessing/passes/bv_gauss.cpp \ + preprocessing/passes/bv_gauss.h \ preprocessing/preprocessing_pass.cpp \ preprocessing/preprocessing_pass.h \ preprocessing/preprocessing_pass_context.cpp \ @@ -320,8 +322,6 @@ libcvc4_la_SOURCES = \ theory/bv/bv_subtheory_inequality.h \ theory/bv/bv_to_bool.cpp \ theory/bv/bv_to_bool.h \ - theory/bv/bvgauss.cpp \ - theory/bv/bvgauss.h \ theory/bv/bvintropow2.cpp \ theory/bv/bvintropow2.h \ theory/bv/slicer.cpp \ diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp new file mode 100644 index 000000000..d1f7d09ee --- /dev/null +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -0,0 +1,823 @@ +/********************* */ +/*! \file bv_gauss.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Gaussian Elimination preprocessing pass. + ** + ** Simplify a given equation system modulo a (prime) number via Gaussian + ** Elimination if possible. + **/ + +#include "preprocessing/passes/bv_gauss.h" + +#include "expr/node.h" +#include "theory/rewriter.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "util/bitvector.h" + +#include +#include + + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +namespace { + +/** + * Represents the result of Gaussian Elimination where the solution + * of the given equation system is + * + * INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b, + * where ci, b and p are + * - bit-vector constants + * - extracts or zero extensions on bit-vector constants + * - of arbitrary nesting level + * and p is co-prime to all bit-vector constants for which + * a multiplicative inverse has to be computed. + * + * UNIQUE ... determined for all unknowns, e.g., x = 4 + * + * PARTIAL ... e.g., x = 4 - 2z + * + * NONE ... no solution + * + * Given a matrix A representing an equation system, the resulting + * matrix B after applying GE represents, e.g.: + * + * B = 1 0 0 2 <- UNIQUE + * 0 1 0 3 <- + * 0 0 1 1 <- + * + * B = 1 0 2 4 <- PARTIAL + * 0 1 3 2 <- + * 0 0 1 1 + * + * B = 1 0 0 1 NONE + * 0 1 1 2 + * 0 0 0 2 <- + */ +enum class Result +{ + INVALID, + UNIQUE, + PARTIAL, + NONE +}; + +bool is_bv_const(Node n) +{ + if (n.isConst()) { return true; } + return Rewriter::rewrite(n).getKind() == kind::CONST_BITVECTOR; +} + +Node get_bv_const(Node n) +{ + Assert(is_bv_const(n)); + return Rewriter::rewrite(n); +} + +Integer get_bv_const_value(Node n) +{ + Assert(is_bv_const(n)); + return get_bv_const(n).getConst().getValue(); +} + +/** + * Determines if an overflow may occur in given 'expr'. + * + * Returns 0 if an overflow may occur, and the minimum required + * bit-width such that no overflow occurs, otherwise. + * + * Note that it would suffice for this function to be Boolean. + * However, it is handy to determine the minimum required bit-width for + * debugging purposes. + * + * Note: getMinBwExpr assumes that 'expr' is rewritten. + * + * If not, all operators that are removed via rewriting (e.g., ror, rol, ...) + * will be handled via the default case, which is not incorrect but also not + * necessarily the minimum. + */ +unsigned getMinBwExpr(Node expr) +{ + std::vector visit; + /* Maps visited nodes to the determined minimum bit-width required. */ + std::unordered_map visited; + std::unordered_map::iterator it; + + visit.push_back(expr); + while (!visit.empty()) + { + Node n = visit.back(); + visit.pop_back(); + it = visited.find(n); + if (it == visited.end()) + { + if (is_bv_const(n)) + { + /* Rewrite const expr, overflows in consts are irrelevant. */ + visited[n] = get_bv_const(n).getConst().getValue().length(); + } + else + { + visited[n] = 0; + visit.push_back(n); + for (const Node &nn : n) { visit.push_back(nn); } + } + } + else if (it->second == 0) + { + Kind k = n.getKind(); + Assert(k != kind::CONST_BITVECTOR); + Assert(!is_bv_const(n)); + switch (k) + { + case kind::BITVECTOR_EXTRACT: + { + const unsigned size = bv::utils::getSize(n); + const unsigned low = bv::utils::getExtractLow(n); + const unsigned child_min_width = visited[n[0]]; + visited[n] = std::min( + size, child_min_width >= low ? child_min_width - low : 0u); + Assert(visited[n] <= visited[n[0]]); + break; + } + + case kind::BITVECTOR_ZERO_EXTEND: + { + visited[n] = visited[n[0]]; + break; + } + + case kind::BITVECTOR_MULT: + { + Integer maxval = Integer(1); + for (const Node& nn : n) + { + if (is_bv_const(nn)) + { + maxval *= get_bv_const_value(nn); + } + else + { + maxval *= BitVector::mkOnes(visited[nn]).getValue(); + } + } + unsigned w = maxval.length(); + if (w > bv::utils::getSize(n)) { return 0; } /* overflow */ + visited[n] = w; + break; + } + + case kind::BITVECTOR_CONCAT: + { + unsigned i, wnz, nc; + for (i = 0, wnz = 0, nc = n.getNumChildren() - 1; i < nc; ++i) + { + unsigned wni = bv::utils::getSize(n[i]); + if (n[i] != bv::utils::mkZero(wni)) { break; } + /* sum of all bit-widths of leading zero concats */ + wnz += wni; + } + /* Do not consider leading zero concats, i.e., + * min bw of current concat is determined as + * min bw of first non-zero term + * plus actual bw of all subsequent terms */ + visited[n] = bv::utils::getSize(n) + visited[n[i]] + - bv::utils::getSize(n[i]) - wnz; + break; + } + + case kind::BITVECTOR_UREM_TOTAL: + case kind::BITVECTOR_LSHR: + case kind::BITVECTOR_ASHR: + { + visited[n] = visited[n[0]]; + break; + } + + case kind::BITVECTOR_OR: + case kind::BITVECTOR_NOR: + case kind::BITVECTOR_XOR: + case kind::BITVECTOR_XNOR: + case kind::BITVECTOR_AND: + case kind::BITVECTOR_NAND: + { + unsigned wmax = 0; + for (const Node &nn : n) + { + if (visited[nn] > wmax) + { + wmax = visited[nn]; + } + } + visited[n] = wmax; + break; + } + + case kind::BITVECTOR_PLUS: + { + Integer maxval = Integer(0); + for (const Node& nn : n) + { + if (is_bv_const(nn)) + { + maxval += get_bv_const_value(nn); + } + else + { + maxval += BitVector::mkOnes(visited[nn]).getValue(); + } + } + unsigned w = maxval.length(); + if (w > bv::utils::getSize(n)) { return 0; } /* overflow */ + visited[n] = w; + break; + } + + default: + { + /* BITVECTOR_UDIV_TOTAL (since x / 0 = -1) + * BITVECTOR_NOT + * BITVECTOR_NEG + * BITVECTOR_SHL */ + visited[n] = bv::utils::getSize(n); + } + } + } + } + Assert(visited.find(expr) != visited.end()); + return visited[expr]; +} + +/** + * Apply Gaussian Elimination modulo a (prime) number. + * The given equation system is represented as a matrix of Integers. + * + * Note that given 'prime' does not have to be prime but can be any + * arbitrary number. However, if 'prime' is indeed prime, GE is guaranteed + * to succeed, which is not the case, otherwise. + * + * Returns INVALID if GE can not be applied, UNIQUE and PARTIAL if GE was + * successful, and NONE, otherwise. + * + * Vectors 'rhs' and 'lhs' represent the right hand side and left hand side + * of the given matrix, respectively. The resulting matrix (in row echelon + * form) is stored in 'rhs' and 'lhs', i.e., the given matrix is overwritten + * with the resulting matrix. + */ +Result gaussElim( + Integer prime, + std::vector& rhs, + std::vector>& lhs) +{ + Assert(prime > 0); + Assert(lhs.size()); + Assert(lhs.size() == rhs.size()); + Assert(lhs.size() <= lhs[0].size()); + + /* special case: zero ring */ + if (prime == 1) + { + rhs = std::vector(rhs.size(), Integer(0)); + lhs = std::vector>( + lhs.size(), std::vector(lhs[0].size(), Integer(0))); + return Result::UNIQUE; + } + + size_t nrows = lhs.size(); + size_t ncols = lhs[0].size(); + + #ifdef CVC4_ASSERTIONS + for (size_t i = 1; i < nrows; ++i) Assert(lhs[i].size() == ncols); + #endif + /* (1) if element in pivot column is non-zero and != 1, divide row elements + * by element in pivot column modulo prime, i.e., multiply row with + * multiplicative inverse of element in pivot column modulo prime + * + * (2) subtract pivot row from all rows below pivot row + * + * (3) subtract (multiple of) current row from all rows above s.t. all + * elements in current pivot column above current row become equal to one + * + * Note: we do not normalize the given matrix to values modulo prime + * beforehand but on-the-fly. */ + + /* pivot = lhs[pcol][pcol] */ + for (size_t pcol = 0, prow = 0; pcol < ncols && prow < nrows; ++pcol, ++prow) + { + /* lhs[j][pcol]: element in pivot column */ + for (size_t j = prow; j < nrows; ++j) + { +#ifdef CVC4_ASSERTIONS + for (size_t k = 0; k < pcol; ++k) { Assert(lhs[j][k] == 0); } +#endif + /* normalize element in pivot column to modulo prime */ + lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime); + /* exchange rows if pivot elem is 0 */ + if (j == prow) + { + while (lhs[j][pcol] == 0) + { + for (size_t k = prow + 1; k < nrows; ++k) + { + lhs[k][pcol] = lhs[k][pcol].euclidianDivideRemainder(prime); + if (lhs[k][pcol] != 0) + { + std::swap(rhs[j], rhs[k]); + std::swap(lhs[j], lhs[k]); + break; + } + } + if (pcol >= ncols - 1) break; + if (lhs[j][pcol] == 0) + { + pcol += 1; + if (lhs[j][pcol] != 0) + lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime); + } + } + } + + if (lhs[j][pcol] != 0) + { + /* (1) */ + if (lhs[j][pcol] != 1) + { + Integer inv = lhs[j][pcol].modInverse(prime); + if (inv == -1) + { + return Result::INVALID; /* not coprime */ + } + for (size_t k = pcol; k < ncols; ++k) + { + lhs[j][k] = lhs[j][k].modMultiply(inv, prime); + if (j <= prow) continue; /* pivot */ + lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k], prime); + } + rhs[j] = rhs[j].modMultiply(inv, prime); + if (j > prow) { rhs[j] = rhs[j].modAdd(-rhs[prow], prime); } + } + /* (2) */ + else if (j != prow) + { + for (size_t k = pcol; k < ncols; ++k) + { + lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k], prime); + } + rhs[j] = rhs[j].modAdd(-rhs[prow], prime); + } + } + } + /* (3) */ + for (size_t j = 0; j < prow; ++j) + { + Integer mul = lhs[j][pcol]; + if (mul != 0) + { + for (size_t k = pcol; k < ncols; ++k) + { + lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k] * mul, prime); + } + rhs[j] = rhs[j].modAdd(-rhs[prow] * mul, prime); + } + } + } + + bool ispart = false; + for (size_t i = 0; i < nrows; ++i) + { + size_t pcol = i; + while (pcol < ncols && lhs[i][pcol] == 0) ++pcol; + if (pcol >= ncols) + { + rhs[i] = rhs[i].euclidianDivideRemainder(prime); + if (rhs[i] != 0) + { + /* no solution */ + return Result::NONE; + } + continue; + } + for (size_t j = i; j < ncols; ++j) + { + if (lhs[i][j] >= prime || lhs[i][j] <= -prime) + { + lhs[i][j] = lhs[i][j].euclidianDivideRemainder(prime); + } + if (j > pcol && lhs[i][j] != 0) + { + ispart = true; + } + } + } + + if (ispart) { return Result::PARTIAL; } + + return Result::UNIQUE; +} + +/** + * Apply Gaussian Elimination on a set of equations modulo some (prime) + * number given as bit-vector equations. + * + * IMPORTANT: Applying GE modulo some number (rather than modulo 2^bw) + * on a set of bit-vector equations is only sound if this set of equations + * has a solution that does not produce overflows. Consequently, we only + * apply GE if the given bit-width guarantees that no overflows can occur + * in the given set of equations. + * + * Note that the given set of equations does not have to be modulo a prime + * but can be modulo any arbitrary number. However, if it is indeed modulo + * prime, GE is guaranteed to succeed, which is not the case, otherwise. + * + * Returns INVALID if GE can not be applied, UNIQUE and PARTIAL if GE was + * successful, and NONE, otherwise. + * + * The resulting constraints are stored in 'res' as a mapping of unknown + * to result (modulo prime). These mapped results are added as constraints + * of the form 'unknown = mapped result' in applyInternal. + */ +Result gaussElimRewriteForUrem( + const std::vector& equations, + std::unordered_map& res) +{ + Assert(res.empty()); + + Node prime; + Integer iprime; + std::unordered_map, NodeHashFunction> vars; + size_t neqs = equations.size(); + std::vector rhs; + std::vector> lhs = + std::vector>(neqs, std::vector()); + + res = std::unordered_map(); + + for (size_t i = 0; i < neqs; ++i) + { + Node eq = equations[i]; + Assert(eq.getKind() == kind::EQUAL); + Node urem, eqrhs; + + if (eq[0].getKind() == kind::BITVECTOR_UREM) + { + urem = eq[0]; + Assert(is_bv_const(eq[1])); + eqrhs = eq[1]; + } + else + { + Assert(eq[1].getKind() == kind::BITVECTOR_UREM); + urem = eq[1]; + Assert(is_bv_const(eq[0])); + eqrhs = eq[0]; + } + if (getMinBwExpr(Rewriter::rewrite(urem[0])) == 0) + { + Trace("bv-gauss-elim") + << "Minimum required bit-width exceeds given bit-width, " + "will not apply Gaussian Elimination." + << std::endl; + return Result::INVALID; + } + rhs.push_back(get_bv_const_value(eqrhs)); + + Assert(is_bv_const(urem[1])); + Assert(i == 0 || get_bv_const_value(urem[1]) == iprime); + if (i == 0) + { + prime = urem[1]; + iprime = get_bv_const_value(prime); + } + + std::unordered_map tmp; + std::vector stack; + stack.push_back(urem[0]); + while (!stack.empty()) + { + Node n = stack.back(); + stack.pop_back(); + + /* Subtract from rhs if const */ + if (is_bv_const(n)) + { + Integer val = get_bv_const_value(n); + if (val > 0) rhs.back() -= val; + continue; + } + + /* Split into matrix columns */ + Kind k = n.getKind(); + if (k == kind::BITVECTOR_PLUS) + { + for (const Node& nn : n) { stack.push_back(nn); } + } + else if (k == kind::BITVECTOR_MULT) + { + Node n0, n1; + /* Flatten mult expression. */ + n = RewriteRule::run(n); + /* Split operands into consts and non-consts */ + NodeBuilder<> nb_consts(NodeManager::currentNM(), k); + NodeBuilder<> nb_nonconsts(NodeManager::currentNM(), k); + for (const Node& nn : n) + { + Node nnrw = Rewriter::rewrite(nn); + if (is_bv_const(nnrw)) + { + nb_consts << nnrw; + } + else + { + nb_nonconsts << nnrw; + } + } + Assert(nb_nonconsts.getNumChildren() > 0); + /* n0 is const */ + unsigned nc = nb_consts.getNumChildren(); + if (nc > 1) + { + n0 = Rewriter::rewrite(nb_consts.constructNode()); + } + else if (nc == 1) + { + n0 = nb_consts[0]; + } + else + { + n0 = bv::utils::mkOne(bv::utils::getSize(n)); + } + /* n1 is a mult with non-const operands */ + if (nb_nonconsts.getNumChildren() > 1) + { + n1 = Rewriter::rewrite(nb_nonconsts.constructNode()); + } + else + { + n1 = nb_nonconsts[0]; + } + Assert(is_bv_const(n0)); + Assert(!is_bv_const(n1)); + tmp[n1] += get_bv_const_value(n0); + } + else + { + tmp[n] += Integer(1); + } + } + + /* Note: "var" is not necessarily a VARIABLE but can be an arbitrary expr */ + + for (const auto& p : tmp) + { + Node var = p.first; + Integer val = p.second; + if (i > 0 && vars.find(var) == vars.end()) + { + /* Add column and fill column elements of rows above with 0. */ + vars[var].insert(vars[var].end(), i, Integer(0)); + } + vars[var].push_back(val); + } + + for (const auto& p : vars) + { + if (tmp.find(p.first) == tmp.end()) + { + vars[p.first].push_back(Integer(0)); + } + } + } + + size_t nvars = vars.size(); + Assert(nvars); + size_t nrows = vars.begin()->second.size(); +#ifdef CVC4_ASSERTIONS + for (const auto& p : vars) { Assert(p.second.size() == nrows); } +#endif + + if (nrows < 1) + { + return Result::INVALID; + } + + for (size_t i = 0; i < nrows; ++i) + { + for (const auto& p : vars) + { + lhs[i].push_back(p.second[i]); + } + } + +#ifdef CVC4_ASSERTIONS + for (const auto& row : lhs) { Assert(row.size() == nvars); } + Assert(lhs.size() == rhs.size()); +#endif + + if (lhs.size() > lhs[0].size()) + { + return Result::INVALID; + } + + Trace("bv-gauss-elim") << "Applying Gaussian Elimination..." << std::endl; + Result ret = gaussElim(iprime, rhs, lhs); + + if (ret != Result::NONE && ret != Result::INVALID) + { + std::vector vvars; + for (const auto& p : vars) { vvars.push_back(p.first); } + Assert(nvars == vvars.size()); + Assert(nrows == lhs.size()); + Assert(nrows == rhs.size()); + NodeManager *nm = NodeManager::currentNM(); + if (ret == Result::UNIQUE) + { + for (size_t i = 0; i < nvars; ++i) + { + res[vvars[i]] = nm->mkConst( + BitVector(bv::utils::getSize(vvars[i]), rhs[i])); + } + } + else + { + Assert(ret == Result::PARTIAL); + + for (size_t pcol = 0, prow = 0; pcol < nvars && prow < nrows; + ++pcol, ++prow) + { + Assert(lhs[prow][pcol] == 0 || lhs[prow][pcol] == 1); + while (pcol < nvars && lhs[prow][pcol] == 0) pcol += 1; + if (pcol >= nvars) + { + Assert(rhs[prow] == 0); + break; + } + if (lhs[prow][pcol] == 0) + { + Assert(rhs[prow] == 0); + continue; + } + Assert(lhs[prow][pcol] == 1); + std::vector stack; + for (size_t i = pcol + 1; i < nvars; ++i) + { + if (lhs[prow][i] == 0) continue; + /* Normalize (no negative numbers, hence no subtraction) + * e.g., x = 4 - 2y --> x = 4 + 9y (modulo 11) */ + Integer m = iprime - lhs[prow][i]; + Node bv = bv::utils::mkConst(bv::utils::getSize(vvars[i]), m); + Node mult = nm->mkNode(kind::BITVECTOR_MULT, vvars[i], bv); + stack.push_back(mult); + } + + if (stack.empty()) + { + res[vvars[pcol]] = nm->mkConst( + BitVector(bv::utils::getSize(vvars[pcol]), rhs[prow])); + } + else + { + Node tmp = stack.size() == 1 + ? stack[0] + : nm->mkNode(kind::BITVECTOR_PLUS, stack); + + if (rhs[prow] != 0) + { + tmp = nm->mkNode(kind::BITVECTOR_PLUS, + bv::utils::mkConst( + bv::utils::getSize(vvars[pcol]), rhs[prow]), + tmp); + } + Assert(!is_bv_const(tmp)); + res[vvars[pcol]] = nm->mkNode(kind::BITVECTOR_UREM, tmp, prime); + } + } + } + } + return ret; +} + +} // namespace + + + +BVGauss::BVGauss(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "bv-gauss") +{ +} + +PreprocessingPassResult BVGauss::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + std::vector assertions(assertionsToPreprocess->ref()); + std::unordered_map, NodeHashFunction> equations; + + while (!assertions.empty()) + { + Node a = assertions.back(); + assertions.pop_back(); + CVC4::Kind k = a.getKind(); + + if (k == kind::AND) + { + for (const Node& aa : a) + { + assertions.push_back(aa); + } + } + else if (k == kind::EQUAL) + { + Node urem; + + if (is_bv_const(a[1]) && a[0].getKind() == kind::BITVECTOR_UREM) + { + urem = a[0]; + } + else if (is_bv_const(a[0]) && a[1].getKind() == kind::BITVECTOR_UREM) + { + urem = a[1]; + } + else + { + continue; + } + + if (urem[0].getKind() == kind::BITVECTOR_PLUS && is_bv_const(urem[1])) + { + equations[urem[1]].push_back(a); + } + } + } + + std::unordered_map subst; + std::vector& atpp = assertionsToPreprocess->ref(); + + for (const auto& eq : equations) + { + if (eq.second.size() <= 1) { continue; } + + std::unordered_map res; + Result ret = gaussElimRewriteForUrem(eq.second, res); + Trace("bv-gauss-elim") << "result: " + << (ret == Result::INVALID + ? "INVALID" + : (ret == Result::UNIQUE + ? "UNIQUE" + : (ret == Result::PARTIAL + ? "PARTIAL" + : "NONE"))) + << std::endl; + if (ret != Result::INVALID) + { + NodeManager *nm = NodeManager::currentNM(); + if (ret == Result::NONE) + { + atpp.clear(); + atpp.push_back(nm->mkConst(false)); + } + else + { + for (const Node& e : eq.second) + { + subst[e] = nm->mkConst(true); + } + /* add resulting constraints */ + for (const auto& p : res) + { + Node a = nm->mkNode(kind::EQUAL, p.first, p.second); + Trace("bv-gauss-elim") << "added assertion: " << a << std::endl; + atpp.push_back(a); + } + } + } + } + + if (!subst.empty()) + { + /* delete (= substitute with true) obsolete assertions */ + for (auto& a : atpp) + { + a = a.substitute(subst.begin(), subst.end()); + } + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h new file mode 100644 index 000000000..a902f391c --- /dev/null +++ b/src/preprocessing/passes/bv_gauss.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file bv_gauss.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** 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 Gaussian Elimination preprocessing pass. + ** + ** Simplify a given equation system modulo a (prime) number via Gaussian + ** Elimination if possible. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#define __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class BVGauss : public PreprocessingPass +{ + public: + BVGauss(PreprocessingPassContext* preprocContext); + + protected: + /** + * Apply Gaussian Elimination on (possibly multiple) set(s) of equations + * modulo some (prime) number given as bit-vector equations. + * + * Note that these sets of equations do not have to be modulo some prime + * but can be modulo any arbitrary number. However, GE is guaranteed to + * succeed modulo a prime number, which is not necessarily the case if a + * given set of equations is modulo a non-prime number. + */ + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 029fb84c9..ea51df8c9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -69,6 +69,7 @@ #include "options/theory_options.h" #include "options/uf_options.h" #include "preprocessing/passes/int_to_bv.h" +#include "preprocessing/passes/bv_gauss.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -91,7 +92,6 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/pseudoboolean_proc.h" #include "theory/booleans/circuit_propagator.h" -#include "theory/bv/bvgauss.h" #include "theory/bv/bvintropow2.h" #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" @@ -2551,7 +2551,9 @@ void SmtEnginePrivate::finishInit() { // TODO: register passes here (this will likely change when we add support for // actually assembling preprocessing pipelines). std::unique_ptr intToBV(new IntToBV(d_preprocessingPassContext.get())); + std::unique_ptr bvGauss(new BVGauss(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); + d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) @@ -3986,10 +3988,10 @@ void SmtEnginePrivate::processAssertions() { return; } - if(options::bvGaussElim()) + if (options::bvGaussElim()) { TimerStat::CodeTimer gaussElimTimer(d_smt.d_stats->d_gaussElimTime); - theory::bv::BVGaussElim::gaussElimRewrite(d_assertions.ref()); + d_preprocessingPassRegistry.getPass("bv-gauss")->apply(&d_assertions); } if (d_assertionsProcessed && options::incrementalSolving()) { @@ -4089,7 +4091,8 @@ void SmtEnginePrivate::processAssertions() { */ } - if (options::solveIntAsBV() > 0) { + if (options::solveIntAsBV() > 0) + { d_preprocessingPassRegistry.getPass("int-to-bv")->apply(&d_assertions); } diff --git a/src/theory/bv/bvgauss.cpp b/src/theory/bv/bvgauss.cpp deleted file mode 100644 index e36ef3aef..000000000 --- a/src/theory/bv/bvgauss.cpp +++ /dev/null @@ -1,715 +0,0 @@ -/********************* */ -/*! \file bvgauss.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 Gaussian Elimination preprocessing pass. - ** - ** Simplify a given equation system modulo a (prime) number via Gaussian - ** Elimination if possible. - **/ - -#include "theory/bv/bvgauss.h" - -#include - -#include "theory/rewriter.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/bv/theory_bv_rewrite_rules_normalization.h" - -using namespace CVC4; - -namespace CVC4 { -namespace theory { -namespace bv { - -static bool is_bv_const(Node n) -{ - if (n.isConst()) { return true; } - return Rewriter::rewrite(n).getKind() == kind::CONST_BITVECTOR; -} - -static Node get_bv_const(Node n) -{ - Assert(is_bv_const(n)); - return Rewriter::rewrite(n); -} - -static Integer get_bv_const_value(Node n) -{ - Assert(is_bv_const(n)); - return get_bv_const(n).getConst().getValue(); -} - -/* Note: getMinBwExpr assumes that 'expr' is rewritten. - * - * If not, all operators that are removed via rewriting (e.g., ror, rol, ...) - * will be handled via the default case, which is not incorrect but also not - * necessarily the minimum. */ -unsigned BVGaussElim::getMinBwExpr(Node expr) -{ - std::vector visit; - /* Maps visited nodes to the determined minimum bit-width required. */ - std::unordered_map visited; - std::unordered_map::iterator it; - - visit.push_back(expr); - while (!visit.empty()) - { - Node n = visit.back(); - visit.pop_back(); - it = visited.find(n); - if (it == visited.end()) - { - if (is_bv_const(n)) - { - /* Rewrite const expr, overflows in consts are irrelevant. */ - visited[n] = get_bv_const(n).getConst().getValue().length(); - } - else - { - visited[n] = 0; - visit.push_back(n); - for (const Node &nn : n) { visit.push_back(nn); } - } - } - else if (it->second == 0) - { - Kind k = n.getKind(); - Assert(k != kind::CONST_BITVECTOR); - Assert(!is_bv_const(n)); - switch (k) - { - case kind::BITVECTOR_EXTRACT: - { - const unsigned size = utils::getSize(n); - const unsigned low = utils::getExtractLow(n); - const unsigned child_min_width = visited[n[0]]; - visited[n] = std::min( - size, child_min_width >= low ? child_min_width - low : 0u); - Assert(visited[n] <= visited[n[0]]); - break; - } - - case kind::BITVECTOR_ZERO_EXTEND: - { - visited[n] = visited[n[0]]; - break; - } - - case kind::BITVECTOR_MULT: - { - Integer maxval = Integer(1); - for (const Node& nn : n) - { - if (is_bv_const(nn)) - { - maxval *= get_bv_const_value(nn); - } - else - { - maxval *= BitVector::mkOnes(visited[nn]).getValue(); - } - } - unsigned w = maxval.length(); - if (w > utils::getSize(n)) { return 0; } /* overflow */ - visited[n] = w; - break; - } - - case kind::BITVECTOR_CONCAT: - { - unsigned i, wnz, nc; - for (i = 0, wnz = 0, nc = n.getNumChildren() - 1; i < nc; ++i) - { - unsigned wni = utils::getSize(n[i]); - if (n[i] != utils::mkZero(wni)) { break; } - /* sum of all bit-widths of leading zero concats */ - wnz += wni; - } - /* Do not consider leading zero concats, i.e., - * min bw of current concat is determined as - * min bw of first non-zero term - * plus actual bw of all subsequent terms */ - visited[n] = utils::getSize(n) - + visited[n[i]] - utils::getSize(n[i]) - - wnz; - break; - } - - case kind::BITVECTOR_UREM_TOTAL: - case kind::BITVECTOR_LSHR: - case kind::BITVECTOR_ASHR: - { - visited[n] = visited[n[0]]; - break; - } - - case kind::BITVECTOR_OR: - case kind::BITVECTOR_NOR: - case kind::BITVECTOR_XOR: - case kind::BITVECTOR_XNOR: - case kind::BITVECTOR_AND: - case kind::BITVECTOR_NAND: - { - unsigned wmax = 0; - for (const Node &nn : n) - { - if (visited[nn] > wmax) - { - wmax = visited[nn]; - } - } - visited[n] = wmax; - break; - } - - case kind::BITVECTOR_PLUS: - { - Integer maxval = Integer(0); - for (const Node& nn : n) - { - if (is_bv_const(nn)) - { - maxval += get_bv_const_value(nn); - } - else - { - maxval += BitVector::mkOnes(visited[nn]).getValue(); - } - } - unsigned w = maxval.length(); - if (w > utils::getSize(n)) { return 0; } /* overflow */ - visited[n] = w; - break; - } - - default: - { - /* BITVECTOR_UDIV_TOTAL (since x / 0 = -1) - * BITVECTOR_NOT - * BITVECTOR_NEG - * BITVECTOR_SHL */ - visited[n] = utils::getSize(n); - } - } - } - } - Assert(visited.find(expr) != visited.end()); - return visited[expr]; -} - -BVGaussElim::Result BVGaussElim::gaussElim( - Integer prime, - std::vector& rhs, - std::vector>& lhs) -{ - Assert(prime > 0); - Assert(lhs.size()); - Assert(lhs.size() == rhs.size()); - Assert(lhs.size() <= lhs[0].size()); - - /* special case: zero ring */ - if (prime == 1) - { - rhs = std::vector(rhs.size(), Integer(0)); - lhs = std::vector>( - lhs.size(), std::vector(lhs[0].size(), Integer(0))); - return BVGaussElim::Result::UNIQUE; - } - - size_t nrows = lhs.size(); - size_t ncols = lhs[0].size(); - - #ifdef CVC4_ASSERTIONS - for (size_t i = 1; i < nrows; ++i) Assert(lhs[i].size() == ncols); - #endif - /* (1) if element in pivot column is non-zero and != 1, divide row elements - * by element in pivot column modulo prime, i.e., multiply row with - * multiplicative inverse of element in pivot column modulo prime - * - * (2) subtract pivot row from all rows below pivot row - * - * (3) subtract (multiple of) current row from all rows above s.t. all - * elements in current pivot column above current row become equal to one - * - * Note: we do not normalize the given matrix to values modulo prime - * beforehand but on-the-fly. */ - - /* pivot = lhs[pcol][pcol] */ - for (size_t pcol = 0, prow = 0; pcol < ncols && prow < nrows; ++pcol, ++prow) - { - /* lhs[j][pcol]: element in pivot column */ - for (size_t j = prow; j < nrows; ++j) - { -#ifdef CVC4_ASSERTIONS - for (size_t k = 0; k < pcol; ++k) { Assert(lhs[j][k] == 0); } -#endif - /* normalize element in pivot column to modulo prime */ - lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime); - /* exchange rows if pivot elem is 0 */ - if (j == prow) - { - while (lhs[j][pcol] == 0) - { - for (size_t k = prow + 1; k < nrows; ++k) - { - lhs[k][pcol] = lhs[k][pcol].euclidianDivideRemainder(prime); - if (lhs[k][pcol] != 0) - { - std::swap(rhs[j], rhs[k]); - std::swap(lhs[j], lhs[k]); - break; - } - } - if (pcol >= ncols - 1) break; - if (lhs[j][pcol] == 0) - { - pcol += 1; - if (lhs[j][pcol] != 0) - lhs[j][pcol] = lhs[j][pcol].euclidianDivideRemainder(prime); - } - } - } - - if (lhs[j][pcol] != 0) - { - /* (1) */ - if (lhs[j][pcol] != 1) - { - Integer inv = lhs[j][pcol].modInverse(prime); - if (inv == -1) - { - return BVGaussElim::Result::INVALID; /* not coprime */ - } - for (size_t k = pcol; k < ncols; ++k) - { - lhs[j][k] = lhs[j][k].modMultiply(inv, prime); - if (j <= prow) continue; /* pivot */ - lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k], prime); - } - rhs[j] = rhs[j].modMultiply(inv, prime); - if (j > prow) { rhs[j] = rhs[j].modAdd(-rhs[prow], prime); } - } - /* (2) */ - else if (j != prow) - { - for (size_t k = pcol; k < ncols; ++k) - { - lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k], prime); - } - rhs[j] = rhs[j].modAdd(-rhs[prow], prime); - } - } - } - /* (3) */ - for (size_t j = 0; j < prow; ++j) - { - Integer mul = lhs[j][pcol]; - if (mul != 0) - { - for (size_t k = pcol; k < ncols; ++k) - { - lhs[j][k] = lhs[j][k].modAdd(-lhs[prow][k] * mul, prime); - } - rhs[j] = rhs[j].modAdd(-rhs[prow] * mul, prime); - } - } - } - - bool ispart = false; - for (size_t i = 0; i < nrows; ++i) - { - size_t pcol = i; - while (pcol < ncols && lhs[i][pcol] == 0) ++pcol; - if (pcol >= ncols) - { - rhs[i] = rhs[i].euclidianDivideRemainder(prime); - if (rhs[i] != 0) - { - /* no solution */ - return BVGaussElim::Result::NONE; - } - continue; - } - for (size_t j = i; j < ncols; ++j) - { - if (lhs[i][j] >= prime || lhs[i][j] <= -prime) - { - lhs[i][j] = lhs[i][j].euclidianDivideRemainder(prime); - } - if (j > pcol && lhs[i][j] != 0) - { - ispart = true; - } - } - } - - if (ispart) { return BVGaussElim::Result::PARTIAL; } - - return BVGaussElim::Result::UNIQUE; -} - -BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( - const std::vector& equations, - std::unordered_map& res) -{ - Assert(res.empty()); - - Node prime; - Integer iprime; - std::unordered_map, NodeHashFunction> vars; - size_t neqs = equations.size(); - std::vector rhs; - std::vector> lhs = - std::vector>(neqs, std::vector()); - - res = std::unordered_map(); - - for (size_t i = 0; i < neqs; ++i) - { - Node eq = equations[i]; - Assert(eq.getKind() == kind::EQUAL); - Node urem, eqrhs; - - if (eq[0].getKind() == kind::BITVECTOR_UREM) - { - urem = eq[0]; - Assert(is_bv_const(eq[1])); - eqrhs = eq[1]; - } - else - { - Assert(eq[1].getKind() == kind::BITVECTOR_UREM); - urem = eq[1]; - Assert(is_bv_const(eq[0])); - eqrhs = eq[0]; - } - if (getMinBwExpr(Rewriter::rewrite(urem[0])) == 0) - { - Trace("bv-gauss-elim") - << "Minimum required bit-width exceeds given bit-width, " - "will not apply Gaussian Elimination." - << std::endl; - return BVGaussElim::Result::INVALID; - } - rhs.push_back(get_bv_const_value(eqrhs)); - - Assert(is_bv_const(urem[1])); - Assert(i == 0 || get_bv_const_value(urem[1]) == iprime); - if (i == 0) - { - prime = urem[1]; - iprime = get_bv_const_value(prime); - } - - std::unordered_map tmp; - std::vector stack; - stack.push_back(urem[0]); - while (!stack.empty()) - { - Node n = stack.back(); - stack.pop_back(); - - /* Subtract from rhs if const */ - if (is_bv_const(n)) - { - Integer val = get_bv_const_value(n); - if (val > 0) rhs.back() -= val; - continue; - } - - /* Split into matrix columns */ - Kind k = n.getKind(); - if (k == kind::BITVECTOR_PLUS) - { - for (const Node& nn : n) { stack.push_back(nn); } - } - else if (k == kind::BITVECTOR_MULT) - { - Node n0, n1; - /* Flatten mult expression. */ - n = RewriteRule::run(n); - /* Split operands into consts and non-consts */ - NodeBuilder<> nb_consts(NodeManager::currentNM(), k); - NodeBuilder<> nb_nonconsts(NodeManager::currentNM(), k); - for (const Node& nn : n) - { - Node nnrw = Rewriter::rewrite(nn); - if (is_bv_const(nnrw)) - { - nb_consts << nnrw; - } - else - { - nb_nonconsts << nnrw; - } - } - Assert(nb_nonconsts.getNumChildren() > 0); - /* n0 is const */ - unsigned nc = nb_consts.getNumChildren(); - if (nc > 1) - { - n0 = Rewriter::rewrite(nb_consts.constructNode()); - } - else if (nc == 1) - { - n0 = nb_consts[0]; - } - else - { - n0 = utils::mkOne(utils::getSize(n)); - } - /* n1 is a mult with non-const operands */ - if (nb_nonconsts.getNumChildren() > 1) - { - n1 = Rewriter::rewrite(nb_nonconsts.constructNode()); - } - else - { - n1 = nb_nonconsts[0]; - } - Assert(is_bv_const(n0)); - Assert(!is_bv_const(n1)); - tmp[n1] += get_bv_const_value(n0); - } - else - { - tmp[n] += Integer(1); - } - } - - /* Note: "var" is not necessarily a VARIABLE but can be an arbitrary expr */ - - for (const auto& p : tmp) - { - Node var = p.first; - Integer val = p.second; - if (i > 0 && vars.find(var) == vars.end()) - { - /* Add column and fill column elements of rows above with 0. */ - vars[var].insert(vars[var].end(), i, Integer(0)); - } - vars[var].push_back(val); - } - - for (const auto& p : vars) - { - if (tmp.find(p.first) == tmp.end()) - { - vars[p.first].push_back(Integer(0)); - } - } - } - - size_t nvars = vars.size(); - Assert(nvars); - size_t nrows = vars.begin()->second.size(); -#ifdef CVC4_ASSERTIONS - for (const auto& p : vars) { Assert(p.second.size() == nrows); } -#endif - - if (nrows < 1) - { - return BVGaussElim::Result::INVALID; - } - - for (size_t i = 0; i < nrows; ++i) - { - for (const auto& p : vars) - { - lhs[i].push_back(p.second[i]); - } - } - -#ifdef CVC4_ASSERTIONS - for (const auto& row : lhs) { Assert(row.size() == nvars); } - Assert(lhs.size() == rhs.size()); -#endif - - if (lhs.size() > lhs[0].size()) - { - return BVGaussElim::Result::INVALID; - } - - Trace("bv-gauss-elim") << "Applying Gaussian Elimination..." << std::endl; - Result ret = gaussElim(iprime, rhs, lhs); - - if (ret != BVGaussElim::Result::NONE && ret != BVGaussElim::Result::INVALID) - { - std::vector vvars; - for (const auto& p : vars) { vvars.push_back(p.first); } - Assert(nvars == vvars.size()); - Assert(nrows == lhs.size()); - Assert(nrows == rhs.size()); - NodeManager *nm = NodeManager::currentNM(); - if (ret == BVGaussElim::Result::UNIQUE) - { - for (size_t i = 0; i < nvars; ++i) - { - res[vvars[i]] = nm->mkConst( - BitVector(utils::getSize(vvars[i]), rhs[i])); - } - } - else - { - Assert(ret == BVGaussElim::Result::PARTIAL); - - for (size_t pcol = 0, prow = 0; pcol < nvars && prow < nrows; - ++pcol, ++prow) - { - Assert(lhs[prow][pcol] == 0 || lhs[prow][pcol] == 1); - while (pcol < nvars && lhs[prow][pcol] == 0) pcol += 1; - if (pcol >= nvars) - { - Assert(rhs[prow] == 0); - break; - } - if (lhs[prow][pcol] == 0) - { - Assert(rhs[prow] == 0); - continue; - } - Assert(lhs[prow][pcol] == 1); - std::vector stack; - for (size_t i = pcol + 1; i < nvars; ++i) - { - if (lhs[prow][i] == 0) continue; - /* Normalize (no negative numbers, hence no subtraction) - * e.g., x = 4 - 2y --> x = 4 + 9y (modulo 11) */ - Integer m = iprime - lhs[prow][i]; - Node bv = utils::mkConst(utils::getSize(vvars[i]), m); - Node mult = nm->mkNode(kind::BITVECTOR_MULT, vvars[i], bv); - stack.push_back(mult); - } - - if (stack.empty()) - { - res[vvars[pcol]] = nm->mkConst( - BitVector(utils::getSize(vvars[pcol]), rhs[prow])); - } - else - { - Node tmp = stack.size() == 1 - ? stack[0] - : nm->mkNode(kind::BITVECTOR_PLUS, stack); - - if (rhs[prow] != 0) - { - tmp = nm->mkNode(kind::BITVECTOR_PLUS, - utils::mkConst( - utils::getSize(vvars[pcol]), rhs[prow]), - tmp); - } - Assert(!is_bv_const(tmp)); - res[vvars[pcol]] = nm->mkNode(kind::BITVECTOR_UREM, tmp, prime); - } - } - } - } - return ret; -} - -void BVGaussElim::gaussElimRewrite(std::vector &assertionsToPreprocess) -{ - std::vector assertions(assertionsToPreprocess); - std::unordered_map, NodeHashFunction> equations; - - while (!assertions.empty()) - { - Node a = assertions.back(); - assertions.pop_back(); - CVC4::Kind k = a.getKind(); - - if (k == kind::AND) - { - for (const Node& aa : a) - { - assertions.push_back(aa); - } - } - else if (k == kind::EQUAL) - { - Node urem; - - if (is_bv_const(a[1]) && a[0].getKind() == kind::BITVECTOR_UREM) - { - urem = a[0]; - } - else if (is_bv_const(a[0]) && a[1].getKind() == kind::BITVECTOR_UREM) - { - urem = a[1]; - } - else - { - continue; - } - - if (urem[0].getKind() == kind::BITVECTOR_PLUS && is_bv_const(urem[1])) - { - equations[urem[1]].push_back(a); - } - } - } - - std::unordered_map subst; - - for (const auto& eq : equations) - { - if (eq.second.size() <= 1) { continue; } - - std::unordered_map res; - BVGaussElim::Result ret = gaussElimRewriteForUrem(eq.second, res); - Trace("bv-gauss-elim") << "result: " - << (ret == BVGaussElim::Result::INVALID - ? "INVALID" - : (ret == BVGaussElim::Result::UNIQUE - ? "UNIQUE" - : (ret == BVGaussElim::Result::PARTIAL - ? "PARTIAL" - : "NONE"))) - << std::endl; - if (ret != BVGaussElim::Result::INVALID) - { - NodeManager *nm = NodeManager::currentNM(); - if (ret == BVGaussElim::Result::NONE) - { - assertionsToPreprocess.clear(); - assertionsToPreprocess.push_back(nm->mkConst(false)); - } - else - { - for (const Node& e : eq.second) - { - subst[e] = nm->mkConst(true); - } - /* add resulting constraints */ - for (const auto& p : res) - { - Node a = nm->mkNode(kind::EQUAL, p.first, p.second); - Trace("bv-gauss-elim") << "added assertion: " << a << std::endl; - assertionsToPreprocess.push_back(a); - } - } - } - } - - if (!subst.empty()) - { - /* delete (= substitute with true) obsolete assertions */ - for (auto& a : assertionsToPreprocess) - { - a = a.substitute(subst.begin(), subst.end()); - } - } -} - -} // namespace bv -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/bv/bvgauss.h b/src/theory/bv/bvgauss.h deleted file mode 100644 index 6cd80729d..000000000 --- a/src/theory/bv/bvgauss.h +++ /dev/null @@ -1,151 +0,0 @@ -/********************* */ -/*! \file bvgauss.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** 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 Gaussian Elimination preprocessing pass. - ** - ** Simplify a given equation system modulo a (prime) number via Gaussian - ** Elimination if possible. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__BV__BV_GAUSS_ELIM_H -#define __CVC4__THEORY__BV__BV_GAUSS_ELIM_H - -#include "expr/node.h" -#include "util/bitvector.h" - -#include -#include - -namespace CVC4 { -namespace theory { -namespace bv { - -class BVGaussElim -{ - public: - /** - * Apply Gaussian Elimination on (possibly multiple) set(s) of equations - * modulo some (prime) number given as bit-vector equations. - * - * Note that these sets of equations do not have to be modulo some prime - * but can be modulo any arbitrary number. However, GE is guaranteed to - * succeed modulo a prime number, which is not necessarily the case if a - * given set of equations is modulo a non-prime number. - */ - static void gaussElimRewrite(std::vector& assertionsToPreprocess); - - private: - /** - * Represents the result of Gaussian Elimination where the solution - * of the given equation system is - * - * INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b, - * where ci, b and p are - * - bit-vector constants - * - extracts or zero extensions on bit-vector constants - * - of arbitrary nesting level - * and p is co-prime to all bit-vector constants for which - * a multiplicative inverse has to be computed. - * - * UNIQUE ... determined for all unknowns, e.g., x = 4 - * - * PARTIAL ... e.g., x = 4 - 2z - * - * NONE ... no solution - * - * Given a matrix A representing an equation system, the resulting - * matrix B after applying GE represents, e.g.: - * - * B = 1 0 0 2 <- UNIQUE - * 0 1 0 3 <- - * 0 0 1 1 <- - * - * B = 1 0 2 4 <- PARTIAL - * 0 1 3 2 <- - * 0 0 1 1 - * - * B = 1 0 0 1 NONE - * 0 1 1 2 - * 0 0 0 2 <- - */ - enum class Result - { - INVALID, - UNIQUE, - PARTIAL, - NONE - }; - - /** - * Determines if an overflow may occur in given 'expr'. - * - * Returns 0 if an overflow may occur, and the minimum required - * bit-width such that no overflow occurs, otherwise. - * - * Note that it would suffice for this function to be Boolean. - * However, it is handy to determine the minimum required bit-width for - * debugging purposes. - */ - static unsigned getMinBwExpr(Node expr); - - /** - * Apply Gaussian Elimination on a set of equations modulo some (prime) - * number given as bit-vector equations. - * - * IMPORTANT: Applying GE modulo some number (rather than modulo 2^bw) - * on a set of bit-vector equations is only sound if this set of equations - * has a solution that does not produce overflows. Consequently, we only - * apply GE if the given bit-width guarantees that no overflows can occur - * in the given set of equations. - * - * Note that the given set of equations does not have to be modulo a prime - * but can be modulo any arbitrary number. However, if it is indeed modulo - * prime, GE is guaranteed to succeed, which is not the case, otherwise. - * - * Returns INVALID if GE can not be applied, UNIQUE and PARTIAL if GE was - * successful, and NONE, otherwise. - * - * The resulting constraints are stored in 'res' as a mapping of unknown - * to result (modulo prime). These mapped results are added as constraints - * of the form 'unknown = mapped result' in gaussElimRewrite. - */ - static Result gaussElimRewriteForUrem( - const std::vector& equations, - std::unordered_map& res); - - /** - * Apply Gaussian Elimination modulo a (prime) number. - * The given equation system is represented as a matrix of Integers. - * - * Note that given 'prime' does not have to be prime but can be any - * arbitrary number. However, if 'prime' is indeed prime, GE is guaranteed - * to succeed, which is not the case, otherwise. - * - * Returns INVALID if GE can not be applied, UNIQUE and PARTIAL if GE was - * successful, and NONE, otherwise. - * - * Vectors 'rhs' and 'lhs' represent the right hand side and left hand side - * of the given matrix, respectively. The resulting matrix (in row echelon - * form) is stored in 'rhs' and 'lhs', i.e., the given matrix is overwritten - * with the resulting matrix. - */ - static Result gaussElim(Integer prime, - std::vector& rhs, - std::vector>& lhs); -}; - -} // namespace bv -} // namespace theory -} // namespace CVC4 - -#endif diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index b445583ac..cc9f6fb1b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -9,7 +9,6 @@ UNIT_TESTS += \ theory/logic_info_white \ theory/theory_arith_white \ theory/theory_black \ - theory/theory_bv_bvgauss_white \ theory/theory_bv_white \ theory/theory_engine_white \ theory/theory_quantifiers_bv_instantiator_white \ @@ -31,6 +30,7 @@ UNIT_TESTS += \ expr/type_node_white \ parser/parser_black \ parser/parser_builder_black \ + preprocessing/pass_bv_gauss_white \ prop/cnf_stream_white \ context/context_black \ context/context_white \ diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h new file mode 100644 index 000000000..e39c7d6c3 --- /dev/null +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -0,0 +1,3036 @@ +/********************* */ +/*! \file theory_bv_bvgauss_white.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** 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 Gaussian Elimination preprocessing pass. + ** + ** Unit tests for Gaussian Elimination preprocessing pass. + **/ + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/passes/bv_gauss.cpp" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" + +#include +#include +#include + +using namespace CVC4; +using namespace CVC4::preprocessing; +using namespace CVC4::theory; +using namespace CVC4::smt; + +static void print_matrix_dbg(std::vector &rhs, + std::vector> &lhs) +{ + for (size_t m = 0, nrows = lhs.size(), ncols = lhs[0].size(); m < nrows; ++m) + { + for (size_t n = 0; n < ncols; ++n) + { + std::cout << " " << lhs[m][n]; + } + std::cout << " " << rhs[m]; + std::cout << std::endl; + } +} + +static void testGaussElimX(Integer prime, + std::vector rhs, + std::vector> lhs, + passes::Result expected, + std::vector *rrhs = nullptr, + std::vector> *rlhs = nullptr) +{ + size_t nrows = lhs.size(); + size_t ncols = lhs[0].size(); + passes::Result ret; + std::vector resrhs = std::vector(rhs); + std::vector> reslhs = + std::vector>(lhs); + + std::cout << "Input: " << std::endl; + print_matrix_dbg(rhs, lhs); + + ret = passes::gaussElim(prime, resrhs, reslhs); + + std::cout << "passes::Result: " + << (ret == passes::Result::INVALID + ? "INVALID" + : (ret == passes::Result::UNIQUE + ? "UNIQUE" + : (ret == passes::Result::PARTIAL ? "PARTIAL" + : "NONE"))) + << std::endl; + print_matrix_dbg(resrhs, reslhs); + + TS_ASSERT_EQUALS(expected, ret); + + if (expected == passes::Result::UNIQUE) + { + /* map result value to column index + * e.g.: + * 1 0 0 2 -> res = { 2, 0, 3} + * 0 0 1 3 */ + std::vector res = std::vector(ncols, Integer(0)); + for (size_t i = 0; i < nrows; ++i) + for (size_t j = 0; j < ncols; ++j) + { + if (reslhs[i][j] == 1) + res[j] = resrhs[i]; + else + TS_ASSERT(reslhs[i][j] == 0); + } + + for (size_t i = 0; i < nrows; ++i) + { + Integer tmp = Integer(0); + for (size_t j = 0; j < ncols; ++j) + tmp = tmp.modAdd(lhs[i][j].modMultiply(res[j], prime), prime); + TS_ASSERT(tmp == rhs[i].euclidianDivideRemainder(prime)); + } + } + if (rrhs != nullptr && rlhs != nullptr) + { + for (size_t i = 0; i < nrows; ++i) + { + for (size_t j = 0; j < ncols; ++j) + { + TS_ASSERT(reslhs[i][j] == (*rlhs)[i][j]); + } + TS_ASSERT(resrhs[i] == (*rrhs)[i]); + } + } +} + +template +static void testGaussElimT(Integer prime, + std::vector rhs, + std::vector> lhs) +{ + TS_ASSERT_THROWS(passes::gaussElim(prime, rhs, lhs), T); +} + +class TheoryBVGaussWhite : public CxxTest::TestSuite +{ + ExprManager *d_em; + NodeManager *d_nm; + SmtEngine *d_smt; + SmtScope *d_scope; + Node d_p; + Node d_x; + Node d_y; + Node d_z; + Node d_zero; + Node d_one; + Node d_two; + Node d_three; + Node d_four; + Node d_five; + Node d_six; + Node d_seven; + Node d_eight; + Node d_nine; + Node d_ten; + Node d_twelve; + Node d_eighteen; + Node d_twentyfour; + Node d_thirty; + Node d_one32; + Node d_two32; + Node d_three32; + Node d_four32; + Node d_five32; + Node d_six32; + Node d_seven32; + Node d_eight32; + Node d_nine32; + Node d_ten32; + Node d_x_mul_one; + Node d_x_mul_two; + Node d_x_mul_four; + Node d_y_mul_one; + Node d_y_mul_three; + Node d_y_mul_four; + Node d_y_mul_five; + Node d_y_mul_seven; + Node d_z_mul_one; + Node d_z_mul_three; + Node d_z_mul_five; + Node d_z_mul_twelve; + Node d_z_mul_six; + Node d_z_mul_nine; + + public: + TheoryBVGaussWhite() {} + + void setUp() + { + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_scope = new SmtScope(d_smt); + + d_zero = bv::utils::mkZero(16); + + d_p = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 11u))); + d_x = bv::utils::mkConcat( + d_zero, d_nm->mkVar("x", d_nm->mkBitVectorType(16))); + d_y = bv::utils::mkConcat( + d_zero, d_nm->mkVar("y", d_nm->mkBitVectorType(16))); + d_z = bv::utils::mkConcat( + d_zero, d_nm->mkVar("z", d_nm->mkBitVectorType(16))); + + d_one = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 1u))); + d_two = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 2u))); + d_three = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 3u))); + d_four = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 4u))); + d_five = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 5u))); + d_six = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 6u))); + d_seven = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 7u))); + d_eight = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 8u))); + d_nine = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 9u))); + d_ten = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 10u))); + d_twelve = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 12u))); + d_eighteen = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 18u))); + d_twentyfour = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 24u))); + d_thirty = bv::utils::mkConcat( + d_zero, d_nm->mkConst(BitVector(16, 30u))); + + d_one32 = d_nm->mkConst(BitVector(32, 1u)); + d_two32 = d_nm->mkConst(BitVector(32, 2u)); + d_three32 = d_nm->mkConst(BitVector(32, 3u)); + d_four32 = d_nm->mkConst(BitVector(32, 4u)); + d_five32 = d_nm->mkConst(BitVector(32, 5u)); + d_six32 = d_nm->mkConst(BitVector(32, 6u)); + d_seven32 = d_nm->mkConst(BitVector(32, 7u)); + d_eight32 = d_nm->mkConst(BitVector(32, 8u)); + d_nine32 = d_nm->mkConst(BitVector(32, 9u)); + d_ten32 = d_nm->mkConst(BitVector(32, 10u)); + + d_x_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_one); + d_x_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_two); + d_x_mul_four = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four); + d_y_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three); + d_y_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_one); + d_y_mul_four = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_four); + d_y_mul_five = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_five); + d_y_mul_seven = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven); + d_z_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_one); + d_z_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_three); + d_z_mul_five = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_five); + d_z_mul_six = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_six); + d_z_mul_twelve = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_twelve); + d_z_mul_nine = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_nine); + } + + void tearDown() + { + (void)d_scope; + d_p = Node::null(); + d_x = Node::null(); + d_y = Node::null(); + d_z = Node::null(); + d_zero = Node::null(); + d_one = Node::null(); + d_two = Node::null(); + d_three = Node::null(); + d_four = Node::null(); + d_five = Node::null(); + d_six = Node::null(); + d_seven = Node::null(); + d_eight = Node::null(); + d_nine = Node::null(); + d_ten = Node::null(); + d_twelve = Node::null(); + d_eighteen = Node::null(); + d_twentyfour = Node::null(); + d_thirty = Node::null(); + d_one32 = Node::null(); + d_two32 = Node::null(); + d_three32 = Node::null(); + d_four32 = Node::null(); + d_five32 = Node::null(); + d_six32 = Node::null(); + d_seven32 = Node::null(); + d_eight32 = Node::null(); + d_nine32 = Node::null(); + d_ten32 = Node::null(); + d_x_mul_one = Node::null(); + d_x_mul_two = Node::null(); + d_x_mul_four = Node::null(); + d_y_mul_one = Node::null(); + d_y_mul_four = Node::null(); + d_y_mul_seven = Node::null(); + d_y_mul_five = Node::null(); + d_y_mul_three = Node::null(); + d_z_mul_one = Node::null(); + d_z_mul_three = Node::null(); + d_z_mul_five = Node::null(); + d_z_mul_six = Node::null(); + d_z_mul_twelve = Node::null(); + d_z_mul_nine = Node::null(); + delete d_scope; + delete d_smt; + delete d_em; + } + + void testGaussElimMod() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs modulo { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 } + * --^-- ^ + * 1 1 1 5 + * 2 3 5 8 + * 4 0 5 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(2)}; + lhs = {{Integer(1), Integer(1), Integer(1)}, + {Integer(2), Integer(3), Integer(5)}, + {Integer(4), Integer(0), Integer(5)}}; + std::cout << "matrix 0, modulo 0" << std::endl; // throws + testGaussElimT(Integer(0), rhs, lhs); + std::cout << "matrix 0, modulo 1" << std::endl; + testGaussElimX(Integer(1), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 0, modulo 2" << std::endl; + testGaussElimX(Integer(2), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 0, modulo 3" << std::endl; + testGaussElimX(Integer(3), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 0, modulo 4" << std::endl; // no inverse + testGaussElimX(Integer(4), rhs, lhs, passes::Result::INVALID); + std::cout << "matrix 0, modulo 5" << std::endl; + testGaussElimX(Integer(5), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 0, modulo 6" << std::endl; // no inverse + testGaussElimX(Integer(6), rhs, lhs, passes::Result::INVALID); + std::cout << "matrix 0, modulo 7" << std::endl; + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 0, modulo 8" << std::endl; // no inverse + testGaussElimX(Integer(8), rhs, lhs, passes::Result::INVALID); + std::cout << "matrix 0, modulo 9" << std::endl; + testGaussElimX(Integer(9), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 0, modulo 10" << std::endl; // no inverse + testGaussElimX(Integer(10), rhs, lhs, passes::Result::INVALID); + std::cout << "matrix 0, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + } + + void testGaussElimUniqueDone() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 17 + * --^--- ^ --^-- ^ + * 1 0 0 4 --> 1 0 0 4 + * 0 1 0 15 0 1 0 15 + * 0 0 1 3 0 0 1 3 + * ------------------------------------------------------------------- */ + rhs = {Integer(4), Integer(15), Integer(3)}; + lhs = {{Integer(1), Integer(0), Integer(0)}, + {Integer(0), Integer(1), Integer(0)}, + {Integer(0), Integer(0), Integer(1)}}; + std::cout << "matrix 1, modulo 17" << std::endl; + testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE); + } + + void testGaussElimUnique() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs modulo { 11,17,59 } + * --^--- ^ + * 2 4 6 18 + * 4 5 6 24 + * 3 1 -2 4 + * ------------------------------------------------------------------- */ + rhs = {Integer(18), Integer(24), Integer(4)}; + lhs = {{Integer(2), Integer(4), Integer(6)}, + {Integer(4), Integer(5), Integer(6)}, + {Integer(3), Integer(1), Integer(-2)}}; + std::cout << "matrix 2, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 2, modulo 17" << std::endl; + testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE); + std::cout << "matrix 2, modulo 59" << std::endl; + testGaussElimX(Integer(59), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * -----^----- ^ ---^--- ^ + * 1 1 2 0 1 --> 1 0 0 0 1 + * 2 -1 0 1 -2 0 1 0 0 2 + * 1 -1 -1 -2 4 0 0 1 0 -1 + * 2 -1 2 -1 0 0 0 0 1 -2 + * ------------------------------------------------------------------- */ + rhs = {Integer(1), Integer(-2), Integer(4), Integer(0)}; + lhs = {{Integer(1), Integer(1), Integer(2), Integer(0)}, + {Integer(2), Integer(-1), Integer(0), Integer(1)}, + {Integer(1), Integer(-1), Integer(-1), Integer(-2)}, + {Integer(2), Integer(-1), Integer(2), Integer(-1)}}; + std::cout << "matrix 3, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + } + + void testGaussElimUniqueZero1() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 0 4 5 2 --> 1 0 0 4 + * 1 1 1 5 0 1 0 3 + * 3 2 5 8 0 0 1 9 + * ------------------------------------------------------------------- */ + rhs = {Integer(2), Integer(5), Integer(8)}; + lhs = {{Integer(0), Integer(4), Integer(5)}, + {Integer(1), Integer(1), Integer(1)}, + {Integer(3), Integer(2), Integer(5)}}; + std::cout << "matrix 4, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 1 1 5 --> 1 0 0 4 + * 0 4 5 2 0 1 0 3 + * 3 2 5 8 0 0 1 9 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(2), Integer(8)}; + lhs = {{Integer(1), Integer(1), Integer(1)}, + {Integer(0), Integer(4), Integer(5)}, + {Integer(3), Integer(2), Integer(5)}}; + std::cout << "matrix 5, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 1 1 5 --> 1 0 0 4 + * 3 2 5 8 0 1 0 9 + * 0 4 5 2 0 0 1 3 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(2)}; + lhs = {{Integer(1), Integer(1), Integer(1)}, + {Integer(3), Integer(2), Integer(5)}, + {Integer(0), Integer(4), Integer(5)}}; + std::cout << "matrix 6, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + } + + void testGaussElimUniqueZero2() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 0 0 5 2 1 0 0 10 + * 1 1 1 5 --> 0 1 0 10 + * 3 2 5 8 0 0 1 7 + * ------------------------------------------------------------------- */ + rhs = {Integer(2), Integer(5), Integer(8)}; + lhs = {{Integer(0), Integer(0), Integer(5)}, + {Integer(1), Integer(1), Integer(1)}, + {Integer(3), Integer(2), Integer(5)}}; + std::cout << "matrix 7, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 1 1 5 --> 1 0 0 10 + * 0 0 5 2 0 1 0 10 + * 3 2 5 8 0 0 1 7 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(2), Integer(8)}; + lhs = {{Integer(1), Integer(1), Integer(1)}, + {Integer(0), Integer(0), Integer(5)}, + {Integer(3), Integer(2), Integer(5)}}; + std::cout << "matrix 8, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 1 1 5 --> 1 0 0 10 + * 3 2 5 8 0 1 0 10 + * 0 0 5 2 0 0 1 7 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(2)}; + lhs = {{Integer(1), Integer(1), Integer(1)}, + {Integer(3), Integer(2), Integer(5)}, + {Integer(0), Integer(0), Integer(5)}}; + std::cout << "matrix 9, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + } + + void testGaussElimUniqueZero3() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 7 + * --^-- ^ --^-- ^ + * 2 0 6 4 1 0 0 3 + * 0 0 0 0 --> 0 0 0 0 + * 4 0 6 3 0 0 1 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(4), Integer(0), Integer(3)}; + lhs = {{Integer(2), Integer(0), Integer(6)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(4), Integer(0), Integer(6)}}; + std::cout << "matrix 10, modulo 7" << std::endl; + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 7 + * --^-- ^ --^-- ^ + * 2 6 0 4 1 0 0 3 + * 0 0 0 0 --> 0 0 0 0 + * 4 6 0 3 0 0 1 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(4), Integer(0), Integer(3)}; + lhs = {{Integer(2), Integer(6), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(4), Integer(6), Integer(0)}}; + std::cout << "matrix 11, modulo 7" << std::endl; + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); + } + + void testGaussElimUniqueZero4() + { + std::vector rhs, resrhs; + std::vector> lhs, reslhs; + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 0 1 1 5 + * 0 0 0 0 + * 0 0 5 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(0), Integer(2)}; + lhs = {{Integer(0), Integer(1), Integer(1)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(0), Integer(0), Integer(5)}}; + std::cout << "matrix 12, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 0 1 1 5 + * 0 3 5 8 + * 0 0 0 0 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(0)}; + lhs = {{Integer(0), Integer(1), Integer(1)}, + {Integer(0), Integer(3), Integer(5)}, + {Integer(0), Integer(0), Integer(0)}}; + std::cout << "matrix 13, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 0 0 0 0 + * 0 3 5 8 + * 0 0 5 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(0), Integer(8), Integer(2)}; + lhs = {{Integer(0), Integer(0), Integer(0)}, + {Integer(0), Integer(3), Integer(5)}, + {Integer(0), Integer(0), Integer(5)}}; + std::cout << "matrix 14, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 0 1 5 + * 0 0 0 0 + * 4 0 5 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(0), Integer(2)}; + lhs = {{Integer(1), Integer(0), Integer(1)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(4), Integer(0), Integer(5)}}; + std::cout << "matrix 15, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 0 1 5 + * 2 0 5 8 + * 0 0 0 0 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(0)}; + lhs = {{Integer(1), Integer(0), Integer(1)}, + {Integer(2), Integer(0), Integer(5)}, + {Integer(0), Integer(0), Integer(0)}}; + std::cout << "matrix 16, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 0 0 0 0 + * 2 0 5 8 + * 4 0 5 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(0), Integer(8), Integer(2)}; + lhs = {{Integer(0), Integer(0), Integer(0)}, + {Integer(2), Integer(0), Integer(5)}, + {Integer(4), Integer(0), Integer(5)}}; + std::cout << "matrix 17, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 1 0 5 + * 0 0 0 0 + * 4 0 0 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(0), Integer(2)}; + lhs = {{Integer(1), Integer(1), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(4), Integer(0), Integer(0)}}; + std::cout << "matrix 18, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 1 0 5 + * 2 3 0 8 + * 0 0 0 0 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(0)}; + lhs = {{Integer(1), Integer(1), Integer(0)}, + {Integer(2), Integer(3), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}}; + std::cout << "matrix 18, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 0 0 0 0 + * 2 3 0 8 + * 4 0 0 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(0), Integer(8), Integer(2)}; + lhs = {{Integer(0), Integer(0), Integer(0)}, + {Integer(2), Integer(3), Integer(0)}, + {Integer(4), Integer(0), Integer(0)}}; + std::cout << "matrix 19, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 2 + * ----^--- ^ + * 2 4 6 18 0 0 0 0 + * 4 5 6 24 = 0 1 0 0 + * 2 7 12 30 0 1 0 0 + * ------------------------------------------------------------------- */ + rhs = {Integer(18), Integer(24), Integer(30)}; + lhs = {{Integer(2), Integer(4), Integer(6)}, + {Integer(4), Integer(5), Integer(6)}, + {Integer(2), Integer(7), Integer(12)}}; + std::cout << "matrix 20, modulo 2" << std::endl; + resrhs = {Integer(0), Integer(0), Integer(0)}; + reslhs = {{Integer(0), Integer(1), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(2), rhs, lhs, passes::Result::UNIQUE, &resrhs, &reslhs); + } + + void testGaussElimUniquePartial() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 7 + * --^-- ^ --^-- ^ + * 2 0 6 4 1 0 0 3 + * 4 0 6 3 0 0 1 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(4), Integer(3)}; + lhs = {{Integer(2), Integer(0), Integer(6)}, + {Integer(4), Integer(0), Integer(6)}}; + std::cout << "matrix 21, modulo 7" << std::endl; + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 7 + * --^-- ^ --^-- ^ + * 2 6 0 4 1 0 0 3 + * 4 6 0 3 0 1 0 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(4), Integer(3)}; + lhs = {{Integer(2), Integer(6), Integer(0)}, + {Integer(4), Integer(6), Integer(0)}}; + std::cout << "matrix 22, modulo 7" << std::endl; + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); + } + + void testGaussElimNone() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs modulo 9 + * --^--- ^ + * 2 4 6 18 --> not coprime (no inverse) + * 4 5 6 24 + * 3 1 -2 4 + * ------------------------------------------------------------------- */ + rhs = {Integer(18), Integer(24), Integer(4)}; + lhs = {{Integer(2), Integer(4), Integer(6)}, + {Integer(4), Integer(5), Integer(6)}, + {Integer(3), Integer(1), Integer(-2)}}; + std::cout << "matrix 23, modulo 9" << std::endl; + testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 59 + * ----^--- ^ + * 1 -2 -6 12 --> no solution + * 2 4 12 -17 + * 1 -4 -12 22 + * ------------------------------------------------------------------- */ + rhs = {Integer(12), Integer(-17), Integer(22)}; + lhs = {{Integer(1), Integer(-2), Integer(-6)}, + {Integer(2), Integer(4), Integer(12)}, + {Integer(1), Integer(-4), Integer(-12)}}; + std::cout << "matrix 24, modulo 59" << std::endl; + testGaussElimX(Integer(59), rhs, lhs, passes::Result::NONE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 9 + * ----^--- ^ + * 2 4 6 18 --> not coprime (no inverse) + * 4 5 6 24 + * 2 7 12 30 + * ------------------------------------------------------------------- */ + rhs = {Integer(18), Integer(24), Integer(30)}; + lhs = {{Integer(2), Integer(4), Integer(6)}, + {Integer(4), Integer(5), Integer(6)}, + {Integer(2), Integer(7), Integer(12)}}; + std::cout << "matrix 25, modulo 9" << std::endl; + testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID); + } + + void testGaussElimNoneZero() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 0 1 1 5 + * 0 3 5 8 + * 0 0 5 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(2)}; + lhs = {{Integer(0), Integer(1), Integer(1)}, + {Integer(0), Integer(3), Integer(5)}, + {Integer(0), Integer(0), Integer(5)}}; + std::cout << "matrix 26, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 0 1 5 + * 2 0 5 8 + * 4 0 5 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(2)}; + lhs = {{Integer(1), Integer(0), Integer(1)}, + {Integer(2), Integer(0), Integer(5)}, + {Integer(4), Integer(0), Integer(5)}}; + std::cout << "matrix 27, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE); + + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 1 0 5 + * 2 3 0 8 + * 4 0 0 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8), Integer(2)}; + lhs = {{Integer(1), Integer(1), Integer(0)}, + {Integer(2), Integer(3), Integer(0)}, + {Integer(4), Integer(0), Integer(0)}}; + std::cout << "matrix 28, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE); + } + + void testGaussElimPartial1() + { + std::vector rhs, resrhs; + std::vector> lhs, reslhs; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * ------------------------------------------------------------------- */ + rhs = {Integer(7), Integer(9)}; + lhs = {{Integer(1), Integer(0), Integer(9)}, + {Integer(0), Integer(1), Integer(3)}}; + std::cout << "matrix 29, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 3 0 7 --> 1 3 0 7 + * 0 0 1 9 0 0 1 9 + * ------------------------------------------------------------------- */ + rhs = {Integer(7), Integer(9)}; + lhs = {{Integer(1), Integer(3), Integer(0)}, + {Integer(0), Integer(0), Integer(1)}}; + std::cout << "matrix 30, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 1 1 5 --> 1 0 9 7 + * 2 3 5 8 0 1 3 9 + * ------------------------------------------------------------------- */ + rhs = {Integer(5), Integer(8)}; + lhs = {{Integer(1), Integer(1), Integer(1)}, + {Integer(2), Integer(3), Integer(5)}}; + std::cout << "matrix 31, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); + + /* ------------------------------------------------------------------- + * lhs rhs modulo { 3, 5, 7, 11, 17, 31, 59 } + * ----^--- ^ + * 2 4 6 18 + * 4 5 6 24 + * 2 7 12 30 + * ------------------------------------------------------------------- */ + rhs = {Integer(18), Integer(24), Integer(30)}; + lhs = {{Integer(2), Integer(4), Integer(6)}, + {Integer(4), Integer(5), Integer(6)}, + {Integer(2), Integer(7), Integer(12)}}; + std::cout << "matrix 32, modulo 3" << std::endl; + resrhs = {Integer(0), Integer(0), Integer(0)}; + reslhs = {{Integer(1), Integer(2), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(3), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); + resrhs = {Integer(1), Integer(4), Integer(0)}; + std::cout << "matrix 32, modulo 5" << std::endl; + reslhs = {{Integer(1), Integer(0), Integer(4)}, + {Integer(0), Integer(1), Integer(2)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(5), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); + std::cout << "matrix 32, modulo 7" << std::endl; + reslhs = {{Integer(1), Integer(0), Integer(6)}, + {Integer(0), Integer(1), Integer(2)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(7), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); + std::cout << "matrix 32, modulo 11" << std::endl; + reslhs = {{Integer(1), Integer(0), Integer(10)}, + {Integer(0), Integer(1), Integer(2)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(11), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); + std::cout << "matrix 32, modulo 17" << std::endl; + reslhs = {{Integer(1), Integer(0), Integer(16)}, + {Integer(0), Integer(1), Integer(2)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(17), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); + std::cout << "matrix 32, modulo 59" << std::endl; + reslhs = {{Integer(1), Integer(0), Integer(58)}, + {Integer(0), Integer(1), Integer(2)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(59), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 3 + * ----^--- ^ --^-- ^ + * 4 6 2 18 --> 1 0 2 0 + * 5 6 4 24 0 0 0 0 + * 7 12 2 30 0 0 0 0 + * ------------------------------------------------------------------- */ + rhs = {Integer(18), Integer(24), Integer(30)}; + lhs = {{Integer(4), Integer(6), Integer(2)}, + {Integer(5), Integer(6), Integer(4)}, + {Integer(7), Integer(12), Integer(2)}}; + std::cout << "matrix 33, modulo 3" << std::endl; + resrhs = {Integer(0), Integer(0), Integer(0)}; + reslhs = {{Integer(1), Integer(0), Integer(2)}, + {Integer(0), Integer(0), Integer(0)}, + {Integer(0), Integer(0), Integer(0)}}; + testGaussElimX( + Integer(3), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); + } + + void testGaussElimPartial2() + { + std::vector rhs; + std::vector> lhs; + + /* ------------------------------------------------------------------- + * lhs rhs --> lhs rhs modulo 11 + * ---^--- ^ ---^--- ^ + * x y z w x y z w + * 1 2 0 6 2 1 2 0 0 1 + * 0 0 2 2 2 0 0 1 0 10 + * 0 0 0 1 2 0 0 0 1 2 + * ------------------------------------------------------------------- */ + rhs = {Integer(2), Integer(2), Integer(2)}; + lhs = {{Integer(1), Integer(2), Integer(6), Integer(0)}, + {Integer(0), Integer(0), Integer(2), Integer(2)}, + {Integer(0), Integer(0), Integer(1), Integer(0)}}; + std::cout << "matrix 34, modulo 11" << std::endl; + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); + } + void testGaussElimRewriteForUremUnique1() + { + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 1 1 5 + * 2 3 5 8 + * 4 0 5 2 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), + d_z_mul_one), + d_p), + d_five); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + d_z_mul_five), + d_p), + d_eight); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), + d_p), + d_two); + + std::vector eqs = {eq1, eq2, eq3}; + std::unordered_map res; + passes::Result ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::UNIQUE); + TS_ASSERT(res.size() == 3); + TS_ASSERT(res[d_x] == d_three32); + TS_ASSERT(res[d_y] == d_four32); + TS_ASSERT(res[d_z] == d_nine32); + } + + void testGaussElimRewriteForUremUnique2() + { + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 1 1 5 + * 2 3 5 8 + * 4 0 5 2 + * ------------------------------------------------------------------- */ + + Node zextop6 = d_nm->mkConst(BitVectorZeroExtend(6)); + + Node p = d_nm->mkNode( + zextop6, + bv::utils::mkConcat(bv::utils::mkZero(6), + d_nm->mkNode(kind::BITVECTOR_PLUS, + bv::utils::mkConst(20, 7), + bv::utils::mkConst(20, 4)))); + + Node x_mul_one = + d_nm->mkNode(kind::BITVECTOR_MULT, + d_nm->mkNode(kind::BITVECTOR_SUB, d_five, d_four), + d_x); + Node y_mul_one = + d_nm->mkNode(kind::BITVECTOR_MULT, + d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, d_one, d_five), + d_y); + Node z_mul_one = + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkOne(32), d_z); + + Node x_mul_two = d_nm->mkNode( + kind::BITVECTOR_MULT, + d_nm->mkNode( + kind::BITVECTOR_SHL, bv::utils::mkOne(32), bv::utils::mkOne(32)), + d_x); + Node y_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, + d_nm->mkNode(kind::BITVECTOR_LSHR, + bv::utils::mkOnes(32), + bv::utils::mkConst(32, 30)), + d_y); + Node z_mul_five = d_nm->mkNode(kind::BITVECTOR_MULT, + bv::utils::mkExtract( + d_nm->mkNode( + zextop6, d_nm->mkNode(kind::BITVECTOR_PLUS, d_three, d_two)), + 31, 0), + d_z); + + Node x_mul_four = d_nm->mkNode(kind::BITVECTOR_MULT, + d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_MULT, + bv::utils::mkConst(32, 4), + bv::utils::mkConst(32, 5)), + bv::utils::mkConst(32, 4)), + bv::utils::mkConst(32, 6)), + d_x); + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, + x_mul_one, + y_mul_one), + z_mul_one), + p), + d_five); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, x_mul_two, y_mul_three), + z_mul_five), + p), + d_eight); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, x_mul_four, z_mul_five), + d_p), + d_two); + + std::vector eqs = {eq1, eq2, eq3}; + std::unordered_map res; + passes::Result ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::UNIQUE); + TS_ASSERT(res.size() == 3); + TS_ASSERT(res[d_x] == d_three32); + TS_ASSERT(res[d_y] == d_four32); + TS_ASSERT(res[d_z] == d_nine32); + } + + void testGaussElimRewriteForUremPartial1() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine), + d_p), + d_seven); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three), + d_p), + d_nine); + + std::vector eqs = {eq1, eq2}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 2); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_seven32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), + d_p); + Node y1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nine32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), + d_p); + + Node x2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), + d_p); + Node z2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), + d_p); + + Node y3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), + d_p); + Node z3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), + d_p); + + /* result depends on order of variables in matrix */ + if (res.find(d_x) == res.end()) + { + /* + * y z x y z x + * 0 9 1 7 --> 1 0 7 3 + * 1 3 0 9 0 1 5 2 + * + * z y x z y x + * 9 0 1 7 --> 1 0 5 2 + * 3 1 0 9 0 1 7 3 + */ + TS_ASSERT(res[d_y] == y3); + TS_ASSERT(res[d_z] == z3); + } + else if (res.find(d_y) == res.end()) + { + /* + * x z y x z y + * 1 9 0 7 --> 1 0 8 2 + * 0 3 1 9 0 1 4 3 + * + * z x y z x y + * 9 1 0 7 --> 1 0 4 3 + * 3 0 1 9 0 1 8 2 + */ + TS_ASSERT(res[d_x] == x2); + TS_ASSERT(res[d_z] == z2); + } + else + { + TS_ASSERT(res.find(d_z) == res.end()); + /* + * x y z x y z + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * + * y x z y x z + * 0 1 9 7 --> 1 0 3 9 + * 1 0 3 9 0 1 9 7 + */ + TS_ASSERT(res[d_x] == x1); + TS_ASSERT(res[d_y] == y1); + } + } + + void testGaussElimRewriteForUremPartial1a() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x, d_z_mul_nine), + d_p), + d_seven); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_y, d_z_mul_three), + d_p), + d_nine); + + std::vector eqs = {eq1, eq2}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 2); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_seven32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), + d_p); + Node y1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nine32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), + d_p); + + Node x2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), + d_p); + Node z2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), + d_p); + + Node y3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), + d_p); + Node z3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), + d_p); + + /* result depends on order of variables in matrix */ + if (res.find(d_x) == res.end()) + { + /* + * y z x y z x + * 0 9 1 7 --> 1 0 7 3 + * 1 3 0 9 0 1 5 2 + * + * z y x z y x + * 9 0 1 7 --> 1 0 5 2 + * 3 1 0 9 0 1 7 3 + */ + TS_ASSERT(res[d_y] == y3); + TS_ASSERT(res[d_z] == z3); + } + else if (res.find(d_y) == res.end()) + { + /* + * x z y x z y + * 1 9 0 7 --> 1 0 8 2 + * 0 3 1 9 0 1 4 3 + * + * z x y z x y + * 9 1 0 7 --> 1 0 4 3 + * 3 0 1 9 0 1 8 2 + */ + TS_ASSERT(res[d_x] == x2); + TS_ASSERT(res[d_z] == z2); + } + else + { + TS_ASSERT(res.find(d_z) == res.end()); + /* + * x y z x y z + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * + * y x z y x z + * 0 1 9 7 --> 1 0 3 9 + * 1 0 3 9 0 1 9 7 + */ + TS_ASSERT(res[d_x] == x1); + TS_ASSERT(res[d_y] == y1); + } + } + + void testGaussElimRewriteForUremPartial2() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 3 0 7 --> 1 3 0 7 + * 0 0 1 9 0 0 1 9 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_three), + d_p), + d_seven); + + Node eq2 = + d_nm->mkNode(kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, d_z_mul_one, d_p), + d_nine); + + std::vector eqs = {eq1, eq2}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 2); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_seven32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_eight32)), + d_p); + Node y2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_six32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_seven32)), + d_p); + + /* result depends on order of variables in matrix */ + if (res.find(d_x) == res.end()) + { + /* + * x y z x y z + * 1 3 0 7 --> 1 3 0 7 + * 0 0 1 9 0 0 1 9 + * + * x z y x z y + * 1 0 3 7 --> 1 0 3 7 + * 0 1 0 9 0 1 0 9 + * + * z x y z x y + * 0 1 3 7 --> 1 0 0 9 + * 1 0 0 9 0 1 3 7 + */ + TS_ASSERT(res[d_y] == y2); + TS_ASSERT(res[d_z] == d_nine32); + } + else if (res.find(d_y) == res.end()) + { + /* + * z y x z y x + * 0 3 1 7 --> 1 0 0 9 + * 1 0 0 9 0 1 4 6 + * + * y x z y x z + * 3 1 0 7 --> 1 4 0 6 + * 0 0 1 9 0 0 1 9 + * + * y z x y z x + * 3 0 1 7 --> 1 0 4 6 + * 0 1 0 9 0 1 0 9 + */ + TS_ASSERT(res[d_x] == x1); + TS_ASSERT(res[d_z] == d_nine32); + } + else + { + TS_ASSERT(false); + } + } + + void testGaussElimRewriteForUremPartial3() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 1 1 5 --> 1 0 9 7 + * 2 3 5 8 0 1 3 9 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y), + d_z_mul_one), + d_p), + d_five); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + d_z_mul_five), + d_p), + d_eight); + + std::vector eqs = {eq1, eq2}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 2); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_seven32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), + d_p); + Node y1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nine32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), + d_p); + Node x2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), + d_p); + Node z2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), + d_p); + Node y3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), + d_p); + Node z3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), + d_p); + + /* result depends on order of variables in matrix */ + if (res.find(d_x) == res.end()) + { + /* + * y z x y z x + * 1 1 1 5 --> 1 0 7 3 + * 3 5 2 8 0 1 5 2 + * + * z y x z y x + * 1 1 1 5 --> 1 0 5 2 + * 5 3 2 8 0 1 7 3 + */ + TS_ASSERT(res[d_y] == y3); + TS_ASSERT(res[d_z] == z3); + } + else if (res.find(d_y) == res.end()) + { + /* + * x z y x z y + * 1 1 1 5 --> 1 0 8 2 + * 2 5 3 8 0 1 4 3 + * + * z x y z x y + * 1 1 1 5 --> 1 0 4 3 + * 5 2 3 9 0 1 8 2 + */ + TS_ASSERT(res[d_x] == x2); + TS_ASSERT(res[d_z] == z2); + } + else + { + TS_ASSERT(res.find(d_z) == res.end()); + /* + * x y z x y z + * 1 1 1 5 --> 1 0 9 7 + * 2 3 5 8 0 1 3 9 + * + * y x z y x z + * 1 1 1 5 --> 1 0 3 9 + * 3 2 5 8 0 1 9 7 + */ + TS_ASSERT(res[d_x] == x1); + TS_ASSERT(res[d_y] == y1); + } + } + + void testGaussElimRewriteForUremPartial4() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * ----^--- ^ ---^--- ^ + * 2 4 6 18 --> 1 0 10 1 + * 4 5 6 24 0 1 2 4 + * 2 7 12 30 0 0 0 0 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four), + d_z_mul_six), + d_p), + d_eighteen); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five), + d_z_mul_six), + d_p), + d_twentyfour); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven), + d_z_mul_twelve), + d_p), + d_thirty); + + std::vector eqs = {eq1, eq2, eq3}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 2); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_one32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_one32)), + d_p); + Node y1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_four32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_nine32)), + d_p); + Node x2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)), + d_p); + Node z2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)), + d_p); + Node y3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_six32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_nine32)), + d_p); + Node z3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_ten32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_one32)), + d_p); + + /* result depends on order of variables in matrix */ + if (res.find(d_x) == res.end()) + { + /* + * y z x y z x + * 4 6 2 18 --> 1 0 2 6 + * 5 6 4 24 0 1 10 10 + * 7 12 2 30 0 0 0 0 + * + * z y x z y x + * 6 4 2 18 --> 1 0 10 10 + * 6 5 4 24 0 1 2 6 + * 12 12 2 30 0 0 0 0 + * + */ + TS_ASSERT(res[d_y] == y3); + TS_ASSERT(res[d_z] == z3); + } + else if (res.find(d_y) == res.end()) + { + /* + * x z y x z y + * 2 6 4 18 --> 1 0 6 3 + * 4 6 5 24 0 1 6 2 + * 2 12 7 30 0 0 0 0 + * + * z x y z x y + * 6 2 4 18 --> 1 0 6 2 + * 6 4 5 24 0 1 6 3 + * 12 2 12 30 0 0 0 0 + * + */ + TS_ASSERT(res[d_x] == x2); + TS_ASSERT(res[d_z] == z2); + } + else + { + TS_ASSERT(res.find(d_z) == res.end()); + /* + * x y z x y z + * 2 4 6 18 --> 1 0 10 1 + * 4 5 6 24 0 1 2 4 + * 2 7 12 30 0 0 0 0 + * + * y x z y x z + * 4 2 6 18 --> 1 0 2 49 + * 5 4 6 24 0 1 10 1 + * 7 2 12 30 0 0 0 0 + */ + TS_ASSERT(res[d_x] == x1); + TS_ASSERT(res[d_y] == y1); + } + } + + void testGaussElimRewriteForUremPartial5() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 3 + * ----^--- ^ --^-- ^ + * 2 4 6 18 --> 1 2 0 0 + * 4 5 6 24 0 0 0 0 + * 2 7 12 30 0 0 0 0 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four), + d_z_mul_six), + d_three), + d_eighteen); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five), + d_z_mul_six), + d_three), + d_twentyfour); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven), + d_z_mul_twelve), + d_three), + d_thirty); + + std::vector eqs = {eq1, eq2, eq3}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 1); + + Node x1 = d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_one32), + d_three); + Node y2 = d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_one32), + d_three); + + /* result depends on order of variables in matrix */ + if (res.find(d_x) == res.end()) + { + /* + * y x z y x z + * 4 2 6 18 --> 1 2 0 0 + * 5 4 6 24 0 0 0 0 + * 7 2 12 30 0 0 0 0 + * + * y z x y z x + * 4 6 2 18 --> 1 0 2 0 + * 5 6 4 24 0 0 0 0 + * 7 12 2 30 0 0 0 0 + * + * z y x z y x + * 6 4 2 18 --> 0 1 2 0 + * 6 5 4 24 0 0 0 0 + * 12 12 2 30 0 0 0 0 + * + */ + TS_ASSERT(res[d_y] == y2); + } + else if (res.find(d_y) == res.end()) + { + /* + * x y z x y z + * 2 4 6 18 --> 1 2 0 0 + * 4 5 6 24 0 0 0 0 + * 2 7 12 30 0 0 0 0 + * + * x z y x z y + * 2 6 4 18 --> 1 0 2 0 + * 4 6 5 24 0 0 0 0 + * 2 12 7 30 0 0 0 0 + * + * z x y z x y + * 6 2 4 18 --> 0 1 2 0 + * 6 4 5 24 0 0 0 0 + * 12 2 12 30 0 0 0 0 + * + */ + TS_ASSERT(res[d_x] == x1); + } + else + { + TS_ASSERT(false); + } + } + + void testGaussElimRewriteForUremPartial6() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs --> lhs rhs modulo 11 + * ---^--- ^ ---^--- ^ + * x y z w x y z w + * 1 2 0 6 2 1 2 0 6 2 + * 0 0 2 2 2 0 0 1 1 1 + * 0 0 0 1 2 0 0 0 1 2 + * ------------------------------------------------------------------- */ + + Node y_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_two); + Node z_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two); + Node w = bv::utils::mkConcat( + d_zero, d_nm->mkVar("w", d_nm->mkBitVectorType(16))); + Node w_mul_six = d_nm->mkNode(kind::BITVECTOR_MULT, w, d_six); + Node w_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, w, d_two); + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, y_mul_two), + w_mul_six), + d_p), + d_two); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, z_mul_two, w_mul_two), + d_p), + d_two); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, w, d_p), + d_two); + + std::vector eqs = {eq1, eq2, eq3}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 3); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_one32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_nine32)), + d_p); + Node z1 = d_ten32; + Node w1 = d_two32; + + Node y2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_six32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_five32)), + d_p); + Node z2 = d_ten32; + Node w2 = d_two32; + + /* result depends on order of variables in matrix */ + if (res.find(d_x) == res.end()) + { + TS_ASSERT(res[d_y] == y2); + TS_ASSERT(res[d_z] == z2); + TS_ASSERT(res[w] == w2); + } + else if (res.find(d_y) == res.end()) + { + TS_ASSERT(res[d_x] == x1); + TS_ASSERT(res[d_z] == z1); + TS_ASSERT(res[w] == w1); + } + else + { + TS_ASSERT(false); + } + } + + void testGaussElimRewriteForUremWithExprPartial() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * ------------------------------------------------------------------- */ + + Node zero = bv::utils::mkZero(8); + Node xx = d_nm->mkVar("xx", d_nm->mkBitVectorType(8)); + Node yy = d_nm->mkVar("yy", d_nm->mkBitVectorType(8)); + Node zz = d_nm->mkVar("zz", d_nm->mkBitVectorType(8)); + + Node x = bv::utils::mkConcat( + d_zero, + bv::utils::mkConcat( + zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, xx), 7, 0))); + Node y = bv::utils::mkConcat( + d_zero, + bv::utils::mkConcat( + zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, yy), 7, 0))); + Node z = bv::utils::mkConcat( + d_zero, + bv::utils::mkConcat( + zero, bv::utils::mkExtract(bv::utils::mkConcat(zero, zz), 7, 0))); + + Node x_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, x, d_one32); + Node nine_mul_z = d_nm->mkNode(kind::BITVECTOR_MULT, d_nine32, z); + Node one_mul_y = d_nm->mkNode(kind::BITVECTOR_MULT, d_one, y); + Node z_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, z, d_three); + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, x_mul_one, nine_mul_z), + d_p), + d_seven); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, one_mul_y, z_mul_three), + d_p), + d_nine); + + std::vector eqs = {eq1, eq2}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 2); + + x = Rewriter::rewrite(x); + y = Rewriter::rewrite(y); + z = Rewriter::rewrite(z); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_seven32, + d_nm->mkNode(kind::BITVECTOR_MULT, z, d_two32)), + d_p); + Node y1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nine32, + d_nm->mkNode(kind::BITVECTOR_MULT, z, d_eight32)), + d_p); + + Node x2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, y, d_three32)), + d_p); + Node z2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, y, d_seven32)), + d_p); + + Node y3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, x, d_four32)), + d_p); + Node z3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, x, d_six32)), + d_p); + + /* result depends on order of variables in matrix */ + if (res.find(x) == res.end()) + { + /* + * y z x y z x + * 0 9 1 7 --> 1 0 7 3 + * 1 3 0 9 0 1 5 2 + * + * z y x z y x + * 9 0 1 7 --> 1 0 5 2 + * 3 1 0 9 0 1 7 3 + */ + TS_ASSERT(res[Rewriter::rewrite(y)] == y3); + TS_ASSERT(res[Rewriter::rewrite(z)] == z3); + } + else if (res.find(y) == res.end()) + { + /* + * x z y x z y + * 1 9 0 7 --> 1 0 8 2 + * 0 3 1 9 0 1 4 3 + * + * z x y z x y + * 9 1 0 7 --> 1 0 4 3 + * 3 0 1 9 0 1 8 2 + */ + TS_ASSERT(res[x] == x2); + TS_ASSERT(res[z] == z2); + } + else + { + TS_ASSERT(res.find(z) == res.end()); + /* + * x y z x y z + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * + * y x z y x z + * 0 1 9 7 --> 1 0 3 9 + * 1 0 3 9 0 1 9 7 + */ + TS_ASSERT(res[x] == x1); + TS_ASSERT(res[y] == y1); + } + } + + void testGaussElimRewriteForUremNAryPartial() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * ------------------------------------------------------------------- */ + + Node zero = bv::utils::mkZero(8); + Node xx = d_nm->mkVar("xx", d_nm->mkBitVectorType(8)); + Node yy = d_nm->mkVar("yy", d_nm->mkBitVectorType(8)); + Node zz = d_nm->mkVar("zz", d_nm->mkBitVectorType(8)); + + Node x = bv::utils::mkConcat( + d_zero, + bv::utils::mkConcat( + zero, + bv::utils::mkExtract( + d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, xx), 7, 0))); + Node y = bv::utils::mkConcat( + d_zero, + bv::utils::mkConcat( + zero, + bv::utils::mkExtract( + d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, yy), 7, 0))); + Node z = bv::utils::mkConcat( + d_zero, + bv::utils::mkConcat( + zero, + bv::utils::mkExtract( + d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0))); + + NodeBuilder<> nbx(d_nm, kind::BITVECTOR_MULT); + nbx << d_x << d_one << x; + Node x_mul_one_mul_xx = nbx.constructNode(); + NodeBuilder<> nby(d_nm, kind::BITVECTOR_MULT); + nby << d_y << y << d_one; + Node y_mul_yy_mul_one = nby.constructNode(); + NodeBuilder<> nbz(d_nm, kind::BITVECTOR_MULT); + nbz << d_three << d_z << z; + Node three_mul_z_mul_zz = nbz.constructNode(); + NodeBuilder<> nbz2(d_nm, kind::BITVECTOR_MULT); + nbz2 << d_z << d_nine << z; + Node z_mul_nine_mul_zz = nbz2.constructNode(); + + Node x_mul_xx = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, x); + Node y_mul_yy = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, y); + Node z_mul_zz = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, z); + + Node eq1 = d_nm->mkNode(kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + x_mul_one_mul_xx, + z_mul_nine_mul_zz), + d_p), + d_seven); + + Node eq2 = d_nm->mkNode(kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + y_mul_yy_mul_one, + three_mul_z_mul_zz), + d_p), + d_nine); + + std::vector eqs = {eq1, eq2}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); + TS_ASSERT(res.size() == 2); + + x_mul_xx = Rewriter::rewrite(x_mul_xx); + y_mul_yy = Rewriter::rewrite(y_mul_yy); + z_mul_zz = Rewriter::rewrite(z_mul_zz); + + Node x1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_seven32, + d_nm->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_two32)), + d_p); + Node y1 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nine32, + d_nm->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_eight32)), + d_p); + + Node x2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_three32)), + d_p); + Node z2 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_seven32)), + d_p); + + Node y3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_four32)), + d_p); + Node z3 = d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_six32)), + d_p); + + /* result depends on order of variables in matrix */ + if (res.find(x_mul_xx) == res.end()) + { + /* + * y z x y z x + * 0 9 1 7 --> 1 0 7 3 + * 1 3 0 9 0 1 5 2 + * + * z y x z y x + * 9 0 1 7 --> 1 0 5 2 + * 3 1 0 9 0 1 7 3 + */ + TS_ASSERT(res[y_mul_yy] == y3); + TS_ASSERT(res[z_mul_zz] == z3); + } + else if (res.find(y_mul_yy) == res.end()) + { + /* + * x z y x z y + * 1 9 0 7 --> 1 0 8 2 + * 0 3 1 9 0 1 4 3 + * + * z x y z x y + * 9 1 0 7 --> 1 0 4 3 + * 3 0 1 9 0 1 8 2 + */ + TS_ASSERT(res[x_mul_xx] == x2); + TS_ASSERT(res[z_mul_zz] == z2); + } + else + { + TS_ASSERT(res.find(z_mul_zz) == res.end()); + /* + * x y z x y z + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * + * y x z y x z + * 0 1 9 7 --> 1 0 3 9 + * 1 0 3 9 0 1 9 7 + */ + TS_ASSERT(res[x_mul_xx] == x1); + TS_ASSERT(res[y_mul_yy] == y1); + } + } + + void testGaussElimRewriteForUremNotInvalid1() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * 3x / 2z = 4 modulo 11 + * 2x % 5y = 2 + * y O z = 5 + * ------------------------------------------------------------------- */ + + Node n1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, + d_nm->mkNode(kind::BITVECTOR_MULT, d_three, d_x), + d_nm->mkNode(kind::BITVECTOR_MULT, d_two, d_y)); + Node n2 = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, + d_nm->mkNode(kind::BITVECTOR_MULT, d_two, d_x), + d_nm->mkNode(kind::BITVECTOR_MULT, d_five, d_y)); + + Node n3 = bv::utils::mkConcat( + d_zero, + bv::utils::mkExtract( + d_nm->mkNode(kind::BITVECTOR_CONCAT, d_y, d_z), 15, 0)); + + Node eq1 = d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n1, d_p), d_four); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n2, d_p), d_two); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n3, d_p), d_five); + + std::vector eqs = {eq1, eq2, eq3}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::UNIQUE); + TS_ASSERT(res.size() == 3); + + TS_ASSERT(res[n1] == d_four32); + TS_ASSERT(res[n2] == d_two32); + TS_ASSERT(res[n3] == d_five32); + } + + void testGaussElimRewriteForUremNotInvalid2() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * x*y = 4 modulo 11 + * x*y*z = 2 + * 2*x*y + 2*z = 9 + * ------------------------------------------------------------------- */ + + Node zero32 = bv::utils::mkZero(32); + + Node x = bv::utils::mkConcat(zero32, + d_nm->mkVar("x", d_nm->mkBitVectorType(16))); + Node y = bv::utils::mkConcat(zero32, + d_nm->mkVar("y", d_nm->mkBitVectorType(16))); + Node z = bv::utils::mkConcat(zero32, + d_nm->mkVar("z", d_nm->mkBitVectorType(16))); + + Node n1 = d_nm->mkNode(kind::BITVECTOR_MULT, x, y); + Node n2 = d_nm->mkNode( + kind::BITVECTOR_MULT, d_nm->mkNode(kind::BITVECTOR_MULT, x, y), z); + Node n3 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_MULT, + d_nm->mkNode(kind::BITVECTOR_MULT, x, y), + bv::utils::mkConcat(d_zero, d_two)), + d_nm->mkNode( + kind::BITVECTOR_MULT, bv::utils::mkConcat(d_zero, d_two), z)); + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, n1, bv::utils::mkConcat(d_zero, d_p)), + bv::utils::mkConcat(d_zero, d_four)); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, n2, bv::utils::mkConcat(d_zero, d_p)), + bv::utils::mkConcat(d_zero, d_two)); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, n3, bv::utils::mkConcat(d_zero, d_p)), + bv::utils::mkConcat(d_zero, d_nine)); + + std::vector eqs = {eq1, eq2, eq3}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::UNIQUE); + TS_ASSERT(res.size() == 3); + + n1 = Rewriter::rewrite(n1); + n2 = Rewriter::rewrite(n2); + z = Rewriter::rewrite(z); + + TS_ASSERT(res[n1] ==bv::utils::mkConst(48, 4)); + TS_ASSERT(res[n2] ==bv::utils::mkConst(48, 2)); + + Integer twoxy = (res[n1].getConst().getValue() * Integer(2)) + .euclidianDivideRemainder(Integer(48)); + Integer twoz = (res[z].getConst().getValue() * Integer(2)) + .euclidianDivideRemainder(Integer(48)); + Integer r = (twoxy + twoz).euclidianDivideRemainder(Integer(11)); + TS_ASSERT(r == Integer(9)); + } + + void testGaussElimRewriteForUremInvalid() + { + std::unordered_map res; + passes::Result ret; + + /* ------------------------------------------------------------------- + * x*y = 4 modulo 11 + * x*y*z = 2 + * 2*x*y = 9 + * ------------------------------------------------------------------- */ + + Node zero32 = bv::utils::mkZero(32); + + Node x = bv::utils::mkConcat(zero32, + d_nm->mkVar("x", d_nm->mkBitVectorType(16))); + Node y = bv::utils::mkConcat(zero32, + d_nm->mkVar("y", d_nm->mkBitVectorType(16))); + Node z = bv::utils::mkConcat(zero32, + d_nm->mkVar("z", d_nm->mkBitVectorType(16))); + + Node n1 = d_nm->mkNode(kind::BITVECTOR_MULT, x, y); + Node n2 = d_nm->mkNode( + kind::BITVECTOR_MULT, d_nm->mkNode(kind::BITVECTOR_MULT, x, y), z); + Node n3 = d_nm->mkNode(kind::BITVECTOR_MULT, + d_nm->mkNode(kind::BITVECTOR_MULT, x, y), + bv::utils::mkConcat(d_zero, d_two)); + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, n1, bv::utils::mkConcat(d_zero, d_p)), + bv::utils::mkConcat(d_zero, d_four)); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, n2, bv::utils::mkConcat(d_zero, d_p)), + bv::utils::mkConcat(d_zero, d_two)); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, n3, bv::utils::mkConcat(d_zero, d_p)), + bv::utils::mkConcat(d_zero, d_nine)); + + std::vector eqs = {eq1, eq2, eq3}; + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::INVALID); + } + + void testGaussElimRewriteUnique1() + { + /* ------------------------------------------------------------------- + * lhs rhs modulo 11 + * --^-- ^ + * 1 1 1 5 + * 2 3 5 8 + * 4 0 5 2 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), + d_z_mul_one), + d_p), + d_five); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + d_z_mul_five), + d_p), + d_eight); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), + d_p), + d_two); + + Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); + + AssertionPipeline apipe; + apipe.push_back(a); + passes::BVGauss bgauss(nullptr); + std::unordered_map res; + PreprocessingPassResult pres = bgauss.applyInternal(&apipe); + TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT); + Node resx = d_nm->mkNode( + kind::EQUAL, d_x, d_nm->mkConst(BitVector(32, 3u))); + Node resy = d_nm->mkNode( + kind::EQUAL, d_y, d_nm->mkConst(BitVector(32, 4u))); + Node resz = d_nm->mkNode( + kind::EQUAL, d_z, d_nm->mkConst(BitVector(32, 9u))); + TS_ASSERT(apipe.size() == 4); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resx) != apipe.end()); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resy) != apipe.end()); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resz) != apipe.end()); + } + + void testGaussElimRewriteUnique2() + { + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 1 1 5 1 0 0 3 + * 2 3 5 8 0 1 0 4 + * 4 0 5 2 0 0 1 9 + * + * lhs rhs lhs rhs modulo 7 + * --^-- ^ --^-- ^ + * 2 6 0 4 1 0 0 3 + * 4 6 0 3 0 1 0 2 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), + d_z_mul_one), + d_p), + d_five); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), + d_z_mul_five), + d_p), + d_eight); + + Node eq3 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), + d_p), + d_two); + + Node y_mul_six = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_six); + + Node eq4 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode(kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, y_mul_six), + d_seven), + d_four); + + Node eq5 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, y_mul_six), + d_seven), + d_three); + + Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); + + AssertionPipeline apipe; + apipe.push_back(a); + apipe.push_back(eq4); + apipe.push_back(eq5); + passes::BVGauss bgauss(nullptr); + std::unordered_map res; + PreprocessingPassResult pres = bgauss.applyInternal(&apipe); + TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT); + Node resx1 = d_nm->mkNode( + kind::EQUAL, d_x, d_nm->mkConst(BitVector(32, 3u))); + Node resx2 = d_nm->mkNode( + kind::EQUAL, d_x, d_nm->mkConst(BitVector(32, 3u))); + Node resy1 = d_nm->mkNode( + kind::EQUAL, d_y, d_nm->mkConst(BitVector(32, 4u))); + Node resy2 = d_nm->mkNode( + kind::EQUAL, d_y, d_nm->mkConst(BitVector(32, 2u))); + Node resz = d_nm->mkNode( + kind::EQUAL, d_z, d_nm->mkConst(BitVector(32, 9u))); + TS_ASSERT(apipe.size() == 8); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resx1) != apipe.end()); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resx2) != apipe.end()); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resy1) != apipe.end()); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resy2) != apipe.end()); + TS_ASSERT(std::find(apipe.begin(), apipe.end(), resz) != apipe.end()); + } + + void testGaussElimRewritePartial() + { + /* ------------------------------------------------------------------- + * lhs rhs lhs rhs modulo 11 + * --^-- ^ --^-- ^ + * 1 0 9 7 --> 1 0 9 7 + * 0 1 3 9 0 1 3 9 + * ------------------------------------------------------------------- */ + + Node eq1 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine), + d_p), + d_seven); + + Node eq2 = d_nm->mkNode( + kind::EQUAL, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three), + d_p), + d_nine); + + AssertionPipeline apipe; + apipe.push_back(eq1); + apipe.push_back(eq2); + passes::BVGauss bgauss(nullptr); + std::unordered_map res; + PreprocessingPassResult pres = bgauss.applyInternal(&apipe); + TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT); + TS_ASSERT(apipe.size() == 4); + + Node resx1 = d_nm->mkNode( + kind::EQUAL, + d_x, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_seven32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), + d_p)); + Node resy1 = d_nm->mkNode( + kind::EQUAL, + d_y, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_nine32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), + d_p)); + + Node resx2 = d_nm->mkNode( + kind::EQUAL, + d_x, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), + d_p)); + Node resz2 = d_nm->mkNode( + kind::EQUAL, + d_z, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), + d_p)); + + Node resy3 = d_nm->mkNode( + kind::EQUAL, + d_y, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_three32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), + d_p)); + Node resz3 = d_nm->mkNode( + kind::EQUAL, + d_z, + d_nm->mkNode( + kind::BITVECTOR_UREM, + d_nm->mkNode(kind::BITVECTOR_PLUS, + d_two32, + d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), + d_p)); + + bool fx1 = std::find(apipe.begin(), apipe.end(), resx1) != apipe.end(); + bool fy1 = std::find(apipe.begin(), apipe.end(), resy1) != apipe.end(); + bool fx2 = std::find(apipe.begin(), apipe.end(), resx2) != apipe.end(); + bool fz2 = std::find(apipe.begin(), apipe.end(), resz2) != apipe.end(); + bool fy3 = std::find(apipe.begin(), apipe.end(), resy3) != apipe.end(); + bool fz3 = std::find(apipe.begin(), apipe.end(), resz3) != apipe.end(); + + /* result depends on order of variables in matrix */ + TS_ASSERT((fx1 && fy1) || (fx2 && fz2) || (fy3 && fz3)); + } + + void testGetMinBw1() + { + TS_ASSERT(passes::getMinBwExpr(bv::utils::mkConst(32, 11)) == 4); + + TS_ASSERT(passes::getMinBwExpr(d_p) == 4); + TS_ASSERT(passes::getMinBwExpr(d_x) == 16); + + Node extp = bv::utils::mkExtract(d_p, 4, 0); + TS_ASSERT(passes::getMinBwExpr(extp) == 4); + Node extx = bv::utils::mkExtract(d_x, 4, 0); + TS_ASSERT(passes::getMinBwExpr(extx) == 5); + + Node zextop8 = d_nm->mkConst(BitVectorZeroExtend(8)); + Node zextop16 = d_nm->mkConst(BitVectorZeroExtend(16)); + Node zextop32 = d_nm->mkConst(BitVectorZeroExtend(32)); + Node zextop40 = d_nm->mkConst(BitVectorZeroExtend(40)); + + Node zext40p = d_nm->mkNode(zextop8, d_p); + TS_ASSERT(passes::getMinBwExpr(zext40p) == 4); + Node zext40x = d_nm->mkNode(zextop8, d_x); + TS_ASSERT(passes::getMinBwExpr(zext40x) == 16); + + Node zext48p = d_nm->mkNode(zextop16, d_p); + TS_ASSERT(passes::getMinBwExpr(zext48p) == 4); + Node zext48x = d_nm->mkNode(zextop16, d_x); + TS_ASSERT(passes::getMinBwExpr(zext48x) == 16); + + Node p8 = d_nm->mkConst(BitVector(8, 11u)); + Node x8 = d_nm->mkVar("x8", d_nm->mkBitVectorType(8)); + + Node zext48p8 = d_nm->mkNode(zextop40, p8); + TS_ASSERT(passes::getMinBwExpr(zext48p8) == 4); + Node zext48x8 = d_nm->mkNode(zextop40, x8); + TS_ASSERT(passes::getMinBwExpr(zext48x8) == 8); + + Node mult1p = d_nm->mkNode(kind::BITVECTOR_MULT, extp, extp); + TS_ASSERT(passes::getMinBwExpr(mult1p) == 5); + Node mult1x = d_nm->mkNode(kind::BITVECTOR_MULT, extx, extx); + TS_ASSERT(passes::getMinBwExpr(mult1x) == 0); + + Node mult2p = d_nm->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p); + TS_ASSERT(passes::getMinBwExpr(mult2p) == 7); + Node mult2x = d_nm->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x); + TS_ASSERT(passes::getMinBwExpr(mult2x) == 32); + + NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT); + nbmult3p << zext48p << zext48p << zext48p; + Node mult3p = nbmult3p; + TS_ASSERT(passes::getMinBwExpr(mult3p) == 11); + NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT); + nbmult3x << zext48x << zext48x << zext48x; + Node mult3x = nbmult3x; + TS_ASSERT(passes::getMinBwExpr(mult3x) == 48); + + NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT); + nbmult4p << zext48p << zext48p8 << zext48p; + Node mult4p = nbmult4p; + TS_ASSERT(passes::getMinBwExpr(mult4p) == 11); + NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT); + nbmult4x << zext48x << zext48x8 << zext48x; + Node mult4x = nbmult4x; + TS_ASSERT(passes::getMinBwExpr(mult4x) == 40); + + Node concat1p = bv::utils::mkConcat(d_p, zext48p); + TS_ASSERT(passes::getMinBwExpr(concat1p) == 52); + Node concat1x = bv::utils::mkConcat(d_x, zext48x); + TS_ASSERT(passes::getMinBwExpr(concat1x) == 64); + + Node concat2p = bv::utils::mkConcat(bv::utils::mkZero(16), zext48p); + TS_ASSERT(passes::getMinBwExpr(concat2p) == 4); + Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x); + TS_ASSERT(passes::getMinBwExpr(concat2x) == 16); + + Node udiv1p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p); + TS_ASSERT(passes::getMinBwExpr(udiv1p) == 1); + Node udiv1x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x); + TS_ASSERT(passes::getMinBwExpr(udiv1x) == 48); + + Node udiv2p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p8); + TS_ASSERT(passes::getMinBwExpr(udiv2p) == 1); + Node udiv2x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x8); + TS_ASSERT(passes::getMinBwExpr(udiv2x) == 48); + + Node urem1p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p); + TS_ASSERT(passes::getMinBwExpr(urem1p) == 1); + Node urem1x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x); + TS_ASSERT(passes::getMinBwExpr(urem1x) == 1); + + Node urem2p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p8); + TS_ASSERT(passes::getMinBwExpr(urem2p) == 1); + Node urem2x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x8); + TS_ASSERT(passes::getMinBwExpr(urem2x) == 16); + + Node urem3p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p8, zext48p); + TS_ASSERT(passes::getMinBwExpr(urem3p) == 1); + Node urem3x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x8, zext48x); + TS_ASSERT(passes::getMinBwExpr(urem3x) == 8); + + Node add1p = d_nm->mkNode(kind::BITVECTOR_PLUS, extp, extp); + TS_ASSERT(passes::getMinBwExpr(add1p) == 5); + Node add1x = d_nm->mkNode(kind::BITVECTOR_PLUS, extx, extx); + TS_ASSERT(passes::getMinBwExpr(add1x) == 0); + + Node add2p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p); + TS_ASSERT(passes::getMinBwExpr(add2p) == 5); + Node add2x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x); + TS_ASSERT(passes::getMinBwExpr(add2x) == 17); + + Node add3p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p); + TS_ASSERT(passes::getMinBwExpr(add3p) == 5); + Node add3x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x); + TS_ASSERT(passes::getMinBwExpr(add3x) == 17); + + NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS); + nbadd4p << zext48p << zext48p << zext48p; + Node add4p = nbadd4p; + TS_ASSERT(passes::getMinBwExpr(add4p) == 6); + NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS); + nbadd4x << zext48x << zext48x << zext48x; + Node add4x = nbadd4x; + TS_ASSERT(passes::getMinBwExpr(add4x) == 18); + + NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS); + nbadd5p << zext48p << zext48p8 << zext48p; + Node add5p = nbadd5p; + TS_ASSERT(passes::getMinBwExpr(add5p) == 6); + NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS); + nbadd5x << zext48x << zext48x8 << zext48x; + Node add5x = nbadd5x; + TS_ASSERT(passes::getMinBwExpr(add5x) == 18); + + NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS); + nbadd6p << zext48p << zext48p << zext48p << zext48p; + Node add6p = nbadd6p; + TS_ASSERT(passes::getMinBwExpr(add6p) == 6); + NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS); + nbadd6x << zext48x << zext48x << zext48x << zext48x; + Node add6x = nbadd6x; + TS_ASSERT(passes::getMinBwExpr(add6x) == 18); + + Node not1p = d_nm->mkNode(kind::BITVECTOR_NOT, zext40p); + TS_ASSERT(passes::getMinBwExpr(not1p) == 40); + Node not1x = d_nm->mkNode(kind::BITVECTOR_NOT, zext40x); + TS_ASSERT(passes::getMinBwExpr(not1x) == 40); + } + + void testGetMinBw2() + { + /* ((_ zero_extend 5) + * ((_ extract 7 0) ((_ zero_extend 15) d_p))) */ + Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); + Node zextop15 = d_nm->mkConst(BitVectorZeroExtend(15)); + Node zext1 = d_nm->mkNode(zextop15, d_p); + Node ext = bv::utils::mkExtract(zext1, 7, 0); + Node zext2 = d_nm->mkNode(zextop5, ext); + TS_ASSERT(passes::getMinBwExpr(zext2) == 4); + } + + void testGetMinBw3a() + { + /* ((_ zero_extend 5) + * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z))) + * ((_ extract 4 0) z))) */ + Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); + Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); + Node z = d_nm->mkVar("z", d_nm->mkBitVectorType(16)); + Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); + Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y); + Node zext1 = d_nm->mkNode(zextop5, udiv1); + Node ext1 = bv::utils::mkExtract(zext1, 4, 0); + Node ext2 = bv::utils::mkExtract(z, 4, 0); + Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2); + Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); + TS_ASSERT(passes::getMinBwExpr(zext2) == 5); + } + + void testGetMinBw3b() + { + /* ((_ zero_extend 5) + * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z))) + * ((_ extract 4 0) z))) */ + Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); + Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y); + Node zext1 = d_nm->mkNode(zextop5, udiv1); + Node ext1 = bv::utils::mkExtract(zext1, 4, 0); + Node ext2 = bv::utils::mkExtract(d_z, 4, 0); + Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2); + Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); + TS_ASSERT(passes::getMinBwExpr(zext2) == 5); + } + + void testGetMinBw4a() + { + /* (bvadd + * ((_ zero_extend 5) + * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y))) + * ((_ extract 4 0) z))) + * ((_ zero_extend 7) + * (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y))) + * ((_ extract 2 0) z))) */ + Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); + Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); + Node z = d_nm->mkVar("z", d_nm->mkBitVectorType(16)); + Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); + Node zextop7 = d_nm->mkConst(BitVectorZeroExtend(7)); + + Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y); + Node zext1 = d_nm->mkNode(zextop5, udiv1); + + Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0); + Node ext2_1 = bv::utils::mkExtract(z, 4, 0); + Node udiv2_1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1); + Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1); + + Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0); + Node ext2_2 = bv::utils::mkExtract(z, 2, 0); + Node udiv2_2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2); + Node zext2_2 = d_nm->mkNode(zextop7, udiv2_2); + + Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); + + TS_ASSERT(passes::getMinBwExpr(plus) == 6); + } + + void testGetMinBw4b() + { + /* (bvadd + * ((_ zero_extend 5) + * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y))) + * ((_ extract 4 0) z))) + * ((_ zero_extend 7) + * (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y))) + * ((_ extract 2 0) z))) */ + Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); + Node zextop7 = d_nm->mkConst(BitVectorZeroExtend(7)); + + Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y); + Node zext1 = d_nm->mkNode(zextop5, udiv1); + + Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0); + Node ext2_1 = bv::utils::mkExtract(d_z, 4, 0); + Node udiv2_1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1); + Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1); + + Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0); + Node ext2_2 = bv::utils::mkExtract(d_z, 2, 0); + Node udiv2_2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2); + Node zext2_2 = d_nm->mkNode(zextop7, udiv2_2); + + Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); + + TS_ASSERT(passes::getMinBwExpr(plus) == 6); + } + + void testGetMinBw5a() + { + /* (bvadd + * (bvadd + * (bvadd + * (bvadd + * (bvadd + * (bvadd + * (bvadd (bvmul (_ bv86 13) + * ((_ zero_extend 5) + * ((_ extract 7 0) ((_ zero_extend 15) x)))) + * (bvmul (_ bv41 13) + * ((_ zero_extend 5) + * ((_ extract 7 0) ((_ zero_extend 15) y))))) + * (bvmul (_ bv37 13) + * ((_ zero_extend 5) + * ((_ extract 7 0) ((_ zero_extend 15) z))))) + * (bvmul (_ bv170 13) + * ((_ zero_extend 5) + * ((_ extract 7 0) ((_ zero_extend 15) u))))) + * (bvmul (_ bv112 13) + * ((_ zero_extend 5) + * ((_ extract 7 0) ((_ zero_extend 15) v))))) + * (bvmul (_ bv195 13) ((_ zero_extend 5) ((_ extract 15 8) s)))) + * (bvmul (_ bv124 13) ((_ zero_extend 5) ((_ extract 7 0) s)))) + * (bvmul (_ bv83 13) + * ((_ zero_extend 5) ((_ extract 7 0) ((_ zero_extend 15) w))))) + */ + Node x =bv::utils::mkVar(1); + Node y =bv::utils::mkVar(1); + Node z =bv::utils::mkVar(1); + Node u =bv::utils::mkVar(1); + Node v =bv::utils::mkVar(1); + Node w =bv::utils::mkVar(1); + Node s =bv::utils::mkVar(16); + + Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); + Node zextop15 = d_nm->mkConst(BitVectorZeroExtend(15)); + + Node zext15x = d_nm->mkNode(zextop15, x); + Node zext15y = d_nm->mkNode(zextop15, y); + Node zext15z = d_nm->mkNode(zextop15, z); + Node zext15u = d_nm->mkNode(zextop15, u); + Node zext15v = d_nm->mkNode(zextop15, v); + Node zext15w = d_nm->mkNode(zextop15, w); + + Node ext7x = bv::utils::mkExtract(zext15x, 7, 0); + Node ext7y = bv::utils::mkExtract(zext15y, 7, 0); + Node ext7z = bv::utils::mkExtract(zext15z, 7, 0); + Node ext7u = bv::utils::mkExtract(zext15u, 7, 0); + Node ext7v = bv::utils::mkExtract(zext15v, 7, 0); + Node ext7w = bv::utils::mkExtract(zext15w, 7, 0); + Node ext7s = bv::utils::mkExtract(s, 7, 0); + Node ext15s = bv::utils::mkExtract(s, 15, 8); + + Node xx = bv::utils::mkConcat(bv::utils::mkZero(5), ext7x); + Node yy = bv::utils::mkConcat(bv::utils::mkZero(5), ext7y); + Node zz = bv::utils::mkConcat(bv::utils::mkZero(5), ext7z); + Node uu = bv::utils::mkConcat(bv::utils::mkZero(5), ext7u); + Node vv = bv::utils::mkConcat(bv::utils::mkZero(5), ext7v); + Node ww = bv::utils::mkConcat(bv::utils::mkZero(5), ext7w); + Node s7 = bv::utils::mkConcat(bv::utils::mkZero(5), ext7s); + Node s15 = bv::utils::mkConcat(bv::utils::mkZero(5), ext15s); + + Node plus1 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 86), xx), + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 41), yy)); + Node plus2 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus1, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 37), zz)); + Node plus3 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus2, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 170), uu)); + Node plus4 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus3, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 112), uu)); + Node plus5 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus4, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 195), s15)); + Node plus6 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus5, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 124), s7)); + Node plus7 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus6, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(13, 83), ww)); + + TS_ASSERT(passes::getMinBwExpr(plus7) == 0); + } + + void testGetMinBw5b() + { + /* (bvadd + * (bvadd + * (bvadd + * (bvadd + * (bvadd + * (bvadd + * (bvadd (bvmul (_ bv86 20) + * ((_ zero_extend 12) + * ((_ extract 7 0) ((_ zero_extend 15) x)))) + * (bvmul (_ bv41 20) + * ((_ zero_extend 12) + * ((_ extract 7 0) ((_ zero_extend 15) y))))) + * (bvmul (_ bv37 20) + * ((_ zero_extend 12) + * ((_ extract 7 0) ((_ zero_extend 15) z))))) + * (bvmul (_ bv170 20) + * ((_ zero_extend 12) + * ((_ extract 7 0) ((_ zero_extend 15) u))))) + * (bvmul (_ bv112 20) + * ((_ zero_extend 12) + * ((_ extract 7 0) ((_ zero_extend 15) v))))) + * (bvmul (_ bv195 20) ((_ zero_extend 12) ((_ extract 15 8) s)))) + * (bvmul (_ bv124 20) ((_ zero_extend 12) ((_ extract 7 0) s)))) + * (bvmul (_ bv83 20) + * ((_ zero_extend 12) ((_ extract 7 0) ((_ zero_extend 15) w))))) + */ + Node x =bv::utils::mkVar(1); + Node y =bv::utils::mkVar(1); + Node z =bv::utils::mkVar(1); + Node u =bv::utils::mkVar(1); + Node v =bv::utils::mkVar(1); + Node w =bv::utils::mkVar(1); + Node s =bv::utils::mkVar(16); + + Node zextop15 = d_nm->mkConst(BitVectorZeroExtend(15)); + + Node zext15x = d_nm->mkNode(zextop15, x); + Node zext15y = d_nm->mkNode(zextop15, y); + Node zext15z = d_nm->mkNode(zextop15, z); + Node zext15u = d_nm->mkNode(zextop15, u); + Node zext15v = d_nm->mkNode(zextop15, v); + Node zext15w = d_nm->mkNode(zextop15, w); + + Node ext7x = bv::utils::mkExtract(zext15x, 7, 0); + Node ext7y = bv::utils::mkExtract(zext15y, 7, 0); + Node ext7z = bv::utils::mkExtract(zext15z, 7, 0); + Node ext7u = bv::utils::mkExtract(zext15u, 7, 0); + Node ext7v = bv::utils::mkExtract(zext15v, 7, 0); + Node ext7w = bv::utils::mkExtract(zext15w, 7, 0); + Node ext7s = bv::utils::mkExtract(s, 7, 0); + Node ext15s = bv::utils::mkExtract(s, 15, 8); + + Node xx = bv::utils::mkConcat(bv::utils::mkZero(12), ext7x); + Node yy = bv::utils::mkConcat(bv::utils::mkZero(12), ext7y); + Node zz = bv::utils::mkConcat(bv::utils::mkZero(12), ext7z); + Node uu = bv::utils::mkConcat(bv::utils::mkZero(12), ext7u); + Node vv = bv::utils::mkConcat(bv::utils::mkZero(12), ext7v); + Node ww = bv::utils::mkConcat(bv::utils::mkZero(12), ext7w); + Node s7 = bv::utils::mkConcat(bv::utils::mkZero(12), ext7s); + Node s15 = bv::utils::mkConcat(bv::utils::mkZero(12), ext15s); + + Node plus1 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 86), xx), + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 41), yy)); + Node plus2 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus1, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 37), zz)); + Node plus3 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus2, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 170), uu)); + Node plus4 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus3, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 112), uu)); + Node plus5 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus4, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 195), s15)); + Node plus6 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus5, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 124), s7)); + Node plus7 = d_nm->mkNode( + kind::BITVECTOR_PLUS, + plus6, + d_nm->mkNode(kind::BITVECTOR_MULT, bv::utils::mkConst(20, 83), ww)); + + TS_ASSERT(passes::getMinBwExpr(plus7) == 19); + TS_ASSERT(passes::getMinBwExpr(Rewriter::rewrite(plus7)) == 17); + } + +}; diff --git a/test/unit/theory/theory_bv_bvgauss_white.h b/test/unit/theory/theory_bv_bvgauss_white.h deleted file mode 100644 index a0e2b235b..000000000 --- a/test/unit/theory/theory_bv_bvgauss_white.h +++ /dev/null @@ -1,2965 +0,0 @@ -/********************* */ -/*! \file theory_bv_bvgauss_white.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** 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 Gaussian Elimination preprocessing pass. - ** - ** Unit tests for Gaussian Elimination preprocessing pass. - **/ - -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/rewriter.h" -#include "theory/bv/bvgauss.h" -#include "theory/bv/theory_bv_utils.h" -#include "util/bitvector.h" - -#include -#include -#include - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; -using namespace CVC4::theory::bv::utils; -using namespace CVC4::smt; - -static void print_matrix_dbg(std::vector &rhs, - std::vector> &lhs) -{ - for (size_t m = 0, nrows = lhs.size(), ncols = lhs[0].size(); m < nrows; ++m) - { - for (size_t n = 0; n < ncols; ++n) - { - std::cout << " " << lhs[m][n]; - } - std::cout << " " << rhs[m]; - std::cout << std::endl; - } -} - -static void testGaussElimX(Integer prime, - std::vector rhs, - std::vector> lhs, - BVGaussElim::Result expected, - std::vector *rrhs = nullptr, - std::vector> *rlhs = nullptr) -{ - size_t nrows = lhs.size(); - size_t ncols = lhs[0].size(); - BVGaussElim::Result ret; - std::vector resrhs = std::vector(rhs); - std::vector> reslhs = - std::vector>(lhs); - - std::cout << "Input: " << std::endl; - print_matrix_dbg(rhs, lhs); - - ret = BVGaussElim::gaussElim(prime, resrhs, reslhs); - - std::cout << "Result: " - << (ret == BVGaussElim::Result::INVALID - ? "INVALID" - : (ret == BVGaussElim::Result::UNIQUE - ? "UNIQUE" - : (ret == BVGaussElim::Result::PARTIAL ? "PARTIAL" - : "NONE"))) - << std::endl; - print_matrix_dbg(resrhs, reslhs); - - TS_ASSERT_EQUALS(expected, ret); - - if (expected == BVGaussElim::Result::UNIQUE) - { - /* map result value to column index - * e.g.: - * 1 0 0 2 -> res = { 2, 0, 3} - * 0 0 1 3 */ - std::vector res = std::vector(ncols, Integer(0)); - for (size_t i = 0; i < nrows; ++i) - for (size_t j = 0; j < ncols; ++j) - { - if (reslhs[i][j] == 1) - res[j] = resrhs[i]; - else - TS_ASSERT(reslhs[i][j] == 0); - } - - for (size_t i = 0; i < nrows; ++i) - { - Integer tmp = Integer(0); - for (size_t j = 0; j < ncols; ++j) - tmp = tmp.modAdd(lhs[i][j].modMultiply(res[j], prime), prime); - TS_ASSERT(tmp == rhs[i].euclidianDivideRemainder(prime)); - } - } - if (rrhs != nullptr && rlhs != nullptr) - { - for (size_t i = 0; i < nrows; ++i) - { - for (size_t j = 0; j < ncols; ++j) - { - TS_ASSERT(reslhs[i][j] == (*rlhs)[i][j]); - } - TS_ASSERT(resrhs[i] == (*rrhs)[i]); - } - } -} - -template -static void testGaussElimT(Integer prime, - std::vector rhs, - std::vector> lhs) -{ - TS_ASSERT_THROWS(BVGaussElim::gaussElim(prime, rhs, lhs), T); -} - -class TheoryBVGaussWhite : public CxxTest::TestSuite -{ - ExprManager *d_em; - NodeManager *d_nm; - SmtEngine *d_smt; - SmtScope *d_scope; - Node d_p; - Node d_x; - Node d_y; - Node d_z; - Node d_zero; - Node d_one; - Node d_two; - Node d_three; - Node d_four; - Node d_five; - Node d_six; - Node d_seven; - Node d_eight; - Node d_nine; - Node d_ten; - Node d_twelve; - Node d_eighteen; - Node d_twentyfour; - Node d_thirty; - Node d_one32; - Node d_two32; - Node d_three32; - Node d_four32; - Node d_five32; - Node d_six32; - Node d_seven32; - Node d_eight32; - Node d_nine32; - Node d_ten32; - Node d_x_mul_one; - Node d_x_mul_two; - Node d_x_mul_four; - Node d_y_mul_one; - Node d_y_mul_three; - Node d_y_mul_four; - Node d_y_mul_five; - Node d_y_mul_seven; - Node d_z_mul_one; - Node d_z_mul_three; - Node d_z_mul_five; - Node d_z_mul_twelve; - Node d_z_mul_six; - Node d_z_mul_nine; - - public: - TheoryBVGaussWhite() {} - - void setUp() - { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); - d_scope = new SmtScope(d_smt); - - d_zero = mkZero(16); - - d_p = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 11u))); - d_x = mkConcat(d_zero, d_nm->mkVar("x", d_nm->mkBitVectorType(16))); - d_y = mkConcat(d_zero, d_nm->mkVar("y", d_nm->mkBitVectorType(16))); - d_z = mkConcat(d_zero, d_nm->mkVar("z", d_nm->mkBitVectorType(16))); - - d_one = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 1u))); - d_two = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 2u))); - d_three = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 3u))); - d_four = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 4u))); - d_five = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 5u))); - d_six = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 6u))); - d_seven = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 7u))); - d_eight = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 8u))); - d_nine = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 9u))); - d_ten = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 10u))); - d_twelve = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 12u))); - d_eighteen = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 18u))); - d_twentyfour = - mkConcat(d_zero, d_nm->mkConst(BitVector(16, 24u))); - d_thirty = mkConcat(d_zero, d_nm->mkConst(BitVector(16, 30u))); - - d_one32 = d_nm->mkConst(BitVector(32, 1u)); - d_two32 = d_nm->mkConst(BitVector(32, 2u)); - d_three32 = d_nm->mkConst(BitVector(32, 3u)); - d_four32 = d_nm->mkConst(BitVector(32, 4u)); - d_five32 = d_nm->mkConst(BitVector(32, 5u)); - d_six32 = d_nm->mkConst(BitVector(32, 6u)); - d_seven32 = d_nm->mkConst(BitVector(32, 7u)); - d_eight32 = d_nm->mkConst(BitVector(32, 8u)); - d_nine32 = d_nm->mkConst(BitVector(32, 9u)); - d_ten32 = d_nm->mkConst(BitVector(32, 10u)); - - d_x_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_one); - d_x_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_two); - d_x_mul_four = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four); - d_y_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three); - d_y_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_one); - d_y_mul_four = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_four); - d_y_mul_five = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_five); - d_y_mul_seven = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven); - d_z_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_one); - d_z_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_three); - d_z_mul_five = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_five); - d_z_mul_six = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_six); - d_z_mul_twelve = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_twelve); - d_z_mul_nine = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_nine); - } - - void tearDown() - { - (void)d_scope; - d_p = Node::null(); - d_x = Node::null(); - d_y = Node::null(); - d_z = Node::null(); - d_zero = Node::null(); - d_one = Node::null(); - d_two = Node::null(); - d_three = Node::null(); - d_four = Node::null(); - d_five = Node::null(); - d_six = Node::null(); - d_seven = Node::null(); - d_eight = Node::null(); - d_nine = Node::null(); - d_ten = Node::null(); - d_twelve = Node::null(); - d_eighteen = Node::null(); - d_twentyfour = Node::null(); - d_thirty = Node::null(); - d_one32 = Node::null(); - d_two32 = Node::null(); - d_three32 = Node::null(); - d_four32 = Node::null(); - d_five32 = Node::null(); - d_six32 = Node::null(); - d_seven32 = Node::null(); - d_eight32 = Node::null(); - d_nine32 = Node::null(); - d_ten32 = Node::null(); - d_x_mul_one = Node::null(); - d_x_mul_two = Node::null(); - d_x_mul_four = Node::null(); - d_y_mul_one = Node::null(); - d_y_mul_four = Node::null(); - d_y_mul_seven = Node::null(); - d_y_mul_five = Node::null(); - d_y_mul_three = Node::null(); - d_z_mul_one = Node::null(); - d_z_mul_three = Node::null(); - d_z_mul_five = Node::null(); - d_z_mul_six = Node::null(); - d_z_mul_twelve = Node::null(); - d_z_mul_nine = Node::null(); - delete d_scope; - delete d_smt; - delete d_em; - } - - void testGaussElimMod() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs modulo { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 } - * --^-- ^ - * 1 1 1 5 - * 2 3 5 8 - * 4 0 5 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(2)}; - lhs = {{Integer(1), Integer(1), Integer(1)}, - {Integer(2), Integer(3), Integer(5)}, - {Integer(4), Integer(0), Integer(5)}}; - std::cout << "matrix 0, modulo 0" << std::endl; // throws - testGaussElimT(Integer(0), rhs, lhs); - std::cout << "matrix 0, modulo 1" << std::endl; - testGaussElimX(Integer(1), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 0, modulo 2" << std::endl; - testGaussElimX(Integer(2), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 0, modulo 3" << std::endl; - testGaussElimX(Integer(3), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 0, modulo 4" << std::endl; // no inverse - testGaussElimX(Integer(4), rhs, lhs, BVGaussElim::Result::INVALID); - std::cout << "matrix 0, modulo 5" << std::endl; - testGaussElimX(Integer(5), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 0, modulo 6" << std::endl; // no inverse - testGaussElimX(Integer(6), rhs, lhs, BVGaussElim::Result::INVALID); - std::cout << "matrix 0, modulo 7" << std::endl; - testGaussElimX(Integer(7), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 0, modulo 8" << std::endl; // no inverse - testGaussElimX(Integer(8), rhs, lhs, BVGaussElim::Result::INVALID); - std::cout << "matrix 0, modulo 9" << std::endl; - testGaussElimX(Integer(9), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 0, modulo 10" << std::endl; // no inverse - testGaussElimX(Integer(10), rhs, lhs, BVGaussElim::Result::INVALID); - std::cout << "matrix 0, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - } - - void testGaussElimUniqueDone() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 17 - * --^--- ^ --^-- ^ - * 1 0 0 4 --> 1 0 0 4 - * 0 1 0 15 0 1 0 15 - * 0 0 1 3 0 0 1 3 - * ------------------------------------------------------------------- */ - rhs = {Integer(4), Integer(15), Integer(3)}; - lhs = {{Integer(1), Integer(0), Integer(0)}, - {Integer(0), Integer(1), Integer(0)}, - {Integer(0), Integer(0), Integer(1)}}; - std::cout << "matrix 1, modulo 17" << std::endl; - testGaussElimX(Integer(17), rhs, lhs, BVGaussElim::Result::UNIQUE); - } - - void testGaussElimUnique() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs modulo { 11,17,59 } - * --^--- ^ - * 2 4 6 18 - * 4 5 6 24 - * 3 1 -2 4 - * ------------------------------------------------------------------- */ - rhs = {Integer(18), Integer(24), Integer(4)}; - lhs = {{Integer(2), Integer(4), Integer(6)}, - {Integer(4), Integer(5), Integer(6)}, - {Integer(3), Integer(1), Integer(-2)}}; - std::cout << "matrix 2, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 2, modulo 17" << std::endl; - testGaussElimX(Integer(17), rhs, lhs, BVGaussElim::Result::UNIQUE); - std::cout << "matrix 2, modulo 59" << std::endl; - testGaussElimX(Integer(59), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * -----^----- ^ ---^--- ^ - * 1 1 2 0 1 --> 1 0 0 0 1 - * 2 -1 0 1 -2 0 1 0 0 2 - * 1 -1 -1 -2 4 0 0 1 0 -1 - * 2 -1 2 -1 0 0 0 0 1 -2 - * ------------------------------------------------------------------- */ - rhs = {Integer(1), Integer(-2), Integer(4), Integer(0)}; - lhs = {{Integer(1), Integer(1), Integer(2), Integer(0)}, - {Integer(2), Integer(-1), Integer(0), Integer(1)}, - {Integer(1), Integer(-1), Integer(-1), Integer(-2)}, - {Integer(2), Integer(-1), Integer(2), Integer(-1)}}; - std::cout << "matrix 3, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - } - - void testGaussElimUniqueZero1() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 0 4 5 2 --> 1 0 0 4 - * 1 1 1 5 0 1 0 3 - * 3 2 5 8 0 0 1 9 - * ------------------------------------------------------------------- */ - rhs = {Integer(2), Integer(5), Integer(8)}; - lhs = {{Integer(0), Integer(4), Integer(5)}, - {Integer(1), Integer(1), Integer(1)}, - {Integer(3), Integer(2), Integer(5)}}; - std::cout << "matrix 4, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 1 1 5 --> 1 0 0 4 - * 0 4 5 2 0 1 0 3 - * 3 2 5 8 0 0 1 9 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(2), Integer(8)}; - lhs = {{Integer(1), Integer(1), Integer(1)}, - {Integer(0), Integer(4), Integer(5)}, - {Integer(3), Integer(2), Integer(5)}}; - std::cout << "matrix 5, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 1 1 5 --> 1 0 0 4 - * 3 2 5 8 0 1 0 9 - * 0 4 5 2 0 0 1 3 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(2)}; - lhs = {{Integer(1), Integer(1), Integer(1)}, - {Integer(3), Integer(2), Integer(5)}, - {Integer(0), Integer(4), Integer(5)}}; - std::cout << "matrix 6, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - } - - void testGaussElimUniqueZero2() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 0 0 5 2 1 0 0 10 - * 1 1 1 5 --> 0 1 0 10 - * 3 2 5 8 0 0 1 7 - * ------------------------------------------------------------------- */ - rhs = {Integer(2), Integer(5), Integer(8)}; - lhs = {{Integer(0), Integer(0), Integer(5)}, - {Integer(1), Integer(1), Integer(1)}, - {Integer(3), Integer(2), Integer(5)}}; - std::cout << "matrix 7, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 1 1 5 --> 1 0 0 10 - * 0 0 5 2 0 1 0 10 - * 3 2 5 8 0 0 1 7 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(2), Integer(8)}; - lhs = {{Integer(1), Integer(1), Integer(1)}, - {Integer(0), Integer(0), Integer(5)}, - {Integer(3), Integer(2), Integer(5)}}; - std::cout << "matrix 8, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 1 1 5 --> 1 0 0 10 - * 3 2 5 8 0 1 0 10 - * 0 0 5 2 0 0 1 7 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(2)}; - lhs = {{Integer(1), Integer(1), Integer(1)}, - {Integer(3), Integer(2), Integer(5)}, - {Integer(0), Integer(0), Integer(5)}}; - std::cout << "matrix 9, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - } - - void testGaussElimUniqueZero3() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 7 - * --^-- ^ --^-- ^ - * 2 0 6 4 1 0 0 3 - * 0 0 0 0 --> 0 0 0 0 - * 4 0 6 3 0 0 1 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(4), Integer(0), Integer(3)}; - lhs = {{Integer(2), Integer(0), Integer(6)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(4), Integer(0), Integer(6)}}; - std::cout << "matrix 10, modulo 7" << std::endl; - testGaussElimX(Integer(7), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 7 - * --^-- ^ --^-- ^ - * 2 6 0 4 1 0 0 3 - * 0 0 0 0 --> 0 0 0 0 - * 4 6 0 3 0 0 1 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(4), Integer(0), Integer(3)}; - lhs = {{Integer(2), Integer(6), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(4), Integer(6), Integer(0)}}; - std::cout << "matrix 11, modulo 7" << std::endl; - testGaussElimX(Integer(7), rhs, lhs, BVGaussElim::Result::UNIQUE); - } - - void testGaussElimUniqueZero4() - { - std::vector rhs, resrhs; - std::vector> lhs, reslhs; - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 0 1 1 5 - * 0 0 0 0 - * 0 0 5 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(0), Integer(2)}; - lhs = {{Integer(0), Integer(1), Integer(1)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(0), Integer(0), Integer(5)}}; - std::cout << "matrix 12, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 0 1 1 5 - * 0 3 5 8 - * 0 0 0 0 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(0)}; - lhs = {{Integer(0), Integer(1), Integer(1)}, - {Integer(0), Integer(3), Integer(5)}, - {Integer(0), Integer(0), Integer(0)}}; - std::cout << "matrix 13, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 0 0 0 0 - * 0 3 5 8 - * 0 0 5 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(0), Integer(8), Integer(2)}; - lhs = {{Integer(0), Integer(0), Integer(0)}, - {Integer(0), Integer(3), Integer(5)}, - {Integer(0), Integer(0), Integer(5)}}; - std::cout << "matrix 14, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 0 1 5 - * 0 0 0 0 - * 4 0 5 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(0), Integer(2)}; - lhs = {{Integer(1), Integer(0), Integer(1)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(4), Integer(0), Integer(5)}}; - std::cout << "matrix 15, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 0 1 5 - * 2 0 5 8 - * 0 0 0 0 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(0)}; - lhs = {{Integer(1), Integer(0), Integer(1)}, - {Integer(2), Integer(0), Integer(5)}, - {Integer(0), Integer(0), Integer(0)}}; - std::cout << "matrix 16, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 0 0 0 0 - * 2 0 5 8 - * 4 0 5 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(0), Integer(8), Integer(2)}; - lhs = {{Integer(0), Integer(0), Integer(0)}, - {Integer(2), Integer(0), Integer(5)}, - {Integer(4), Integer(0), Integer(5)}}; - std::cout << "matrix 17, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 1 0 5 - * 0 0 0 0 - * 4 0 0 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(0), Integer(2)}; - lhs = {{Integer(1), Integer(1), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(4), Integer(0), Integer(0)}}; - std::cout << "matrix 18, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 1 0 5 - * 2 3 0 8 - * 0 0 0 0 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(0)}; - lhs = {{Integer(1), Integer(1), Integer(0)}, - {Integer(2), Integer(3), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}}; - std::cout << "matrix 18, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 0 0 0 0 - * 2 3 0 8 - * 4 0 0 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(0), Integer(8), Integer(2)}; - lhs = {{Integer(0), Integer(0), Integer(0)}, - {Integer(2), Integer(3), Integer(0)}, - {Integer(4), Integer(0), Integer(0)}}; - std::cout << "matrix 19, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 2 - * ----^--- ^ - * 2 4 6 18 0 0 0 0 - * 4 5 6 24 = 0 1 0 0 - * 2 7 12 30 0 1 0 0 - * ------------------------------------------------------------------- */ - rhs = {Integer(18), Integer(24), Integer(30)}; - lhs = {{Integer(2), Integer(4), Integer(6)}, - {Integer(4), Integer(5), Integer(6)}, - {Integer(2), Integer(7), Integer(12)}}; - std::cout << "matrix 20, modulo 2" << std::endl; - resrhs = {Integer(0), Integer(0), Integer(0)}; - reslhs = {{Integer(0), Integer(1), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(2), rhs, lhs, BVGaussElim::Result::UNIQUE, &resrhs, &reslhs); - } - - void testGaussElimUniquePartial() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 7 - * --^-- ^ --^-- ^ - * 2 0 6 4 1 0 0 3 - * 4 0 6 3 0 0 1 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(4), Integer(3)}; - lhs = {{Integer(2), Integer(0), Integer(6)}, - {Integer(4), Integer(0), Integer(6)}}; - std::cout << "matrix 21, modulo 7" << std::endl; - testGaussElimX(Integer(7), rhs, lhs, BVGaussElim::Result::UNIQUE); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 7 - * --^-- ^ --^-- ^ - * 2 6 0 4 1 0 0 3 - * 4 6 0 3 0 1 0 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(4), Integer(3)}; - lhs = {{Integer(2), Integer(6), Integer(0)}, - {Integer(4), Integer(6), Integer(0)}}; - std::cout << "matrix 22, modulo 7" << std::endl; - testGaussElimX(Integer(7), rhs, lhs, BVGaussElim::Result::UNIQUE); - } - - void testGaussElimNone() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs modulo 9 - * --^--- ^ - * 2 4 6 18 --> not coprime (no inverse) - * 4 5 6 24 - * 3 1 -2 4 - * ------------------------------------------------------------------- */ - rhs = {Integer(18), Integer(24), Integer(4)}; - lhs = {{Integer(2), Integer(4), Integer(6)}, - {Integer(4), Integer(5), Integer(6)}, - {Integer(3), Integer(1), Integer(-2)}}; - std::cout << "matrix 23, modulo 9" << std::endl; - testGaussElimX(Integer(9), rhs, lhs, BVGaussElim::Result::INVALID); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 59 - * ----^--- ^ - * 1 -2 -6 12 --> no solution - * 2 4 12 -17 - * 1 -4 -12 22 - * ------------------------------------------------------------------- */ - rhs = {Integer(12), Integer(-17), Integer(22)}; - lhs = {{Integer(1), Integer(-2), Integer(-6)}, - {Integer(2), Integer(4), Integer(12)}, - {Integer(1), Integer(-4), Integer(-12)}}; - std::cout << "matrix 24, modulo 59" << std::endl; - testGaussElimX(Integer(59), rhs, lhs, BVGaussElim::Result::NONE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 9 - * ----^--- ^ - * 2 4 6 18 --> not coprime (no inverse) - * 4 5 6 24 - * 2 7 12 30 - * ------------------------------------------------------------------- */ - rhs = {Integer(18), Integer(24), Integer(30)}; - lhs = {{Integer(2), Integer(4), Integer(6)}, - {Integer(4), Integer(5), Integer(6)}, - {Integer(2), Integer(7), Integer(12)}}; - std::cout << "matrix 25, modulo 9" << std::endl; - testGaussElimX(Integer(9), rhs, lhs, BVGaussElim::Result::INVALID); - } - - void testGaussElimNoneZero() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 0 1 1 5 - * 0 3 5 8 - * 0 0 5 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(2)}; - lhs = {{Integer(0), Integer(1), Integer(1)}, - {Integer(0), Integer(3), Integer(5)}, - {Integer(0), Integer(0), Integer(5)}}; - std::cout << "matrix 26, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::NONE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 0 1 5 - * 2 0 5 8 - * 4 0 5 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(2)}; - lhs = {{Integer(1), Integer(0), Integer(1)}, - {Integer(2), Integer(0), Integer(5)}, - {Integer(4), Integer(0), Integer(5)}}; - std::cout << "matrix 27, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::NONE); - - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 1 0 5 - * 2 3 0 8 - * 4 0 0 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8), Integer(2)}; - lhs = {{Integer(1), Integer(1), Integer(0)}, - {Integer(2), Integer(3), Integer(0)}, - {Integer(4), Integer(0), Integer(0)}}; - std::cout << "matrix 28, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::NONE); - } - - void testGaussElimPartial1() - { - std::vector rhs, resrhs; - std::vector> lhs, reslhs; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * ------------------------------------------------------------------- */ - rhs = {Integer(7), Integer(9)}; - lhs = {{Integer(1), Integer(0), Integer(9)}, - {Integer(0), Integer(1), Integer(3)}}; - std::cout << "matrix 29, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::PARTIAL); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 3 0 7 --> 1 3 0 7 - * 0 0 1 9 0 0 1 9 - * ------------------------------------------------------------------- */ - rhs = {Integer(7), Integer(9)}; - lhs = {{Integer(1), Integer(3), Integer(0)}, - {Integer(0), Integer(0), Integer(1)}}; - std::cout << "matrix 30, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::PARTIAL); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 1 1 5 --> 1 0 9 7 - * 2 3 5 8 0 1 3 9 - * ------------------------------------------------------------------- */ - rhs = {Integer(5), Integer(8)}; - lhs = {{Integer(1), Integer(1), Integer(1)}, - {Integer(2), Integer(3), Integer(5)}}; - std::cout << "matrix 31, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::PARTIAL); - - /* ------------------------------------------------------------------- - * lhs rhs modulo { 3, 5, 7, 11, 17, 31, 59 } - * ----^--- ^ - * 2 4 6 18 - * 4 5 6 24 - * 2 7 12 30 - * ------------------------------------------------------------------- */ - rhs = {Integer(18), Integer(24), Integer(30)}; - lhs = {{Integer(2), Integer(4), Integer(6)}, - {Integer(4), Integer(5), Integer(6)}, - {Integer(2), Integer(7), Integer(12)}}; - std::cout << "matrix 32, modulo 3" << std::endl; - resrhs = {Integer(0), Integer(0), Integer(0)}; - reslhs = {{Integer(1), Integer(2), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(3), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); - resrhs = {Integer(1), Integer(4), Integer(0)}; - std::cout << "matrix 32, modulo 5" << std::endl; - reslhs = {{Integer(1), Integer(0), Integer(4)}, - {Integer(0), Integer(1), Integer(2)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(5), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); - std::cout << "matrix 32, modulo 7" << std::endl; - reslhs = {{Integer(1), Integer(0), Integer(6)}, - {Integer(0), Integer(1), Integer(2)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(7), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); - std::cout << "matrix 32, modulo 11" << std::endl; - reslhs = {{Integer(1), Integer(0), Integer(10)}, - {Integer(0), Integer(1), Integer(2)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(11), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); - std::cout << "matrix 32, modulo 17" << std::endl; - reslhs = {{Integer(1), Integer(0), Integer(16)}, - {Integer(0), Integer(1), Integer(2)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(17), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); - std::cout << "matrix 32, modulo 59" << std::endl; - reslhs = {{Integer(1), Integer(0), Integer(58)}, - {Integer(0), Integer(1), Integer(2)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(59), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 3 - * ----^--- ^ --^-- ^ - * 4 6 2 18 --> 1 0 2 0 - * 5 6 4 24 0 0 0 0 - * 7 12 2 30 0 0 0 0 - * ------------------------------------------------------------------- */ - rhs = {Integer(18), Integer(24), Integer(30)}; - lhs = {{Integer(4), Integer(6), Integer(2)}, - {Integer(5), Integer(6), Integer(4)}, - {Integer(7), Integer(12), Integer(2)}}; - std::cout << "matrix 33, modulo 3" << std::endl; - resrhs = {Integer(0), Integer(0), Integer(0)}; - reslhs = {{Integer(1), Integer(0), Integer(2)}, - {Integer(0), Integer(0), Integer(0)}, - {Integer(0), Integer(0), Integer(0)}}; - testGaussElimX( - Integer(3), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); - } - - void testGaussElimPartial2() - { - std::vector rhs; - std::vector> lhs; - - /* ------------------------------------------------------------------- - * lhs rhs --> lhs rhs modulo 11 - * ---^--- ^ ---^--- ^ - * x y z w x y z w - * 1 2 0 6 2 1 2 0 0 1 - * 0 0 2 2 2 0 0 1 0 10 - * 0 0 0 1 2 0 0 0 1 2 - * ------------------------------------------------------------------- */ - rhs = {Integer(2), Integer(2), Integer(2)}; - lhs = {{Integer(1), Integer(2), Integer(6), Integer(0)}, - {Integer(0), Integer(0), Integer(2), Integer(2)}, - {Integer(0), Integer(0), Integer(1), Integer(0)}}; - std::cout << "matrix 34, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::PARTIAL); - } - void testGaussElimRewriteForUremUnique1() - { - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 1 1 5 - * 2 3 5 8 - * 4 0 5 2 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), - d_z_mul_one), - d_p), - d_five); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), - d_z_mul_five), - d_p), - d_eight); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), - d_p), - d_two); - - std::vector eqs = {eq1, eq2, eq3}; - std::unordered_map res; - BVGaussElim::Result ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::UNIQUE); - TS_ASSERT(res.size() == 3); - TS_ASSERT(res[d_x] == d_three32); - TS_ASSERT(res[d_y] == d_four32); - TS_ASSERT(res[d_z] == d_nine32); - } - - void testGaussElimRewriteForUremUnique2() - { - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 1 1 5 - * 2 3 5 8 - * 4 0 5 2 - * ------------------------------------------------------------------- */ - - Node zextop6 = d_nm->mkConst(BitVectorZeroExtend(6)); - - Node p = d_nm->mkNode(zextop6, mkConcat(mkZero(6), - d_nm->mkNode(kind::BITVECTOR_PLUS, mkConst(20, 7), mkConst(20, 4)))); - - Node x_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, - d_nm->mkNode(kind::BITVECTOR_SUB, d_five, d_four), d_x); - Node y_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, - d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, d_one, d_five), d_y); - Node z_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, mkOne(32), d_z); - - Node x_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, - d_nm->mkNode(kind::BITVECTOR_SHL, mkOne(32), mkOne(32)), d_x); - Node y_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, - d_nm->mkNode(kind::BITVECTOR_LSHR, mkOnes(32), mkConst(32, 30)), d_y); - Node z_mul_five = d_nm->mkNode(kind::BITVECTOR_MULT, - mkExtract( - d_nm->mkNode( - zextop6, d_nm->mkNode(kind::BITVECTOR_PLUS, d_three, d_two)), - 31, 0), - d_z); - - Node x_mul_four = d_nm->mkNode(kind::BITVECTOR_MULT, - d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_MULT, - mkConst(32, 4), - mkConst(32, 5)), - mkConst(32, 4)), - mkConst(32, 6)), - d_x); - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, - x_mul_one, - y_mul_one), - z_mul_one), - p), - d_five); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, x_mul_two, y_mul_three), - z_mul_five), - p), - d_eight); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, x_mul_four, z_mul_five), - d_p), - d_two); - - std::vector eqs = {eq1, eq2, eq3}; - std::unordered_map res; - BVGaussElim::Result ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::UNIQUE); - TS_ASSERT(res.size() == 3); - TS_ASSERT(res[d_x] == d_three32); - TS_ASSERT(res[d_y] == d_four32); - TS_ASSERT(res[d_z] == d_nine32); - } - - void testGaussElimRewriteForUremPartial1() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine), - d_p), - d_seven); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three), - d_p), - d_nine); - - std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 2); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_seven32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), - d_p); - Node y1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nine32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), - d_p); - - Node x2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), - d_p); - Node z2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), - d_p); - - Node y3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), - d_p); - Node z3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), - d_p); - - /* result depends on order of variables in matrix */ - if (res.find(d_x) == res.end()) - { - /* - * y z x y z x - * 0 9 1 7 --> 1 0 7 3 - * 1 3 0 9 0 1 5 2 - * - * z y x z y x - * 9 0 1 7 --> 1 0 5 2 - * 3 1 0 9 0 1 7 3 - */ - TS_ASSERT(res[d_y] == y3); - TS_ASSERT(res[d_z] == z3); - } - else if (res.find(d_y) == res.end()) - { - /* - * x z y x z y - * 1 9 0 7 --> 1 0 8 2 - * 0 3 1 9 0 1 4 3 - * - * z x y z x y - * 9 1 0 7 --> 1 0 4 3 - * 3 0 1 9 0 1 8 2 - */ - TS_ASSERT(res[d_x] == x2); - TS_ASSERT(res[d_z] == z2); - } - else - { - TS_ASSERT(res.find(d_z) == res.end()); - /* - * x y z x y z - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * - * y x z y x z - * 0 1 9 7 --> 1 0 3 9 - * 1 0 3 9 0 1 9 7 - */ - TS_ASSERT(res[d_x] == x1); - TS_ASSERT(res[d_y] == y1); - } - } - - void testGaussElimRewriteForUremPartial1a() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x, d_z_mul_nine), - d_p), - d_seven); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_y, d_z_mul_three), - d_p), - d_nine); - - std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 2); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_seven32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), - d_p); - Node y1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nine32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), - d_p); - - Node x2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), - d_p); - Node z2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), - d_p); - - Node y3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), - d_p); - Node z3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), - d_p); - - /* result depends on order of variables in matrix */ - if (res.find(d_x) == res.end()) - { - /* - * y z x y z x - * 0 9 1 7 --> 1 0 7 3 - * 1 3 0 9 0 1 5 2 - * - * z y x z y x - * 9 0 1 7 --> 1 0 5 2 - * 3 1 0 9 0 1 7 3 - */ - TS_ASSERT(res[d_y] == y3); - TS_ASSERT(res[d_z] == z3); - } - else if (res.find(d_y) == res.end()) - { - /* - * x z y x z y - * 1 9 0 7 --> 1 0 8 2 - * 0 3 1 9 0 1 4 3 - * - * z x y z x y - * 9 1 0 7 --> 1 0 4 3 - * 3 0 1 9 0 1 8 2 - */ - TS_ASSERT(res[d_x] == x2); - TS_ASSERT(res[d_z] == z2); - } - else - { - TS_ASSERT(res.find(d_z) == res.end()); - /* - * x y z x y z - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * - * y x z y x z - * 0 1 9 7 --> 1 0 3 9 - * 1 0 3 9 0 1 9 7 - */ - TS_ASSERT(res[d_x] == x1); - TS_ASSERT(res[d_y] == y1); - } - } - - void testGaussElimRewriteForUremPartial2() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 3 0 7 --> 1 3 0 7 - * 0 0 1 9 0 0 1 9 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_three), - d_p), - d_seven); - - Node eq2 = - d_nm->mkNode(kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, d_z_mul_one, d_p), - d_nine); - - std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 2); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_seven32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_eight32)), - d_p); - Node y2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_six32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_seven32)), - d_p); - - /* result depends on order of variables in matrix */ - if (res.find(d_x) == res.end()) - { - /* - * x y z x y z - * 1 3 0 7 --> 1 3 0 7 - * 0 0 1 9 0 0 1 9 - * - * x z y x z y - * 1 0 3 7 --> 1 0 3 7 - * 0 1 0 9 0 1 0 9 - * - * z x y z x y - * 0 1 3 7 --> 1 0 0 9 - * 1 0 0 9 0 1 3 7 - */ - TS_ASSERT(res[d_y] == y2); - TS_ASSERT(res[d_z] == d_nine32); - } - else if (res.find(d_y) == res.end()) - { - /* - * z y x z y x - * 0 3 1 7 --> 1 0 0 9 - * 1 0 0 9 0 1 4 6 - * - * y x z y x z - * 3 1 0 7 --> 1 4 0 6 - * 0 0 1 9 0 0 1 9 - * - * y z x y z x - * 3 0 1 7 --> 1 0 4 6 - * 0 1 0 9 0 1 0 9 - */ - TS_ASSERT(res[d_x] == x1); - TS_ASSERT(res[d_z] == d_nine32); - } - else - { - TS_ASSERT(false); - } - } - - void testGaussElimRewriteForUremPartial3() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 1 1 5 --> 1 0 9 7 - * 2 3 5 8 0 1 3 9 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y), - d_z_mul_one), - d_p), - d_five); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), - d_z_mul_five), - d_p), - d_eight); - - std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 2); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_seven32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), - d_p); - Node y1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nine32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), - d_p); - Node x2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), - d_p); - Node z2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), - d_p); - Node y3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), - d_p); - Node z3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), - d_p); - - /* result depends on order of variables in matrix */ - if (res.find(d_x) == res.end()) - { - /* - * y z x y z x - * 1 1 1 5 --> 1 0 7 3 - * 3 5 2 8 0 1 5 2 - * - * z y x z y x - * 1 1 1 5 --> 1 0 5 2 - * 5 3 2 8 0 1 7 3 - */ - TS_ASSERT(res[d_y] == y3); - TS_ASSERT(res[d_z] == z3); - } - else if (res.find(d_y) == res.end()) - { - /* - * x z y x z y - * 1 1 1 5 --> 1 0 8 2 - * 2 5 3 8 0 1 4 3 - * - * z x y z x y - * 1 1 1 5 --> 1 0 4 3 - * 5 2 3 9 0 1 8 2 - */ - TS_ASSERT(res[d_x] == x2); - TS_ASSERT(res[d_z] == z2); - } - else - { - TS_ASSERT(res.find(d_z) == res.end()); - /* - * x y z x y z - * 1 1 1 5 --> 1 0 9 7 - * 2 3 5 8 0 1 3 9 - * - * y x z y x z - * 1 1 1 5 --> 1 0 3 9 - * 3 2 5 8 0 1 9 7 - */ - TS_ASSERT(res[d_x] == x1); - TS_ASSERT(res[d_y] == y1); - } - } - - void testGaussElimRewriteForUremPartial4() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * ----^--- ^ ---^--- ^ - * 2 4 6 18 --> 1 0 10 1 - * 4 5 6 24 0 1 2 4 - * 2 7 12 30 0 0 0 0 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four), - d_z_mul_six), - d_p), - d_eighteen); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five), - d_z_mul_six), - d_p), - d_twentyfour); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven), - d_z_mul_twelve), - d_p), - d_thirty); - - std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 2); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_one32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_one32)), - d_p); - Node y1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_four32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_nine32)), - d_p); - Node x2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)), - d_p); - Node z2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_five32)), - d_p); - Node y3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_six32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_nine32)), - d_p); - Node z3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_ten32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_one32)), - d_p); - - /* result depends on order of variables in matrix */ - if (res.find(d_x) == res.end()) - { - /* - * y z x y z x - * 4 6 2 18 --> 1 0 2 6 - * 5 6 4 24 0 1 10 10 - * 7 12 2 30 0 0 0 0 - * - * z y x z y x - * 6 4 2 18 --> 1 0 10 10 - * 6 5 4 24 0 1 2 6 - * 12 12 2 30 0 0 0 0 - * - */ - TS_ASSERT(res[d_y] == y3); - TS_ASSERT(res[d_z] == z3); - } - else if (res.find(d_y) == res.end()) - { - /* - * x z y x z y - * 2 6 4 18 --> 1 0 6 3 - * 4 6 5 24 0 1 6 2 - * 2 12 7 30 0 0 0 0 - * - * z x y z x y - * 6 2 4 18 --> 1 0 6 2 - * 6 4 5 24 0 1 6 3 - * 12 2 12 30 0 0 0 0 - * - */ - TS_ASSERT(res[d_x] == x2); - TS_ASSERT(res[d_z] == z2); - } - else - { - TS_ASSERT(res.find(d_z) == res.end()); - /* - * x y z x y z - * 2 4 6 18 --> 1 0 10 1 - * 4 5 6 24 0 1 2 4 - * 2 7 12 30 0 0 0 0 - * - * y x z y x z - * 4 2 6 18 --> 1 0 2 49 - * 5 4 6 24 0 1 10 1 - * 7 2 12 30 0 0 0 0 - */ - TS_ASSERT(res[d_x] == x1); - TS_ASSERT(res[d_y] == y1); - } - } - - void testGaussElimRewriteForUremPartial5() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 3 - * ----^--- ^ --^-- ^ - * 2 4 6 18 --> 1 2 0 0 - * 4 5 6 24 0 0 0 0 - * 2 7 12 30 0 0 0 0 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_four), - d_z_mul_six), - d_three), - d_eighteen); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_y_mul_five), - d_z_mul_six), - d_three), - d_twentyfour); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_seven), - d_z_mul_twelve), - d_three), - d_thirty); - - std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 1); - - Node x1 = d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_one32), - d_three); - Node y2 = d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_one32), - d_three); - - /* result depends on order of variables in matrix */ - if (res.find(d_x) == res.end()) - { - /* - * y x z y x z - * 4 2 6 18 --> 1 2 0 0 - * 5 4 6 24 0 0 0 0 - * 7 2 12 30 0 0 0 0 - * - * y z x y z x - * 4 6 2 18 --> 1 0 2 0 - * 5 6 4 24 0 0 0 0 - * 7 12 2 30 0 0 0 0 - * - * z y x z y x - * 6 4 2 18 --> 0 1 2 0 - * 6 5 4 24 0 0 0 0 - * 12 12 2 30 0 0 0 0 - * - */ - TS_ASSERT(res[d_y] == y2); - } - else if (res.find(d_y) == res.end()) - { - /* - * x y z x y z - * 2 4 6 18 --> 1 2 0 0 - * 4 5 6 24 0 0 0 0 - * 2 7 12 30 0 0 0 0 - * - * x z y x z y - * 2 6 4 18 --> 1 0 2 0 - * 4 6 5 24 0 0 0 0 - * 2 12 7 30 0 0 0 0 - * - * z x y z x y - * 6 2 4 18 --> 0 1 2 0 - * 6 4 5 24 0 0 0 0 - * 12 2 12 30 0 0 0 0 - * - */ - TS_ASSERT(res[d_x] == x1); - } - else - { - TS_ASSERT(false); - } - } - - void testGaussElimRewriteForUremPartial6() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs --> lhs rhs modulo 11 - * ---^--- ^ ---^--- ^ - * x y z w x y z w - * 1 2 0 6 2 1 2 0 6 2 - * 0 0 2 2 2 0 0 1 1 1 - * 0 0 0 1 2 0 0 0 1 2 - * ------------------------------------------------------------------- */ - - Node y_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_two); - Node z_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two); - Node w = mkConcat(d_zero, d_nm->mkVar("w", d_nm->mkBitVectorType(16))); - Node w_mul_six = d_nm->mkNode(kind::BITVECTOR_MULT, w, d_six); - Node w_mul_two = d_nm->mkNode(kind::BITVECTOR_MULT, w, d_two); - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, y_mul_two), - w_mul_six), - d_p), - d_two); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, z_mul_two, w_mul_two), - d_p), - d_two); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, w, d_p), - d_two); - - std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 3); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_one32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_nine32)), - d_p); - Node z1 = d_ten32; - Node w1 = d_two32; - - Node y2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_six32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_five32)), - d_p); - Node z2 = d_ten32; - Node w2 = d_two32; - - /* result depends on order of variables in matrix */ - if (res.find(d_x) == res.end()) - { - TS_ASSERT(res[d_y] == y2); - TS_ASSERT(res[d_z] == z2); - TS_ASSERT(res[w] == w2); - } - else if (res.find(d_y) == res.end()) - { - TS_ASSERT(res[d_x] == x1); - TS_ASSERT(res[d_z] == z1); - TS_ASSERT(res[w] == w1); - } - else - { - TS_ASSERT(false); - } - } - - void testGaussElimRewriteForUremWithExprPartial() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * ------------------------------------------------------------------- */ - - Node zero = mkZero(8); - Node xx = d_nm->mkVar("xx", d_nm->mkBitVectorType(8)); - Node yy = d_nm->mkVar("yy", d_nm->mkBitVectorType(8)); - Node zz = d_nm->mkVar("zz", d_nm->mkBitVectorType(8)); - - Node x = - mkConcat(d_zero, mkConcat(zero, mkExtract(mkConcat(zero, xx), 7, 0))); - Node y = - mkConcat(d_zero, mkConcat(zero, mkExtract(mkConcat(zero, yy), 7, 0))); - Node z = - mkConcat(d_zero, mkConcat(zero, mkExtract(mkConcat(zero, zz), 7, 0))); - Node x_mul_one = d_nm->mkNode(kind::BITVECTOR_MULT, x, d_one32); - Node nine_mul_z = d_nm->mkNode(kind::BITVECTOR_MULT, d_nine32, z); - Node one_mul_y = d_nm->mkNode(kind::BITVECTOR_MULT, d_one, y); - Node z_mul_three = d_nm->mkNode(kind::BITVECTOR_MULT, z, d_three); - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, x_mul_one, nine_mul_z), - d_p), - d_seven); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, one_mul_y, z_mul_three), - d_p), - d_nine); - - std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 2); - - x = Rewriter::rewrite(x); - y = Rewriter::rewrite(y); - z = Rewriter::rewrite(z); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_seven32, - d_nm->mkNode(kind::BITVECTOR_MULT, z, d_two32)), - d_p); - Node y1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nine32, - d_nm->mkNode(kind::BITVECTOR_MULT, z, d_eight32)), - d_p); - - Node x2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, y, d_three32)), - d_p); - Node z2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, y, d_seven32)), - d_p); - - Node y3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, x, d_four32)), - d_p); - Node z3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, x, d_six32)), - d_p); - - /* result depends on order of variables in matrix */ - if (res.find(x) == res.end()) - { - /* - * y z x y z x - * 0 9 1 7 --> 1 0 7 3 - * 1 3 0 9 0 1 5 2 - * - * z y x z y x - * 9 0 1 7 --> 1 0 5 2 - * 3 1 0 9 0 1 7 3 - */ - TS_ASSERT(res[Rewriter::rewrite(y)] == y3); - TS_ASSERT(res[Rewriter::rewrite(z)] == z3); - } - else if (res.find(y) == res.end()) - { - /* - * x z y x z y - * 1 9 0 7 --> 1 0 8 2 - * 0 3 1 9 0 1 4 3 - * - * z x y z x y - * 9 1 0 7 --> 1 0 4 3 - * 3 0 1 9 0 1 8 2 - */ - TS_ASSERT(res[x] == x2); - TS_ASSERT(res[z] == z2); - } - else - { - TS_ASSERT(res.find(z) == res.end()); - /* - * x y z x y z - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * - * y x z y x z - * 0 1 9 7 --> 1 0 3 9 - * 1 0 3 9 0 1 9 7 - */ - TS_ASSERT(res[x] == x1); - TS_ASSERT(res[y] == y1); - } - } - - void testGaussElimRewriteForUremNAryPartial() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * ------------------------------------------------------------------- */ - - Node zero = mkZero(8); - Node xx = d_nm->mkVar("xx", d_nm->mkBitVectorType(8)); - Node yy = d_nm->mkVar("yy", d_nm->mkBitVectorType(8)); - Node zz = d_nm->mkVar("zz", d_nm->mkBitVectorType(8)); - - Node x = mkConcat( - d_zero, - mkConcat( - zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, xx), 7, 0))); - Node y = mkConcat( - d_zero, - mkConcat( - zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, yy), 7, 0))); - Node z = mkConcat( - d_zero, - mkConcat( - zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0))); - - NodeBuilder<> nbx(d_nm, kind::BITVECTOR_MULT); - nbx << d_x << d_one << x; - Node x_mul_one_mul_xx = nbx.constructNode(); - NodeBuilder<> nby(d_nm, kind::BITVECTOR_MULT); - nby << d_y << y << d_one; - Node y_mul_yy_mul_one = nby.constructNode(); - NodeBuilder<> nbz(d_nm, kind::BITVECTOR_MULT); - nbz << d_three << d_z << z; - Node three_mul_z_mul_zz = nbz.constructNode(); - NodeBuilder<> nbz2(d_nm, kind::BITVECTOR_MULT); - nbz2 << d_z << d_nine << z; - Node z_mul_nine_mul_zz = nbz2.constructNode(); - - Node x_mul_xx = d_nm->mkNode(kind::BITVECTOR_MULT, d_x, x); - Node y_mul_yy = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, y); - Node z_mul_zz = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, z); - - Node eq1 = d_nm->mkNode(kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - x_mul_one_mul_xx, - z_mul_nine_mul_zz), - d_p), - d_seven); - - Node eq2 = d_nm->mkNode(kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - y_mul_yy_mul_one, - three_mul_z_mul_zz), - d_p), - d_nine); - - std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); - TS_ASSERT(res.size() == 2); - - x_mul_xx = Rewriter::rewrite(x_mul_xx); - y_mul_yy = Rewriter::rewrite(y_mul_yy); - z_mul_zz = Rewriter::rewrite(z_mul_zz); - - Node x1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_seven32, - d_nm->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_two32)), - d_p); - Node y1 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nine32, - d_nm->mkNode(kind::BITVECTOR_MULT, z_mul_zz, d_eight32)), - d_p); - - Node x2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_three32)), - d_p); - Node z2 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, y_mul_yy, d_seven32)), - d_p); - - Node y3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_four32)), - d_p); - Node z3 = d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, x_mul_xx, d_six32)), - d_p); - - /* result depends on order of variables in matrix */ - if (res.find(x_mul_xx) == res.end()) - { - /* - * y z x y z x - * 0 9 1 7 --> 1 0 7 3 - * 1 3 0 9 0 1 5 2 - * - * z y x z y x - * 9 0 1 7 --> 1 0 5 2 - * 3 1 0 9 0 1 7 3 - */ - TS_ASSERT(res[y_mul_yy] == y3); - TS_ASSERT(res[z_mul_zz] == z3); - } - else if (res.find(y_mul_yy) == res.end()) - { - /* - * x z y x z y - * 1 9 0 7 --> 1 0 8 2 - * 0 3 1 9 0 1 4 3 - * - * z x y z x y - * 9 1 0 7 --> 1 0 4 3 - * 3 0 1 9 0 1 8 2 - */ - TS_ASSERT(res[x_mul_xx] == x2); - TS_ASSERT(res[z_mul_zz] == z2); - } - else - { - TS_ASSERT(res.find(z_mul_zz) == res.end()); - /* - * x y z x y z - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * - * y x z y x z - * 0 1 9 7 --> 1 0 3 9 - * 1 0 3 9 0 1 9 7 - */ - TS_ASSERT(res[x_mul_xx] == x1); - TS_ASSERT(res[y_mul_yy] == y1); - } - } - - void testGaussElimRewriteForUremNotInvalid1() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * 3x / 2z = 4 modulo 11 - * 2x % 5y = 2 - * y O z = 5 - * ------------------------------------------------------------------- */ - - Node n1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, - d_nm->mkNode(kind::BITVECTOR_MULT, d_three, d_x), - d_nm->mkNode(kind::BITVECTOR_MULT, d_two, d_y)); - Node n2 = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, - d_nm->mkNode(kind::BITVECTOR_MULT, d_two, d_x), - d_nm->mkNode(kind::BITVECTOR_MULT, d_five, d_y)); - Node n3 = mkConcat( - d_zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, d_y, d_z), 15, 0)); - - Node eq1 = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n1, d_p), d_four); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n2, d_p), d_two); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, d_nm->mkNode(kind::BITVECTOR_UREM, n3, d_p), d_five); - - std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::UNIQUE); - TS_ASSERT(res.size() == 3); - - TS_ASSERT(res[n1] == d_four32); - TS_ASSERT(res[n2] == d_two32); - TS_ASSERT(res[n3] == d_five32); - } - - void testGaussElimRewriteForUremNotInvalid2() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * x*y = 4 modulo 11 - * x*y*z = 2 - * 2*x*y + 2*z = 9 - * ------------------------------------------------------------------- */ - - Node zero32 = mkZero(32); - - Node x = mkConcat(zero32, d_nm->mkVar("x", d_nm->mkBitVectorType(16))); - Node y = mkConcat(zero32, d_nm->mkVar("y", d_nm->mkBitVectorType(16))); - Node z = mkConcat(zero32, d_nm->mkVar("z", d_nm->mkBitVectorType(16))); - - Node n1 = d_nm->mkNode(kind::BITVECTOR_MULT, x, y); - Node n2 = d_nm->mkNode( - kind::BITVECTOR_MULT, d_nm->mkNode(kind::BITVECTOR_MULT, x, y), z); - Node n3 = d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_MULT, - d_nm->mkNode(kind::BITVECTOR_MULT, x, y), - mkConcat(d_zero, d_two)), - d_nm->mkNode(kind::BITVECTOR_MULT, mkConcat(d_zero, d_two), z)); - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, n1, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_four)); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, n2, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_two)); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, n3, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_nine)); - - std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::UNIQUE); - TS_ASSERT(res.size() == 3); - - n1 = Rewriter::rewrite(n1); - n2 = Rewriter::rewrite(n2); - z = Rewriter::rewrite(z); - - TS_ASSERT(res[n1] == mkConst(48, 4)); - TS_ASSERT(res[n2] == mkConst(48, 2)); - - Integer twoxy = (res[n1].getConst().getValue() * Integer(2)) - .euclidianDivideRemainder(Integer(48)); - Integer twoz = (res[z].getConst().getValue() * Integer(2)) - .euclidianDivideRemainder(Integer(48)); - Integer r = (twoxy + twoz).euclidianDivideRemainder(Integer(11)); - TS_ASSERT(r == Integer(9)); - } - - void testGaussElimRewriteForUremInvalid() - { - std::unordered_map res; - BVGaussElim::Result ret; - - /* ------------------------------------------------------------------- - * x*y = 4 modulo 11 - * x*y*z = 2 - * 2*x*y = 9 - * ------------------------------------------------------------------- */ - - Node zero32 = mkZero(32); - - Node x = mkConcat(zero32, d_nm->mkVar("x", d_nm->mkBitVectorType(16))); - Node y = mkConcat(zero32, d_nm->mkVar("y", d_nm->mkBitVectorType(16))); - Node z = mkConcat(zero32, d_nm->mkVar("z", d_nm->mkBitVectorType(16))); - - Node n1 = d_nm->mkNode(kind::BITVECTOR_MULT, x, y); - Node n2 = d_nm->mkNode( - kind::BITVECTOR_MULT, d_nm->mkNode(kind::BITVECTOR_MULT, x, y), z); - Node n3 = d_nm->mkNode(kind::BITVECTOR_MULT, - d_nm->mkNode(kind::BITVECTOR_MULT, x, y), - mkConcat(d_zero, d_two)); - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, n1, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_four)); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, n2, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_two)); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, n3, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_nine)); - - std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::INVALID); - } - - void testGaussElimRewriteUnique1() - { - /* ------------------------------------------------------------------- - * lhs rhs modulo 11 - * --^-- ^ - * 1 1 1 5 - * 2 3 5 8 - * 4 0 5 2 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), - d_z_mul_one), - d_p), - d_five); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), - d_z_mul_five), - d_p), - d_eight); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), - d_p), - d_two); - - Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - - std::vector ass = {a}; - std::unordered_map res; - BVGaussElim::gaussElimRewrite(ass); - Node resx = d_nm->mkNode( - kind::EQUAL, d_x, d_nm->mkConst(BitVector(32, 3u))); - Node resy = d_nm->mkNode( - kind::EQUAL, d_y, d_nm->mkConst(BitVector(32, 4u))); - Node resz = d_nm->mkNode( - kind::EQUAL, d_z, d_nm->mkConst(BitVector(32, 9u))); - TS_ASSERT(ass.size() == 4); - TS_ASSERT(std::find(ass.begin(), ass.end(), resx) != ass.end()); - TS_ASSERT(std::find(ass.begin(), ass.end(), resy) != ass.end()); - TS_ASSERT(std::find(ass.begin(), ass.end(), resz) != ass.end()); - } - - void testGaussElimRewriteUnique2() - { - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 1 1 5 1 0 0 3 - * 2 3 5 8 0 1 0 4 - * 4 0 5 2 0 0 1 9 - * - * lhs rhs lhs rhs modulo 7 - * --^-- ^ --^-- ^ - * 2 6 0 4 1 0 0 3 - * 4 6 0 3 0 1 0 2 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_y_mul_one), - d_z_mul_one), - d_p), - d_five); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode( - kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, d_y_mul_three), - d_z_mul_five), - d_p), - d_eight); - - Node eq3 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, d_z_mul_five), - d_p), - d_two); - - Node y_mul_six = d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_six); - - Node eq4 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode(kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_two, y_mul_six), - d_seven), - d_four); - - Node eq5 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_four, y_mul_six), - d_seven), - d_three); - - Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - - std::vector ass = {a, eq4, eq5}; - std::unordered_map res; - BVGaussElim::gaussElimRewrite(ass); - Node resx1 = d_nm->mkNode( - kind::EQUAL, d_x, d_nm->mkConst(BitVector(32, 3u))); - Node resx2 = d_nm->mkNode( - kind::EQUAL, d_x, d_nm->mkConst(BitVector(32, 3u))); - Node resy1 = d_nm->mkNode( - kind::EQUAL, d_y, d_nm->mkConst(BitVector(32, 4u))); - Node resy2 = d_nm->mkNode( - kind::EQUAL, d_y, d_nm->mkConst(BitVector(32, 2u))); - Node resz = d_nm->mkNode( - kind::EQUAL, d_z, d_nm->mkConst(BitVector(32, 9u))); - TS_ASSERT(ass.size() == 8); - TS_ASSERT(std::find(ass.begin(), ass.end(), resx1) != ass.end()); - TS_ASSERT(std::find(ass.begin(), ass.end(), resx2) != ass.end()); - TS_ASSERT(std::find(ass.begin(), ass.end(), resy1) != ass.end()); - TS_ASSERT(std::find(ass.begin(), ass.end(), resy2) != ass.end()); - TS_ASSERT(std::find(ass.begin(), ass.end(), resz) != ass.end()); - } - - void testGaussElimRewritePartial() - { - /* ------------------------------------------------------------------- - * lhs rhs lhs rhs modulo 11 - * --^-- ^ --^-- ^ - * 1 0 9 7 --> 1 0 9 7 - * 0 1 3 9 0 1 3 9 - * ------------------------------------------------------------------- */ - - Node eq1 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_x_mul_one, d_z_mul_nine), - d_p), - d_seven); - - Node eq2 = d_nm->mkNode( - kind::EQUAL, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, d_y_mul_one, d_z_mul_three), - d_p), - d_nine); - - std::vector ass = {eq1, eq2}; - BVGaussElim::gaussElimRewrite(ass); - TS_ASSERT(ass.size() == 4); - - Node resx1 = d_nm->mkNode( - kind::EQUAL, - d_x, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_seven32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_two32)), - d_p)); - Node resy1 = d_nm->mkNode( - kind::EQUAL, - d_y, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nine32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_eight32)), - d_p)); - - Node resx2 = d_nm->mkNode( - kind::EQUAL, - d_x, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_three32)), - d_p)); - Node resz2 = d_nm->mkNode( - kind::EQUAL, - d_z, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_y, d_seven32)), - d_p)); - - Node resy3 = d_nm->mkNode( - kind::EQUAL, - d_y, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_three32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_four32)), - d_p)); - Node resz3 = d_nm->mkNode( - kind::EQUAL, - d_z, - d_nm->mkNode( - kind::BITVECTOR_UREM, - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_two32, - d_nm->mkNode(kind::BITVECTOR_MULT, d_x, d_six32)), - d_p)); - - bool fx1 = std::find(ass.begin(), ass.end(), resx1) != ass.end(); - bool fy1 = std::find(ass.begin(), ass.end(), resy1) != ass.end(); - bool fx2 = std::find(ass.begin(), ass.end(), resx2) != ass.end(); - bool fz2 = std::find(ass.begin(), ass.end(), resz2) != ass.end(); - bool fy3 = std::find(ass.begin(), ass.end(), resy3) != ass.end(); - bool fz3 = std::find(ass.begin(), ass.end(), resz3) != ass.end(); - - /* result depends on order of variables in matrix */ - TS_ASSERT((fx1 && fy1) || (fx2 && fz2) || (fy3 && fz3)); - } - - void testGetMinBw1() - { - TS_ASSERT(BVGaussElim::getMinBwExpr(utils::mkConst(32, 11)) == 4); - - TS_ASSERT(BVGaussElim::getMinBwExpr(d_p) == 4); - TS_ASSERT(BVGaussElim::getMinBwExpr(d_x) == 16); - - Node extp = mkExtract(d_p, 4, 0); - TS_ASSERT(BVGaussElim::getMinBwExpr(extp) == 4); - Node extx = mkExtract(d_x, 4, 0); - TS_ASSERT(BVGaussElim::getMinBwExpr(extx) == 5); - - Node zextop8 = d_nm->mkConst(BitVectorZeroExtend(8)); - Node zextop16 = d_nm->mkConst(BitVectorZeroExtend(16)); - Node zextop32 = d_nm->mkConst(BitVectorZeroExtend(32)); - Node zextop40 = d_nm->mkConst(BitVectorZeroExtend(40)); - - Node zext40p = d_nm->mkNode(zextop8, d_p); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext40p) == 4); - Node zext40x = d_nm->mkNode(zextop8, d_x); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext40x) == 16); - - Node zext48p = d_nm->mkNode(zextop16, d_p); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext48p) == 4); - Node zext48x = d_nm->mkNode(zextop16, d_x); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext48x) == 16); - - Node p8 = d_nm->mkConst(BitVector(8, 11u)); - Node x8 = d_nm->mkVar("x8", d_nm->mkBitVectorType(8)); - - Node zext48p8 = d_nm->mkNode(zextop40, p8); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext48p8) == 4); - Node zext48x8 = d_nm->mkNode(zextop40, x8); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext48x8) == 8); - - Node mult1p = d_nm->mkNode(kind::BITVECTOR_MULT, extp, extp); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult1p) == 5); - Node mult1x = d_nm->mkNode(kind::BITVECTOR_MULT, extx, extx); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult1x) == 0); - - Node mult2p = d_nm->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult2p) == 7); - Node mult2x = d_nm->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult2x) == 32); - - NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT); - nbmult3p << zext48p << zext48p << zext48p; - Node mult3p = nbmult3p; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult3p) == 11); - NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT); - nbmult3x << zext48x << zext48x << zext48x; - Node mult3x = nbmult3x; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult3x) == 48); - - NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT); - nbmult4p << zext48p << zext48p8 << zext48p; - Node mult4p = nbmult4p; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult4p) == 11); - NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT); - nbmult4x << zext48x << zext48x8 << zext48x; - Node mult4x = nbmult4x; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult4x) == 40); - - Node concat1p = mkConcat(d_p, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(concat1p) == 52); - Node concat1x = mkConcat(d_x, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(concat1x) == 64); - - Node concat2p = mkConcat(mkZero(16), zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(concat2p) == 4); - Node concat2x = mkConcat(mkZero(16), zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(concat2x) == 16); - - Node udiv1p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(udiv1p) == 1); - Node udiv1x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(udiv1x) == 48); - - Node udiv2p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p8); - TS_ASSERT(BVGaussElim::getMinBwExpr(udiv2p) == 1); - Node udiv2x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x8); - TS_ASSERT(BVGaussElim::getMinBwExpr(udiv2x) == 48); - - Node urem1p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem1p) == 1); - Node urem1x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem1x) == 1); - - Node urem2p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p8); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem2p) == 1); - Node urem2x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x8); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem2x) == 16); - - Node urem3p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p8, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem3p) == 1); - Node urem3x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x8, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem3x) == 8); - - Node add1p = d_nm->mkNode(kind::BITVECTOR_PLUS, extp, extp); - TS_ASSERT(BVGaussElim::getMinBwExpr(add1p) == 5); - Node add1x = d_nm->mkNode(kind::BITVECTOR_PLUS, extx, extx); - TS_ASSERT(BVGaussElim::getMinBwExpr(add1x) == 0); - - Node add2p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p); - TS_ASSERT(BVGaussElim::getMinBwExpr(add2p) == 5); - Node add2x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x); - TS_ASSERT(BVGaussElim::getMinBwExpr(add2x) == 17); - - Node add3p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(add3p) == 5); - Node add3x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(add3x) == 17); - - NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS); - nbadd4p << zext48p << zext48p << zext48p; - Node add4p = nbadd4p; - TS_ASSERT(BVGaussElim::getMinBwExpr(add4p) == 6); - NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS); - nbadd4x << zext48x << zext48x << zext48x; - Node add4x = nbadd4x; - TS_ASSERT(BVGaussElim::getMinBwExpr(add4x) == 18); - - NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS); - nbadd5p << zext48p << zext48p8 << zext48p; - Node add5p = nbadd5p; - TS_ASSERT(BVGaussElim::getMinBwExpr(add5p) == 6); - NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS); - nbadd5x << zext48x << zext48x8 << zext48x; - Node add5x = nbadd5x; - TS_ASSERT(BVGaussElim::getMinBwExpr(add5x) == 18); - - NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS); - nbadd6p << zext48p << zext48p << zext48p << zext48p; - Node add6p = nbadd6p; - TS_ASSERT(BVGaussElim::getMinBwExpr(add6p) == 6); - NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS); - nbadd6x << zext48x << zext48x << zext48x << zext48x; - Node add6x = nbadd6x; - TS_ASSERT(BVGaussElim::getMinBwExpr(add6x) == 18); - - Node not1p = d_nm->mkNode(kind::BITVECTOR_NOT, zext40p); - TS_ASSERT(BVGaussElim::getMinBwExpr(not1p) == 40); - Node not1x = d_nm->mkNode(kind::BITVECTOR_NOT, zext40x); - TS_ASSERT(BVGaussElim::getMinBwExpr(not1x) == 40); - } - - void testGetMinBw2() - { - /* ((_ zero_extend 5) - * ((_ extract 7 0) ((_ zero_extend 15) d_p))) */ - Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); - Node zextop15 = d_nm->mkConst(BitVectorZeroExtend(15)); - Node zext1 = d_nm->mkNode(zextop15, d_p); - Node ext = mkExtract(zext1, 7, 0); - Node zext2 = d_nm->mkNode(zextop5, ext); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext2) == 4); - } - - void testGetMinBw3a() - { - /* ((_ zero_extend 5) - * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z))) - * ((_ extract 4 0) z))) */ - Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); - Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); - Node z = d_nm->mkVar("z", d_nm->mkBitVectorType(16)); - Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); - Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y); - Node zext1 = d_nm->mkNode(zextop5, udiv1); - Node ext1 = mkExtract(zext1, 4, 0); - Node ext2 = mkExtract(z, 4, 0); - Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2); - Node zext2 = mkConcat(mkZero(5), udiv2); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext2) == 5); - } - - void testGetMinBw3b() - { - /* ((_ zero_extend 5) - * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x z))) - * ((_ extract 4 0) z))) */ - Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); - Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y); - Node zext1 = d_nm->mkNode(zextop5, udiv1); - Node ext1 = mkExtract(zext1, 4, 0); - Node ext2 = mkExtract(d_z, 4, 0); - Node udiv2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2); - Node zext2 = mkConcat(mkZero(5), udiv2); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext2) == 5); - } - - void testGetMinBw4a() - { - /* (bvadd - * ((_ zero_extend 5) - * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y))) - * ((_ extract 4 0) z))) - * ((_ zero_extend 7) - * (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y))) - * ((_ extract 2 0) z))) */ - Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); - Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); - Node z = d_nm->mkVar("z", d_nm->mkBitVectorType(16)); - Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); - Node zextop7 = d_nm->mkConst(BitVectorZeroExtend(7)); - - Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y); - Node zext1 = d_nm->mkNode(zextop5, udiv1); - - Node ext1_1 = mkExtract(zext1, 4, 0); - Node ext2_1 = mkExtract(z, 4, 0); - Node udiv2_1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1); - Node zext2_1 = mkConcat(mkZero(5), udiv2_1); - - Node ext1_2 = mkExtract(zext1, 2, 0); - Node ext2_2 = mkExtract(z, 2, 0); - Node udiv2_2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2); - Node zext2_2 = d_nm->mkNode(zextop7, udiv2_2); - - Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); - - TS_ASSERT(BVGaussElim::getMinBwExpr(plus) == 6); - } - - void testGetMinBw4b() - { - /* (bvadd - * ((_ zero_extend 5) - * (bvudiv ((_ extract 4 0) ((_ zero_extend 5) (bvudiv x y))) - * ((_ extract 4 0) z))) - * ((_ zero_extend 7) - * (bvudiv ((_ extract 2 0) ((_ zero_extend 5) (bvudiv x y))) - * ((_ extract 2 0) z))) */ - Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); - Node zextop7 = d_nm->mkConst(BitVectorZeroExtend(7)); - - Node udiv1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y); - Node zext1 = d_nm->mkNode(zextop5, udiv1); - - Node ext1_1 = mkExtract(zext1, 4, 0); - Node ext2_1 = mkExtract(d_z, 4, 0); - Node udiv2_1 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1); - Node zext2_1 = mkConcat(mkZero(5), udiv2_1); - - Node ext1_2 = mkExtract(zext1, 2, 0); - Node ext2_2 = mkExtract(d_z, 2, 0); - Node udiv2_2 = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2); - Node zext2_2 = d_nm->mkNode(zextop7, udiv2_2); - - Node plus = d_nm->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2); - - TS_ASSERT(BVGaussElim::getMinBwExpr(plus) == 6); - } - - void testGetMinBw5a() - { - /* (bvadd - * (bvadd - * (bvadd - * (bvadd - * (bvadd - * (bvadd - * (bvadd (bvmul (_ bv86 13) - * ((_ zero_extend 5) - * ((_ extract 7 0) ((_ zero_extend 15) x)))) - * (bvmul (_ bv41 13) - * ((_ zero_extend 5) - * ((_ extract 7 0) ((_ zero_extend 15) y))))) - * (bvmul (_ bv37 13) - * ((_ zero_extend 5) - * ((_ extract 7 0) ((_ zero_extend 15) z))))) - * (bvmul (_ bv170 13) - * ((_ zero_extend 5) - * ((_ extract 7 0) ((_ zero_extend 15) u))))) - * (bvmul (_ bv112 13) - * ((_ zero_extend 5) - * ((_ extract 7 0) ((_ zero_extend 15) v))))) - * (bvmul (_ bv195 13) ((_ zero_extend 5) ((_ extract 15 8) s)))) - * (bvmul (_ bv124 13) ((_ zero_extend 5) ((_ extract 7 0) s)))) - * (bvmul (_ bv83 13) - * ((_ zero_extend 5) ((_ extract 7 0) ((_ zero_extend 15) w))))) - */ - Node x = mkVar(1); - Node y = mkVar(1); - Node z = mkVar(1); - Node u = mkVar(1); - Node v = mkVar(1); - Node w = mkVar(1); - Node s = mkVar(16); - - Node zextop5 = d_nm->mkConst(BitVectorZeroExtend(5)); - Node zextop15 = d_nm->mkConst(BitVectorZeroExtend(15)); - - Node zext15x = d_nm->mkNode(zextop15, x); - Node zext15y = d_nm->mkNode(zextop15, y); - Node zext15z = d_nm->mkNode(zextop15, z); - Node zext15u = d_nm->mkNode(zextop15, u); - Node zext15v = d_nm->mkNode(zextop15, v); - Node zext15w = d_nm->mkNode(zextop15, w); - - Node ext7x = mkExtract(zext15x, 7, 0); - Node ext7y = mkExtract(zext15y, 7, 0); - Node ext7z = mkExtract(zext15z, 7, 0); - Node ext7u = mkExtract(zext15u, 7, 0); - Node ext7v = mkExtract(zext15v, 7, 0); - Node ext7w = mkExtract(zext15w, 7, 0); - Node ext7s = mkExtract(s, 7, 0); - Node ext15s = mkExtract(s, 15, 8); - - Node xx = mkConcat(mkZero(5), ext7x); - Node yy = mkConcat(mkZero(5), ext7y); - Node zz = mkConcat(mkZero(5), ext7z); - Node uu = mkConcat(mkZero(5), ext7u); - Node vv = mkConcat(mkZero(5), ext7v); - Node ww = mkConcat(mkZero(5), ext7w); - Node s7 = mkConcat(mkZero(5), ext7s); - Node s15 = mkConcat(mkZero(5), ext15s); - - Node plus1 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 86), xx), - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 41), yy)); - Node plus2 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus1, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 37), zz)); - Node plus3 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus2, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 170), uu)); - Node plus4 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus3, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 112), uu)); - Node plus5 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus4, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 195), s15)); - Node plus6 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus5, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 124), s7)); - Node plus7 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus6, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(13, 83), ww)); - - TS_ASSERT(BVGaussElim::getMinBwExpr(plus7) == 0); - } - - void testGetMinBw5b() - { - /* (bvadd - * (bvadd - * (bvadd - * (bvadd - * (bvadd - * (bvadd - * (bvadd (bvmul (_ bv86 20) - * ((_ zero_extend 12) - * ((_ extract 7 0) ((_ zero_extend 15) x)))) - * (bvmul (_ bv41 20) - * ((_ zero_extend 12) - * ((_ extract 7 0) ((_ zero_extend 15) y))))) - * (bvmul (_ bv37 20) - * ((_ zero_extend 12) - * ((_ extract 7 0) ((_ zero_extend 15) z))))) - * (bvmul (_ bv170 20) - * ((_ zero_extend 12) - * ((_ extract 7 0) ((_ zero_extend 15) u))))) - * (bvmul (_ bv112 20) - * ((_ zero_extend 12) - * ((_ extract 7 0) ((_ zero_extend 15) v))))) - * (bvmul (_ bv195 20) ((_ zero_extend 12) ((_ extract 15 8) s)))) - * (bvmul (_ bv124 20) ((_ zero_extend 12) ((_ extract 7 0) s)))) - * (bvmul (_ bv83 20) - * ((_ zero_extend 12) ((_ extract 7 0) ((_ zero_extend 15) w))))) - */ - Node x = mkVar(1); - Node y = mkVar(1); - Node z = mkVar(1); - Node u = mkVar(1); - Node v = mkVar(1); - Node w = mkVar(1); - Node s = mkVar(16); - - Node zextop15 = d_nm->mkConst(BitVectorZeroExtend(15)); - - Node zext15x = d_nm->mkNode(zextop15, x); - Node zext15y = d_nm->mkNode(zextop15, y); - Node zext15z = d_nm->mkNode(zextop15, z); - Node zext15u = d_nm->mkNode(zextop15, u); - Node zext15v = d_nm->mkNode(zextop15, v); - Node zext15w = d_nm->mkNode(zextop15, w); - - Node ext7x = mkExtract(zext15x, 7, 0); - Node ext7y = mkExtract(zext15y, 7, 0); - Node ext7z = mkExtract(zext15z, 7, 0); - Node ext7u = mkExtract(zext15u, 7, 0); - Node ext7v = mkExtract(zext15v, 7, 0); - Node ext7w = mkExtract(zext15w, 7, 0); - Node ext7s = mkExtract(s, 7, 0); - Node ext15s = mkExtract(s, 15, 8); - - Node xx = mkConcat(mkZero(12), ext7x); - Node yy = mkConcat(mkZero(12), ext7y); - Node zz = mkConcat(mkZero(12), ext7z); - Node uu = mkConcat(mkZero(12), ext7u); - Node vv = mkConcat(mkZero(12), ext7v); - Node ww = mkConcat(mkZero(12), ext7w); - Node s7 = mkConcat(mkZero(12), ext7s); - Node s15 = mkConcat(mkZero(12), ext15s); - - Node plus1 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 86), xx), - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 41), yy)); - Node plus2 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus1, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 37), zz)); - Node plus3 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus2, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 170), uu)); - Node plus4 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus3, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 112), uu)); - Node plus5 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus4, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 195), s15)); - Node plus6 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus5, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 124), s7)); - Node plus7 = - d_nm->mkNode(kind::BITVECTOR_PLUS, - plus6, - d_nm->mkNode(kind::BITVECTOR_MULT, mkConst(20, 83), ww)); - - TS_ASSERT(BVGaussElim::getMinBwExpr(plus7) == 19); - TS_ASSERT(BVGaussElim::getMinBwExpr(Rewriter::rewrite(plus7)) == 17); - } - -};