diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-19 23:16:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-19 23:16:45 -0500 |
| commit | db83224b35a218a0bb449850530f0d2bea484eae (patch) | |
| tree | 648d33a0c6c4df66e6b0c60e9192fcc6995b4916 /src/theory/quantifiers/ematching/trigger.cpp | |
| parent | 3b6ef254e92ab0918db05a0c6084baa8892a2183 (diff) | |
Enable CEGQI for non-linear (#1674)
Diffstat (limited to 'src/theory/quantifiers/ematching/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index b73c3368d..430d261a1 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -393,16 +393,6 @@ bool Trigger::isRelationalTrigger( Node n ) { bool Trigger::isRelationalTriggerKind( Kind k ) { return k==EQUAL || k==GEQ; } - -bool Trigger::isCbqiKind( Kind k ) { - if( quantifiers::TermUtil::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 || t == THEORY_BOOL; - } -} bool Trigger::isSimpleTrigger( Node n ){ Node t = n.getKind()==NOT ? n[0] : n; |