Minor improvements to inst match generator (#1415)

8 files changed, 76 insertions, 102 deletions

diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ho_trigger.cpp
index 6354047cf..6456fb2f6 100644
--- a/src/theory/quantifiers/ho_trigger.cpp
+++ b/src/theory/quantifiers/ho_trigger.cpp
@@ -186,10 +186,10 @@ void HigherOrderTrigger::collectHoVarApplyTerms(
   }
 }
 
-int HigherOrderTrigger::addInstantiations(InstMatch& baseMatch)
+int HigherOrderTrigger::addInstantiations()
 {
   // call the base class implementation
-  int addedFoLemmas = Trigger::addInstantiations(baseMatch);
+  int addedFoLemmas = Trigger::addInstantiations();
   // also adds predicate lemms to force app completion
   int addedHoLemmas = addHoTypeMatchPredicateLemmas();
   return addedHoLemmas + addedFoLemmas;
@@ -202,11 +202,11 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     // get substitution corresponding to m
     std::vector<TNode> vars;
     std::vector<TNode> subs;
-    for (unsigned i = 0, size = d_f[0].getNumChildren(); i < size; i++)
+    quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
+    for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
     {
       subs.push_back(m.d_vals[i]);
-      vars.push_back(
-          d_quantEngine->getTermUtil()->getInstantiationConstant(d_f, i));
+      vars.push_back(tutil->getInstantiationConstant(d_quant, i));
     }
 
     Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
@@ -353,7 +353,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
   else
   {
     // do not run higher-order matching
-    return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
   }
 }
 
@@ -364,7 +364,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
   if (var_index == d_ho_var_list.size())
   {
     // we now have an instantiation to try
-    return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
   }
   else
   {
diff --git a/src/theory/quantifiers/ho_trigger.h b/src/theory/quantifiers/ho_trigger.h
index e5112abce..4db3a660f 100644
--- a/src/theory/quantifiers/ho_trigger.h
+++ b/src/theory/quantifiers/ho_trigger.h
@@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger
    * Extends Trigger::addInstantiations to also send
    * lemmas based on addHoTypeMatchPredicateLemmas.
    */
-  virtual int addInstantiations(InstMatch& baseMatch) override;
+  virtual int addInstantiations() override;
 
  protected:
   /**
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 5cdb2a64b..884ed29f5 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -48,7 +48,6 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
   d_match_pattern = pat;
   d_match_pattern_type = pat.getType();
   d_next = NULL;
-  d_matchPolicy = MATCH_GEN_DEFAULT;
   d_independent_gen = false;
 }
 
@@ -57,7 +56,6 @@ InstMatchGenerator::InstMatchGenerator() {
   d_needsReset = true;
   d_active_add = true;
   d_next = NULL;
-  d_matchPolicy = MATCH_GEN_DEFAULT;
   d_independent_gen = false;
 }
 
@@ -135,7 +133,8 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
     //now, collect children of d_match_pattern
     if (d_match_pattern.getKind() == INST_CONSTANT)
     {
-      d_var_num[0] = d_match_pattern.getAttribute(InstVarNumAttribute());
+      d_children_types.push_back(
+          d_match_pattern.getAttribute(InstVarNumAttribute()));
     }
     else
     {
@@ -151,13 +150,12 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
           {
             d_children.push_back(cimg);
             d_children_index.push_back(i);
-            d_children_types.push_back(1);
+            d_children_types.push_back(-2);
           }else{
             if (d_match_pattern[i].getKind() == INST_CONSTANT && qa == q)
             {
-              d_var_num[i] =
-                  d_match_pattern[i].getAttribute(InstVarNumAttribute());
-              d_children_types.push_back(0);
+              d_children_types.push_back(
+                  d_match_pattern[i].getAttribute(InstVarNumAttribute()));
             }
             else
             {
@@ -204,9 +202,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
         d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
       }
     }else{
-      d_cg = new CandidateGeneratorQueue( qe );
       Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
-      d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
     }
   }
   gens.insert( gens.end(), d_children.begin(), d_children.end() );
@@ -219,7 +215,8 @@ int InstMatchGenerator::getMatch(
   Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
                     << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
   Assert( !d_match_pattern.isNull() );
-  if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
+  if (d_cg == nullptr)
+  {
     Trace("matching-fail") << "Internal error for match generator." << std::endl;
     return -2;
   }else{
@@ -235,21 +232,28 @@ int InstMatchGenerator::getMatch(
     Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
     //first, check if ground arguments are not equal, or a match is in conflict
     Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
-    for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
-      if( d_children_types[i]==0 ){
-        Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl;
-        bool addToPrev = m.get( d_var_num[i] ).isNull();
-        if (!m.set(q, d_var_num[i], t[i]))
+    for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
+    {
+      int ct = d_children_types[i];
+      if (ct >= 0)
+      {
+        Trace("matching-debug2") << "Setting " << ct << " to " << t[i] << "..."
+                                 << std::endl;
+        bool addToPrev = m.get(ct).isNull();
+        if (!m.set(q, ct, t[i]))
         {
           //match is in conflict
-          Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << t[i] << std::endl;
+          Trace("matching-fail") << "Match fail: " << m.get(ct) << " and "
+                                 << t[i] << std::endl;
           success = false;
           break;
         }else if( addToPrev ){
           Trace("matching-debug2") << "Success." << std::endl;
-          prev.push_back( d_var_num[i] );
+          prev.push_back(ct);
         }
-      }else if( d_children_types[i]==-1 ){
+      }
+      else if (ct == -1)
+      {
         if( !q->areEqual( d_match_pattern[i], t[i] ) ){
           Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
           //ground arguments are not equal
@@ -261,13 +265,13 @@ int InstMatchGenerator::getMatch(
     Trace("matching-debug2") << "Done setting immediate matches, success = " << success << "." << std::endl;
     //for variable matching
     if( d_match_pattern.getKind()==INST_CONSTANT ){
-      bool addToPrev = m.get( d_var_num[0] ).isNull();
-      if (!m.set(q, d_var_num[0], t))
+      bool addToPrev = m.get(d_children_types[0]).isNull();
+      if (!m.set(q, d_children_types[0], t))
       {
         success = false;
       }else{
         if( addToPrev ){
-          prev.push_back( d_var_num[0] );
+          prev.push_back(d_children_types[0]);
         }
       }
     //for relational matching
@@ -312,7 +316,8 @@ int InstMatchGenerator::getMatch(
       Trace("matching-debug2") << "Reset children..." << std::endl;
       //now, fit children into match
       //we will be requesting candidates for matching terms for each child
-      for( unsigned i=0; i<d_children.size(); i++ ){
+      for (unsigned i = 0, size = d_children.size(); i < size; i++)
+      {
         if( !d_children[i]->reset( t[ d_children_index[i] ], qe ) ){
           success = false;
           break;
@@ -324,9 +329,9 @@ int InstMatchGenerator::getMatch(
       }
     }
     if( ret_val<0 ){
-      //m = InstMatch( &prev );
-      for( unsigned i=0; i<prev.size(); i++ ){
-        m.d_vals[prev[i]] = Node::null();
+      for (int& pv : prev)
+      {
+        m.d_vals[pv] = Node::null();
       }
     }
     return ret_val;
@@ -439,7 +444,6 @@ int InstMatchGenerator::getNextMatch(Node f,
 }
 
 int InstMatchGenerator::addInstantiations(Node f,
-                                          InstMatch& baseMatch,
                                           QuantifiersEngine* qe,
                                           Trigger* tparent)
 {
@@ -449,7 +453,6 @@ int InstMatchGenerator::addInstantiations(Node f,
   while (getNextMatch(f, m, qe, tparent) > 0)
   {
     if( !d_active_add ){
-      m.add( baseMatch );
       if (sendInstantiation(tparent, m))
       {
         addedLemmas++;
@@ -563,7 +566,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
 
 VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) :
   InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) {
-  d_var_num[0] = var.getAttribute(InstVarNumAttribute());
+  d_children_types.push_back(var.getAttribute(InstVarNumAttribute()));
 }
 
 int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
@@ -575,8 +578,8 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
   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_var_num[0] ).isNull();
-    if (!m.set(qe->getEqualityQuery(), d_var_num[0], s))
+    d_rm_prev = m.get(d_children_types[0]).isNull();
+    if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
     {
       return -1;
     }else{
@@ -587,7 +590,7 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
     }
   }
   if( d_rm_prev ){
-    m.d_vals[d_var_num[0]] = Node::null();
+    m.d_vals[d_children_types[0]] = Node::null();
     d_rm_prev = false;
   }
   return ret_val;
@@ -595,7 +598,7 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
 
 VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
   InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
-  d_var_num[0] = d_var.getAttribute(InstVarNumAttribute());
+  d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
   d_var_type = d_var.getType();
 }
 
@@ -612,8 +615,8 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q,
     Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl;
     d_eq_class = Node::null();
     //if( s.getType().isSubtypeOf( d_var_type ) ){
-    d_rm_prev = m.get( d_var_num[0] ).isNull();
-    if (!m.set(qe->getEqualityQuery(), d_var_num[0], s))
+    d_rm_prev = m.get(d_children_types[0]).isNull();
+    if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
     {
       return -1;
     }else{
@@ -624,7 +627,7 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q,
     }
   }
   if( d_rm_prev ){
-    m.d_vals[d_var_num[0]] = Node::null();
+    m.d_vals[d_children_types[0]] = Node::null();
     d_rm_prev = false;
   }
   return -1;
@@ -838,7 +841,6 @@ bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
 }
 
 int InstMatchGeneratorMulti::addInstantiations(Node q,
-                                               InstMatch& baseMatch,
                                                QuantifiersEngine* qe,
                                                Trigger* tparent)
 {
@@ -1033,7 +1035,6 @@ void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe )
   
 }
 int InstMatchGeneratorSimple::addInstantiations(Node q,
-                                                InstMatch& baseMatch,
                                                 QuantifiersEngine* qe,
                                                 Trigger* tparent)
 {
@@ -1052,7 +1053,6 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
         for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
           if( it->first!=r ){
             InstMatch m( q );
-            m.add( baseMatch );
             addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
             if( qe->inConflict() ){
               break;
@@ -1066,7 +1066,6 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
   Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
   if( tat ){
     InstMatch m( q );
-    m.add( baseMatch );
     addInstantiations( m, qe, addedLemmas, 0, tat );
   }
   return addedLemmas;
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index e36ee2b58..95faf0279 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -89,14 +89,10 @@ public:
   * using the implemented matching algorithm. It typically is implemented as a
   * fixed point of getNextMatch above.
   *
-  * baseMatch is a mapping of default values that should be used for variables
-  * that are not bound by this (not frequently used). (TODO remove #1389)
-  *
   * It returns the number of instantiations added using calls to calls to
   * Instantiate::addInstantiation(...).
   */
   virtual int addInstantiations(Node q,
-                                InstMatch& baseMatch,
                                 QuantifiersEngine* qe,
                                 Trigger* tparent)
   {
@@ -198,13 +194,6 @@ class InstMatchGenerator : public IMGenerator {
 public:
  /** destructor */
  virtual ~InstMatchGenerator() throw();
- enum
- {
-   // options for producing matches
-   MATCH_GEN_DEFAULT = 0,
-   // others (internally used)
-   MATCH_GEN_INTERNAL_ERROR,
- };
 
  /** Reset instantiation round. */
  void resetInstantiationRound(QuantifiersEngine* qe) override;
@@ -217,7 +206,6 @@ public:
                   Trigger* tparent) override;
  /** Add instantiations. */
  int addInstantiations(Node q,
-                       InstMatch& baseMatch,
                        QuantifiersEngine* qe,
                        Trigger* tparent) override;
 
@@ -329,11 +317,6 @@ protected:
   * (e.g. a matchable term, a variable, a relation, etc.).
   */
  CandidateGenerator* d_cg;
- /** policy to use for matching
-  * This is one of MATCH_GEN_* above.
-  * TODO: this can be simplified/removed (#1283).
-  */
- int d_matchPolicy;
  /** children generators
   * These match generators correspond to the children of the term
   * we are matching with this generator.
@@ -347,7 +330,16 @@ protected:
   * of the term.
   */
  std::vector<int> d_children_index;
- /** children types 0 : variable, 1 : child term, -1 : ground term */
+ /** children types
+  *
+  * If d_match_pattern is an instantiation constant, then this is a singleton
+  * vector containing the variable number of the d_match_pattern itself.
+  * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
+  * index i, d_children[i] stores the type of node ti is, where:
+  *   >= 0 : variable (indicates its number),
+  *   -1 : ground term,
+  *   -2 : child term.
+  */
  std::vector<int> d_children_types;
  /** The next generator in the linked list
   * that this generator is a part of.
@@ -358,13 +350,6 @@ protected:
  /** If non-null, then this is a relational trigger of the form x ~
   * d_eq_class_rel. */
  Node d_eq_class_rel;
- /** For each child index of this node, the variable numbers of the children.
- * For example, if this is generator is for the term f( x3, a, x1, x2 )
- *  the quantified formula
- *    forall x1 x2 x3. (...).
- * Then d_var_num[0] = 2, d_var_num[2] = 0 and d_var_num[3] = 1.
- */
- std::map<int, int> d_var_num;
  /** Excluded matches
  * Stores the terms we are not allowed to match.
  * These can for instance be specified by the smt2
@@ -575,7 +560,6 @@ class InstMatchGeneratorMulti : public IMGenerator {
   bool reset(Node eqc, QuantifiersEngine* qe) override;
   /** Add instantiations. */
   int addInstantiations(Node q,
-                        InstMatch& baseMatch,
                         QuantifiersEngine* qe,
                         Trigger* tparent) override;
 
@@ -663,7 +647,6 @@ class InstMatchGeneratorSimple : public IMGenerator {
   void resetInstantiationRound(QuantifiersEngine* qe) override;
   /** Add instantiations. */
   int addInstantiations(Node q,
-                        InstMatch& baseMatch,
                         QuantifiersEngine* qe,
                         Trigger* tparent) override;
   /** Get active score. */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index f7e5891f9..c39df58c6 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -106,8 +106,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
           Trace("process-trigger") << "  Process (user) ";
           d_user_gen[f][i]->debugPrint("process-trigger");
           Trace("process-trigger") << "..." << std::endl;
-          InstMatch baseMatch( f );
-          int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
+          int numInst = d_user_gen[f][i]->addInstantiations();
           Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
           d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
           if( d_user_gen[f][i]->isMultiTrigger() ){
@@ -249,8 +248,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
               Trace("process-trigger") << "  Process ";
               tr->debugPrint("process-trigger");
               Trace("process-trigger") << "..." << std::endl;
-              InstMatch baseMatch( f );
-              int numInst = tr->addInstantiations( baseMatch );
+              int numInst = tr->addInstantiations();
               hasInst = numInst>0 || hasInst;
               Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
               d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index dba04ce51..fbd122bd6 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -717,7 +717,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
         tr->reset( Node::null() );
         //d_qe->d_optInstMakeRepresentative = false;
         //d_qe->d_optMatchIgnoreModelBasis = true;
-        addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
+        addedLemmas += tr->addInstantiations();
       }
     }
   }
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 40079933e..2d97bd160 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -48,24 +48,25 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
 }
 
 /** trigger class constructor */
-Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
-    : d_quantEngine( qe ), d_f( f ) {
+Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
+    : d_quantEngine(qe), d_quant(q)
+{
   d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
-  Trace("trigger") << "Trigger for " << f << ": " << std::endl;
+  Trace("trigger") << "Trigger for " << q << ": " << std::endl;
   for( unsigned i=0; i<d_nodes.size(); i++ ){
     Trace("trigger") << "   " << d_nodes[i] << std::endl;
   }
   if( d_nodes.size()==1 ){
     if( isSimpleTrigger( d_nodes[0] ) ){
-      d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe );
+      d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe);
     }else{
-      d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
+      d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe);
     }
   }else{
     if( options::multiTriggerCache() ){
-      d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
+      d_mg = new InstMatchGeneratorMulti(q, d_nodes, qe);
     }else{
-      d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( f, d_nodes, qe );
+      d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe);
     }
   }
   if( d_nodes.size()==1 ){
@@ -75,14 +76,14 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
       ++(qe->d_statistics.d_simple_triggers);
     }
   }else{
-    Trace("multi-trigger") << "Trigger for " << f << ": " << std::endl;
+    Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
     for( unsigned i=0; i<d_nodes.size(); i++ ){
       Trace("multi-trigger") << "   " << d_nodes[i] << std::endl;
     }
     ++(qe->d_statistics.d_multi_triggers);
   }
 
-  //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
+  // Notice() << "Trigger : " << (*this) << "  for " << q << std::endl;
   Trace("trigger-debug") << "Finished making trigger." << std::endl;
 }
 
@@ -102,10 +103,9 @@ Node Trigger::getInstPattern(){
   return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
 }
 
-int Trigger::addInstantiations(InstMatch& baseMatch)
+int Trigger::addInstantiations()
 {
-  int addedLemmas =
-      d_mg->addInstantiations(d_f, baseMatch, d_quantEngine, this);
+  int addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
   if( addedLemmas>0 ){
     if (Debug.isOn("inst-trigger"))
     {
@@ -123,7 +123,7 @@ int Trigger::addInstantiations(InstMatch& baseMatch)
 
 bool Trigger::sendInstantiation(InstMatch& m)
 {
-  return d_quantEngine->getInstantiate()->addInstantiation(d_f, m);
+  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
 }
 
 bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 2beafb984..e897c0b06 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -118,10 +118,9 @@ class TriggerTermInfo {
 * t->resetInstantiationRound();
 * // will produce instantiations based on matching with all terms
 * t->reset( Node::null() );
-* InstMatch baseMatch;
 * // add all instantiations based on E-matching with this trigger and the
 * // current context
-* t->addInstantiations( baseMatch );
+* t->addInstantiations();
 *
 * This will result in (a set of) calls to
 * Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
@@ -187,13 +186,8 @@ class Trigger {
   * of the underlying match generator. It can be extended to
   * produce instantiations beyond what is produced by the match generator
   * (for example, see theory/quantifiers/ho_trigger.h).
-  *
-  * baseMatch : a mapping of default values that should be used for variables
-  *             that are not bound as a result of matching terms from this
-  *             trigger. These default values are not frequently used in
-  *             instantiations.  (TODO : remove #1389)
   */
-  virtual int addInstantiations(InstMatch& baseMatch);
+  virtual int addInstantiations();
   /** Return whether this is a multi-trigger. */
   bool isMultiTrigger() { return d_nodes.size()>1; }
   /** Get instantiation pattern list associated with this trigger.
@@ -367,7 +361,7 @@ class Trigger {
 
  protected:
   /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
-  Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );
+  Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& nodes);
   /** is subterm of trigger usable (helper function for isUsableTrigger) */
   static bool isUsable( Node n, Node q );
   /** returns an equality that is equivalent to the equality eq and
@@ -437,7 +431,7 @@ class Trigger {
   /** The quantifiers engine associated with this trigger. */
   QuantifiersEngine* d_quantEngine;
   /** The quantified formula this trigger is for. */
-  Node d_f;
+  Node d_quant;
   /** match generator
    *
   * This is the back-end utility that implements the underlying matching