From e7caa82b1def3cab78a95b38841242264124efe7 Mon Sep 17 00:00:00 2001 From: makaimann Date: Mon, 7 Dec 2020 13:39:15 -0800 Subject: [PATCH] Add bitwise refinement mode for IAND (#5328) Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits. For example, with a 1-bit granularity, you might learn a lemma like: ((_ iand 4) x y), value = 1 actual (2, 3) = 2 bv-value = #b0001 bv-actual (#b0010, #b0011) = #b0010 IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y))) (and (and true (= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0))) (= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0)))) ; BITWISE_REFINE which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics. --- src/CMakeLists.txt | 4 +- src/preprocessing/passes/bv_to_int.cpp | 8 +- src/preprocessing/passes/bv_to_int.h | 6 +- src/theory/arith/inference_id.cpp | 1 + src/theory/arith/inference_id.h | 4 +- src/theory/arith/inference_manager.cpp | 9 +- src/theory/arith/inference_manager.h | 3 +- src/theory/arith/nl/iand_solver.cpp | 109 ++++++++++++------ src/theory/arith/nl/iand_solver.h | 24 ++-- .../nl/{iand_table.cpp => iand_utils.cpp} | 75 ++++++++++-- .../arith/nl/{iand_table.h => iand_utils.h} | 49 +++++++- test/regress/regress1/nl/iand-native-1.smt2 | 6 + test/regress/regress1/nl/iand-native-2.smt2 | 1 + .../nl/iand-native-granularities.smt2 | 22 ++++ ...eck_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 | 1 + 15 files changed, 240 insertions(+), 82 deletions(-) rename src/theory/arith/nl/{iand_table.cpp => iand_utils.cpp} (75%) rename src/theory/arith/nl/{iand_table.h => iand_utils.h} (76%) create mode 100644 test/regress/regress1/nl/iand-native-granularities.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4b5c37d9e..3da032021 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -373,8 +373,8 @@ libcvc4_add_sources( theory/arith/nl/icp/icp_solver.h theory/arith/nl/icp/intersection.cpp theory/arith/nl/icp/intersection.h - theory/arith/nl/iand_table.cpp - theory/arith/nl/iand_table.h + theory/arith/nl/iand_utils.cpp + theory/arith/nl/iand_utils.h theory/arith/nl/nl_lemma_utils.cpp theory/arith/nl/nl_lemma_utils.h theory/arith/nl/nl_model.cpp diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index f14eafcc4..8539e639d 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -424,10 +424,10 @@ Node BVToInt::translateWithChildren(Node original, // Construct a sum of ites, based on granularity. Assert(translated_children.size() == 2); returnNode = - d_iandTable.createBitwiseNode(translated_children[0], - translated_children[1], - bvsize, - options::BVAndIntegerGranularity()); + d_iandUtils.createSumNode(translated_children[0], + translated_children[1], + bvsize, + options::BVAndIntegerGranularity()); } break; } diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index 0f6a6a4bb..dd830d7cf 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -47,8 +47,6 @@ ** Tr((bvand s t)) = ** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g) ** - ** More details and examples for this case are described next to - ** the function createBitwiseNode. ** Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor. ** ** Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of @@ -75,7 +73,7 @@ #include "context/context.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" -#include "theory/arith/nl/iand_table.h" +#include "theory/arith/nl/iand_utils.h" namespace CVC4 { namespace preprocessing { @@ -284,7 +282,7 @@ class BVToInt : public PreprocessingPass Node d_one; /** helper class for handeling bvand translation */ - theory::arith::nl::IAndTable d_iandTable; + theory::arith::nl::IAndUtils d_iandUtils; }; } // namespace passes diff --git a/src/theory/arith/inference_id.cpp b/src/theory/arith/inference_id.cpp index 0c2ead445..4bdbacbc7 100644 --- a/src/theory/arith/inference_id.cpp +++ b/src/theory/arith/inference_id.cpp @@ -41,6 +41,7 @@ const char* toString(InferenceId i) case InferenceId::NL_IAND_INIT_REFINE: return "IAND_INIT_REFINE"; case InferenceId::NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE"; case InferenceId::NL_IAND_SUM_REFINE: return "IAND_SUM_REFINE"; + case InferenceId::NL_IAND_BITWISE_REFINE: return "IAND_BITWISE_REFINE"; case InferenceId::NL_CAD_CONFLICT: return "CAD_CONFLICT"; case InferenceId::NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL"; case InferenceId::NL_ICP_CONFLICT: return "ICP_CONFLICT"; diff --git a/src/theory/arith/inference_id.h b/src/theory/arith/inference_id.h index ea7fd6fe9..853965dc9 100644 --- a/src/theory/arith/inference_id.h +++ b/src/theory/arith/inference_id.h @@ -71,8 +71,10 @@ enum class InferenceId : uint32_t NL_IAND_INIT_REFINE, // value refinements (IAndSolver::checkFullRefine) NL_IAND_VALUE_REFINE, - // sum refinements (IAndSulver::checkFullRefine) + // sum refinements (IAndSolver::checkFullRefine) NL_IAND_SUM_REFINE, + // bitwise refinements (IAndSolver::checkFullRefine) + NL_IAND_BITWISE_REFINE, //-------------------- cad solver // conflict / infeasible subset obtained from cad NL_CAD_CONFLICT, diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 08d223137..e22be81e3 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -69,11 +69,12 @@ void InferenceManager::addPendingArithLemma(const ArithLemma& lemma, void InferenceManager::addPendingArithLemma(const Node& lemma, InferenceId inftype, ProofGenerator* pg, - bool isWaiting) + bool isWaiting, + LemmaProperty p) { - addPendingArithLemma(std::unique_ptr(new ArithLemma( - lemma, LemmaProperty::NONE, pg, inftype)), - isWaiting); + addPendingArithLemma( + std::unique_ptr(new ArithLemma(lemma, p, pg, inftype)), + isWaiting); } void InferenceManager::flushWaitingLemmas() diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 66710cd7b..0f2614fd7 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -71,7 +71,8 @@ class InferenceManager : public InferenceManagerBuffered void addPendingArithLemma(const Node& lemma, InferenceId inftype, ProofGenerator* pg = nullptr, - bool isWaiting = false); + bool isWaiting = false, + LemmaProperty p = LemmaProperty::NONE); /** * Flush all waiting lemmas to this inference manager (as pending diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 4d17080a6..f908145fe 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -34,12 +34,11 @@ IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model) d_initRefine(state.getUserContext()) { NodeManager* nm = NodeManager::currentNM(); - d_true = nm->mkConst(true); d_false = nm->mkConst(false); + d_true = nm->mkConst(true); d_zero = nm->mkConst(Rational(0)); d_one = nm->mkConst(Rational(1)); d_two = nm->mkConst(Rational(2)); - d_neg_one = nm->mkConst(Rational(-1)); } IAndSolver::~IAndSolver() {} @@ -90,7 +89,7 @@ void IAndSolver::checkInitialRefine() // conj.push_back(i.eqNode(nm->mkNode(IAND, op, i[1], i[0]))); // 0 <= iand(x,y) < 2^k conj.push_back(nm->mkNode(LEQ, d_zero, i)); - conj.push_back(nm->mkNode(LT, i, twoToK(k))); + conj.push_back(nm->mkNode(LT, i, d_iandUtils.twoToK(k))); // iand(x,y)<=x conj.push_back(nm->mkNode(LEQ, i, i[0])); // iand(x,y)<=y @@ -151,12 +150,24 @@ void IAndSolver::checkFullRefine() Node lem = sumBasedLemma(i); // add lemmas based on sum mode Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; - d_im.addPendingArithLemma( - lem, InferenceId::NL_IAND_SUM_REFINE, nullptr, true); + // lemma can contain div/mod so need to tag it with the PREPROCESS lemma property + d_im.addPendingArithLemma(lem, + InferenceId::NL_IAND_SUM_REFINE, + nullptr, + true, + LemmaProperty::PREPROCESS); } else if (options::iandMode() == options::IandMode::BITWISE) { - // add lemmas based on sum mode + Node lem = bitwiseLemma(i); // check for violated bitwise axioms + Trace("iand-lemma") + << "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl; + // lemma can contain div/mod so need to tag it with the PREPROCESS lemma property + d_im.addPendingArithLemma(lem, + InferenceId::NL_IAND_BITWISE_REFINE, + nullptr, + true, + LemmaProperty::PREPROCESS); } else { @@ -164,8 +175,12 @@ void IAndSolver::checkFullRefine() Node lem = valueBasedLemma(i); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; - d_im.addPendingArithLemma( - lem, InferenceId::NL_IAND_VALUE_REFINE, nullptr, true); + // value lemmas should not contain div/mod so we don't need to tag it with PREPROCESS + d_im.addPendingArithLemma(lem, + InferenceId::NL_IAND_VALUE_REFINE, + nullptr, + true, + LemmaProperty::NONE); } } } @@ -180,24 +195,6 @@ Node IAndSolver::convertToBvK(unsigned k, Node n) const return Rewriter::rewrite(bn); } -Node IAndSolver::twoToK(unsigned k) const -{ - // could be faster - NodeManager* nm = NodeManager::currentNM(); - Node ret = nm->mkNode(POW, d_two, nm->mkConst(Rational(k))); - ret = Rewriter::rewrite(ret); - return ret; -} - -Node IAndSolver::twoToKMinusOne(unsigned k) const -{ - // could be faster - NodeManager* nm = NodeManager::currentNM(); - Node ret = nm->mkNode(MINUS, twoToK(k), d_one); - ret = Rewriter::rewrite(ret); - return ret; -} - Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const { NodeManager* nm = NodeManager::currentNM(); @@ -217,17 +214,7 @@ Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const Node IAndSolver::mkINot(unsigned k, Node x) const { NodeManager* nm = NodeManager::currentNM(); - Node ret = nm->mkNode(MINUS, twoToKMinusOne(k), x); - ret = Rewriter::rewrite(ret); - return ret; -} - -Node IAndSolver::iextract(unsigned i, unsigned j, Node n) const -{ - NodeManager* nm = NodeManager::currentNM(); - // ((_ extract i j) n) is n / 2^j mod 2^{i-j+1} - Node n2j = nm->mkNode(INTS_DIVISION_TOTAL, n, twoToK(j)); - Node ret = nm->mkNode(INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1)); + Node ret = nm->mkNode(MINUS, d_iandUtils.twoToKMinusOne(k), x); ret = Rewriter::rewrite(ret); return ret; } @@ -259,7 +246,53 @@ Node IAndSolver::sumBasedLemma(Node i) uint64_t granularity = options::BVAndIntegerGranularity(); NodeManager* nm = NodeManager::currentNM(); Node lem = nm->mkNode( - EQUAL, i, d_iandTable.createBitwiseNode(x, y, bvsize, granularity)); + EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity)); + return lem; +} + +Node IAndSolver::bitwiseLemma(Node i) +{ + Assert(i.getKind() == IAND); + Node x = i[0]; + Node y = i[1]; + + unsigned bvsize = i.getOperator().getConst().d_size; + uint64_t granularity = options::BVAndIntegerGranularity(); + + Rational absI = d_model.computeAbstractModelValue(i).getConst(); + Rational concI = d_model.computeConcreteModelValue(i).getConst(); + + Assert(absI.isIntegral()); + Assert(concI.isIntegral()); + + BitVector bvAbsI = BitVector(bvsize, absI.getNumerator()); + BitVector bvConcI = BitVector(bvsize, concI.getNumerator()); + + NodeManager* nm = NodeManager::currentNM(); + Node lem = d_true; + + // compare each bit to bvI + Node cond; + Node bitIAnd; + unsigned high_bit; + for (unsigned j = 0; j < bvsize; j += granularity) + { + high_bit = j + granularity - 1; + // don't let high_bit pass bvsize + if (high_bit >= bvsize) + { + high_bit = bvsize - 1; + } + + // check if the abstraction differs from the concrete one on these bits + if (bvAbsI.extract(high_bit, j) != bvConcI.extract(high_bit, j)) + { + bitIAnd = d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j); + // enforce bitwise equality + lem = nm->mkNode( + AND, lem, d_iandUtils.iextract(high_bit, j, i).eqNode(bitIAnd)); + } + } return lem; } diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 8d91cc28a..c854f3ab7 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/iand_table.h" +#include "theory/arith/nl/iand_utils.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" @@ -83,13 +83,13 @@ class IAndSolver /** Reference to the non-linear model object */ NlModel& d_model; /** commonly used terms */ + Node d_false; + Node d_true; Node d_zero; Node d_one; - Node d_neg_one; Node d_two; - Node d_true; - Node d_false; - IAndTable d_iandTable; + + IAndUtils d_iandUtils; /** IAND terms that have been given initial refinement lemmas */ NodeSet d_initRefine; /** all IAND terms, for each bit-width */ @@ -100,20 +100,12 @@ class IAndSolver * equivalent to Rewriter::rewrite( ((_ intToBv k) n) ). */ Node convertToBvK(unsigned k, Node n) const; - /** 2^k */ - Node twoToK(unsigned k) const; - /** 2^k-1 */ - Node twoToKMinusOne(unsigned k) const; /** make iand */ Node mkIAnd(unsigned k, Node x, Node y) const; /** make ior */ Node mkIOr(unsigned k, Node x, Node y) const; /** make inot */ Node mkINot(unsigned k, Node i) const; - /** extract from integer - * ((_ extract i j) n) is n / 2^j mod 2^{i-j+1} - */ - Node iextract(unsigned i, unsigned j, Node n) const; /** * Value-based refinement lemma for i of the form ((_ iand k) x y). Returns: * x = M(x) ^ y = M(y) => @@ -127,6 +119,12 @@ class IAndSolver * and min is defined with an ite. */ Node sumBasedLemma(Node i); + /** Bitwise refinement lemma for i of the form ((_ iand k) x y). Returns: + * x[j] & y[j] == ite(x[j] == 1 /\ y[j] == 1, 1, 0) + * for all j where M(x)[j] ^ M(y)[j] + * does not match M(((_ iand k) x y)) + */ + Node bitwiseLemma(Node i); }; /* class IAndSolver */ } // namespace nl diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_utils.cpp similarity index 75% rename from src/theory/arith/nl/iand_table.cpp rename to src/theory/arith/nl/iand_utils.cpp index 550f36d92..8f0441c28 100644 --- a/src/theory/arith/nl/iand_table.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file iand_table.cpp +/*! \file iand_utils.cpp ** \verbatim ** Top contributors (to current version): ** Yoni Zohar @@ -13,7 +13,7 @@ ** the value of iand. **/ -#include "theory/arith/nl/iand_table.h" +#include "theory/arith/nl/iand_utils.h" #include @@ -52,7 +52,15 @@ Node intExtract(Node x, uint64_t i, uint64_t size) return extract; } -Node IAndTable::createITEFromTable( +IAndUtils::IAndUtils() +{ + NodeManager* nm = NodeManager::currentNM(); + d_zero = nm->mkConst(Rational(0)); + d_one = nm->mkConst(Rational(1)); + d_two = nm->mkConst(Rational(2)); +} + +Node IAndUtils::createITEFromTable( Node x, Node y, uint64_t granularity, @@ -90,10 +98,10 @@ Node IAndTable::createITEFromTable( return ite; } -Node IAndTable::createBitwiseNode(Node x, - Node y, - uint64_t bvsize, - uint64_t granularity) +Node IAndUtils::createSumNode(Node x, + Node y, + uint64_t bvsize, + uint64_t granularity) { NodeManager* nm = NodeManager::currentNM(); Assert(0 < granularity && granularity <= 8); @@ -146,7 +154,35 @@ Node IAndTable::createBitwiseNode(Node x, return sumNode; } -void IAndTable::computeAndTable(uint64_t granularity) +Node IAndUtils::createBitwiseIAndNode(Node x, + Node y, + uint64_t high, + uint64_t low) +{ + uint64_t granularity = high - low + 1; + Assert(granularity <= 8); + // compute the table for the current granularity if needed + if (d_bvandTable.find(granularity) == d_bvandTable.end()) + { + computeAndTable(granularity); + } + const std::map, uint64_t>& table = + d_bvandTable[granularity]; + return createITEFromTable( + iextract(high, low, x), iextract(high, low, y), granularity, table); +} + +Node IAndUtils::iextract(unsigned i, unsigned j, Node n) const +{ + NodeManager* nm = NodeManager::currentNM(); + // ((_ extract i j) n) is n / 2^j mod 2^{i-j+1} + Node n2j = nm->mkNode(kind::INTS_DIVISION_TOTAL, n, twoToK(j)); + Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1)); + ret = Rewriter::rewrite(ret); + return ret; +} + +void IAndUtils::computeAndTable(uint64_t granularity) { Assert(d_bvandTable.find(granularity) == d_bvandTable.end()); // the table was not yet computed @@ -176,12 +212,13 @@ void IAndTable::computeAndTable(uint64_t granularity) } // optimize the table by identifying and adding the default value addDefaultValue(table, num_of_values); - Assert(table.size() == 1 + (static_cast(num_of_values * num_of_values))); + Assert(table.size() + == 1 + (static_cast(num_of_values * num_of_values))); // store the table in the cache and return it d_bvandTable[granularity] = table; } -void IAndTable::addDefaultValue( +void IAndUtils::addDefaultValue( std::map, uint64_t>& table, uint64_t num_of_values) { @@ -216,6 +253,24 @@ void IAndTable::addDefaultValue( table[std::make_pair(-1, -1)] = most_common_result; } +Node IAndUtils::twoToK(unsigned k) const +{ + // could be faster + NodeManager* nm = NodeManager::currentNM(); + Node ret = nm->mkNode(kind::POW, d_two, nm->mkConst(Rational(k))); + ret = Rewriter::rewrite(ret); + return ret; +} + +Node IAndUtils::twoToKMinusOne(unsigned k) const +{ + // could be faster + NodeManager* nm = NodeManager::currentNM(); + Node ret = nm->mkNode(kind::MINUS, twoToK(k), d_one); + ret = Rewriter::rewrite(ret); + return ret; +} + } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/iand_table.h b/src/theory/arith/nl/iand_utils.h similarity index 76% rename from src/theory/arith/nl/iand_table.h rename to src/theory/arith/nl/iand_utils.h index 39eb82355..a05defc0a 100644 --- a/src/theory/arith/nl/iand_table.h +++ b/src/theory/arith/nl/iand_utils.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file iand_table.h +/*! \file iand_utils.h ** \verbatim ** Top contributors (to current version): ** Yoni Zohar @@ -18,6 +18,7 @@ #include #include + #include "expr/node.h" namespace CVC4 { @@ -29,9 +30,11 @@ namespace nl { * A class that computes tables for iand values * with various bit-widths */ -class IAndTable +class IAndUtils { public: + IAndUtils(); + /** * A generic function that creates a node that represents a bvand * operation. @@ -81,10 +84,34 @@ class IAndTable * pass. * @return A node that represents the operation, as described above. */ - Node createBitwiseNode(Node x, Node y, uint64_t bvsize, uint64_t granularity); + Node createSumNode(Node x, Node y, uint64_t bvsize, uint64_t granularity); + + /** Create a bitwise integer And node for two integers x and y for bits + * between hgih and low Example for high = 0, low = 0 (e.g. granularity 1) + * ite(x[0] == 1 & y[0] == 1, #b1, #b0) + * + * It makes use of computeAndTable + * + * @param x an integer operand corresponding to the first original + * bit-vector operand + * @param y an integer operand corresponding to the second original + * bit-vector operand + * @param high the upper bit index + * @param low the lower bit index + * @return an integer node corresponding to a bitwise AND applied to + * integers for the bits between high and low + */ + Node createBitwiseIAndNode(Node x, Node y, uint64_t high, uint64_t low); + + /** extract from integer + * ((_ extract i j) n) is n / 2^j mod 2^{i-j+1} + */ + Node iextract(unsigned i, unsigned j, Node n) const; + + // Helpers /** - * A helper function for createBitwiseNode + * A helper function for createSumNode and createBitwiseIAndNode * @param x integer node corresponding to the original first bit-vector * argument * @param y integer node corresponding to the original second bit-vector @@ -118,14 +145,26 @@ class IAndTable void addDefaultValue(std::map, uint64_t>& table, uint64_t num_of_values); + /** 2^k */ + Node twoToK(unsigned k) const; + + /** 2^k-1 */ + Node twoToKMinusOne(unsigned k) const; + /** * For each granularity between 1 and 8, we store a separate table * in d_bvandTable[granularity]. * The definition of these tables is given in the description of - * createBitwiseNode. + * createSumNode. */ std::map, uint64_t>> d_bvandTable; + + private: + /** commonly used terms */ + Node d_zero; + Node d_one; + Node d_two; }; } // namespace nl diff --git a/test/regress/regress1/nl/iand-native-1.smt2 b/test/regress/regress1/nl/iand-native-1.smt2 index 0f50dcaed..051264cfc 100644 --- a/test/regress/regress1/nl/iand-native-1.smt2 +++ b/test/regress/regress1/nl/iand-native-1.smt2 @@ -1,5 +1,11 @@ ; COMMAND-LINE: --iand-mode=value --no-check-models ; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find --no-check-models +; COMMAND-LINE: --iand-mode=bitwise +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=1 +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=2 +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=4 +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=5 +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=6 ; EXPECT: sat (set-logic QF_NIA) (set-info :status sat) diff --git a/test/regress/regress1/nl/iand-native-2.smt2 b/test/regress/regress1/nl/iand-native-2.smt2 index 6b39598ea..a3474784b 100644 --- a/test/regress/regress1/nl/iand-native-2.smt2 +++ b/test/regress/regress1/nl/iand-native-2.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --iand-mode=value ; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=bitwise ; EXPECT: unsat (set-logic QF_NIA) (set-info :status unsat) diff --git a/test/regress/regress1/nl/iand-native-granularities.smt2 b/test/regress/regress1/nl/iand-native-granularities.smt2 new file mode 100644 index 000000000..92cdfb1ab --- /dev/null +++ b/test/regress/regress1/nl/iand-native-granularities.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --iand-mode=value --no-check-models +; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find --no-check-models +; COMMAND-LINE: --iand-mode=bitwise +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=1 +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=3 +; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=4 +; EXPECT: unsat +(set-logic QF_NIA) +(set-info :status unsat) +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (>= x 0)) +(assert (>= y 0)) + +(assert (<= (+ x y) 32)) + +(assert (or + (>= ((_ iand 5) x y) 32) + (>= ((_ iand 6) x y) 32))) + +(check-sat) \ No newline at end of file diff --git a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 index ed8543050..c4988e3c6 100644 --- a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: --solve-bv-as-int=bv ; COMMAND-LINE: --solve-bv-as-int=sum ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum +; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=bitwise ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value ; EXPECT: unsat (set-logic ALL) -- 2.30.2