Minor reorganization for ematching (#1701)

6 files changed, 493 insertions, 90 deletions

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
new file mode 100644
index 000000000..ea5e8592d
--- /dev/null
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -0,0 +1,309 @@
+/*********************                                                        */
+/*! \file candidate_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of theory uf candidate generator class
+ **/
+
+#include "theory/quantifiers/ematching/candidate_generator.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::inst;
+
+bool CandidateGenerator::isLegalCandidate( Node n ){
+  return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
+}
+
+void CandidateGeneratorQueue::addCandidate( Node n ) {
+  if( isLegalCandidate( n ) ){
+    d_candidates.push_back( n );
+  }
+}
+
+void CandidateGeneratorQueue::reset( Node eqc ){
+  if( d_candidate_index>0 ){
+    d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index );
+    d_candidate_index = 0;
+  }
+  if( !eqc.isNull() ){
+    d_candidates.push_back( eqc );
+  }
+}
+Node CandidateGeneratorQueue::getNextCandidate(){
+  if( d_candidate_index<(int)d_candidates.size() ){
+    Node n = d_candidates[d_candidate_index];
+    d_candidate_index++;
+    return n;
+  }else{
+    d_candidate_index = 0;
+    d_candidates.clear();
+    return Node::null();
+  }
+}
+
+CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
+CandidateGenerator( qe ), d_term_iter( -1 ){
+  d_op = qe->getTermDatabase()->getMatchOperator( pat );
+  Assert( !d_op.isNull() );
+  d_op_arity = pat.getNumChildren();
+}
+
+void CandidateGeneratorQE::resetInstantiationRound(){
+  d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op );
+}
+
+void CandidateGeneratorQE::reset( Node eqc ){
+  d_term_iter = 0;
+  if( eqc.isNull() ){
+    d_mode = cand_term_db;
+  }else{
+    if( isExcludedEqc( eqc ) ){
+      d_mode = cand_term_none;
+    }else{
+      eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+      if( ee->hasTerm( eqc ) ){
+        quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op );
+        if( tat ){
+#if 1
+          //create an equivalence class iterator in eq class eqc
+          Node rep = ee->getRepresentative( eqc );
+          d_eqc_iter = eq::EqClassIterator( rep, ee );
+          d_mode = cand_term_eqc;
+#else
+          d_tindex.push_back( tat );
+          d_tindex_iter.push_back( tat->d_data.begin() );
+          d_mode = cand_term_tindex;
+#endif     
+        }else{
+          d_mode = cand_term_none;
+        }   
+      }else{
+        //the only match is this term itself
+        d_n = eqc;
+        d_mode = cand_term_ident;
+      }
+    }
+  }
+}
+bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
+  if( n.hasOperator() ){
+    if( isLegalCandidate( n ) ){
+      return d_qe->getTermDatabase()->getMatchOperator( n )==d_op;
+    }
+  }
+  return false;
+}
+
+Node CandidateGeneratorQE::getNextCandidate(){
+  if( d_mode==cand_term_db ){
+    Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
+    //get next candidate term in the uf term database
+    while( d_term_iter<d_term_iter_limit ){
+      Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
+      d_term_iter++;
+      if( isLegalCandidate( n ) ){
+        if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+          if( d_exclude_eqc.empty() ){
+            return n;
+          }else{
+            Node r = d_qe->getEqualityQuery()->getRepresentative( n );
+            if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
+              Debug("cand-gen-qe") << "...returning " << n << std::endl;
+              return n;
+            }
+          }
+        }
+      }
+    }
+  }else if( d_mode==cand_term_eqc ){
+    Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
+    while( !d_eqc_iter.isFinished() ){
+      Node n = *d_eqc_iter;
+      ++d_eqc_iter;
+      if( isLegalOpCandidate( n ) ){
+        Debug("cand-gen-qe") << "...returning " << n << std::endl;
+        return n;
+      }
+    }
+  }else if( d_mode==cand_term_tindex ){
+    Debug("cand-gen-qe") << "...get next candidate in tindex " << d_op << " " << d_op_arity << std::endl;
+    //increment the term index iterator
+    if( !d_tindex.empty() ){
+      //populate the vector
+      while( d_tindex_iter.size()<=d_op_arity ){
+        Assert( !d_tindex_iter.empty() );
+        Assert( !d_tindex_iter.back()->second.d_data.empty() );
+        d_tindex.push_back( &(d_tindex_iter.back()->second) );
+        d_tindex_iter.push_back( d_tindex_iter.back()->second.d_data.begin() );
+      }
+      //get the current node
+      Assert( d_tindex_iter.back()->second.hasNodeData() );
+      Node n = d_tindex_iter.back()->second.getNodeData();
+      Debug("cand-gen-qe") << "...returning " << n << std::endl;
+      Assert( !n.isNull() );
+      Assert( isLegalOpCandidate( n ) );
+      //increment
+      bool success = false;
+      do{
+        ++d_tindex_iter.back();
+        if( d_tindex_iter.back()==d_tindex.back()->d_data.end() ){
+          d_tindex.pop_back();
+          d_tindex_iter.pop_back();
+        }else{
+          success = true;
+        }
+      }while( !success && !d_tindex.empty() );
+      return n;   
+    } 
+  }else if( d_mode==cand_term_ident ){
+    Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
+    if( !d_n.isNull() ){
+      Node n = d_n;
+      d_n = Node::null();
+      if( isLegalOpCandidate( n ) ){
+        return n;
+      }
+    }
+  }
+  return Node::null();
+}
+
+CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
+  CandidateGenerator( qe ), d_match_pattern( mpat ){
+  Assert( mpat.getKind()==EQUAL );
+  for( unsigned i=0; i<2; i++ ){
+    if( !quantifiers::TermUtil::hasInstConstAttr(mpat[i]) ){
+      d_match_gterm = mpat[i];
+    }
+  }
+}
+void CandidateGeneratorQELitEq::resetInstantiationRound(){
+
+}
+void CandidateGeneratorQELitEq::reset( Node eqc ){
+  if( d_match_gterm.isNull() ){
+    d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  }else{
+    d_do_mgt = true;
+  }
+}
+Node CandidateGeneratorQELitEq::getNextCandidate(){
+  if( d_match_gterm.isNull() ){
+    while( !d_eq.isFinished() ){
+      Node n = (*d_eq);
+      ++d_eq;
+      if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
+        //an equivalence class with the same type as the pattern, return reflexive equality
+        return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+      }
+    }
+  }else{
+    if( d_do_mgt ){
+      d_do_mgt = false;
+      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm );
+    }
+  }
+  return Node::null();
+}
+
+
+CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
+CandidateGenerator( qe ), d_match_pattern( mpat ){
+
+  Assert( d_match_pattern.getKind()==EQUAL );
+  d_match_pattern_type = d_match_pattern[0].getType();
+}
+
+void CandidateGeneratorQELitDeq::resetInstantiationRound(){
+
+}
+
+void CandidateGeneratorQELitDeq::reset( Node eqc ){
+  Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
+  d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
+}
+
+Node CandidateGeneratorQELitDeq::getNextCandidate(){
+  //get next candidate term in equivalence class
+  while( !d_eqc_false.isFinished() ){
+    Node n = (*d_eqc_false);
+    ++d_eqc_false;
+    if( n.getKind()==d_match_pattern.getKind() ){
+      if( n[0].getType().isComparableTo( d_match_pattern_type ) ){
+        //found an iff or equality, try to match it
+        //DO_THIS: cache to avoid redundancies?
+        //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
+        return n;
+      }
+    }
+  }
+  return Node::null();
+}
+
+
+CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
+  CandidateGenerator( qe ), d_match_pattern( mpat ){
+  d_match_pattern_type = mpat.getType();
+  Assert( mpat.getKind()==INST_CONSTANT );
+  d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
+  d_index = mpat.getAttribute(InstVarNumAttribute());
+  d_firstTime = false;
+}
+
+void CandidateGeneratorQEAll::resetInstantiationRound() {
+
+}
+
+void CandidateGeneratorQEAll::reset( Node eqc ) {
+  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  d_firstTime = true;
+}
+
+Node CandidateGeneratorQEAll::getNextCandidate() {
+  while( !d_eq.isFinished() ){
+    TNode n = (*d_eq);
+    ++d_eq;
+    if( n.getType().isComparableTo( d_match_pattern_type ) ){
+      TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
+      if( !nh.isNull() ){
+        if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
+          nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
+          //don't consider this if already the instantiation is ineligible
+          if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){
+            nh = Node::null();
+          }
+        }
+        if( !nh.isNull() ){
+          d_firstTime = false;
+          //an equivalence class with the same type as the pattern, return it
+          return nh;
+        }
+      }
+    }
+  }
+  if( d_firstTime ){
+    //must return something
+    d_firstTime = false;
+    return d_qe->getInstantiate()->getTermForType(d_match_pattern_type);
+  }
+  return Node::null();
+}
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
new file mode 100644
index 000000000..4662d7c4c
--- /dev/null
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -0,0 +1,179 @@
+/*********************                                                        */
+/*! \file candidate_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Theory uf candidate generator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace quantifiers {
+  class TermArgTrie;
+}
+
+class QuantifiersEngine;
+
+namespace inst {
+
+/** base class for generating candidates for matching */
+class CandidateGenerator {
+protected:
+  QuantifiersEngine* d_qe;
+public:
+  CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){}
+  virtual ~CandidateGenerator(){}
+
+  /** Get candidates functions.  These set up a context to get all match candidates.
+      cg->reset( eqc );
+      do{
+        Node cand = cg->getNextCandidate();
+        //.......
+      }while( !cand.isNull() );
+
+      eqc is the equivalence class you are searching in
+  */
+  virtual void reset( Node eqc ) = 0;
+  virtual Node getNextCandidate() = 0;
+  /** add candidate to list of nodes returned by this generator */
+  virtual void addCandidate( Node n ) {}
+  /** call this at the beginning of each instantiation round */
+  virtual void resetInstantiationRound() = 0;
+public:
+  /** legal candidate */
+  bool isLegalCandidate( Node n );
+};/* class CandidateGenerator */
+
+/** candidate generator queue (for manual candidate generation) */
+class CandidateGeneratorQueue : public CandidateGenerator {
+ private:
+  std::vector< Node > d_candidates;
+  int d_candidate_index;
+
+ public:
+  CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){}
+
+  void addCandidate(Node n) override;
+
+  void resetInstantiationRound() override {}
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
+};/* class CandidateGeneratorQueue */
+
+//the default generator
+class CandidateGeneratorQE : public CandidateGenerator
+{
+  friend class CandidateGeneratorQEDisequal;
+
+ private:
+  //operator you are looking for
+  Node d_op;
+  //the equality class iterator
+  unsigned d_op_arity;
+  std::vector< quantifiers::TermArgTrie* > d_tindex;
+  std::vector< std::map< TNode, quantifiers::TermArgTrie >::iterator > d_tindex_iter;
+  eq::EqClassIterator d_eqc_iter;
+  //std::vector< Node > d_eqc;
+  int d_term_iter;
+  int d_term_iter_limit;
+  bool d_using_term_db;
+  enum {
+    cand_term_db,
+    cand_term_ident,
+    cand_term_eqc,
+    cand_term_tindex,
+    cand_term_none,
+  };
+  short d_mode;
+  bool isLegalOpCandidate( Node n );
+  Node d_n;
+  std::map< Node, bool > d_exclude_eqc;
+
+ public:
+  CandidateGeneratorQE( QuantifiersEngine* qe, Node pat );
+
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
+  void excludeEqc( Node r ) { d_exclude_eqc[r] = true; }
+  bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); }
+};
+
+class CandidateGeneratorQELitEq : public CandidateGenerator
+{
+ private:
+  //the equality classes iterator
+  eq::EqClassesIterator d_eq;
+  //equality you are trying to match equalities for
+  Node d_match_pattern;
+  Node d_match_gterm;
+  bool d_do_mgt;
+
+ public:
+  CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
+
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
+};
+
+class CandidateGeneratorQELitDeq : public CandidateGenerator
+{
+ private:
+  //the equality class iterator for false
+  eq::EqClassIterator d_eqc_false;
+  //equality you are trying to match disequalities for
+  Node d_match_pattern;
+  //type of disequality
+  TypeNode d_match_pattern_type;
+
+ public:
+  CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
+
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
+};
+
+class CandidateGeneratorQEAll : public CandidateGenerator
+{
+ private:
+  //the equality classes iterator
+  eq::EqClassesIterator d_eq;
+  //equality you are trying to match equalities for
+  Node d_match_pattern;
+  TypeNode d_match_pattern_type;
+  // quantifier/index for the variable we are matching
+  Node d_f;
+  unsigned d_index;
+  //first time
+  bool d_firstTime;
+
+ public:
+  CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
+
+  void resetInstantiationRound() override;
+  void reset(Node eqc) override;
+  Node getNextCandidate() override;
+};
+
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index c36597e3e..ec0a4039a 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -17,11 +17,11 @@
 #include "expr/datatype.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ematching/candidate_generator.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace std;
