FCSimplex branch merge

1 files changed, 16 insertions, 14 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 20eb7373b..dbdf95613 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/quantifiers/inst_strategy_cbqi.h"
 #include "theory/arith/theory_arith.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith_private.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
@@ -46,11 +48,11 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
   d_tableaux.clear();
   d_ceTableaux.clear();
   //search for instantiation rows in simplex tableaux
-  ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;
-  ArithVarNodeMap::var_iterator vi, vend;
+  ArithVariables& avnm = d_th->d_internal->d_partialModel;
+  ArithVariables::var_iterator vi, vend;
   for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
     ArithVar x = *vi;
-    if( d_th->d_partialModel.hasEitherBound( x ) ){
+    if( d_th->d_internal->d_partialModel.hasEitherBound( x ) ){
       Node n = avnm.asNode(x);
       Node f;
       NodeBuilder<> t(kind::PLUS);
@@ -168,23 +170,23 @@ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder
 }
 
 void InstStrategySimplex::debugPrint( const char* c ){
-  const ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;
-  ArithVarNodeMap::var_iterator vi, vend;
+  ArithVariables& avnm = d_th->d_internal->d_partialModel;
+  ArithVariables::var_iterator vi, vend;
   for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
     ArithVar x = *vi;
     Node n = avnm.asNode(x);
     //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
       Debug(c) << x << " : " << n << ", bounds = ";
-      if( d_th->d_partialModel.hasLowerBound( x ) ){
-        Debug(c) << d_th->d_partialModel.getLowerBound( x );
+      if( d_th->d_internal->d_partialModel.hasLowerBound( x ) ){
+        Debug(c) << d_th->d_internal->d_partialModel.getLowerBound( x );
       }else{
         Debug(c) << "-infty";
       }
       Debug(c) << " <= ";
-      Debug(c) << d_th->d_partialModel.getAssignment( x );
+      Debug(c) << d_th->d_internal->d_partialModel.getAssignment( x );
       Debug(c) << " <= ";
-      if( d_th->d_partialModel.hasUpperBound( x ) ){
-        Debug(c) << d_th->d_partialModel.getUpperBound( x );
+      if( d_th->d_internal->d_partialModel.hasUpperBound( x ) ){
+        Debug(c) << d_th->d_internal->d_partialModel.getUpperBound( x );
       }else{
         Debug(c) << "+infty";
       }
@@ -273,8 +275,8 @@ bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstM
 }
 
 Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
-  if( d_th->d_arithvarNodeMap.hasArithVar(n) ){
-    ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );
+  if( d_th->d_internal->d_partialModel.hasArithVar(n) ){
+    ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n );
     return getTableauxValue( v, minus_delta );
   }else{
     return NodeManager::currentNM()->mkConst( Rational(0) );
@@ -282,8 +284,8 @@ Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
 }
 
 Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
-  const Rational& delta = d_th->d_partialModel.getDelta();
-  DeltaRational drv = d_th->d_partialModel.getAssignment( v );
+  const Rational& delta = d_th->d_internal->d_partialModel.getDelta();
+  DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v );
   Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
   return mkRationalNode(qmodel);
 }