diff options
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index e1e2f96c2..30ff5242b 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -321,7 +321,7 @@ Node BoundedIntegers::getNextDecisionRequest() { return Node::null(); } -void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { +void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { l = d_bounds[0][f][v]; u = d_bounds[1][f][v]; if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){ @@ -356,6 +356,10 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); } } +} + +void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { + getBounds( f, v, rsi, l, u ); Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl; l = d_quantEngine->getModel()->getCurrentModelValue( l ); u = d_quantEngine->getModel()->getCurrentModelValue( u ); |