@@ -541,14 +541,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
   }
   Trace("var-trigger-debug") << "Is " << n << " a variable trigger?"
                              << std::endl;
-  if (Trigger::isBooleanTermTrigger(n))
-  {
-    VarMatchGeneratorBooleanTerm* vmg =
-        new VarMatchGeneratorBooleanTerm(n[0], n[1]);
-    Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0]
-                         << std::endl;
-    return vmg;
-  }
   Node x;
   if (options::purifyTriggers())
   {
@@ -565,38 +557,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
   return new InstMatchGenerator(n);
 }
 
-VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) :
-  InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) {
-  d_children_types.push_back(var.getAttribute(InstVarNumAttribute()));
-}
-
-int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
-                                               InstMatch& m,
-                                               QuantifiersEngine* qe,
-                                               Trigger* tparent)
-{
-  int ret_val = -1;
-  if( !d_eq_class.isNull() ){
-    Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
-    d_eq_class = Node::null();
-    d_rm_prev = m.get(d_children_types[0]).isNull();
-    if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
-    {
-      return -1;
-    }else{
-      ret_val = continueNextMatch(q, m, qe, tparent);
-      if( ret_val>0 ){
-        return ret_val;
-      }
-    }
-  }
-  if( d_rm_prev ){
-    m.d_vals[d_children_types[0]] = Node::null();
-    d_rm_prev = false;
-  }
-  return ret_val;
-}
-
 VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
   InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
   d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 6c38db13b..cbd5702a0 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -418,32 +418,6 @@ class InstMatchGenerator : public IMGenerator {
   static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
 };/* class InstMatchGenerator */
 
