6 files changed, 35 insertions, 29 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index d7d46bb4b..358efede7 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -127,6 +127,23 @@ bool CegInstantiator::isEligible( Node n ) {
   return d_inelig.find( n )==d_inelig.end();
 }
 
+bool CegInstantiator::isCbqiKind(Kind k)
+{
+  if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ
+      || k == EQUAL
+      || k == MULT
+      || k == NONLINEAR_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 CegInstantiator::hasVariable( Node n, Node pv ) {
   computeProgVars( n );
   return d_prog_var[n].find( pv )!=d_prog_var[n].end();
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index c12890b83..6cbc7418c 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -297,6 +297,14 @@ class CegInstantiator {
   bool useVtsInfinity() { return d_use_vts_inf; }
   /** are we processing a nested quantified formula? */
   bool hasNestedQuantification() { return d_is_nested_quant; }
+  /** 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);
+
  private:
   /** quantified formula associated with this instantiator */
   QuantifiersEngine* d_qe;
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index bb210edcc..b526fb1ee 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -155,12 +155,11 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
         }
         Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
       }
-      if( options::cbqiAll() ){
-        // when not pure LIA/LRA, we must check whether the lhs contains pv
-        if( TermUtil::containsTerm( val, pv ) ){
-          Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
-          return 0;
-        }
+      // when not pure LIA/LRA, we must check whether the lhs contains pv
+      if (TermUtil::containsTerm(val, pv))
+      {
+        Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
+        return 0;
       }
       if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
         //redo, split integer/non-integer parts
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 8de3dbfcb..c07ddcd8f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -484,13 +483,13 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
     if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){
-      if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
+      if (!CegInstantiator::isCbqiKind(n.getKind()))
+      {
         Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
         return true;
-      }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
-        Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
-        return true;
-      }else if( n.getKind()==FORALL ){
+      }
+      else if (n.getKind() == FORALL || n.getKind() == CHOICE)
+      {
         return hasNonCbqiOperator( n[1], visited );
       }else{
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
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 )? */