From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 24 Jan 2021 18:43:54 +0000 (-0600)
Subject: Initial cleaning of inst match generator (#5794)
X-Git-Tag: cvc5-1.0.0~2364
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d8a3b458b11961026ee1e58782ff073de29f93b;p=cvc5.git

Initial cleaning of inst match generator (#5794)

In preparation towards breaking this file up into multiple files.

No code changes, only updates to conform to new guidelines.
---

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 588ec031d..c8e821dd7 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -24,11 +24,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
-using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
 
 namespace CVC4 {
 namespace theory {
@@ -40,22 +36,22 @@ bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m)
 }
 
 InstMatchGenerator::InstMatchGenerator( Node pat ){
-  d_cg = NULL;
+  d_cg = nullptr;
   d_needsReset = true;
   d_active_add = true;
   Assert(quantifiers::TermUtil::hasInstConstAttr(pat));
   d_pattern = pat;
   d_match_pattern = pat;
   d_match_pattern_type = pat.getType();
-  d_next = NULL;
+  d_next = nullptr;
   d_independent_gen = false;
 }
 
 InstMatchGenerator::InstMatchGenerator() {
-  d_cg = NULL;
+  d_cg = nullptr;
   d_needsReset = true;
   d_active_add = true;
-  d_next = NULL;
+  d_next = nullptr;
   d_independent_gen = false;
 }
 
@@ -69,7 +65,8 @@ InstMatchGenerator::~InstMatchGenerator()
 
 void InstMatchGenerator::setActiveAdd(bool val){
   d_active_add = val;
-  if( d_next!=NULL ){
+  if (d_next != nullptr)
+  {
     d_next->setActiveAdd(val);
   }
 }
@@ -87,175 +84,186 @@ int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
     unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
     Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
     return ngtt;
-//  }else if( d_match_pattern_getKind()==EQUAL ){
-    
-  }else{
-    return -1;
   }
+  return -1;
 }
 
-void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
-  if( !d_pattern.isNull() ){
-    Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
-    if( d_match_pattern.getKind()==NOT ){
-      Assert(d_pattern.getKind() == NOT);
-      //we want to add the children of the NOT
-      d_match_pattern = d_match_pattern[0];
-    }
+void InstMatchGenerator::initialize(Node q,
+                                    QuantifiersEngine* qe,
+                                    std::vector<InstMatchGenerator*>& gens)
+{
+  if (d_pattern.isNull())
+  {
+    gens.insert(gens.end(), d_children.begin(), d_children.end());
+    return;
+  }
+  Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern
+                          << std::endl;
+  if (d_match_pattern.getKind() == NOT)
+  {
+    Assert(d_pattern.getKind() == NOT);
+    // we want to add the children of the NOT
+    d_match_pattern = d_match_pattern[0];
+  }
 
-    if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL
-        && d_match_pattern[0].getKind() == INST_CONSTANT
-        && d_match_pattern[1].getKind() == INST_CONSTANT)
-    {
-      // special case: disequalities between variables x != y will match ground
-      // disequalities.
-    }
-    else if (d_match_pattern.getKind() == EQUAL
-             || d_match_pattern.getKind() == GEQ)
+  if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL
+      && d_match_pattern[0].getKind() == INST_CONSTANT
+      && d_match_pattern[1].getKind() == INST_CONSTANT)
+  {
+    // special case: disequalities between variables x != y will match ground
+    // disequalities.
+  }
+  else if (d_match_pattern.getKind() == EQUAL
+           || d_match_pattern.getKind() == GEQ)
+  {
+    // We are one of the following cases:
+    //   f(x)~a, f(x)~y, x~a, x~y
+    // If we are the first or third case, we ensure that f(x)/x is on the left
+    // hand side of the relation d_pattern, d_match_pattern is f(x)/x and
+    // d_eq_class_rel (indicating the equivalence class that we are related
+    // to) is set to a.
+    for (size_t i = 0; i < 2; i++)
     {
-      // We are one of the following cases:
-      //   f(x)~a, f(x)~y, x~a, x~y
-      // If we are the first or third case, we ensure that f(x)/x is on the left
-      // hand side of the relation d_pattern, d_match_pattern is f(x)/x and
-      // d_eq_class_rel (indicating the equivalence class that we are related
-      // to) is set to a.
-      for( unsigned i=0; i<2; i++ ){
-        Node mp = d_match_pattern[i];
-        Node mpo = d_match_pattern[1 - i];
-        // If this side has free variables, and the other side does not or
-        // it is a free variable, then we will match on this side of the
-        // relation.
-        if (quantifiers::TermUtil::hasInstConstAttr(mp)
-            && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
-                || mpo.getKind() == INST_CONSTANT))
+      Node mp = d_match_pattern[i];
+      Node mpo = d_match_pattern[1 - i];
+      // If this side has free variables, and the other side does not or
+      // it is a free variable, then we will match on this side of the
+      // relation.
+      if (quantifiers::TermUtil::hasInstConstAttr(mp)
+          && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
+              || mpo.getKind() == INST_CONSTANT))
+      {
+        if (i == 1)
         {
-          if (i == 1)
+          if (d_match_pattern.getKind() == GEQ)
           {
-            if (d_match_pattern.getKind() == GEQ)
-            {
-              d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
-              d_pattern = d_pattern.negate();
-            }
-            else
-            {
-              d_pattern = NodeManager::currentNM()->mkNode(
-                  d_match_pattern.getKind(), mp, mpo);
-            }
+            d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
+            d_pattern = d_pattern.negate();
+          }
+          else
+          {
+            d_pattern = NodeManager::currentNM()->mkNode(
+                d_match_pattern.getKind(), mp, mpo);
           }
-          d_eq_class_rel = mpo;
-          d_match_pattern = mp;
-          // we won't find a term in the other direction
-          break;
         }
+        d_eq_class_rel = mpo;
+        d_match_pattern = mp;
+        // we won't find a term in the other direction
+        break;
       }
     }
-    d_match_pattern_type = d_match_pattern.getType();
-    Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
-    d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+  }
+  d_match_pattern_type = d_match_pattern.getType();
+  Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is "
+                          << d_match_pattern << std::endl;
+  d_match_pattern_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
 
