diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 79279eb41..524c440ba 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -16,10 +16,11 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" +#include "options/theory_options.h" #include "options/uf_options.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" @@ -672,7 +673,8 @@ Node TermDb::evaluateTerm2(TNode n, for (unsigned j = 0; j < 2; j++) { std::pair<bool, Node> et = te->entailmentCheck( - THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate()); + options::TheoryOfMode::THEORY_OF_TYPE_BASED, + j == 0 ? ret : ret.negate()); if (et.first) { ret = j == 0 ? d_true : d_false; @@ -905,11 +907,16 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { return d_has_map.find( n )!=d_has_map.end(); }else{ //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE - if( options::termDbMode()==TERM_DB_ALL ){ + if (options::termDbMode() == options::TermDbMode::ALL) + { return true; - }else if( options::termDbMode()==TERM_DB_RELEVANT ){ + } + else if (options::termDbMode() == options::TermDbMode::RELEVANT) + { return d_has_map.find( n )!=d_has_map.end(); - }else{ + } + else + { Assert(false); return false; } @@ -1061,7 +1068,9 @@ bool TermDb::reset( Theory::Effort effort ){ } //compute has map - if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){ + if (options::termDbMode() == options::TermDbMode::RELEVANT + || options::lteRestrictInstClosure()) + { d_has_map.clear(); d_term_elig_eqc.clear(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); |