initial modifications for per-ic cbqi

1 files changed, 117 insertions, 94 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index a5031a061..4fe4072a3 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -41,6 +41,19 @@ bool InstStrategySimplex::calculateShouldProcess( Node f ){
   return false;
 }
 
+void getInstantiationConstants( Node n, std::vector< Node >& ics ){
+  if( n.getKind()==INST_CONSTANT ){
+    if( std::find( ics.begin(), ics.end(), n )==ics.end() ){
+      ics.push_back( n );
+    }
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      getInstantiationConstants( n[i], ics );
+    }
+  }
+}
+
+
 void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
   Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
   d_instRows.clear();
@@ -54,121 +67,128 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
     ArithVar x = *vi;
     if( d_th->d_internal->d_partialModel.hasEitherBound( x ) ){
       Node n = avnm.asNode(x);
-      Node f;
-      NodeBuilder<> t(kind::PLUS);
-      if( n.getKind()==PLUS ){
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          addTermToRow( x, n[i], f, t );
+
+      //collect instantiation constants
+      std::vector< Node > ics;
+      getInstantiationConstants( n, ics );
+      for( unsigned i=0; i<ics.size(); i++ ){
+
+        NodeBuilder<> t(kind::PLUS);
+        if( n.getKind()==PLUS ){
+          for( int j=0; j<(int)n.getNumChildren(); j++ ){
+            addTermToRow( ics[i], x, n[j], t );
+          }
+        }else{
+          addTermToRow( ics[i], x, n, t );
         }
-      }else{
-        addTermToRow( x, n, f, t );
-      }
-      if( f!=Node::null() ){
-        d_instRows[f].push_back( x );
+        d_instRows[ics[i]].push_back( x );
         //this theory has constraints from f
+        Node f = TermDb::getInstConstAttr(ics[i]);
         Debug("quant-arith") << "Has constraints from " << f << std::endl;
         //set that we should process it
         d_quantActive[ f ] = true;
         //set tableaux term
         if( t.getNumChildren()==0 ){
-          d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
+          d_tableaux_term[ics[i]][x] = NodeManager::currentNM()->mkConst( Rational(0) );
         }else if( t.getNumChildren()==1 ){
-          d_tableaux_term[x] = t.getChild( 0 );
+          d_tableaux_term[ics[i]][x] = t.getChild( 0 );
         }else{
-          d_tableaux_term[x] = t;
+          d_tableaux_term[ics[i]][x] = t;
         }
       }
     }
   }
   //print debug
+  Debug("quant-arith-debug") << std::endl;
   debugPrint( "quant-arith-debug" );
   d_counter++;
 }
 