-    //now, collect children of d_match_pattern
-    Kind mpk = d_match_pattern.getKind();
-    if (mpk == INST_CONSTANT)
-    {
-      d_children_types.push_back(
-          d_match_pattern.getAttribute(InstVarNumAttribute()));
-    }
-    else
+  // now, collect children of d_match_pattern
+  Kind mpk = d_match_pattern.getKind();
+  if (mpk == INST_CONSTANT)
+  {
+    d_children_types.push_back(
+        d_match_pattern.getAttribute(InstVarNumAttribute()));
+  }
+  else
+  {
+    for (size_t i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
     {
-      for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size;
-           i++)
+      Node pat = d_match_pattern[i];
+      Node qa = quantifiers::TermUtil::getInstConstAttr(pat);
+      if (!qa.isNull())
       {
-        Node pat = d_match_pattern[i];
-        Node qa = quantifiers::TermUtil::getInstConstAttr(pat);
-        if (!qa.isNull())
+        if (pat.getKind() == INST_CONSTANT && qa == q)
+        {
+          d_children_types.push_back(pat.getAttribute(InstVarNumAttribute()));
+        }
+        else
         {
-          if (pat.getKind() == INST_CONSTANT && qa == q)
+          InstMatchGenerator* cimg = getInstMatchGenerator(q, pat);
+          if (cimg)
           {
-            d_children_types.push_back(pat.getAttribute(InstVarNumAttribute()));
+            d_children.push_back(cimg);
+            d_children_index.push_back(i);
+            d_children_types.push_back(-2);
           }
           else
           {
-            InstMatchGenerator* cimg = getInstMatchGenerator(q, pat);
-            if (cimg)
-            {
-              d_children.push_back(cimg);
-              d_children_index.push_back(i);
-              d_children_types.push_back(-2);
-            }
-            else
-            {
-              d_children_types.push_back(-1);
-            }
+            d_children_types.push_back(-1);
           }
         }
-        else
-        {
-          d_children_types.push_back(-1);
-        }
+      }
+      else
+      {
+        d_children_types.push_back(-1);
       }
     }
+  }
 
-    //create candidate generator
-    if (mpk == APPLY_SELECTOR)
-    {
-      // candidates for apply selector are a union of correctly and incorrectly
-      // applied selectors
-      d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
-    }
-    else if (Trigger::isAtomicTriggerKind(mpk))
+  // create candidate generator
+  if (mpk == APPLY_SELECTOR)
+  {
+    // candidates for apply selector are a union of correctly and incorrectly
+    // applied selectors
+    d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
+  }
+  else if (Trigger::isAtomicTriggerKind(mpk))
+  {
+    if (mpk == APPLY_CONSTRUCTOR)
     {
-      if (mpk == APPLY_CONSTRUCTOR)
-      {
-        // 1-constructors have a trivial way of generating candidates in a
-        // given equivalence class
-        const DType& dt = d_match_pattern.getType().getDType();
-        if (dt.getNumConstructors() == 1)
-        {
-          d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
-        }
-      }
-      if (d_cg == nullptr)
+      // 1-constructors have a trivial way of generating candidates in a
+      // given equivalence class
+      const DType& dt = d_match_pattern.getType().getDType();
+      if (dt.getNumConstructors() == 1)
       {
-        CandidateGeneratorQE* cg =
-            new CandidateGeneratorQE(qe, d_match_pattern);
-        // we will be scanning lists trying to find ground terms whose operator
-        // is the same as d_match_operator's.
-        d_cg = cg;
-        // if matching on disequality, inform the candidate generator not to
-        // match on eqc
-        if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL)
-        {
-          cg->excludeEqc(d_eq_class_rel);
-          d_eq_class_rel = Node::null();
-        }
+        d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
       }
     }
-    else if (mpk == INST_CONSTANT)
+    if (d_cg == nullptr)
     {
-      if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
-        Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
-        size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
-        const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
-        const DTypeConstructor& c = dt[selectorIndex];
-        Node cOp = c.getConstructor();
-        Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl;
-        d_cg = new inst::CandidateGeneratorQE( qe, cOp );
-      }else{
-        d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
+      CandidateGeneratorQE* cg = new CandidateGeneratorQE(qe, d_match_pattern);
+      // we will be scanning lists trying to find ground terms whose operator
+      // is the same as d_match_operator's.
+      d_cg = cg;
+      // if matching on disequality, inform the candidate generator not to
+      // match on eqc
+      if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL)
+      {
+        cg->excludeEqc(d_eq_class_rel);
+        d_eq_class_rel = Node::null();
       }
     }
