diff options
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
| -rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 903a729f5..5afee3d57 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -19,7 +19,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" using namespace CVC4; @@ -241,7 +241,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol, //if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn } Node conj = n; if( !pol ){ - conj = TermDb::simpleNegate( conj ); + conj = TermUtil::simpleNegate( conj ); } Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl; Assert( conj.getKind()==AND ); @@ -455,7 +455,7 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) { for( unsigned i=0; i<f[0].getNumChildren(); i++) { if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){ TypeNode tn = f[0][i].getType(); - if( tn.isSort() || getTermDatabase()->mayComplete( tn ) ){ + if( tn.isSort() || getTermUtil()->mayComplete( tn ) ){ success = true; setBoundedVar( f, f[0][i], BOUND_FINITE ); break; @@ -808,7 +808,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node tu = u; getBounds( q, v, rsi, tl, tu ); Assert( !tl.isNull() && !tu.isNull() ); - if( ra==d_quantEngine->getTermDatabase()->d_true ){ + if( ra==d_quantEngine->getTermUtil()->d_true ){ long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for( unsigned k=0; k<rr; k++ ){ |