-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( e<2 ){
-    return STATUS_UNFINISHED;
-  }else if( e==2 ){
-    //Notice() << f << std::endl;
-    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
-    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
-    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;
-    for( int j=0; j<(int)d_instRows[f].size(); j++ ){
-      ArithVar x = d_instRows[f][j];
-      if( !d_ceTableaux[x].empty() ){
-        Debug("quant-arith-simplex") << "Check row " << x << std::endl;
-        //instantiation row will be A*e + B*t = beta,
-        // where e is a vector of terms , and t is vector of ground terms.
-        // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
-        // We will construct the term ( beta - B*t)/coeff to use for e_i.
-        InstMatch m;
-        //By default, choose the first instantiation constant to be e_i.
-        Node var = d_ceTableaux[x].begin()->first;
-        if( var.getType().isInteger() ){
-          std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
-          //try to find coefficent that is +/- 1
-          while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
-            ++it;
-            if( it==d_ceTableaux[x].end() ){
-              var = Node::null();
-            }else{
-              var = it->first;
-            }
-          }
-          //otherwise, try one that divides all ground term coefficients? DO_THIS
-        }
-        if( !var.isNull() ){
-          Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
-          doInstantiation( f, d_tableaux_term[x], x, m, var );
-        }else{
-          Debug("quant-arith-simplex") << "Could not find var." << std::endl;
-        }
-        ////choose a new variable based on alternation strategy
-        //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
-        //Node var;
-        //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
-        //  if( index==0 ){
-        //    var = it->first;
-        //    break;
-        //  }
-        //  index--;
-        //}
-        //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
-      }
-    }
-  }
-  return STATUS_UNKNOWN;
-}
-
-
-void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
+void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){
   if( n.getKind()==MULT ){
     if( TermDb::hasInstConstAttr(n[1]) ){
-      f = TermDb::getInstConstAttr(n[1]);
-      if( n[1].getKind()==INST_CONSTANT ){
-        d_ceTableaux[x][ n[1] ] = n[0];
+      if( n[1]==i ){
+        d_ceTableaux[i][x][ n[1] ] = n[0];
       }else{
-        d_tableaux_ce_term[x][ n[1] ] = n[0];
+        d_tableaux_ce_term[i][x][ n[1] ] = n[0];
       }
     }else{
-      d_tableaux[x][ n[1] ] = n[0];
+      d_tableaux[i][x][ n[1] ] = n[0];
       t << n;
     }
   }else{
     if( TermDb::hasInstConstAttr(n) ){
-      f = TermDb::getInstConstAttr(n);
-      if( n.getKind()==INST_CONSTANT ){
-        d_ceTableaux[x][ n ] = Node::null();
+      if( n==i ){
+        d_ceTableaux[i][x][ n ] = Node::null();
       }else{
-        d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+        d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
       }
     }else{
-      d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+      d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
       t << n;
     }
   }
 }
 
+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
+  if( e<2 ){
+    return STATUS_UNFINISHED;
+  }else if( e==2 ){
+    //Notice() << f << std::endl;
+    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
+    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
+    for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+      Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+      Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
+      for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+        ArithVar x = d_instRows[ic][j];
+        if( !d_ceTableaux[ic][x].empty() ){
+          Debug("quant-arith-simplex") << "Check row " << ic << " " << x << std::endl;
+          //instantiation row will be A*e + B*t = beta,
+          // where e is a vector of terms , and t is vector of ground terms.
+          // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+          // We will construct the term ( beta - B*t)/coeff to use for e_i.
+          InstMatch m;
+          //By default, choose the first instantiation constant to be e_i.
+          Node var = d_ceTableaux[ic][x].begin()->first;
+          if( var.getType().isInteger() ){
+            std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
+            //try to find coefficent that is +/- 1
+            while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
+              ++it;
+              if( it==d_ceTableaux[ic][x].end() ){
+                var = Node::null();
+              }else{
+                var = it->first;
+              }
+            }
+            //otherwise, try one that divides all ground term coefficients? DO_THIS
+          }
+          if( !var.isNull() ){
+            Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+            doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var );
+          }else{
+            Debug("quant-arith-simplex") << "Could not find var." << std::endl;
+          }
+          ////choose a new variable based on alternation strategy
+          //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
+          //Node var;
+          //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
+          //  if( index==0 ){
+          //    var = it->first;
+          //    break;
+          //  }
+          //  index--;
+          //}
+          //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
+        }
+      }
+    }
+  }
+  return STATUS_UNKNOWN;
+}
+
+
 void InstStrategySimplex::debugPrint( const char* c ){
   ArithVariables& avnm = d_th->d_internal->d_partialModel;
   ArithVariables::var_iterator vi, vend;
@@ -218,14 +238,17 @@ void InstStrategySimplex::debugPrint( const char* c ){
       Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
     }
     Debug(c) << std::endl;
-    Debug(c) << "   Instantiation rows: ";
-    for( int i=0; i<(int)d_instRows[f].size(); i++ ){
-      if( i>0 ){
-        Debug(c) << ", ";
+    for( int j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
+      Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
+      Debug(c) << "   Instantiation rows for " << ic << " : ";
+      for( int i=0; i<(int)d_instRows[ic].size(); i++ ){
+        if( i>0 ){
+          Debug(c) << ", ";
+        }
+        Debug(c) << d_instRows[ic][i];
       }
-      Debug(c) << d_instRows[f][i];
+      Debug(c) << std::endl;
     }
-    Debug(c) << std::endl;
   }
 }
 
@@ -234,15 +257,15 @@ void InstStrategySimplex::debugPrint( const char* c ){
 // t[e] is a vector of terms containing instantiation constants from f,
 // and term is a ground term (c1*t1 + ... + cn*tn).
 // We construct the term ( beta - term )/coeff to use as an instantiation for var.
-bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
+bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){
   //first try +delta
-  if( doInstantiation2( f, term, x, m, var ) ){
+  if( doInstantiation2( f, ic, term, x, m, var ) ){
     ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);
     return true;
   }else{
 #ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
     //otherwise try -delta
-    if( doInstantiation2( f, term, x, m, var, true ) ){
+    if( doInstantiation2( f, ic, term, x, m, var, true ) ){
       ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);
       return true;
     }else{
@@ -254,16 +277,16 @@ bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMa
   }
 }
 
-bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
+bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
   // make term ( beta - term )/coeff
   Node beta = getTableauxValue( x, minus_delta );
   Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
-  if( !d_ceTableaux[x][var].isNull() ){
+  if( !d_ceTableaux[ic][x][var].isNull() ){
     if( var.getType().isInteger() ){
-      Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
-      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );
+      Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
+      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal );
     }else{
-      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );
+      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() );
       instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
     }
   }