-    else if (mpk == EQUAL)
+  }
+  else if (mpk == INST_CONSTANT)
+  {
+    if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL)
     {
-      //we will be producing candidates via literal matching heuristics
-      if (d_pattern.getKind() == NOT)
-      {
-        // candidates will be all disequalities
-        d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
-      }
+      Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
+      size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
+      const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
+      const DTypeConstructor& c = dt[selectorIndex];
+      Node cOp = c.getConstructor();
+      Trace("inst-match-gen")
+          << "Purify dt trigger " << d_pattern << ", will match terms of op "
+          << cOp << std::endl;
+      d_cg = new inst::CandidateGeneratorQE(qe, cOp);
     }else{
-      Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
+      d_cg = new CandidateGeneratorQEAll(qe, d_match_pattern);
     }
   }
+  else if (mpk == EQUAL)
+  {
+    // we will be producing candidates via literal matching heuristics
+    if (d_pattern.getKind() == NOT)
+    {
+      // candidates will be all disequalities
+      d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+    }
+  }
+  else
+  {
+    Trace("inst-match-gen-warn")
+        << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
+  }
   gens.insert( gens.end(), d_children.begin(), d_children.end() );
 }
 
@@ -270,141 +278,166 @@ int InstMatchGenerator::getMatch(
   {
     Trace("matching-fail") << "Internal error for match generator." << std::endl;
     return -2;
-  }else{
-    EqualityQuery* q = qe->getEqualityQuery();
-    bool success = true;
-    //save previous match
-    //InstMatch prev( &m );
-    std::vector< int > prev;
-    //if t is null
-    Assert(!t.isNull());
-    Assert(!quantifiers::TermUtil::hasInstConstAttr(t));
-    // notice that t may have a different kind or operator from our match
-    // pattern, e.g. for APPLY_SELECTOR triggers.
-    //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, size = d_match_pattern.getNumChildren(); i < size; i++)
+  }
+  EqualityQuery* q = qe->getEqualityQuery();
+  bool success = true;
+  std::vector<int> prev;
+  // if t is null
+  Assert(!t.isNull());
+  Assert(!quantifiers::TermUtil::hasInstConstAttr(t));
+  // notice that t may have a different kind or operator from our match
+  // pattern, e.g. for APPLY_SELECTOR triggers.
+  // first, check if ground arguments are not equal, or a match is in conflict
+  Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
+  for (size_t i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
+  {
+    int64_t ct = d_children_types[i];
+    if (ct >= 0)
     {
-      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]))
       {
-        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(ct) << " and "
-                                 << t[i] << std::endl;
-          success = false;
-          break;
-        }else if( addToPrev ){
-          Trace("matching-debug2") << "Success." << std::endl;
-          prev.push_back(ct);
-        }
+        // match is in conflict
+        Trace("matching-fail")
+            << "Match fail: " << m.get(ct) << " and " << t[i] << std::endl;
+        success = false;
+        break;
       }
-      else if (ct == -1)
+      else if (addToPrev)
       {
-        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
-          success = false;
-          break;
-        }
+        Trace("matching-debug2") << "Success." << std::endl;
+        prev.push_back(ct);
       }
     }
-    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_children_types[0]).isNull();
-      if (!m.set(q, d_children_types[0], t))
+    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
         success = false;
-      }else{
-        if( addToPrev ){
-          prev.push_back(d_children_types[0]);
-        }
+        break;
       }
     }
-    //for relational matching
-    if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT)
+  }
+  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_children_types[0]).isNull();
+    if (!m.set(q, d_children_types[0], t))
     {
-      int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
-      //also must fit match to equivalence class
-      bool pol = d_pattern.getKind()!=NOT;
-      Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
-      Node t_match;
-      if( pol ){
-        if( pat.getKind()==GT ){
-          t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermUtil()->d_one);
-        }else{
-          t_match = t;
-        }
+      success = false;
+    }
+    else
+    {
+      if (addToPrev)
+      {
+        prev.push_back(d_children_types[0]);
+      }
+    }
+  }
+  // for relational matching
+  if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
+    // also must fit match to equivalence class
+    bool pol = d_pattern.getKind() != NOT;
+    Node pat = d_pattern.getKind() == NOT ? d_pattern[0] : d_pattern;
+    Node t_match;
+    if (pol)
+    {
+      if (pat.getKind() == GT)
+      {
+        t_match = nm->mkNode(MINUS, t, nm->mkConst(Rational(1)));
       }else{
-        if( pat.getKind()==EQUAL ){
-          if( t.getType().isBoolean() ){
-            t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) );
-          }else{
-            Assert(t.getType().isReal());
-            t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
-          }
-        }else if( pat.getKind()==GEQ ){
-          t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
-        }else if( pat.getKind()==GT ){
-          t_match = t;
-        }
+        t_match = t;
       }
