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.
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
// 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;
}
** 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
#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 {
Node d_one;
/** helper class for handeling bvand translation */
- theory::arith::nl::IAndTable d_iandTable;
+ theory::arith::nl::IAndUtils d_iandUtils;
};
} // namespace passes
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";
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,
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()
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
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() {}
// 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
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
{
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);
}
}
}
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();
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;
}
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;
}
#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"
/** 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 */
* 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) =>
* 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
+++ /dev/null
-/********************* */
-/*! \file iand_table.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Yoni Zohar
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Utilities to maintain finite tables that represent
- ** the value of iand.
- **/
-
-#include "theory/arith/nl/iand_table.h"
-
-#include <cmath>
-
-#include "cvc4_private.h"
-#include "theory/arith/nl/nl_model.h"
-namespace CVC4 {
-namespace theory {
-namespace arith {
-namespace nl {
-
-static Rational intpow2(uint64_t b)
-{
- return Rational(Integer(2).pow(b), Integer(1));
-}
-
-Node pow2(uint64_t k)
-{
- Assert(k >= 0);
- NodeManager* nm = NodeManager::currentNM();
- return nm->mkConst<Rational>(intpow2(k));
-}
-
-bool oneBitAnd(bool a, bool b) { return (a && b); }
-
-// computes (bv_to_int ((_ extract i+size-1 i) (int_to_bv x))))
-Node intExtract(Node x, uint64_t i, uint64_t size)
-{
- Assert(size > 0);
- NodeManager* nm = NodeManager::currentNM();
- // extract definition in integers is:
- // (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
- Node extract =
- nm->mkNode(kind::INTS_MODULUS_TOTAL,
- nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * size)),
- pow2(size));
- return extract;
-}
-
-Node IAndTable::createITEFromTable(
- Node x,
- Node y,
- uint64_t granularity,
- const std::map<std::pair<int64_t, int64_t>, uint64_t>& table)
-{
- NodeManager* nm = NodeManager::currentNM();
- Assert(granularity <= 8);
- uint64_t num_of_values = ((uint64_t)pow(2, granularity));
- // The table represents a function from pairs of integers to integers, where
- // all integers are between 0 (inclusive) and num_of_values (exclusive).
- // additionally, there is a default value (-1, -1).
- Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
- // start with the default, most common value.
- // this value is represented in the table by (-1, -1).
- Node ite = nm->mkConst<Rational>(table.at(std::make_pair(-1, -1)));
- for (uint64_t i = 0; i < num_of_values; i++)
- {
- for (uint64_t j = 0; j < num_of_values; j++)
- {
- // skip the most common value, as it was already stored.
- if (table.at(std::make_pair(i, j)) == table.at(std::make_pair(-1, -1)))
- {
- continue;
- }
- // append the current value to the ite.
- ite = nm->mkNode(
- kind::ITE,
- nm->mkNode(kind::AND,
- nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
- nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
- nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
- ite);
- }
- }
- return ite;
-}
-
-Node IAndTable::createBitwiseNode(Node x,
- Node y,
- uint64_t bvsize,
- uint64_t granularity)
-{
- NodeManager* nm = NodeManager::currentNM();
- Assert(0 < granularity && granularity <= 8);
- // Standardize granularity.
- // If it is greater than bvsize, it is set to bvsize.
- // Otherwise, it is set to the closest (going down) divider of bvsize.
- if (granularity > bvsize)
- {
- granularity = bvsize;
- }
- else
- {
- while (bvsize % granularity != 0)
- {
- granularity = granularity - 1;
- }
- }
-
- // Create the sum.
- // For granularity 1, the sum has bvsize elements.
- // In contrast, if bvsize = granularity, sum has one element.
- // Each element in the sum is an ite that corresponds to the generated table,
- // multiplied by the appropriate power of two.
- // More details are in bv_to_int.h .
-
- // number of elements in the sum expression
- uint64_t sumSize = bvsize / granularity;
- // initialize the sum
- Node sumNode = nm->mkConst<Rational>(0);
- // 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];
- for (uint64_t i = 0; i < sumSize; i++)
- {
- // compute the current blocks of x and y
- Node xExtract = intExtract(x, i, granularity);
- Node yExtract = intExtract(y, i, granularity);
- // compute the ite for this part
- Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table);
- // append the current block to the sum
- sumNode =
- nm->mkNode(kind::PLUS,
- sumNode,
- nm->mkNode(kind::MULT, pow2(i * granularity), sumPart));
- }
- return sumNode;
-}
-
-void IAndTable::computeAndTable(uint64_t granularity)
-{
- Assert(d_bvandTable.find(granularity) == d_bvandTable.end());
- // the table was not yet computed
- std::map<std::pair<int64_t, int64_t>, uint64_t> table;
- uint64_t num_of_values = ((uint64_t)pow(2, granularity));
- // populate the table with all the values
- for (uint64_t i = 0; i < num_of_values; i++)
- {
- for (uint64_t j = 0; j < num_of_values; j++)
- {
- // compute
- // (bv_to_int (bvand ((int_to_bv granularity) i) ((int_to_bv granularity)
- // j)))
- int64_t sum = 0;
- for (uint64_t n = 0; n < granularity; n++)
- {
- // b is the result of f on the current bit
- bool b = oneBitAnd((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
- // add the corresponding power of 2 only if the result is 1
- if (b)
- {
- sum += 1 << n;
- }
- }
- table[std::make_pair(i, j)] = sum;
- }
- }
- // 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)));
- // store the table in the cache and return it
- d_bvandTable[granularity] = table;
-}
-
-void IAndTable::addDefaultValue(
- std::map<std::pair<int64_t, int64_t>, uint64_t>& table,
- uint64_t num_of_values)
-{
- // map each result to the number of times it occurs
- std::map<uint64_t, uint64_t> counters;
- for (uint64_t i = 0; i <= num_of_values; i++)
- {
- counters[i] = 0;
- }
- for (const std::pair<std::pair<int64_t, int64_t>, uint64_t>& element : table)
- {
- uint64_t result = element.second;
- counters[result]++;
- }
-
- // compute the most common result
- uint64_t most_common_result = 0;
- uint64_t max_num_of_occ = 0;
- for (uint64_t i = 0; i <= num_of_values; i++)
- {
- if (counters[i] >= max_num_of_occ)
- {
- max_num_of_occ = counters[i];
- most_common_result = i;
- }
- }
- // sanity check: some value appears at least once.
- Assert(max_num_of_occ != 0);
-
- // -1 is the default case of the table.
- // add it to the table
- table[std::make_pair(-1, -1)] = most_common_result;
-}
-
-} // namespace nl
-} // namespace arith
-} // namespace theory
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file iand_table.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Yoni Zohar
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Utilities to maintain finite tables that represent
- ** the value of iand.
- **/
-
-#ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
-#define CVC4__THEORY__ARITH__IAND_TABLE_H
-
-#include <tuple>
-#include <vector>
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-namespace nl {
-
-/**
- * A class that computes tables for iand values
- * with various bit-widths
- */
-class IAndTable
-{
- public:
- /**
- * A generic function that creates a node that represents a bvand
- * operation.
- *
- * For example: Suppose bvsize is 4, granularity is 1.
- * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)).
- * The result of this function would be:
- * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3
- *
- * For another example: Suppose bvsize is 4, granularity is 2,
- * and f(x,y) = x && y.
- * Denote by ITE(a,b) the term that corresponds to the following table:
- * a | b | ITE(a,b)
- * ----------------
- * 0 | 0 | 0
- * 0 | 1 | 0
- * 0 | 2 | 0
- * 0 | 3 | 0
- * 1 | 0 | 0
- * 1 | 1 | 1
- * 1 | 2 | 0
- * 1 | 3 | 1
- * 2 | 0 | 0
- * 2 | 1 | 0
- * 2 | 2 | 2
- * 2 | 3 | 2
- * 3 | 0 | 0
- * 3 | 1 | 1
- * 3 | 2 | 2
- * 3 | 3 | 3
- *
- * For example, 2 in binary is 10 and 1 in binary is 01, and so doing
- * "bitwise f" on them gives 00.
- * The result of this function would be:
- * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2
- *
- * More precisely, the ITE term is optimized so that the most common
- * result is in the final "else" branch.
- * Hence in practice, the generated ITEs will be shorter.
- *
- * @param x is an integer operand that correspond to the first original
- * bit-vector operand.
- * @param y is an integer operand that correspond to the second original
- * bit-vector operand.
- * @param bvsize is the bit width of the original bit-vector variables.
- * @param granularity is specified in the options for this preprocessing
- * pass.
- * @return A node that represents the operation, as described above.
- */
- Node createBitwiseNode(Node x, Node y, uint64_t bvsize, uint64_t granularity);
-
- /**
- * A helper function for createBitwiseNode
- * @param x integer node corresponding to the original first bit-vector
- * argument
- * @param y integer node corresponding to the original second bit-vector
- * argument nodes.
- * @param granularity the bitwidth of the original bit-vector nodes.
- * @param table a function from pairs of integers to integers.
- * The domain of this function consists of pairs of
- * integers between 0 (inclusive) and 2^{bitwidth} (exclusive).
- * The domain also includes one additional pair (-1, -1), that
- * represents the default (most common) value.
- * @return An ite term that represents this table.
- */
- Node createITEFromTable(
- Node x,
- Node y,
- uint64_t granularity,
- const std::map<std::pair<int64_t, int64_t>, uint64_t>& table);
-
- /**
- * updates d_bvandTable[granularity] if it wasn't already computed.
- */
- void computeAndTable(uint64_t granularity);
-
- /**
- * @param table a table that represents integer conjunction
- * @param num_of_values the number of rows in the table
- * The function will add a single row to the table.
- * the key will be (-1, -1) and the value will be the most common
- * value of the original table.
- */
- void addDefaultValue(std::map<std::pair<int64_t, int64_t>, uint64_t>& table,
- uint64_t num_of_values);
-
- /**
- * 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.
- */
- std::map<uint64_t, std::map<std::pair<int64_t, int64_t>, uint64_t>>
- d_bvandTable;
-};
-
-} // namespace nl
-} // namespace arith
-} // namespace theory
-} // namespace CVC4
-
-#endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */
--- /dev/null
+/********************* */
+/*! \file iand_utils.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Utilities to maintain finite tables that represent
+ ** the value of iand.
+ **/
+
+#include "theory/arith/nl/iand_utils.h"
+
+#include <cmath>
+
+#include "cvc4_private.h"
+#include "theory/arith/nl/nl_model.h"
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+static Rational intpow2(uint64_t b)
+{
+ return Rational(Integer(2).pow(b), Integer(1));
+}
+
+Node pow2(uint64_t k)
+{
+ Assert(k >= 0);
+ NodeManager* nm = NodeManager::currentNM();
+ return nm->mkConst<Rational>(intpow2(k));
+}
+
+bool oneBitAnd(bool a, bool b) { return (a && b); }
+
+// computes (bv_to_int ((_ extract i+size-1 i) (int_to_bv x))))
+Node intExtract(Node x, uint64_t i, uint64_t size)
+{
+ Assert(size > 0);
+ NodeManager* nm = NodeManager::currentNM();
+ // extract definition in integers is:
+ // (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
+ Node extract =
+ nm->mkNode(kind::INTS_MODULUS_TOTAL,
+ nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * size)),
+ pow2(size));
+ return extract;
+}
+
+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,
+ const std::map<std::pair<int64_t, int64_t>, uint64_t>& table)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Assert(granularity <= 8);
+ uint64_t num_of_values = ((uint64_t)pow(2, granularity));
+ // The table represents a function from pairs of integers to integers, where
+ // all integers are between 0 (inclusive) and num_of_values (exclusive).
+ // additionally, there is a default value (-1, -1).
+ Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
+ // start with the default, most common value.
+ // this value is represented in the table by (-1, -1).
+ Node ite = nm->mkConst<Rational>(table.at(std::make_pair(-1, -1)));
+ for (uint64_t i = 0; i < num_of_values; i++)
+ {
+ for (uint64_t j = 0; j < num_of_values; j++)
+ {
+ // skip the most common value, as it was already stored.
+ if (table.at(std::make_pair(i, j)) == table.at(std::make_pair(-1, -1)))
+ {
+ continue;
+ }
+ // append the current value to the ite.
+ ite = nm->mkNode(
+ kind::ITE,
+ nm->mkNode(kind::AND,
+ nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
+ nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
+ nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
+ ite);
+ }
+ }
+ return ite;
+}
+
+Node IAndUtils::createSumNode(Node x,
+ Node y,
+ uint64_t bvsize,
+ uint64_t granularity)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Assert(0 < granularity && granularity <= 8);
+ // Standardize granularity.
+ // If it is greater than bvsize, it is set to bvsize.
+ // Otherwise, it is set to the closest (going down) divider of bvsize.
+ if (granularity > bvsize)
+ {
+ granularity = bvsize;
+ }
+ else
+ {
+ while (bvsize % granularity != 0)
+ {
+ granularity = granularity - 1;
+ }
+ }
+
+ // Create the sum.
+ // For granularity 1, the sum has bvsize elements.
+ // In contrast, if bvsize = granularity, sum has one element.
+ // Each element in the sum is an ite that corresponds to the generated table,
+ // multiplied by the appropriate power of two.
+ // More details are in bv_to_int.h .
+
+ // number of elements in the sum expression
+ uint64_t sumSize = bvsize / granularity;
+ // initialize the sum
+ Node sumNode = nm->mkConst<Rational>(0);
+ // 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];
+ for (uint64_t i = 0; i < sumSize; i++)
+ {
+ // compute the current blocks of x and y
+ Node xExtract = intExtract(x, i, granularity);
+ Node yExtract = intExtract(y, i, granularity);
+ // compute the ite for this part
+ Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table);
+ // append the current block to the sum
+ sumNode =
+ nm->mkNode(kind::PLUS,
+ sumNode,
+ nm->mkNode(kind::MULT, pow2(i * granularity), sumPart));
+ }
+ return sumNode;
+}
+
+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
+ std::map<std::pair<int64_t, int64_t>, uint64_t> table;
+ uint64_t num_of_values = ((uint64_t)pow(2, granularity));
+ // populate the table with all the values
+ for (uint64_t i = 0; i < num_of_values; i++)
+ {
+ for (uint64_t j = 0; j < num_of_values; j++)
+ {
+ // compute
+ // (bv_to_int (bvand ((int_to_bv granularity) i) ((int_to_bv granularity)
+ // j)))
+ int64_t sum = 0;
+ for (uint64_t n = 0; n < granularity; n++)
+ {
+ // b is the result of f on the current bit
+ bool b = oneBitAnd((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
+ // add the corresponding power of 2 only if the result is 1
+ if (b)
+ {
+ sum += 1 << n;
+ }
+ }
+ table[std::make_pair(i, j)] = sum;
+ }
+ }
+ // 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)));
+ // store the table in the cache and return it
+ d_bvandTable[granularity] = table;
+}
+
+void IAndUtils::addDefaultValue(
+ std::map<std::pair<int64_t, int64_t>, uint64_t>& table,
+ uint64_t num_of_values)
+{
+ // map each result to the number of times it occurs
+ std::map<uint64_t, uint64_t> counters;
+ for (uint64_t i = 0; i <= num_of_values; i++)
+ {
+ counters[i] = 0;
+ }
+ for (const std::pair<std::pair<int64_t, int64_t>, uint64_t>& element : table)
+ {
+ uint64_t result = element.second;
+ counters[result]++;
+ }
+
+ // compute the most common result
+ uint64_t most_common_result = 0;
+ uint64_t max_num_of_occ = 0;
+ for (uint64_t i = 0; i <= num_of_values; i++)
+ {
+ if (counters[i] >= max_num_of_occ)
+ {
+ max_num_of_occ = counters[i];
+ most_common_result = i;
+ }
+ }
+ // sanity check: some value appears at least once.
+ Assert(max_num_of_occ != 0);
+
+ // -1 is the default case of the table.
+ // add it to the table
+ 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
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file iand_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Utilities to maintain finite tables that represent
+ ** the value of iand.
+ **/
+
+#ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
+#define CVC4__THEORY__ARITH__IAND_TABLE_H
+
+#include <tuple>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+/**
+ * A class that computes tables for iand values
+ * with various bit-widths
+ */
+class IAndUtils
+{
+ public:
+ IAndUtils();
+
+ /**
+ * A generic function that creates a node that represents a bvand
+ * operation.
+ *
+ * For example: Suppose bvsize is 4, granularity is 1.
+ * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)).
+ * The result of this function would be:
+ * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3
+ *
+ * For another example: Suppose bvsize is 4, granularity is 2,
+ * and f(x,y) = x && y.
+ * Denote by ITE(a,b) the term that corresponds to the following table:
+ * a | b | ITE(a,b)
+ * ----------------
+ * 0 | 0 | 0
+ * 0 | 1 | 0
+ * 0 | 2 | 0
+ * 0 | 3 | 0
+ * 1 | 0 | 0
+ * 1 | 1 | 1
+ * 1 | 2 | 0
+ * 1 | 3 | 1
+ * 2 | 0 | 0
+ * 2 | 1 | 0
+ * 2 | 2 | 2
+ * 2 | 3 | 2
+ * 3 | 0 | 0
+ * 3 | 1 | 1
+ * 3 | 2 | 2
+ * 3 | 3 | 3
+ *
+ * For example, 2 in binary is 10 and 1 in binary is 01, and so doing
+ * "bitwise f" on them gives 00.
+ * The result of this function would be:
+ * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2
+ *
+ * More precisely, the ITE term is optimized so that the most common
+ * result is in the final "else" branch.
+ * Hence in practice, the generated ITEs will be shorter.
+ *
+ * @param x is an integer operand that correspond to the first original
+ * bit-vector operand.
+ * @param y is an integer operand that correspond to the second original
+ * bit-vector operand.
+ * @param bvsize is the bit width of the original bit-vector variables.
+ * @param granularity is specified in the options for this preprocessing
+ * pass.
+ * @return A node that represents the operation, as described above.
+ */
+ 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 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
+ * argument nodes.
+ * @param granularity the bitwidth of the original bit-vector nodes.
+ * @param table a function from pairs of integers to integers.
+ * The domain of this function consists of pairs of
+ * integers between 0 (inclusive) and 2^{bitwidth} (exclusive).
+ * The domain also includes one additional pair (-1, -1), that
+ * represents the default (most common) value.
+ * @return An ite term that represents this table.
+ */
+ Node createITEFromTable(
+ Node x,
+ Node y,
+ uint64_t granularity,
+ const std::map<std::pair<int64_t, int64_t>, uint64_t>& table);
+
+ /**
+ * updates d_bvandTable[granularity] if it wasn't already computed.
+ */
+ void computeAndTable(uint64_t granularity);
+
+ /**
+ * @param table a table that represents integer conjunction
+ * @param num_of_values the number of rows in the table
+ * The function will add a single row to the table.
+ * the key will be (-1, -1) and the value will be the most common
+ * value of the original table.
+ */
+ 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
+ * 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
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */
; 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)
; 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)
--- /dev/null
+; 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
; 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)
projects / cvc5.git / commitdiff