diff options
Diffstat (limited to 'src/theory/arith/nl/iand_utils.cpp')
-rw-r--r-- | src/theory/arith/nl/iand_utils.cpp | 29 |
1 files changed, 18 insertions, 11 deletions
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 45881e1bb..50e03bfa5 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -22,6 +22,8 @@ #include "theory/rewriter.h" #include "util/rational.h" +using namespace cvc5::kind; + namespace cvc5 { namespace theory { namespace arith { @@ -36,7 +38,7 @@ Node pow2(uint64_t k) { Assert(k >= 0); NodeManager* nm = NodeManager::currentNM(); - return nm->mkConst<Rational>(intpow2(k)); + return nm->mkConst(CONST_RATIONAL, Rational(intpow2(k))); } bool oneBitAnd(bool a, bool b) { return (a && b); } @@ -58,9 +60,9 @@ Node intExtract(Node x, uint64_t i, uint64_t size) IAndUtils::IAndUtils() { NodeManager* nm = NodeManager::currentNM(); - d_zero = nm->mkConst(Rational(0)); - d_one = nm->mkConst(Rational(1)); - d_two = nm->mkConst(Rational(2)); + d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + d_one = nm->mkConst(CONST_RATIONAL, Rational(1)); + d_two = nm->mkConst(CONST_RATIONAL, Rational(2)); } Node IAndUtils::createITEFromTable( @@ -78,7 +80,8 @@ 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<Rational>(table.at(std::make_pair(-1, -1))); + Node ite = + nm->mkConst(CONST_RATIONAL, 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++) @@ -91,10 +94,13 @@ 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<Rational>(i)), - nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))), - nm->mkConst<Rational>(table.at(std::make_pair(i, j))), + 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)))), ite); } } @@ -133,7 +139,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<Rational>(0); + Node sumNode = nm->mkConst(CONST_RATIONAL, Rational(0)); // compute the table for the current granularity if needed if (d_bvandTable.find(granularity) == d_bvandTable.end()) { @@ -260,7 +266,8 @@ 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))); + Node ret = + nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k))); ret = Rewriter::rewrite(ret); return ret; } |