From 6b5b926f28b66c3812d77fd234e93b9eee03f71f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 10 Apr 2018 18:52:54 -0700 Subject: [PATCH] Refactored BVGauss preprocessing pass. (#1766) --- src/Makefile.am | 4 +- .../passes/bv_gauss.cpp} | 218 +++-- src/preprocessing/passes/bv_gauss.h | 53 ++ src/smt/smt_engine.cpp | 11 +- src/theory/bv/bvgauss.h | 151 --- test/unit/Makefile.am | 2 +- .../pass_bv_gauss_white.h} | 859 ++++++++++-------- 7 files changed, 691 insertions(+), 607 deletions(-) rename src/{theory/bv/bvgauss.cpp => preprocessing/passes/bv_gauss.cpp} (74%) create mode 100644 src/preprocessing/passes/bv_gauss.h delete mode 100644 src/theory/bv/bvgauss.h rename test/unit/{theory/theory_bv_bvgauss_white.h => preprocessing/pass_bv_gauss_white.h} (79%) 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/theory/bv/bvgauss.cpp b/src/preprocessing/passes/bv_gauss.cpp similarity index 74% rename from src/theory/bv/bvgauss.cpp rename to src/preprocessing/passes/bv_gauss.cpp index e36ef3aef..d1f7d09ee 100644 --- a/src/theory/bv/bvgauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file bvgauss.cpp +/*! \file bv_gauss.cpp ** \verbatim ** Top contributors (to current version): ** Aina Niemetz @@ -15,44 +15,104 @@ ** Elimination if possible. **/ -#include "theory/bv/bvgauss.h" - -#include +#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 theory { -namespace bv { +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 +}; -static bool is_bv_const(Node n) +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) +Node get_bv_const(Node n) { Assert(is_bv_const(n)); return Rewriter::rewrite(n); } -static Integer get_bv_const_value(Node n) +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. +/** + * 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 BVGaussElim::getMinBwExpr(Node expr) + * necessarily the minimum. + */ +unsigned getMinBwExpr(Node expr) { std::vector visit; /* Maps visited nodes to the determined minimum bit-width required. */ @@ -88,8 +148,8 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) { case kind::BITVECTOR_EXTRACT: { - const unsigned size = utils::getSize(n); - const unsigned low = utils::getExtractLow(n); + 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); @@ -118,7 +178,7 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) } } unsigned w = maxval.length(); - if (w > utils::getSize(n)) { return 0; } /* overflow */ + if (w > bv::utils::getSize(n)) { return 0; } /* overflow */ visited[n] = w; break; } @@ -128,8 +188,8 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) 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; } + 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; } @@ -137,9 +197,8 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) * 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; + visited[n] = bv::utils::getSize(n) + visited[n[i]] + - bv::utils::getSize(n[i]) - wnz; break; } @@ -185,7 +244,7 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) } } unsigned w = maxval.length(); - if (w > utils::getSize(n)) { return 0; } /* overflow */ + if (w > bv::utils::getSize(n)) { return 0; } /* overflow */ visited[n] = w; break; } @@ -196,7 +255,7 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) * BITVECTOR_NOT * BITVECTOR_NEG * BITVECTOR_SHL */ - visited[n] = utils::getSize(n); + visited[n] = bv::utils::getSize(n); } } } @@ -205,7 +264,23 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) return visited[expr]; } -BVGaussElim::Result BVGaussElim::gaussElim( +/** + * 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) @@ -221,7 +296,7 @@ BVGaussElim::Result BVGaussElim::gaussElim( rhs = std::vector(rhs.size(), Integer(0)); lhs = std::vector>( lhs.size(), std::vector(lhs[0].size(), Integer(0))); - return BVGaussElim::Result::UNIQUE; + return Result::UNIQUE; } size_t nrows = lhs.size(); @@ -286,7 +361,7 @@ BVGaussElim::Result BVGaussElim::gaussElim( Integer inv = lhs[j][pcol].modInverse(prime); if (inv == -1) { - return BVGaussElim::Result::INVALID; /* not coprime */ + return Result::INVALID; /* not coprime */ } for (size_t k = pcol; k < ncols; ++k) { @@ -334,7 +409,7 @@ BVGaussElim::Result BVGaussElim::gaussElim( if (rhs[i] != 0) { /* no solution */ - return BVGaussElim::Result::NONE; + return Result::NONE; } continue; } @@ -351,12 +426,33 @@ BVGaussElim::Result BVGaussElim::gaussElim( } } - if (ispart) { return BVGaussElim::Result::PARTIAL; } + if (ispart) { return Result::PARTIAL; } - return BVGaussElim::Result::UNIQUE; + return Result::UNIQUE; } -BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( +/** + * 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) { @@ -397,7 +493,7 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( << "Minimum required bit-width exceeds given bit-width, " "will not apply Gaussian Elimination." << std::endl; - return BVGaussElim::Result::INVALID; + return Result::INVALID; } rhs.push_back(get_bv_const_value(eqrhs)); @@ -464,7 +560,7 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( } else { - n0 = utils::mkOne(utils::getSize(n)); + n0 = bv::utils::mkOne(bv::utils::getSize(n)); } /* n1 is a mult with non-const operands */ if (nb_nonconsts.getNumChildren() > 1) @@ -517,7 +613,7 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( if (nrows < 1) { - return BVGaussElim::Result::INVALID; + return Result::INVALID; } for (size_t i = 0; i < nrows; ++i) @@ -535,13 +631,13 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( if (lhs.size() > lhs[0].size()) { - return BVGaussElim::Result::INVALID; + return 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) + if (ret != Result::NONE && ret != Result::INVALID) { std::vector vvars; for (const auto& p : vars) { vvars.push_back(p.first); } @@ -549,17 +645,17 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( Assert(nrows == lhs.size()); Assert(nrows == rhs.size()); NodeManager *nm = NodeManager::currentNM(); - if (ret == BVGaussElim::Result::UNIQUE) + if (ret == Result::UNIQUE) { for (size_t i = 0; i < nvars; ++i) { res[vvars[i]] = nm->mkConst( - BitVector(utils::getSize(vvars[i]), rhs[i])); + BitVector(bv::utils::getSize(vvars[i]), rhs[i])); } } else { - Assert(ret == BVGaussElim::Result::PARTIAL); + Assert(ret == Result::PARTIAL); for (size_t pcol = 0, prow = 0; pcol < nvars && prow < nrows; ++pcol, ++prow) @@ -584,7 +680,7 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( /* 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 bv = bv::utils::mkConst(bv::utils::getSize(vvars[i]), m); Node mult = nm->mkNode(kind::BITVECTOR_MULT, vvars[i], bv); stack.push_back(mult); } @@ -592,7 +688,7 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( if (stack.empty()) { res[vvars[pcol]] = nm->mkConst( - BitVector(utils::getSize(vvars[pcol]), rhs[prow])); + BitVector(bv::utils::getSize(vvars[pcol]), rhs[prow])); } else { @@ -603,8 +699,8 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( if (rhs[prow] != 0) { tmp = nm->mkNode(kind::BITVECTOR_PLUS, - utils::mkConst( - utils::getSize(vvars[pcol]), rhs[prow]), + bv::utils::mkConst( + bv::utils::getSize(vvars[pcol]), rhs[prow]), tmp); } Assert(!is_bv_const(tmp)); @@ -616,9 +712,19 @@ BVGaussElim::Result BVGaussElim::gaussElimRewriteForUrem( return ret; } -void BVGaussElim::gaussElimRewrite(std::vector &assertionsToPreprocess) +} // namespace + + + +BVGauss::BVGauss(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "bv-gauss") +{ +} + +PreprocessingPassResult BVGauss::applyInternal( + AssertionPipeline* assertionsToPreprocess) { - std::vector assertions(assertionsToPreprocess); + std::vector assertions(assertionsToPreprocess->ref()); std::unordered_map, NodeHashFunction> equations; while (!assertions.empty()) @@ -659,29 +765,30 @@ void BVGaussElim::gaussElimRewrite(std::vector &assertionsToPreprocess) } std::unordered_map subst; + std::vector& atpp = assertionsToPreprocess->ref(); for (const auto& eq : equations) { if (eq.second.size() <= 1) { continue; } std::unordered_map res; - BVGaussElim::Result ret = gaussElimRewriteForUrem(eq.second, res); + Result ret = gaussElimRewriteForUrem(eq.second, res); Trace("bv-gauss-elim") << "result: " - << (ret == BVGaussElim::Result::INVALID + << (ret == Result::INVALID ? "INVALID" - : (ret == BVGaussElim::Result::UNIQUE + : (ret == Result::UNIQUE ? "UNIQUE" - : (ret == BVGaussElim::Result::PARTIAL + : (ret == Result::PARTIAL ? "PARTIAL" : "NONE"))) << std::endl; - if (ret != BVGaussElim::Result::INVALID) + if (ret != Result::INVALID) { NodeManager *nm = NodeManager::currentNM(); - if (ret == BVGaussElim::Result::NONE) + if (ret == Result::NONE) { - assertionsToPreprocess.clear(); - assertionsToPreprocess.push_back(nm->mkConst(false)); + atpp.clear(); + atpp.push_back(nm->mkConst(false)); } else { @@ -694,7 +801,7 @@ void BVGaussElim::gaussElimRewrite(std::vector &assertionsToPreprocess) { Node a = nm->mkNode(kind::EQUAL, p.first, p.second); Trace("bv-gauss-elim") << "added assertion: " << a << std::endl; - assertionsToPreprocess.push_back(a); + atpp.push_back(a); } } } @@ -703,13 +810,14 @@ void BVGaussElim::gaussElimRewrite(std::vector &assertionsToPreprocess) if (!subst.empty()) { /* delete (= substitute with true) obsolete assertions */ - for (auto& a : assertionsToPreprocess) + for (auto& a : atpp) { a = a.substitute(subst.begin(), subst.end()); } } + return PreprocessingPassResult::NO_CONFLICT; } -} // namespace bv -} // namespace theory +} // 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.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/theory/theory_bv_bvgauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h similarity index 79% rename from test/unit/theory/theory_bv_bvgauss_white.h rename to test/unit/preprocessing/pass_bv_gauss_white.h index a0e2b235b..e39c7d6c3 100644 --- a/test/unit/theory/theory_bv_bvgauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -16,10 +16,11 @@ #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/bvgauss.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" @@ -28,9 +29,8 @@ #include using namespace CVC4; +using namespace CVC4::preprocessing; 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, @@ -50,13 +50,13 @@ static void print_matrix_dbg(std::vector &rhs, static void testGaussElimX(Integer prime, std::vector rhs, std::vector> lhs, - BVGaussElim::Result expected, + passes::Result expected, std::vector *rrhs = nullptr, std::vector> *rlhs = nullptr) { size_t nrows = lhs.size(); size_t ncols = lhs[0].size(); - BVGaussElim::Result ret; + passes::Result ret; std::vector resrhs = std::vector(rhs); std::vector> reslhs = std::vector>(lhs); @@ -64,21 +64,21 @@ static void testGaussElimX(Integer prime, std::cout << "Input: " << std::endl; print_matrix_dbg(rhs, lhs); - ret = BVGaussElim::gaussElim(prime, resrhs, reslhs); + ret = passes::gaussElim(prime, resrhs, reslhs); - std::cout << "Result: " - << (ret == BVGaussElim::Result::INVALID + std::cout << "passes::Result: " + << (ret == passes::Result::INVALID ? "INVALID" - : (ret == BVGaussElim::Result::UNIQUE + : (ret == passes::Result::UNIQUE ? "UNIQUE" - : (ret == BVGaussElim::Result::PARTIAL ? "PARTIAL" + : (ret == passes::Result::PARTIAL ? "PARTIAL" : "NONE"))) << std::endl; print_matrix_dbg(resrhs, reslhs); TS_ASSERT_EQUALS(expected, ret); - if (expected == BVGaussElim::Result::UNIQUE) + if (expected == passes::Result::UNIQUE) { /* map result value to column index * e.g.: @@ -120,7 +120,7 @@ static void testGaussElimT(Integer prime, std::vector rhs, std::vector> lhs) { - TS_ASSERT_THROWS(BVGaussElim::gaussElim(prime, rhs, lhs), T); + TS_ASSERT_THROWS(passes::gaussElim(prime, rhs, lhs), T); } class TheoryBVGaussWhite : public CxxTest::TestSuite @@ -183,28 +183,45 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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_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)); @@ -303,27 +320,27 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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); + testGaussElimX(Integer(1), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 0, modulo 2" << std::endl; - testGaussElimX(Integer(2), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(2), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 0, modulo 3" << std::endl; - testGaussElimX(Integer(3), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(3), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 0, modulo 4" << std::endl; // no inverse - testGaussElimX(Integer(4), rhs, lhs, BVGaussElim::Result::INVALID); + testGaussElimX(Integer(4), rhs, lhs, passes::Result::INVALID); std::cout << "matrix 0, modulo 5" << std::endl; - testGaussElimX(Integer(5), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(5), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 0, modulo 6" << std::endl; // no inverse - testGaussElimX(Integer(6), rhs, lhs, BVGaussElim::Result::INVALID); + testGaussElimX(Integer(6), rhs, lhs, passes::Result::INVALID); std::cout << "matrix 0, modulo 7" << std::endl; - testGaussElimX(Integer(7), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 0, modulo 8" << std::endl; // no inverse - testGaussElimX(Integer(8), rhs, lhs, BVGaussElim::Result::INVALID); + testGaussElimX(Integer(8), rhs, lhs, passes::Result::INVALID); std::cout << "matrix 0, modulo 9" << std::endl; - testGaussElimX(Integer(9), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(9), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 0, modulo 10" << std::endl; // no inverse - testGaussElimX(Integer(10), rhs, lhs, BVGaussElim::Result::INVALID); + testGaussElimX(Integer(10), rhs, lhs, passes::Result::INVALID); std::cout << "matrix 0, modulo 11" << std::endl; - testGaussElimX(Integer(11), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); } void testGaussElimUniqueDone() @@ -343,7 +360,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE); } void testGaussElimUnique() @@ -363,11 +380,11 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 2, modulo 17" << std::endl; - testGaussElimX(Integer(17), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(17), rhs, lhs, passes::Result::UNIQUE); std::cout << "matrix 2, modulo 59" << std::endl; - testGaussElimX(Integer(59), rhs, lhs, BVGaussElim::Result::UNIQUE); + testGaussElimX(Integer(59), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -383,7 +400,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); } void testGaussElimUniqueZero1() @@ -403,7 +420,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -417,7 +434,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -431,7 +448,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); } void testGaussElimUniqueZero2() @@ -451,7 +468,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -465,7 +482,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -479,7 +496,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); } void testGaussElimUniqueZero3() @@ -499,7 +516,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 7 @@ -513,7 +530,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); } void testGaussElimUniqueZero4() @@ -533,7 +550,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -547,7 +564,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -561,7 +578,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -575,7 +592,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -589,7 +606,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -603,7 +620,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -617,7 +634,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -631,7 +648,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -645,7 +662,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs modulo 2 @@ -664,7 +681,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {Integer(0), Integer(0), Integer(0)}, {Integer(0), Integer(0), Integer(0)}}; testGaussElimX( - Integer(2), rhs, lhs, BVGaussElim::Result::UNIQUE, &resrhs, &reslhs); + Integer(2), rhs, lhs, passes::Result::UNIQUE, &resrhs, &reslhs); } void testGaussElimUniquePartial() @@ -682,7 +699,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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); + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 7 @@ -694,7 +711,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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); + testGaussElimX(Integer(7), rhs, lhs, passes::Result::UNIQUE); } void testGaussElimNone() @@ -714,7 +731,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID); /* ------------------------------------------------------------------- * lhs rhs modulo 59 @@ -728,7 +745,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(59), rhs, lhs, passes::Result::NONE); /* ------------------------------------------------------------------- * lhs rhs modulo 9 @@ -742,7 +759,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(9), rhs, lhs, passes::Result::INVALID); } void testGaussElimNoneZero() @@ -762,7 +779,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -776,7 +793,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE); /* ------------------------------------------------------------------- * lhs rhs modulo 11 @@ -790,7 +807,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::NONE); } void testGaussElimPartial1() @@ -808,7 +825,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -820,7 +837,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -832,7 +849,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); /* ------------------------------------------------------------------- * lhs rhs modulo { 3, 5, 7, 11, 17, 31, 59 } @@ -851,38 +868,38 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {Integer(0), Integer(0), Integer(0)}, {Integer(0), Integer(0), Integer(0)}}; testGaussElimX( - Integer(3), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); + 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, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); + 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, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); + 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, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); + 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, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); + 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, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); + Integer(59), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 3 @@ -901,7 +918,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {Integer(0), Integer(0), Integer(0)}, {Integer(0), Integer(0), Integer(0)}}; testGaussElimX( - Integer(3), rhs, lhs, BVGaussElim::Result::PARTIAL, &resrhs, &reslhs); + Integer(3), rhs, lhs, passes::Result::PARTIAL, &resrhs, &reslhs); } void testGaussElimPartial2() @@ -922,7 +939,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {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); + testGaussElimX(Integer(11), rhs, lhs, passes::Result::PARTIAL); } void testGaussElimRewriteForUremUnique1() { @@ -966,8 +983,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite std::vector eqs = {eq1, eq2, eq3}; std::unordered_map res; - BVGaussElim::Result ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::UNIQUE); + 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); @@ -986,21 +1003,36 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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 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, mkOne(32), d_z); + 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, mkOne(32), mkOne(32)), d_x); + 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, mkOnes(32), mkConst(32, 30)), d_y); + 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, - mkExtract( + bv::utils::mkExtract( d_nm->mkNode( zextop6, d_nm->mkNode(kind::BITVECTOR_PLUS, d_three, d_two)), 31, 0), @@ -1010,10 +1042,10 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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)), + 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( @@ -1050,8 +1082,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite std::vector eqs = {eq1, eq2, eq3}; std::unordered_map res; - BVGaussElim::Result ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::UNIQUE); + 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); @@ -1061,7 +1093,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremPartial1() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -1087,8 +1119,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 2); Node x1 = d_nm->mkNode( @@ -1179,7 +1211,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremPartial1a() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -1203,8 +1235,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 2); Node x1 = d_nm->mkNode( @@ -1295,7 +1327,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremPartial2() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -1318,8 +1350,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 2); Node x1 = d_nm->mkNode( @@ -1381,7 +1413,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremPartial3() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -1412,8 +1444,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_eight); std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 2); Node x1 = d_nm->mkNode( @@ -1502,7 +1534,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremPartial4() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -1546,8 +1578,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_thirty); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 2); Node x1 = d_nm->mkNode( @@ -1644,7 +1676,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremPartial5() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 3 @@ -1688,8 +1720,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_thirty); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 1); Node x1 = d_nm->mkNode(kind::BITVECTOR_UREM, @@ -1751,7 +1783,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremPartial6() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs --> lhs rhs modulo 11 @@ -1764,7 +1796,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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 = 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); @@ -1794,8 +1827,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_two); std::vector eqs = {eq1, eq2, eq3}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 3); Node x1 = d_nm->mkNode( @@ -1838,7 +1871,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremWithExprPartial() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -1847,17 +1880,24 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite * 0 1 3 9 0 1 3 9 * ------------------------------------------------------------------- */ - Node zero = mkZero(8); + 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 = - 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 = 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); @@ -1878,8 +1918,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 2); x = Rewriter::rewrite(x); @@ -1974,7 +2014,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremNAryPartial() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * lhs rhs lhs rhs modulo 11 @@ -1983,26 +2023,29 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite * 0 1 3 9 0 1 3 9 * ------------------------------------------------------------------- */ - Node zero = mkZero(8); + 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 = mkConcat( + Node x = bv::utils::mkConcat( d_zero, - mkConcat( + bv::utils::mkConcat( zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, xx), 7, 0))); - Node y = mkConcat( + bv::utils::mkExtract( + d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, xx), 7, 0))); + Node y = bv::utils::mkConcat( d_zero, - mkConcat( + bv::utils::mkConcat( zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, yy), 7, 0))); - Node z = mkConcat( + bv::utils::mkExtract( + d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, yy), 7, 0))); + Node z = bv::utils::mkConcat( d_zero, - mkConcat( + bv::utils::mkConcat( zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0))); + 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; @@ -2038,8 +2081,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_nine); std::vector eqs = {eq1, eq2}; - ret = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::PARTIAL); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::PARTIAL); TS_ASSERT(res.size() == 2); x_mul_xx = Rewriter::rewrite(x_mul_xx); @@ -2134,7 +2177,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremNotInvalid1() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * 3x / 2z = 4 modulo 11 @@ -2148,9 +2191,11 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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( + + Node n3 = bv::utils::mkConcat( d_zero, - mkExtract(d_nm->mkNode(kind::BITVECTOR_CONCAT, d_y, d_z), 15, 0)); + 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); @@ -2162,8 +2207,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::UNIQUE); TS_ASSERT(res.size() == 3); TS_ASSERT(res[n1] == d_four32); @@ -2174,7 +2219,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremNotInvalid2() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * x*y = 4 modulo 11 @@ -2182,11 +2227,14 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite * 2*x*y + 2*z = 9 * ------------------------------------------------------------------- */ - Node zero32 = mkZero(32); + Node zero32 = bv::utils::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 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( @@ -2195,35 +2243,39 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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)); + 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, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_four)); + 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, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_two)); + 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, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_nine)); + 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 = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::UNIQUE); + 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] == mkConst(48, 4)); - TS_ASSERT(res[n2] == mkConst(48, 2)); + 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)); @@ -2236,7 +2288,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGaussElimRewriteForUremInvalid() { std::unordered_map res; - BVGaussElim::Result ret; + passes::Result ret; /* ------------------------------------------------------------------- * x*y = 4 modulo 11 @@ -2244,37 +2296,43 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite * 2*x*y = 9 * ------------------------------------------------------------------- */ - Node zero32 = mkZero(32); + Node zero32 = bv::utils::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 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), - mkConcat(d_zero, d_two)); + bv::utils::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)); + 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, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_two)); + 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, mkConcat(d_zero, d_p)), - mkConcat(d_zero, d_nine)); + 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 = BVGaussElim::gaussElimRewriteForUrem(eqs, res); - TS_ASSERT(ret == BVGaussElim::Result::INVALID); + ret = passes::gaussElimRewriteForUrem(eqs, res); + TS_ASSERT(ret == passes::Result::INVALID); } void testGaussElimRewriteUnique1() @@ -2319,19 +2377,22 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - std::vector ass = {a}; + AssertionPipeline apipe; + apipe.push_back(a); + passes::BVGauss bgauss(nullptr); std::unordered_map res; - BVGaussElim::gaussElimRewrite(ass); + 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(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()); + 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() @@ -2398,9 +2459,14 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - std::vector ass = {a, eq4, eq5}; + AssertionPipeline apipe; + apipe.push_back(a); + apipe.push_back(eq4); + apipe.push_back(eq5); + passes::BVGauss bgauss(nullptr); std::unordered_map res; - BVGaussElim::gaussElimRewrite(ass); + 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( @@ -2411,12 +2477,12 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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()); + 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() @@ -2444,9 +2510,14 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_p), d_nine); - std::vector ass = {eq1, eq2}; - BVGaussElim::gaussElimRewrite(ass); - TS_ASSERT(ass.size() == 4); + 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, @@ -2505,12 +2576,12 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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(); + 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)); @@ -2518,15 +2589,15 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite void testGetMinBw1() { - TS_ASSERT(BVGaussElim::getMinBwExpr(utils::mkConst(32, 11)) == 4); + TS_ASSERT(passes::getMinBwExpr(bv::utils::mkConst(32, 11)) == 4); - TS_ASSERT(BVGaussElim::getMinBwExpr(d_p) == 4); - TS_ASSERT(BVGaussElim::getMinBwExpr(d_x) == 16); + TS_ASSERT(passes::getMinBwExpr(d_p) == 4); + TS_ASSERT(passes::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 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)); @@ -2534,132 +2605,132 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node zextop40 = d_nm->mkConst(BitVectorZeroExtend(40)); Node zext40p = d_nm->mkNode(zextop8, d_p); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext40p) == 4); + TS_ASSERT(passes::getMinBwExpr(zext40p) == 4); Node zext40x = d_nm->mkNode(zextop8, d_x); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext40x) == 16); + TS_ASSERT(passes::getMinBwExpr(zext40x) == 16); Node zext48p = d_nm->mkNode(zextop16, d_p); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext48p) == 4); + TS_ASSERT(passes::getMinBwExpr(zext48p) == 4); Node zext48x = d_nm->mkNode(zextop16, d_x); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext48x) == 16); + 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(BVGaussElim::getMinBwExpr(zext48p8) == 4); + TS_ASSERT(passes::getMinBwExpr(zext48p8) == 4); Node zext48x8 = d_nm->mkNode(zextop40, x8); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext48x8) == 8); + TS_ASSERT(passes::getMinBwExpr(zext48x8) == 8); Node mult1p = d_nm->mkNode(kind::BITVECTOR_MULT, extp, extp); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult1p) == 5); + TS_ASSERT(passes::getMinBwExpr(mult1p) == 5); Node mult1x = d_nm->mkNode(kind::BITVECTOR_MULT, extx, extx); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult1x) == 0); + TS_ASSERT(passes::getMinBwExpr(mult1x) == 0); Node mult2p = d_nm->mkNode(kind::BITVECTOR_MULT, zext40p, zext40p); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult2p) == 7); + TS_ASSERT(passes::getMinBwExpr(mult2p) == 7); Node mult2x = d_nm->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x); - TS_ASSERT(BVGaussElim::getMinBwExpr(mult2x) == 32); + TS_ASSERT(passes::getMinBwExpr(mult2x) == 32); NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT); nbmult3p << zext48p << zext48p << zext48p; Node mult3p = nbmult3p; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult3p) == 11); + TS_ASSERT(passes::getMinBwExpr(mult3p) == 11); NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT); nbmult3x << zext48x << zext48x << zext48x; Node mult3x = nbmult3x; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult3x) == 48); + TS_ASSERT(passes::getMinBwExpr(mult3x) == 48); NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT); nbmult4p << zext48p << zext48p8 << zext48p; Node mult4p = nbmult4p; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult4p) == 11); + TS_ASSERT(passes::getMinBwExpr(mult4p) == 11); NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT); nbmult4x << zext48x << zext48x8 << zext48x; Node mult4x = nbmult4x; - TS_ASSERT(BVGaussElim::getMinBwExpr(mult4x) == 40); + TS_ASSERT(passes::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 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 = mkConcat(mkZero(16), zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(concat2p) == 4); - Node concat2x = mkConcat(mkZero(16), zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(concat2x) == 16); + 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(BVGaussElim::getMinBwExpr(udiv1p) == 1); + TS_ASSERT(passes::getMinBwExpr(udiv1p) == 1); Node udiv1x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(udiv1x) == 48); + TS_ASSERT(passes::getMinBwExpr(udiv1x) == 48); Node udiv2p = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p8); - TS_ASSERT(BVGaussElim::getMinBwExpr(udiv2p) == 1); + TS_ASSERT(passes::getMinBwExpr(udiv2p) == 1); Node udiv2x = d_nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x8); - TS_ASSERT(BVGaussElim::getMinBwExpr(udiv2x) == 48); + TS_ASSERT(passes::getMinBwExpr(udiv2x) == 48); Node urem1p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem1p) == 1); + TS_ASSERT(passes::getMinBwExpr(urem1p) == 1); Node urem1x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem1x) == 1); + TS_ASSERT(passes::getMinBwExpr(urem1x) == 1); Node urem2p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p8); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem2p) == 1); + TS_ASSERT(passes::getMinBwExpr(urem2p) == 1); Node urem2x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x8); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem2x) == 16); + TS_ASSERT(passes::getMinBwExpr(urem2x) == 16); Node urem3p = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p8, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem3p) == 1); + TS_ASSERT(passes::getMinBwExpr(urem3p) == 1); Node urem3x = d_nm->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x8, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(urem3x) == 8); + TS_ASSERT(passes::getMinBwExpr(urem3x) == 8); Node add1p = d_nm->mkNode(kind::BITVECTOR_PLUS, extp, extp); - TS_ASSERT(BVGaussElim::getMinBwExpr(add1p) == 5); + TS_ASSERT(passes::getMinBwExpr(add1p) == 5); Node add1x = d_nm->mkNode(kind::BITVECTOR_PLUS, extx, extx); - TS_ASSERT(BVGaussElim::getMinBwExpr(add1x) == 0); + TS_ASSERT(passes::getMinBwExpr(add1x) == 0); Node add2p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40p, zext40p); - TS_ASSERT(BVGaussElim::getMinBwExpr(add2p) == 5); + TS_ASSERT(passes::getMinBwExpr(add2p) == 5); Node add2x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext40x, zext40x); - TS_ASSERT(BVGaussElim::getMinBwExpr(add2x) == 17); + TS_ASSERT(passes::getMinBwExpr(add2x) == 17); Node add3p = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48p8, zext48p); - TS_ASSERT(BVGaussElim::getMinBwExpr(add3p) == 5); + TS_ASSERT(passes::getMinBwExpr(add3p) == 5); Node add3x = d_nm->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x); - TS_ASSERT(BVGaussElim::getMinBwExpr(add3x) == 17); + TS_ASSERT(passes::getMinBwExpr(add3x) == 17); NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS); nbadd4p << zext48p << zext48p << zext48p; Node add4p = nbadd4p; - TS_ASSERT(BVGaussElim::getMinBwExpr(add4p) == 6); + TS_ASSERT(passes::getMinBwExpr(add4p) == 6); NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS); nbadd4x << zext48x << zext48x << zext48x; Node add4x = nbadd4x; - TS_ASSERT(BVGaussElim::getMinBwExpr(add4x) == 18); + TS_ASSERT(passes::getMinBwExpr(add4x) == 18); NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS); nbadd5p << zext48p << zext48p8 << zext48p; Node add5p = nbadd5p; - TS_ASSERT(BVGaussElim::getMinBwExpr(add5p) == 6); + TS_ASSERT(passes::getMinBwExpr(add5p) == 6); NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS); nbadd5x << zext48x << zext48x8 << zext48x; Node add5x = nbadd5x; - TS_ASSERT(BVGaussElim::getMinBwExpr(add5x) == 18); + TS_ASSERT(passes::getMinBwExpr(add5x) == 18); NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS); nbadd6p << zext48p << zext48p << zext48p << zext48p; Node add6p = nbadd6p; - TS_ASSERT(BVGaussElim::getMinBwExpr(add6p) == 6); + TS_ASSERT(passes::getMinBwExpr(add6p) == 6); NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS); nbadd6x << zext48x << zext48x << zext48x << zext48x; Node add6x = nbadd6x; - TS_ASSERT(BVGaussElim::getMinBwExpr(add6x) == 18); + TS_ASSERT(passes::getMinBwExpr(add6x) == 18); Node not1p = d_nm->mkNode(kind::BITVECTOR_NOT, zext40p); - TS_ASSERT(BVGaussElim::getMinBwExpr(not1p) == 40); + TS_ASSERT(passes::getMinBwExpr(not1p) == 40); Node not1x = d_nm->mkNode(kind::BITVECTOR_NOT, zext40x); - TS_ASSERT(BVGaussElim::getMinBwExpr(not1x) == 40); + TS_ASSERT(passes::getMinBwExpr(not1x) == 40); } void testGetMinBw2() @@ -2669,9 +2740,9 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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 ext = bv::utils::mkExtract(zext1, 7, 0); Node zext2 = d_nm->mkNode(zextop5, ext); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext2) == 4); + TS_ASSERT(passes::getMinBwExpr(zext2) == 4); } void testGetMinBw3a() @@ -2685,11 +2756,11 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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 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 = mkConcat(mkZero(5), udiv2); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext2) == 5); + Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); + TS_ASSERT(passes::getMinBwExpr(zext2) == 5); } void testGetMinBw3b() @@ -2700,11 +2771,11 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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 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 = mkConcat(mkZero(5), udiv2); - TS_ASSERT(BVGaussElim::getMinBwExpr(zext2) == 5); + Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2); + TS_ASSERT(passes::getMinBwExpr(zext2) == 5); } void testGetMinBw4a() @@ -2725,19 +2796,19 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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 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 = mkConcat(mkZero(5), udiv2_1); + Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1); - Node ext1_2 = mkExtract(zext1, 2, 0); - Node ext2_2 = mkExtract(z, 2, 0); + 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(BVGaussElim::getMinBwExpr(plus) == 6); + TS_ASSERT(passes::getMinBwExpr(plus) == 6); } void testGetMinBw4b() @@ -2755,19 +2826,19 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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 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 = mkConcat(mkZero(5), udiv2_1); + Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1); - Node ext1_2 = mkExtract(zext1, 2, 0); - Node ext2_2 = mkExtract(d_z, 2, 0); + 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(BVGaussElim::getMinBwExpr(plus) == 6); + TS_ASSERT(passes::getMinBwExpr(plus) == 6); } void testGetMinBw5a() @@ -2798,13 +2869,13 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite * (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 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)); @@ -2816,54 +2887,54 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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)); + 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(BVGaussElim::getMinBwExpr(plus7) == 0); + TS_ASSERT(passes::getMinBwExpr(plus7) == 0); } void testGetMinBw5b() @@ -2894,13 +2965,13 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite * (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 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)); @@ -2911,55 +2982,55 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite 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)); + 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(BVGaussElim::getMinBwExpr(plus7) == 19); - TS_ASSERT(BVGaussElim::getMinBwExpr(Rewriter::rewrite(plus7)) == 17); + TS_ASSERT(passes::getMinBwExpr(plus7) == 19); + TS_ASSERT(passes::getMinBwExpr(Rewriter::rewrite(plus7)) == 17); } }; -- 2.30.2