diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 30 |
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); } |