diff options
Diffstat (limited to 'src/theory/arith/nl/iand_utils.cpp')
| -rw-r--r-- | src/theory/arith/nl/iand_utils.cpp | 37 |
1 files changed, 13 insertions, 24 deletions
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 50e03bfa5..700eb6de9 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -38,7 +38,7 @@ Node pow2(uint64_t k) { Assert(k >= 0); NodeManager* nm = NodeManager::currentNM(); - return nm->mkConst(CONST_RATIONAL, Rational(intpow2(k))); + return nm->mkConstInt(Rational(intpow2(k))); } bool oneBitAnd(bool a, bool b) { return (a && b); } @@ -60,9 +60,9 @@ Node intExtract(Node x, uint64_t i, uint64_t size) IAndUtils::IAndUtils() { NodeManager* nm = NodeManager::currentNM(); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = nm->mkConst(CONST_RATIONAL, Rational(1)); - d_two = nm->mkConst(CONST_RATIONAL, Rational(2)); + d_zero = nm->mkConstInt(Rational(0)); + d_one = nm->mkConstInt(Rational(1)); + d_two = nm->mkConstInt(Rational(2)); } Node IAndUtils::createITEFromTable( @@ -80,8 +80,7 @@ Node IAndUtils::createITEFromTable( 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(CONST_RATIONAL, Rational(table.at(std::make_pair(-1, -1)))); + Node ite = nm->mkConstInt(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++) @@ -94,13 +93,10 @@ Node IAndUtils::createITEFromTable( // append the current value to the ite. ite = nm->mkNode( kind::ITE, - nm->mkNode( - kind::AND, - nm->mkNode( - kind::EQUAL, x, nm->mkConst(CONST_RATIONAL, Rational(i))), - nm->mkNode( - kind::EQUAL, y, nm->mkConst(CONST_RATIONAL, Rational(j)))), - nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(i, j)))), + nm->mkNode(kind::AND, + nm->mkNode(kind::EQUAL, x, nm->mkConstInt(Rational(i))), + nm->mkNode(kind::EQUAL, y, nm->mkConstInt(Rational(j)))), + nm->mkConstInt(Rational(table.at(std::make_pair(i, j)))), ite); } } @@ -139,7 +135,7 @@ Node IAndUtils::createSumNode(Node x, // number of elements in the sum expression uint64_t sumSize = bvsize / granularity; // initialize the sum - Node sumNode = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node sumNode = nm->mkConstInt(Rational(0)); // compute the table for the current granularity if needed if (d_bvandTable.find(granularity) == d_bvandTable.end()) { @@ -186,9 +182,7 @@ 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; + return nm->mkNode(kind::INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1)); } void IAndUtils::computeAndTable(uint64_t granularity) @@ -266,19 +260,14 @@ Node IAndUtils::twoToK(unsigned k) const { // could be faster NodeManager* nm = NodeManager::currentNM(); - Node ret = - nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k))); - ret = Rewriter::rewrite(ret); - return ret; + return nm->mkNode(kind::POW, d_two, nm->mkConstInt(Rational(k))); } 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; + return nm->mkNode(kind::MINUS, twoToK(k), d_one); } } // namespace nl |