From db83224b35a218a0bb449850530f0d2bea484eae Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 19 Mar 2018 23:16:45 -0500
Subject: Enable CEGQI for non-linear (#1674)

---
 src/theory/quantifiers/ematching/trigger.cpp | 10 ----------
 src/theory/quantifiers/ematching/trigger.h   |  7 -------
 2 files changed, 17 deletions(-)

(limited to 'src/theory/quantifiers/ematching')

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 )? */
-- 
cgit v1.2.3