diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 26b526315..b5b9e7d88 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -59,7 +59,7 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n) { NodeManager* nm = NodeManager::currentNM(); - Node cn = nm->mkConst(Rational(n == 0 ? 0 : n - 1)); + Node cn = nm->mkConst(CONST_RATIONAL, Rational(n == 0 ? 0 : n - 1)); return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn); } @@ -81,12 +81,13 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() d_ranges_proxied[curr] = true; NodeManager* nm = NodeManager::currentNM(); Node currLit = getLiteral(curr); - Node lem = - nm->mkNode(EQUAL, - currLit, - nm->mkNode(curr == 0 ? LT : LEQ, - d_range, - nm->mkConst(Rational(curr == 0 ? 0 : curr - 1)))); + Node lem = nm->mkNode( + EQUAL, + currLit, + nm->mkNode( + curr == 0 ? LT : LEQ, + d_range, + nm->mkConst(CONST_RATIONAL, Rational(curr == 0 ? 0 : curr - 1)))); return lem; } @@ -692,7 +693,8 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { } choices.pop_back(); Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i); - Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i))); + Node cMinCard = + nm->mkNode(LEQ, srCardN, nm->mkConst(CONST_RATIONAL, Rational(i))); choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody)); d_setm_choice[sro].push_back(choice_i); } @@ -816,7 +818,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node range = rewrite(nm->mkNode(MINUS, u, l)); // 9999 is an arbitrary range past which we do not do exhaustive // bounded instantation, based on the check below. - Node ra = rewrite(nm->mkNode(LEQ, range, nm->mkConst(Rational(9999)))); + Node ra = rewrite(nm->mkNode( + LEQ, range, nm->mkConst(CONST_RATIONAL, Rational(9999)))); Node tl = l; Node tu = u; getBounds( q, v, rsi, tl, tu ); @@ -827,7 +830,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for (long k = 0; k < rr; k++) { - Node t = nm->mkNode(PLUS, tl, nm->mkConst(Rational(k))); + Node t = + nm->mkNode(PLUS, tl, nm->mkConst(CONST_RATIONAL, Rational(k))); t = rewrite(t); elements.push_back( t ); } |