summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt4
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp8
-rw-r--r--src/preprocessing/passes/bv_to_int.h6
-rw-r--r--src/theory/arith/inference_id.cpp1
-rw-r--r--src/theory/arith/inference_id.h4
-rw-r--r--src/theory/arith/inference_manager.cpp9
-rw-r--r--src/theory/arith/inference_manager.h3
-rw-r--r--src/theory/arith/nl/iand_solver.cpp109
-rw-r--r--src/theory/arith/nl/iand_solver.h24
-rw-r--r--src/theory/arith/nl/iand_utils.cpp (renamed from src/theory/arith/nl/iand_table.cpp)75
-rw-r--r--src/theory/arith/nl/iand_utils.h (renamed from src/theory/arith/nl/iand_table.h)49
-rw-r--r--test/regress/regress1/nl/iand-native-1.smt26
-rw-r--r--test/regress/regress1/nl/iand-native-2.smt21
-rw-r--r--test/regress/regress1/nl/iand-native-granularities.smt222
-rw-r--r--test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt21
15 files changed, 240 insertions, 82 deletions
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<ArithLemma>(new ArithLemma(
- lemma, LemmaProperty::NONE, pg, inftype)),
- isWaiting);
+ addPendingArithLemma(
+ std::unique_ptr<ArithLemma>(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<IntAnd>().d_size;
+ uint64_t granularity = options::BVAndIntegerGranularity();
+
+ Rational absI = d_model.computeAbstractModelValue(i).getConst<Rational>();
+ Rational concI = d_model.computeConcreteModelValue(i).getConst<Rational>();
+
+ 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
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 <cmath>
@@ -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<std::pair<int64_t, int64_t>, 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<uint64_t>(num_of_values * num_of_values)));
+ Assert(table.size()
+ == 1 + (static_cast<uint64_t>(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<std::pair<int64_t, int64_t>, 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
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 <tuple>
#include <vector>
+
#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<std::pair<int64_t, int64_t>, 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, std::map<std::pair<int64_t, int64_t>, 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback