diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 32 |
1 files changed, 3 insertions, 29 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 63eb301b6..9d13dccb7 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -737,8 +737,8 @@ void TheoryArithPrivate::addSharedTerm(TNode n){ } } -Node TheoryArithPrivate::getModelValue(TNode var) { - /*try{ +Node TheoryArithPrivate::getModelValue(TNode term) { + try{ DeltaRational drv = getDeltaValue(term); const Rational& delta = d_partialModel.getDelta(); Rational qmodel = drv.substituteDelta( delta ); @@ -747,33 +747,7 @@ Node TheoryArithPrivate::getModelValue(TNode var) { return Node::null(); } catch (ModelException& me) { return Node::null(); - }*/ - //if( d_partialModel.hasNode( var ) ){ - if( var.getKind()==kind::STRING_LENGTH ){ - Trace("strings-temp") << "Get model value of " << var << std::endl; - /* - ArithVar v; - bool foundV = false; - ArithVariables& avnm = d_partialModel; - ArithVariables::var_iterator vi, vend; - for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ - if( avnm.asNode(*vi)==var ){ - v = *vi; - foundV = true; - break; - } - } - if( foundV ){ - */ - ArithVar v = d_partialModel.asArithVar( var ); - DeltaRational drv = d_partialModel.getAssignment( v ); - const Rational& delta = d_partialModel.getDelta(); - Rational qmodel = drv.substituteDelta( delta ); - Trace("strings-temp") << "Value is " << drv << ", after subs : " << qmodel << std::endl; - return mkRationalNode( qmodel ); - } - //} - return var; + } } namespace attr { |