-      if( !t_match.isNull() ){
-        bool addToPrev = m.get( v ).isNull();
-        if (!m.set(q, v, t_match))
+    }
+    else
+    {
+      if (pat.getKind() == EQUAL)
+      {
+        if (t.getType().isBoolean())
+        {
+          t_match = nm->mkConst(!q->areEqual(nm->mkConst(true), t));
+        }
+        else
         {
-          success = false;
-        }else if( addToPrev ){
-          prev.push_back( v );
+          Assert(t.getType().isReal());
+          t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
         }
       }
+      else if (pat.getKind() == GEQ)
+      {
+        t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
+      }
+      else if (pat.getKind() == GT)
+      {
+        t_match = t;
+      }
     }
-    int ret_val = -1;
-    if( success ){
-      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, size = d_children.size(); i < size; i++)
+    if (!t_match.isNull())
+    {
+      bool addToPrev = m.get(v).isNull();
+      if (!m.set(q, v, t_match))
       {
-        if( !d_children[i]->reset( t[ d_children_index[i] ], qe ) ){
-          success = false;
-          break;
-        }
+        success = false;
       }
-      if( success ){
-        Trace("matching-debug2") << "Continue next " << d_next << std::endl;
-        ret_val = continueNextMatch(f, m, qe, tparent);
+      else if (addToPrev)
+      {
+        prev.push_back(v);
       }
     }
-    if( ret_val<0 ){
-      for (int& pv : prev)
+  }
+  int ret_val = -1;
+  if (success)
+  {
+    Trace("matching-debug2") << "Reset children..." << std::endl;
+    // now, fit children into match
+    // we will be requesting candidates for matching terms for each child
+    for (size_t i = 0, size = d_children.size(); i < size; i++)
+    {
+      if (!d_children[i]->reset(t[d_children_index[i]], qe))
       {
-        m.d_vals[pv] = Node::null();
+        success = false;
+        break;
       }
     }
-    return ret_val;
+    if (success)
+    {
+      Trace("matching-debug2") << "Continue next " << d_next << std::endl;
+      ret_val = continueNextMatch(f, m, qe, tparent);
+    }
+  }
+  if (ret_val < 0)
+  {
+    for (int& pv : prev)
+    {
+      m.d_vals[pv] = Node::null();
+    }
   }
+  return ret_val;
 }
 
