diff options
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index cd363eb70..db8bc90d1 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -16,14 +16,13 @@ #include "theory/quantifiers/conjecture_generator.h" #include "expr/term_canonize.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/ematching/trigger_term_info.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" #include "util/random.h" using namespace CVC4; @@ -316,7 +315,9 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { } bool ConjectureGenerator::isHandledTerm( TNode n ){ - return d_quantEngine->getTermDatabase()->isTermActive( n ) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM ); + return d_quantEngine->getTermDatabase()->isTermActive(n) + && inst::TriggerTermInfo::isAtomicTrigger(n) + && (n.getKind() != APPLY_UF || n.getOperator().getKind() != SKOLEM); } Node ConjectureGenerator::getGroundEqc( TNode r ) { |