From: makaimann Date: Mon, 7 Dec 2020 21:39:15 +0000 (-0800) Subject: Add bitwise refinement mode for IAND (#5328) X-Git-Tag: cvc5-1.0.0~2489 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7caa82b1def3cab78a95b38841242264124efe7;p=cvc5.git 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. --- 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_table.cpp deleted file mode 100644 index 550f36d92..000000000 --- a/src/theory/arith/nl/iand_table.cpp +++ /dev/null @@ -1,222 +0,0 @@ -/********************* */ -/*! \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 - -#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(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, 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(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(i)), - nm->mkNode(kind::EQUAL, y, nm->mkConst(j))), - nm->mkConst(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(0); - // 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]; - 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, 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(num_of_values * num_of_values))); - // store the table in the cache and return it - d_bvandTable[granularity] = table; -} - -void IAndTable::addDefaultValue( - std::map, uint64_t>& table, - uint64_t num_of_values) -{ - // map each result to the number of times it occurs - std::map counters; - for (uint64_t i = 0; i <= num_of_values; i++) - { - counters[i] = 0; - } - for (const std::pair, 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 diff --git a/src/theory/arith/nl/iand_table.h b/src/theory/arith/nl/iand_table.h deleted file mode 100644 index 39eb82355..000000000 --- a/src/theory/arith/nl/iand_table.h +++ /dev/null @@ -1,136 +0,0 @@ -/********************* */ -/*! \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 -#include -#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, 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, 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>> - d_bvandTable; -}; - -} // namespace nl -} // namespace arith -} // namespace theory -} // namespace CVC4 - -#endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */ diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp new file mode 100644 index 000000000..8f0441c28 --- /dev/null +++ b/src/theory/arith/nl/iand_utils.cpp @@ -0,0 +1,277 @@ +/********************* */ +/*! \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 + +#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(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, 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(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(i)), + nm->mkNode(kind::EQUAL, y, nm->mkConst(j))), + nm->mkConst(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(0); + // 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]; + 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, 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, 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(num_of_values * num_of_values))); + // store the table in the cache and return it + d_bvandTable[granularity] = table; +} + +void IAndUtils::addDefaultValue( + std::map, uint64_t>& table, + uint64_t num_of_values) +{ + // map each result to the number of times it occurs + std::map counters; + for (uint64_t i = 0; i <= num_of_values; i++) + { + counters[i] = 0; + } + for (const std::pair, 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 diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h new file mode 100644 index 000000000..a05defc0a --- /dev/null +++ b/src/theory/arith/nl/iand_utils.h @@ -0,0 +1,175 @@ +/********************* */ +/*! \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 +#include + +#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, 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, 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>> + 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 */ 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)