Refactoring finite bounds in Quantifiers Engine (#3261)

1 files changed, 57 insertions, 13 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index def1f969c..a03596060 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/anti_skolem.h"
 #include "theory/quantifiers/conjecture_generator.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/inst_propagator.h"
@@ -384,10 +385,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
   return d_tr_trie.get();
 }
 
-quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const
-{
-  return d_private->d_bint.get();
-}
 quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const
 {
   return d_private->d_synth_e.get();
@@ -445,19 +442,66 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
   return mo==m || mo==NULL;
 }
 
-bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
-  if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){
+bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
+{
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi && bi->isBound(q, v))
+  {
     return true;
-  }else{
-    TypeNode tn = v.getType();
-    if( tn.isSort() && options::finiteModelFind() ){
-      return true;
-    }
-    else if (d_term_enum->mayComplete(tn))
+  }
+  TypeNode tn = v.getType();
+  if (tn.isSort() && options::finiteModelFind())
+  {
+    return true;
+  }
+  else if (d_term_enum->mayComplete(tn))
+  {
+    return true;
+  }
+  return false;
+}
+
+BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
+{
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi)
+  {
+    return bi->getBoundVarType(q, v);
+  }
+  return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
+}
+
+void QuantifiersEngine::getBoundVarIndices(Node q,
+                                           std::vector<unsigned>& indices) const
+{
+  Assert(indices.empty());
+  // we take the bounded variables first
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi)
+  {
+    bi->getBoundVarIndices(q, indices);
+  }
+  // then get the remaining ones
+  for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+  {
+    if (std::find(indices.begin(), indices.end(), i) == indices.end())
     {
-      return true;
+      indices.push_back(i);
     }
   }
+}
+
+bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
+                                         bool initial,
+                                         Node q,
+                                         Node v,
+                                         std::vector<Node>& elements) const
+{
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi)
+  {
+    return bi->getBoundElements(rsi, initial, q, v, elements);
+  }
   return false;
 }