diff options
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 802acc089..ee091919d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -375,8 +375,13 @@ bool Trigger::isRelationalTriggerKind( Kind k ) { } bool Trigger::isCbqiKind( Kind k ) { - return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT || - k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER; + if( quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){ + return true; + }else{ + //CBQI typically works for satisfaction-complete theories + TheoryId t = kindToTheoryId( k ); + return t==THEORY_BV || t==THEORY_DATATYPES; + } } bool Trigger::isSimpleTrigger( Node n ){ |