diff options
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 24f17d0c1..731b53dc4 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -20,6 +20,7 @@ #include "theory/theory_engine.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
using namespace CVC4;
using namespace CVC4::kind;
@@ -1692,8 +1693,9 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { }
bool MatchGen::isHandledUfTerm( TNode n ) {
- return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
- n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
+ //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
+ // n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
+ return inst::Trigger::isAtomicTriggerKind( n.getKind() );
}
Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
|