(Refactor) Decouple rep set iterator and quantifiers (#1339)

* Refactoring rep set iterator, does not modify rep set externally.

* Decouple quantifiers engine and rep set iterator.

* Documentation

* Clang format

* Minor

* Minor

* More

* Format

* Address review.

* Format

* Minor

1 files changed, 112 insertions, 116 deletions

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 5c02b631c..bff5e36cd 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -14,18 +14,14 @@
 
 #include <unordered_set>
 
-#include "theory/quantifiers/bounded_integers.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/rep_set.h"
 #include "theory/type_enumerator.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace theory {
 
 void RepSet::clear(){
   d_type_reps.clear();
@@ -64,6 +60,14 @@ Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
   return it->second[i];
 }
 
+void RepSet::getRepresentatives(TypeNode tn, std::vector<Node>& reps) const
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_reps.find(tn);
+  Assert(it != d_type_reps.end());
+  reps.insert(reps.end(), it->second.begin(), it->second.end());
+}
+
 bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
 {
   if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
@@ -184,43 +188,44 @@ void RepSet::toStream(std::ostream& out){
   }
 }
 
-
-RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
-  d_incomplete = false;
+RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext)
+    : d_rs(rs), d_rext(rext), d_incomplete(false)
+{
 }
 
-int RepSetIterator::domainSize( int i ) {
-  Assert(i>=0);
-  int v = d_var_order[i];
+unsigned RepSetIterator::domainSize(unsigned i)
+{
+  unsigned v = d_var_order[i];
   return d_domain_elements[v].size();
 }
 
-bool RepSetIterator::setQuantifier( Node f, RepBoundExt* rext ){
-  Trace("rsi") << "Make rsi for " << f << std::endl;
+bool RepSetIterator::setQuantifier(Node q)
+{
+  Trace("rsi") << "Make rsi for quantified formula " << q << std::endl;
   Assert( d_types.empty() );
   //store indicies
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    d_types.push_back( f[0][i].getType() );
+  for (size_t i = 0; i < q[0].getNumChildren(); i++)
+  {
+    d_types.push_back(q[0][i].getType());
   }
-  d_owner = f;
-  return initialize( rext );
+  d_owner = q;
+  return initialize();
 }
 
-bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){
-  Trace("rsi") << "Make rsi for " << op << std::endl;
+bool RepSetIterator::setFunctionDomain(Node op)
+{
+  Trace("rsi") << "Make rsi for function " << op << std::endl;
   Assert( d_types.empty() );
   TypeNode tn = op.getType();
   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
     d_types.push_back( tn[i] );
   }
   d_owner = op;
-  return initialize( rext );
+  return initialize();
 }
 
-// TODO : as part of #1199, the portions of this
-// function which modify d_rep_set should be
-// moved to TheoryModel.
-bool RepSetIterator::initialize( RepBoundExt* rext ){
+bool RepSetIterator::initialize()
+{
   Trace("rsi") << "Initialize rep set iterator..." << std::endl;
   for( unsigned v=0; v<d_types.size(); v++ ){
     d_index.push_back( 0 );
@@ -232,103 +237,81 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){
     d_domain_elements.push_back( std::vector< Node >() );
     TypeNode tn = d_types[v];
     Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
-    if( tn.isSort() ){
-      //must ensure uninterpreted type is non-empty.
-      if( !d_rep_set->hasType( tn ) ){
-        //FIXME:
-        // terms in rep_set are now constants which mapped to terms through TheoryModel
-        // thus, should introduce a constant and a term.  for now, just a term.
-
-        //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 );
-        Node var = d_qe->getModel()->getSomeDomainElement( tn );
-        Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
-        d_rep_set->add( tn, var );
-      }
-    }
     bool inc = true;
+    bool setEnum = false;
     //check if it is externally bound
-    if( rext && rext->setBound( d_owner, v, tn, d_domain_elements[v] ) ){
-      d_enum_type.push_back( ENUM_DEFAULT );
-      inc = false;
-    //builtin: check if it is bound by bounded integer module
-    }else if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
-      if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
-        unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
-        if( bvt!=quantifiers::BoundedIntegers::BOUND_FINITE ){
-          d_enum_type.push_back( ENUM_BOUND_INT );
-          inc = false;
-        }else{
-          //will treat in default way
-        }
+    if (d_rext)
+    {
+      inc = !d_rext->initializeRepresentativesForType(tn);
+      RsiEnumType rsiet = d_rext->setBound(d_owner, v, d_domain_elements[v]);
+      if (rsiet != ENUM_INVALID)
+      {
+        d_enum_type.push_back(rsiet);
+        inc = false;
+        setEnum = true;
       }
     }
-    if( !tn.isSort() ){
-      if( inc ){
-        if (d_qe->getTermEnumeration()->mayComplete(tn))
-        {
-          Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
-          d_rep_set->complete( tn );
-          //must have succeeded
-          Assert( d_rep_set->hasType( tn ) );
-        }else{
-          Trace("rsi") << "  variable cannot be bounded." << std::endl;
-          Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
-          d_incomplete = true;
-        }
-      }
+    if (inc)
+    {
+      Trace("fmf-incomplete") << "Incomplete because of quantification of type "
+                              << tn << std::endl;
+      d_incomplete = true;
     }
 
     //if we have yet to determine the type of enumeration
-    if( d_enum_type.size()<=v ){
-      if( d_rep_set->hasType( tn ) ){
+    if (!setEnum)
+    {
+      if (d_rs->hasType(tn))
+      {
         d_enum_type.push_back( ENUM_DEFAULT );
-        for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
-          //d_domain[v].push_back( j );
-          d_domain_elements[v].push_back( d_rep_set->d_type_reps[tn][j] );
-        }
+        d_rs->getRepresentatives(tn, d_domain_elements[v]);
       }else{
         Assert( d_incomplete );
         return false;
       }
     }
   }
-  //must set a variable index order based on bounded integers
-  if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
-    Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
-    std::vector< int > varOrder;
-    for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){
-      Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i );
-      Trace("bound-int-rsi") << "  bound var #" << i << " is " << v << std::endl;
-      varOrder.push_back( d_qe->getTermUtil()->getVariableNum( d_owner, v ) );
-    }
-    for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
-      if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
-        varOrder.push_back(i);
+
+  if (d_rext)
+  {
+    std::vector<unsigned> varOrder;
+    if (d_rext->getVariableOrder(d_owner, varOrder))
+    {
+      if (Trace.isOn("bound-int-rsi"))
+      {
+        Trace("bound-int-rsi") << "Variable order : ";
+        for (unsigned i = 0; i < varOrder.size(); i++)
+        {
+          Trace("bound-int-rsi") << varOrder[i] << " ";
+        }
+        Trace("bound-int-rsi") << std::endl;
       }
+      std::vector<unsigned> indexOrder;
+      indexOrder.resize(varOrder.size());
+      for (unsigned i = 0; i < varOrder.size(); i++)
+      {
+        Assert(varOrder[i] < indexOrder.size());
+        indexOrder[varOrder[i]] = i;
+      }
+      if (Trace.isOn("bound-int-rsi"))
+      {
+        Trace("bound-int-rsi") << "Will use index order : ";
+        for (unsigned i = 0; i < indexOrder.size(); i++)
+        {
+          Trace("bound-int-rsi") << indexOrder[i] << " ";
+        }
+        Trace("bound-int-rsi") << std::endl;
+      }
+      setIndexOrder(indexOrder);
     }
-    Trace("bound-int-rsi") << "Variable order : ";
-    for( unsigned i=0; i<varOrder.size(); i++) {
-      Trace("bound-int-rsi") << varOrder[i] << " ";
-    }
-    Trace("bound-int-rsi") << std::endl;
-    std::vector< int > indexOrder;
-    indexOrder.resize(varOrder.size());
-    for( unsigned i=0; i<varOrder.size(); i++){
-      indexOrder[varOrder[i]] = i;
-    }
-    Trace("bound-int-rsi") << "Will use index order : ";
-    for( unsigned i=0; i<indexOrder.size(); i++) {
-      Trace("bound-int-rsi") << indexOrder[i] << " ";
-    }
-    Trace("bound-int-rsi") << std::endl;
-    setIndexOrder( indexOrder );
   }
   //now reset the indices
   do_reset_increment( -1, true );
   return true;
 }
 
-void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
+void RepSetIterator::setIndexOrder(std::vector<unsigned>& indexOrder)
+{
   d_index_order.clear();
   d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
   //make the d_var_order mapping
@@ -337,20 +320,23 @@ void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
   }
 }
 
-int RepSetIterator::resetIndex( int i, bool initial ) {
+int RepSetIterator::resetIndex(unsigned i, bool initial)
+{
   d_index[i] = 0;
-  int v = d_var_order[i];
+  unsigned v = d_var_order[i];
   Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
-  if( d_enum_type[v]==ENUM_BOUND_INT ){
-    Assert( d_owner.getKind()==FORALL );
-    if( !d_qe->getBoundedIntegers()->getBoundElements( this, initial, d_owner, d_owner[0][v], d_domain_elements[v] ) ){
+  if (d_rext)
+  {
+    if (!d_rext->resetIndex(this, d_owner, v, initial, d_domain_elements[v]))
+    {
       return -1;
     }
   }
   return d_domain_elements[v].empty() ? 0 : 1;
 }
 
-int RepSetIterator::increment2( int i ){
+int RepSetIterator::incrementAtIndex(int i)
+{
   Assert( !isFinished() );
 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
   i = (int)d_index.size()-1;
@@ -402,23 +388,31 @@ int RepSetIterator::do_reset_increment( int i, bool initial ) {
 
 int RepSetIterator::increment(){
   if( !isFinished() ){
-    return increment2( (int)d_index.size()-1 );
+    return incrementAtIndex(d_index.size() - 1);
   }else{
     return -1;
   }
 }
 
-bool RepSetIterator::isFinished(){
-  return d_index.empty();
-}
+bool RepSetIterator::isFinished() const { return d_index.empty(); }
 
-Node RepSetIterator::getCurrentTerm( int v ){
-  int ii = d_index_order[v];
-  int curr = d_index[ii];
+Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm)
+{
+  unsigned ii = d_index_order[v];
+  unsigned curr = d_index[ii];
   Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
   Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl;
-  Assert( 0<=curr && curr<(int)d_domain_elements[v].size() );
-  return d_domain_elements[v][curr];
+  Assert(0 <= curr && curr < d_domain_elements[v].size());
+  Node t = d_domain_elements[v][curr];
+  if (valTerm)
+  {
+    Node tt = d_rs->getTermForRepresentative(t);
+    if (!tt.isNull())
+    {
+      return tt;
+    }
+  }
+  return t;
 }
 
 void RepSetIterator::debugPrint( const char* c ){
@@ -435,3 +429,5 @@ void RepSetIterator::debugPrintSmall( const char* c ){
   Debug( c ) << std::endl;
 }
 
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */