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 | |
parent | 3b6ef254e92ab0918db05a0c6084baa8892a2183 (diff) |
Enable CEGQI for non-linear (#1674)
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.h | 7 |
2 files changed, 0 insertions, 17 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; diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index e91a87e58..cd10e4f8a 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -313,13 +313,6 @@ class Trigger { static bool isRelationalTrigger( Node n ); /** Is k a relational trigger kind? */ static bool isRelationalTriggerKind( Kind k ); - /** Is k a kind for which counterexample-guided instantiation is possible? - * - * This typically corresponds to kinds that correspond to operators that - * have total interpretations and are a part of the signature of - * satisfaction complete theories (see Reynolds et al., CAV 2015). - */ - static bool isCbqiKind( Kind k ); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger( Node n ); /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */ |