Add new symmetry breaking technique for finite model finding. Improvements to bounded integer quantifier instantiation.

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 );