Refactoring finite bounds in Quantifiers Engine (#3261)

5 files changed, 110 insertions, 43 deletions

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 879771903..87f0b1ffe 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -94,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;
@@ -300,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)
@@ -506,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));
+    }
   }
 }
 
@@ -547,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)
     {
@@ -728,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 );
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 8e6738e9e..d668c6f02 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -30,28 +30,23 @@ class RepSetIterator;
 
 namespace quantifiers {
 
-
 class BoundedIntegers : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDHashMap<int, bool> IntBoolMap;
-public:
-  enum {
-    BOUND_FINITE,
-    BOUND_INT_RANGE,
-    BOUND_SET_MEMBER,
-    BOUND_FIXED_SET,
-    BOUND_NONE
-  };
 private:
   //for determining bounds
-  bool isBound( Node f, Node v );
   bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited );
   bool hasNonBoundVar( Node f, Node b );
-  //bound type
-  std::map< Node, std::map< Node, unsigned > > d_bound_type;
+  /** The bound type for each quantified formula, variable pair */
+  std::map<Node, std::map<Node, BoundVarType>> d_bound_type;
+  /**
+   * The ordered list of variables that are finitely bound, for each quantified
+   * formulas. Variables that occur later in this list may depend on having
+   * finite bounds for variables earlier in this list.
+   */
   std::map< Node, std::vector< Node > > d_set;
   std::map< Node, std::map< Node, int > > d_set_nums;
   std::map< Node, std::map< Node, Node > > d_range;
@@ -152,9 +147,6 @@ private:
     }
   };
   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
-private:
-  
-  void setBoundedVar( Node f, Node v, unsigned bound_type );
 public:
   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
   virtual ~BoundedIntegers();
@@ -163,11 +155,54 @@ public:
   bool needsCheck(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
   void checkOwnership(Node q) override;
-  bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
-  unsigned getBoundVarType( Node q, Node v );
-  unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
-  Node getBoundVar( Node q, int i ) { return d_set[q][i]; }
-private:
+  /**
+   * Is v a variable of quantified formula q that this class has inferred to
+   * have a finite bound?
+   */
+  bool isBound(Node q, Node v) const;
+  /**
+   * Get the type of bound that was inferred for variable v of quantified
+   * formula q, or BOUND_NONE if no bound was inferred.
+   */
+  BoundVarType getBoundVarType(Node q, Node v) const;
+  /**
+   * Get the indices of bound variables, in the order they should be processed
+   * in a RepSetIterator. For example, for q:
+   *   forall xyz. 0 <= x < 5 ^ 0 <= z <= x+7 => P(x,y,z)
+   * this would add {1,3} to the vector indices, indicating that x has a finite
+   * bound, z has a finite bound assuming x has a finite bound, and y does not
+   * have a finite bound.
+   */
+  void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
+  /**
+   * Get bound elements
+   *
+   * This gets the (finite) enumeration of the range of variable v of quantified
+   * formula q and adds it into the vector elements in the context of the
+   * iteration being performed by rsi. It returns true if it could successfully
+   * determine this range.
+   *
+   * This method determines the range of a variable depending on the current
+   * state of the iterator rsi and flag initial (which is true when rsi is
+   * being initialized). For example, if q is:
+   *   forall xy. 0 <= x < 5 ^ 0 <= y <= x+7 => P(x,y)
+   * v is y, and rsi currently maps x to 4, then we add the elements 0...11 to
+   * the vector elements.
+   */
+  bool getBoundElements(RepSetIterator* rsi,
+                        bool initial,
+                        Node q,
+                        Node v,
+                        std::vector<Node>& elements);
+  /** Identify this module */
+  std::string identify() const override { return "BoundedIntegers"; }
+
+ private:
+  /**
+   * Set that variable v of quantified formula q has a finite bound, where
+   * bound_type indicates how that bound was inferred.
+   */
+  void setBoundedVar(Node f, Node v, BoundVarType bound_type);
   //for integer range
   Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
   Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; }
@@ -180,11 +215,6 @@ private:
   Node matchBoundVar( Node v, Node t, Node e );
   
   bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
-public:
-  bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements );
-
-  /** Identify this module */
-  std::string identify() const override { return "BoundedIntegers"; }
 };
 
 }
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 0f06cef74..2306a0565 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -19,6 +19,7 @@
 #include "options/uf_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -746,14 +747,15 @@ class RepBoundFmcEntry : public QRepBoundExt
   }
   ~RepBoundFmcEntry() {}
   /** set bound */
-  virtual RepSetIterator::RsiEnumType setBound(
-      Node owner, unsigned i, std::vector<Node>& elements) override
+  virtual RsiEnumType setBound(Node owner,
+                               unsigned i,
+                               std::vector<Node>& elements) override
   {
     if (!d_fm->isStar(d_entry[i]))
     {
       // only need to consider the single point
       elements.push_back(d_entry[i]);
-      return RepSetIterator::ENUM_DEFAULT;
+      return ENUM_DEFAULT;
     }
     return QRepBoundExt::setBound(owner, i, elements);
   }
@@ -820,8 +822,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       int index = riter.increment();
       Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
       if( !riter.isFinished() ){
-        if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_BOUND_INT ) {
-          Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
+        if (index >= 0 && riter.d_index[index] > 0 && addedLemmas > 0
+            && riter.d_enum_type[index] == ENUM_CUSTOM)
+        {
+          Trace("fmc-exh-debug")
+              << "Since this is a custom enumeration, skip to the next..."
+              << std::endl;
           riter.incrementAtIndex(index - 1);
         }
       }
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index cdbc5e391..63f004448 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index f34dc1b85..35d1f82fd 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"