-int InstMatchGenerator::continueNextMatch(Node f,
+int InstMatchGenerator::continueNextMatch(Node q,
                                           InstMatch& m,
                                           QuantifiersEngine* qe,
                                           Trigger* tparent)
 {
   if( d_next!=NULL ){
-    return d_next->getNextMatch(f, m, qe, tparent);
-  }else{
-    if( d_active_add ){
-      return sendInstantiation(tparent, m) ? 1 : -1;
-    }else{
-      return 1;
-    }
+    return d_next->getNextMatch(q, m, qe, tparent);
+  }
+  if (d_active_add)
+  {
+    return sendInstantiation(tparent, m) ? 1 : -1;
   }
+  return 1;
 }
 
 /** reset instantiation round */
@@ -502,12 +535,12 @@ int InstMatchGenerator::getNextMatch(Node f,
   return success;
 }
 
-int InstMatchGenerator::addInstantiations(Node f,
-                                          QuantifiersEngine* qe,
-                                          Trigger* tparent)
+uint64_t InstMatchGenerator::addInstantiations(Node f,
+                                               QuantifiersEngine* qe,
+                                               Trigger* tparent)
 {
   //try to add instantiation for each match produced
-  int addedLemmas = 0;
+  uint64_t addedLemmas = 0;
   InstMatch m( f );
   while (getNextMatch(f, m, qe, tparent) > 0)
   {
@@ -547,10 +580,11 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( Node q, std::
   Assert(gens.size() == pats.size());
   std::vector< Node > patsn;
   std::map< Node, InstMatchGenerator * > pat_map_init;
-  for( unsigned i=0; i<gens.size(); i++ ){
-    Node pn = gens[i]->d_match_pattern;
+  for (InstMatchGenerator* g : gens)
+  {
+    Node pn = g->d_match_pattern;
     patsn.push_back( pn );
-    pat_map_init[pn] = gens[i];
+    pat_map_init[pn] = g;
   }
   //return mkInstMatchGenerator( q, patsn, qe, pat_map_init );
   imgm->d_next = mkInstMatchGenerator( q, patsn, qe, pat_map_init );
@@ -669,21 +703,26 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
         q, pat, var_contains[pat]);
   }
   std::map< Node, std::vector< Node > > var_to_node;
-  for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
-    for( unsigned i=0; i<it->second.size(); i++ ){
-      var_to_node[ it->second[i] ].push_back( it->first );
+  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
+  {
+    for (const Node& n : vc.second)
+    {
+      var_to_node[n].push_back(vc.first);
     }
   }
   std::vector< Node > pats_ordered;
   std::vector< bool > pats_ordered_independent;
   std::map< Node, bool > var_bound;
-  while( pats_ordered.size()<pats.size() ){
+  size_t patsSize = pats.size();
+  while (pats_ordered.size() < patsSize)
+  {
     // score is lexographic ( bound vars, shared vars )
     int score_max_1 = -1;
     int score_max_2 = -1;
     unsigned score_index = 0;
     bool set_score_index = false;
-    for( unsigned i=0; i<pats.size(); i++ ){
+    for (size_t i = 0; i < patsSize; i++)
+    {
       Node p = pats[i];
       if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){
         int score_1 = 0;
@@ -709,28 +748,36 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
     Assert(set_score_index);
     //update the variable bounds
     Node mp = pats[score_index];
-    for( unsigned i=0; i<var_contains[mp].size(); i++ ){
-      var_bound[var_contains[mp][i]] = true;
+    std::vector<Node>& vcm = var_contains[mp];
+    for (const Node& vc : vcm)
+    {
+      var_bound[vc] = true;
     }
     pats_ordered.push_back( mp );
     pats_ordered_independent.push_back( score_max_1==0 );
   }
   
   Trace("multi-trigger-linear") << "Make children for linear multi trigger." << std::endl;
-  for( unsigned i=0; i<pats_ordered.size(); i++ ){
-    Trace("multi-trigger-linear") << "...make for " << pats_ordered[i] << std::endl;
-    InstMatchGenerator* cimg = getInstMatchGenerator(q, pats_ordered[i]);
-    Assert(cimg != NULL);
+  for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++)
+  {
+    Node po = pats_ordered[i];
+    Trace("multi-trigger-linear") << "...make for " << po << std::endl;
+    InstMatchGenerator* cimg = getInstMatchGenerator(q, po);
+    Assert(cimg != nullptr);
     d_children.push_back( cimg );
-    if( i==0 ){  //TODO : improve
+    // this could be improved
+    if (i == 0)
+    {
       cimg->setIndependent();
     }
   }
 }
 
 int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
-  for( unsigned i=0; i<d_children.size(); i++ ){
-    if( !d_children[i]->reset( Node::null(), qe ) ){
+  for (InstMatchGenerator* c : d_children)
+  {
+    if (!c->reset(Node::null(), qe))
+    {
       return -2;
     }
   }
@@ -741,9 +788,8 @@ bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) {
   Assert(eqc.isNull());
   if( options::multiTriggerLinear() ){
     return true;
-  }else{
-    return resetChildren( qe )>0;
   }
+  return resetChildren(qe) > 0;
 }
 
 int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
@@ -760,13 +806,14 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
     }
   }
   Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
-  Assert(d_next != NULL);
+  Assert(d_next != nullptr);
   int ret_val = continueNextMatch(q, m, qe, tparent);
   if( ret_val>0 ){
     Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl;
     if( options::multiTriggerLinear() ){
       // now, restrict everyone
-      for( unsigned i=0; i<d_children.size(); i++ ){
+      for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+      {
         Node mi = d_children[i]->getCurrentMatch();
         Trace("multi-trigger-linear") << "   child " << i << " match : " << mi << std::endl;
         d_children[i]->excludeMatch( mi );
@@ -791,17 +838,21 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
         q, pat, var_contains[pat]);
   }
   //convert to indicies
-  for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
-    Trace("multi-trigger-cache") << "Pattern " << it->first << " contains: ";
-    for( int i=0; i<(int)it->second.size(); i++ ){
-      Trace("multi-trigger-cache") << it->second[i] << " ";
-      int index = it->second[i].getAttribute(InstVarNumAttribute());
-      d_var_contains[ it->first ].push_back( index );
-      d_var_to_node[ index ].push_back( it->first );
+  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
+  {
+    Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: ";
+    for (const Node& vcn : vc.second)
+    {
+      Trace("multi-trigger-cache") << vcn << " ";
+      uint64_t index = vcn.getAttribute(InstVarNumAttribute());
+      d_var_contains[vc.first].push_back(index);
+      d_var_to_node[index].push_back(vc.first);
     }
     Trace("multi-trigger-cache") << std::endl;
   }
-  for( unsigned i=0; i<pats.size(); i++ ){
+  size_t patsSize = pats.size();
+  for (size_t i = 0; i < patsSize; i++)
+  {
     Node n = pats[i];
     //make the match generator
     InstMatchGenerator* img =
@@ -809,40 +860,51 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
     img->setActiveAdd(false);
     d_children.push_back(img);
     //compute unique/shared variables
-    std::vector< int > unique_vars;
-    std::map< int, bool > shared_vars;
-    int numSharedVars = 0;
-    for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
-      if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
-        Trace("multi-trigger-cache") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
-        unique_vars.push_back( d_var_contains[n][j] );
+    std::vector<uint64_t> unique_vars;
+    std::map<uint64_t, bool> shared_vars;
+    unsigned numSharedVars = 0;
+    std::vector<uint64_t>& vctn = d_var_contains[n];
+    for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++)
+    {
+      if (d_var_to_node[vctn[j]].size() == 1)
+      {
+        Trace("multi-trigger-cache")
+            << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl;
+        unique_vars.push_back(vctn[j]);
       }else{
-        shared_vars[ d_var_contains[n][j] ] = true;
+        shared_vars[vctn[j]] = true;
         numSharedVars++;
       }
     }
     //we use the latest shared variables, then unique variables
-    std::vector< int > vars;
-    unsigned index = i==0 ? pats.size()-1 : (i-1);
+    std::vector<uint64_t> vars;
+    size_t index = i == 0 ? pats.size() - 1 : (i - 1);
     while( numSharedVars>0 && index!=i ){
-      for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
-        if( it->second ){
-          if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
-              d_var_contains[ pats[index] ].end() ){
-            vars.push_back( it->first );
-            shared_vars[ it->first ] = false;
+      for (std::pair<const uint64_t, bool>& sv : shared_vars)
+      {
+        if (sv.second)
+        {
+          std::vector<uint64_t>& vctni = d_var_contains[pats[index]];
+          if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end())
+          {
+            vars.push_back(sv.first);
+            shared_vars[sv.first] = false;
             numSharedVars--;
           }
         }
       }
-      index = index==0 ? (int)(pats.size()-1) : (index-1);
+      index = index == 0 ? patsSize - 1 : (index - 1);
     }
     vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
-    Trace("multi-trigger-cache") << "   Index[" << i << "]: ";
-    for( unsigned j=0; j<vars.size(); j++ ){
-      Trace("multi-trigger-cache") << vars[j] << " ";
+    if (Trace.isOn("multi-trigger-cache"))
+    {
+      Trace("multi-trigger-cache") << "   Index[" << i << "]: ";
+      for (uint64_t v : vars)
+      {
+        Trace("multi-trigger-cache") << v << " ";
+      }
+      Trace("multi-trigger-cache") << std::endl;
     }
-    Trace("multi-trigger-cache") << std::endl;
     //make ordered inst match trie
     d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
     d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
@@ -852,38 +914,44 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
 
 InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
 {
-  for( unsigned i=0; i<d_children.size(); i++ ){
+  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+  {
     delete d_children[i];
   }
-  for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){
-    delete it->second;
+  for (std::pair<const size_t, InstMatchTrie::ImtIndexOrder*>& i : d_imtio)
+  {
+    delete i.second;
   }
 }
 
 /** reset instantiation round (call this whenever equivalence classes have changed) */
 void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
-  for( unsigned i=0; i<d_children.size(); i++ ){
-    d_children[i]->resetInstantiationRound( qe );
+  for (InstMatchGenerator* c : d_children)
+  {
+    c->resetInstantiationRound(qe);
   }
 }
 
 /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
-  for( unsigned i=0; i<d_children.size(); i++ ){
-    if( !d_children[i]->reset( eqc, qe ) ){
-      //return false;
+  for (InstMatchGenerator* c : d_children)
+  {
+    if (!c->reset(eqc, qe))
+    {
+      // do not return false here
     }
   }
   return true;
 }
 
-int InstMatchGeneratorMulti::addInstantiations(Node q,
-                                               QuantifiersEngine* qe,
-                                               Trigger* tparent)
+uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
+                                                    QuantifiersEngine* qe,
+                                                    Trigger* tparent)
 {
-  int addedLemmas = 0;
+  uint64_t addedLemmas = 0;
   Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
-  for( unsigned i=0; i<d_children.size(); i++ ){
+  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+  {
     Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
     std::vector< InstMatch > newMatches;
     InstMatch m( q );
@@ -894,7 +962,8 @@ int InstMatchGeneratorMulti::addInstantiations(Node q,
       m.clear();
     }
     Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
-    for( unsigned j=0; j<newMatches.size(); j++ ){
+    for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++)
+    {
       Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl;
       processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
       if( qe->inConflict() ){
@@ -908,8 +977,8 @@ int InstMatchGeneratorMulti::addInstantiations(Node q,
 void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
                                               Trigger* tparent,
                                               InstMatch& m,
-                                              int fromChildIndex,
-                                              int& addedLemmas)
+                                              size_t fromChildIndex,
+                                              uint64_t& addedLemmas)
 {
   //see if these produce new matches
   d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m);
@@ -918,7 +987,7 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
   // we can safely skip the following lines, even when we have already produced this match.
   Trace("multi-trigger-cache-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl;
   //process new instantiations
-  int childIndex = (fromChildIndex+1)%(int)d_children.size();
+  size_t childIndex = (fromChildIndex + 1) % d_children.size();
   processNewInstantiations(qe,
                            tparent,
                            m,
@@ -933,11 +1002,11 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
 void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                                        Trigger* tparent,
                                                        InstMatch& m,
-                                                       int& addedLemmas,
+                                                       uint64_t& addedLemmas,
                                                        InstMatchTrie* tr,
-                                                       int trieIndex,
-                                                       int childIndex,
-                                                       int endChildIndex,
+                                                       size_t trieIndex,
+                                                       size_t childIndex,
+                                                       size_t endChildIndex,
                                                        bool modEq)
 {
   Assert(!qe->inConflict());
@@ -949,8 +1018,12 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
       Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m
                                          << std::endl;
     }
-  }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
-    int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
+    return;
+  }
+  InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering();
+  if (trieIndex < iio->d_order.size())
+  {
+    size_t curr_index = iio->d_order[trieIndex];
     // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
     // curr_index );
     Node n = m.get( curr_index );
@@ -989,43 +1062,44 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                endChildIndex,
                                modEq);
     }
-    if (modEq)
+    if (!modEq)
+    {
+      return;
+    }
+    eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine();
+    // check modulo equality for other possible instantiations
+    if (!ee->hasTerm(n))
+    {
+      return;
+    }
+    eq::EqClassIterator eqc(ee->getRepresentative(n), ee);
+    while (!eqc.isFinished())
     {
-      // check modulo equality for other possible instantiations
-      if (qe->getEqualityQuery()->getEngine()->hasTerm(n))
+      Node en = (*eqc);
+      if (en != n)
       {
-        eq::EqClassIterator eqc(
-            qe->getEqualityQuery()->getEngine()->getRepresentative(n),
-            qe->getEqualityQuery()->getEngine());
-        while (!eqc.isFinished())
+        std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
+        if (itc != tr->d_data.end())
         {
-          Node en = (*eqc);
-          if (en != n)
+          processNewInstantiations(qe,
+                                   tparent,
+                                   m,
+                                   addedLemmas,
+                                   &(itc->second),
+                                   trieIndex + 1,
+                                   childIndex,
+                                   endChildIndex,
+                                   modEq);
+          if (qe->inConflict())
           {
-            std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
-            if (itc != tr->d_data.end())
-            {
-              processNewInstantiations(qe,
-                                       tparent,
-                                       m,
-                                       addedLemmas,
-                                       &(itc->second),
-                                       trieIndex + 1,
-                                       childIndex,
-                                       endChildIndex,
-                                       modEq);
-              if (qe->inConflict())
-              {
-                break;
-              }
-            }
+            break;
           }
-          ++eqc;
         }
       }
+      ++eqc;
     }
   }else{
-    int newChildIndex = (childIndex+1)%(int)d_children.size();
+    size_t newChildIndex = (childIndex + 1) % d_children.size();
     processNewInstantiations(qe,
                              tparent,
                              m,
@@ -1055,7 +1129,8 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
     Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
   }
   Assert(Trigger::isSimpleTrigger(d_match_pattern));
-  for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
+  for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
+  {
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
       if( !options::cegqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
         d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
@@ -1071,11 +1146,11 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
 void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
   
 }
-int InstMatchGeneratorSimple::addInstantiations(Node q,
-                                                QuantifiersEngine* qe,
-                                                Trigger* tparent)
+uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
+                                                     QuantifiersEngine* qe,
+                                                     Trigger* tparent)
 {
-  int addedLemmas = 0;
+  uint64_t addedLemmas = 0;
   TNodeTrie* tat;
   if( d_eqc.isNull() ){
     tat = qe->getTermDatabase()->getTermArgTrie( d_op );
@@ -1114,8 +1189,8 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
 
 void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
                                                  QuantifiersEngine* qe,
-                                                 int& addedLemmas,
-                                                 unsigned argIndex,
+                                                 uint64_t& addedLemmas,
+                                                 size_t argIndex,
                                                  TNodeTrie* tat)
 {
   Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
@@ -1125,14 +1200,14 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     TNode t = tat->getData();
     Debug("simple-trigger") << "Actual term is " << t << std::endl;
     //convert to actual used terms
-    for (std::map<unsigned, int>::iterator it = d_var_num.begin();
-         it != d_var_num.end();
-         ++it)
+    for (const std::pair<unsigned, int>& v : d_var_num)
     {
-      if( it->second>=0 ){
-        Assert(it->first < t.getNumChildren());
-        Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl;
-        m.setValue( it->second, t[it->first] );
+      if (v.second >= 0)
+      {
+        Assert(v.first < t.getNumChildren());
+        Debug("simple-trigger")
+            << "...set " << v.second << " " << t[v.first] << std::endl;
+        m.setValue(v.second, t[v.first]);
       }
     }
     // we do not need the trigger parent for simple triggers (no post-processing
@@ -1142,43 +1217,48 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
     }
-  }else{
-    if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
-      int v = d_var_num[argIndex];
-      if( v!=-1 ){
-        for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
+    return;
+  }
+  if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
+  {
+    int v = d_var_num[argIndex];
+    if (v != -1)
+    {
+      for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
+      {
+        Node t = tt.first;
+        Node prev = m.get(v);
+        // using representatives, just check if equal
+        Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
+        if (prev.isNull() || prev == t)
         {
-          Node t = tt.first;
-          Node prev = m.get( v );
-          //using representatives, just check if equal
-          Assert(
-              t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
-          if( prev.isNull() || prev==t ){
-            m.setValue( v, t);
-            addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
-            m.setValue( v, prev);
-            if( qe->inConflict() ){
-              break;
-            }
+          m.setValue(v, t);
+          addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
+          m.setValue(v, prev);
+          if (qe->inConflict())
+          {
+            break;
           }
         }
-        return;
       }
-      //inst constant from another quantified formula, treat as ground term  TODO: remove this?
-    }
-    Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
-    std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
-    if( it!=tat->d_data.end() ){
-      addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+      return;
     }
+    // inst constant from another quantified formula, treat as ground term TODO:
+    // remove this?
+  }
+  Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]);
+  std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
+  if (it != tat->d_data.end())
+  {
+    addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second));
   }
 }
 
 int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
   Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
-  unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+  size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f);
   Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl;
-  return ngt;   
+  return static_cast<int>(ngt);
 }
 
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index c3b021acd..99816c040 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -90,9 +90,9 @@ public:
   * It returns the number of instantiations added using calls to calls to
   * Instantiate::addInstantiation(...).
   */
-  virtual int addInstantiations(Node q,
-                                QuantifiersEngine* qe,
-                                Trigger* tparent)
+  virtual uint64_t addInstantiations(Node q,
+                                     QuantifiersEngine* qe,
+                                     Trigger* tparent)
   {
     return 0;
   }
@@ -203,9 +203,9 @@ class InstMatchGenerator : public IMGenerator {
                    QuantifiersEngine* qe,
                    Trigger* tparent) override;
   /** Add instantiations. */
-  int addInstantiations(Node q,
-                        QuantifiersEngine* qe,
-                        Trigger* tparent) override;
+  uint64_t addInstantiations(Node q,
+                             QuantifiersEngine* qe,
+                             Trigger* tparent) override;
 
   /** set active add flag (true by default)
    *
@@ -327,7 +327,7 @@ class InstMatchGenerator : public IMGenerator {
    * in the example (EX1) above, indicating it is the 2nd child
    * of the term.
    */
-  std::vector<int> d_children_index;
+  std::vector<size_t> d_children_index;
   /** children types
    *
    * If d_match_pattern is an instantiation constant, then this is a singleton
@@ -338,7 +338,7 @@ class InstMatchGenerator : public IMGenerator {
    *   -1 : ground term,
    *   -2 : child term.
    */
-  std::vector<int> d_children_types;
+  std::vector<int64_t> d_children_types;
   /** The next generator in the linked list
    * that this generator is a part of.
    */
@@ -528,13 +528,11 @@ class InstMatchGeneratorMulti : public IMGenerator {
   /** Reset. */
   bool reset(Node eqc, QuantifiersEngine* qe) override;
   /** Add instantiations. */
-  int addInstantiations(Node q,
-                        QuantifiersEngine* qe,
-                        Trigger* tparent) override;
+  uint64_t addInstantiations(Node q,
+                             QuantifiersEngine* qe,
+                             Trigger* tparent) override;
 
  private:
-  /** indexed trie */
-  typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
   /** process new match
    *
    * Called during addInstantiations(...).
@@ -545,8 +543,8 @@ class InstMatchGeneratorMulti : public IMGenerator {
   void processNewMatch(QuantifiersEngine* qe,
                        Trigger* tparent,
                        InstMatch& m,
-                       int fromChildIndex,
-                       int& addedLemmas);
+                       size_t fromChildIndex,
+                       uint64_t& addedLemmas);
   /** helper for process new match
    * tr is the inst match trie (term index) we are currently traversing.
    * trieIndex is depth we are in trie tr.
@@ -560,16 +558,16 @@ class InstMatchGeneratorMulti : public IMGenerator {
   void processNewInstantiations(QuantifiersEngine* qe,
                                 Trigger* tparent,
                                 InstMatch& m,
-                                int& addedLemmas,
+                                uint64_t& addedLemmas,
                                 InstMatchTrie* tr,
-                                int trieIndex,
-                                int childIndex,
-                                int endChildIndex,
+                                size_t trieIndex,
+                                size_t childIndex,
+                                size_t endChildIndex,
                                 bool modEq);
   /** Map from pattern nodes to indices of variables they contain. */
-  std::map< Node, std::vector< int > > d_var_contains;
+  std::map<Node, std::vector<uint64_t> > d_var_contains;
   /** Map from variable indices to pattern nodes that contain them. */
-  std::map< int, std::vector< Node > > d_var_to_node;
+  std::map<uint64_t, std::vector<Node> > d_var_to_node;
   /** quantified formula we are producing matches for */
   Node d_quant;
   /** children generators
@@ -580,7 +578,7 @@ class InstMatchGeneratorMulti : public IMGenerator {
    * Stores a heuristically determined variable ordering (unique
    * variables first) for each term in the multi trigger.
    */
-  std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio;
+  std::map<size_t, InstMatchTrie::ImtIndexOrder*> d_imtio;
   /** inst match tries for each child node
    * This data structure stores all InstMatch objects generated
    * by matching for each term in the multi trigger.
@@ -614,9 +612,9 @@ class InstMatchGeneratorSimple : public IMGenerator {
   /** Reset instantiation round. */
   void resetInstantiationRound(QuantifiersEngine* qe) override;
   /** Add instantiations. */
-  int addInstantiations(Node q,
-                        QuantifiersEngine* qe,
-                        Trigger* tparent) override;
+  uint64_t addInstantiations(Node q,
+                             QuantifiersEngine* qe,
+                             Trigger* tparent) override;
   /** Get active score. */
   int getActiveScore(QuantifiersEngine* qe) override;
 
@@ -646,7 +644,7 @@ class InstMatchGeneratorSimple : public IMGenerator {
    * Map from child number of d_match_pattern to variable index, or -1 if the
    * child is not a variable.
    */
-  std::map<unsigned, int> d_var_num;
+  std::map<size_t, int> d_var_num;
   /** add instantiations, helper function.
    *
    * m is the current match we are building,
@@ -658,8 +656,8 @@ class InstMatchGeneratorSimple : public IMGenerator {
    */
   void addInstantiations(InstMatch& m,
                          QuantifiersEngine* qe,
-                         int& addedLemmas,
-                         unsigned argIndex,
+                         uint64_t& addedLemmas,
+                         size_t argIndex,
                          TNodeTrie* tat);
 };/* class InstMatchGeneratorSimple */
 }