-/** match generator for Boolean term ITEs
-* This handles the special case of triggers that look like ite( x, BV1, BV0 ).
-*/
-class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
-public:
-  VarMatchGeneratorBooleanTerm( Node var, Node comp );
-
-  /** Reset */
-  bool reset(Node eqc, QuantifiersEngine* qe) override
-  {
-    d_eq_class = eqc; 
-    return true;
-  }
-  /** Get the next match. */
-  int getNextMatch(Node q,
-                   InstMatch& m,
-                   QuantifiersEngine* qe,
-                   Trigger* tparent) override;
-
- private:
-  /** stores the true branch of the Boolean ITE */
-  Node d_comp;
-  /** stores whether we have written a value for var in the current match. */
-  bool d_rm_prev;
-};
-
 /** match generator for purified terms
 * This handles the special case of invertible terms like x+1 (see
 * Trigger::getTermInversionVariable).
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 430d261a1..4039c632f 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -15,7 +15,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
@@ -262,9 +262,8 @@ bool Trigger::isUsable( Node n, Node q ){
       return true;
     }else{
       std::map< Node, Node > coeffs;
-      if( isBooleanTermTrigger( n ) ){
-        return true;
-      }else if( options::purifyTriggers() ){
+      if (options::purifyTriggers())
+      {
         Node x = getInversionVariable( n );
         if( !x.isNull() ){
           return true;
@@ -522,22 +521,6 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
   }
 }
 
-bool Trigger::isBooleanTermTrigger( Node n ) {
-  if( n.getKind()==ITE ){
-    //check for boolean term converted to ITE
-    if( n[0].getKind()==INST_CONSTANT &&
-        n[1].getKind()==CONST_BITVECTOR &&
-        n[2].getKind()==CONST_BITVECTOR ){
-      if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
-          n[1].getConst<BitVector>().toInteger()==1 &&
-          n[2].getConst<BitVector>().toInteger()==0 ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
 bool Trigger::isPureTheoryTrigger( Node n ) {
   if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){  //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
     return false;
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index cd10e4f8a..28d227bf7 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -315,8 +315,6 @@ class Trigger {
   static bool isRelationalTriggerKind( 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 )? */
-  static bool isBooleanTermTrigger( Node n );
   /** is n a pure theory trigger, e.g. head( x )? */
   static bool isPureTheoryTrigger( Node n );
   /** get trigger weight