1 files changed, 43 insertions, 13 deletions

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index f873b94f2..87f0b1ffe 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4;
@@ -93,10 +94,6 @@ void BoundedIntegers::presolve() {
   d_bnd_it.clear();
 }
 
-bool BoundedIntegers::isBound( Node f, Node v ) {
-  return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
-}
-
 bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) {
   if( visited.find( b )==visited.end() ){
     visited[b] = true;
@@ -299,11 +296,13 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
   }
   Trace("bint-engine") << "   addedLemma = " << addedLemma << std::endl;
 }
-void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
+void BoundedIntegers::setBoundedVar(Node q, Node v, BoundVarType bound_type)
+{
   d_bound_type[q][v] = bound_type;
   d_set_nums[q][v] = d_set[q].size();
   d_set[q].push_back( v );
-  Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; 
+  Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v
+                         << std::endl;
 }
 
 void BoundedIntegers::checkOwnership(Node f)
@@ -505,12 +504,43 @@ void BoundedIntegers::checkOwnership(Node f)
   }
 }
 
-unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) {
-  std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v );
-  if( it==d_bound_type[q].end() ){
+bool BoundedIntegers::isBound(Node q, Node v) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator its = d_set.find(q);
+  if (its == d_set.end())
+  {
+    return false;
+  }
+  return std::find(its->second.begin(), its->second.end(), v)
+         != its->second.end();
+}
+
+BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const
+{
+  std::map<Node, std::map<Node, BoundVarType> >::const_iterator itb =
+      d_bound_type.find(q);
+  if (itb == d_bound_type.end())
+  {
     return BOUND_NONE;
-  }else{
-    return it->second;
+  }
+  std::map<Node, BoundVarType>::const_iterator it = itb->second.find(v);
+  if (it == itb->second.end())
+  {
+    return BOUND_NONE;
+  }
+  return it->second;
+}
+
+void BoundedIntegers::getBoundVarIndices(Node q,
+                                         std::vector<unsigned>& indices) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it = d_set.find(q);
+  if (it != d_set.end())
+  {
+    for (const Node& v : it->second)
+    {
+      indices.push_back(d_quantEngine->getTermUtil()->getVariableNum(q, v));
+    }
   }
 }
 
@@ -546,7 +576,7 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
 
 bool BoundedIntegers::isGroundRange(Node q, Node v)
 {
-  if (isBoundVar(q, v))
+  if (isBound(q, v))
   {
     if (d_bound_type[q][v] == BOUND_INT_RANGE)
     {
@@ -727,7 +757,7 @@ Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
 bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
   if( initial || !isGroundRange( q, v ) ){
     elements.clear();
-    unsigned bvt = getBoundVarType( q, v );
+    BoundVarType bvt = getBoundVarType(q, v);
     if( bvt==BOUND_INT_RANGE ){
       Node l, u;
       getBoundValues( q, v, rsi, l, u );