Format

20 files changed, 393 insertions, 343 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 48933eff6..478d4cff6 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -187,7 +187,7 @@ Node ExtendedRewriter::extendedRewrite(Node n)
   if (new_ret.isNull())
   {
     TheoryId tid;
-    if( ret.getKind()==ITE )
+    if (ret.getKind() == ITE)
     {
       tid = Theory::theoryOf(ret.getType());
     }
@@ -195,7 +195,8 @@ Node ExtendedRewriter::extendedRewrite(Node n)
     {
       tid = Theory::theoryOf(ret);
     }
-    Trace("q-ext-rewrite-debug") << "theoryOf( " << ret << " )= " << tid << std::endl;
+    Trace("q-ext-rewrite-debug")
+        << "theoryOf( " << ret << " )= " << tid << std::endl;
     if (tid == THEORY_ARITH)
     {
       new_ret = extendedRewriteArith(ret);
@@ -1464,9 +1465,9 @@ bool ExtendedRewriter::inferSubstitution(Node n,
     Node v[2];
     for (unsigned i = 0; i < 2; i++)
     {
-      if( n[i].isConst() )
+      if (n[i].isConst())
       {
-        vars.push_back(n[1-i]);
+        vars.push_back(n[1 - i]);
         subs.push_back(n[i]);
         return true;
       }
@@ -1677,51 +1678,56 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
     }
     debugExtendedRewrite(ret, new_ret, "BV-eq-solve");
   }
-  else if (k == ITE )
+  else if (k == ITE)
   {
-    if( ret[0].getKind()==EQUAL && ret[0][0].getType().isBitVector() )
+    if (ret[0].getKind() == EQUAL && ret[0][0].getType().isBitVector())
     {
-      for( unsigned i=0; i<2; i++ )
+      for (unsigned i = 0; i < 2; i++)
       {
         Node ct = ret[0][i];
-        Node cto = ret[0][1-i];
-        if( ct.isConst() && bv::utils::getSize(ct)==1 )
+        Node cto = ret[0][1 - i];
+        if (ct.isConst() && bv::utils::getSize(ct) == 1)
         {
           // do they differ by exactly one bit?
-          std::vector< Node > rcc;
-          int diff_index = spliceBvConstBit(ret[1],ret[2],rcc);
-          if( diff_index>=0 )
+          std::vector<Node> rcc;
+          int diff_index = spliceBvConstBit(ret[1], ret[2], rcc);
+          if (diff_index >= 0)
           {
-            Node rpl = rcc[diff_index]==ct ? cto : TermUtil::mkNegate(BITVECTOR_NOT,cto);
+            Node rpl = rcc[diff_index] == ct
+                           ? cto
+                           : TermUtil::mkNegate(BITVECTOR_NOT, cto);
             rcc[diff_index] = rpl;
-            new_ret = rcc.size()==1 ? rcc[0] : nm->mkNode( BITVECTOR_CONCAT, rcc );
+            new_ret =
+                rcc.size() == 1 ? rcc[0] : nm->mkNode(BITVECTOR_CONCAT, rcc);
             debugExtendedRewrite(ret, new_ret, "BV 1bit ITE");
           }
         }
-        else if( ct.getKind()==BITVECTOR_EXTRACT )
+        else if (ct.getKind() == BITVECTOR_EXTRACT)
         {
           Node cte = ct[0];
-          if( cte==ret[1] || cte==ret[2] )
+          if (cte == ret[1] || cte == ret[2])
           {
             // get the other branch
-            Node ob = ret[cte==ret[1] ? 2 : 1];
+            Node ob = ret[cte == ret[1] ? 2 : 1];
             // get the extension of the extract
-            std::vector< Node > exs;
+            std::vector<Node> exs;
             exs.push_back(ct);
-            Node ext = extendBv(cte,exs);
-            Assert(ext.getType()==ob.getType());
+            Node ext = extendBv(cte, exs);
+            Assert(ext.getType() == ob.getType());
             // now, splice the other branch
-            std::vector< Node > extc;
-            std::vector< Node > obc;
-            spliceBv(ext,ob,extc,obc);
-            if( obc.size()==2 && ( cto==obc[0] || cto==obc[1] ) )
+            std::vector<Node> extc;
+            std::vector<Node> obc;
+            spliceBv(ext, ob, extc, obc);
+            if (obc.size() == 2 && (cto == obc[0] || cto == obc[1]))
             {
-              unsigned cflip_index = cto==obc[0] ? 1 : 0;
-              if( obc[cflip_index].isConst() && bv::utils::getSize(obc[cflip_index])==1 )
+              unsigned cflip_index = cto == obc[0] ? 1 : 0;
+              if (obc[cflip_index].isConst()
+                  && bv::utils::getSize(obc[cflip_index]) == 1)
               {
-                obc[cflip_index] = TermUtil::mkNegate(BITVECTOR_NOT,obc[cflip_index]);
-                Node new_eq = cte.eqNode( nm->mkNode( BITVECTOR_CONCAT, obc ) );
-                new_ret = nm->mkNode( ITE, new_eq, ret[1], ret[2] );
+                obc[cflip_index] =
+                    TermUtil::mkNegate(BITVECTOR_NOT, obc[cflip_index]);
+                Node new_eq = cte.eqNode(nm->mkNode(BITVECTOR_CONCAT, obc));
+                new_ret = nm->mkNode(ITE, new_eq, ret[1], ret[2]);
                 debugExtendedRewrite(ret, new_ret, "BV 1bit exrem ITE");
               }
             }
@@ -1842,25 +1848,26 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
         }
       }
     }
-    else if( ck==BITVECTOR_CONCAT )
+    else if (ck == BITVECTOR_CONCAT)
     {
       // negating odd numbers flips all but the lsb
       // -concat( t, 1 ) ---> concat( ~t, 1 )
-      Node last_child = ret[0][ret[0].getNumChildren()-1];
-      if( last_child.isConst() )
+      Node last_child = ret[0][ret[0].getNumChildren() - 1];
+      if (last_child.isConst())
       {
-        if( bv::utils::getBit(last_child,0) )
+        if (bv::utils::getBit(last_child, 0))
         {
-          std::vector< Node > children;
-          for( unsigned j=0, size=ret[0].getNumChildren(); j<size-1; j++ )
+          std::vector<Node> children;
+          for (unsigned j = 0, size = ret[0].getNumChildren(); j < size - 1;
+               j++)
           {
-            children.push_back(TermUtil::mkNegate(BITVECTOR_NOT,ret[0][j]));
+            children.push_back(TermUtil::mkNegate(BITVECTOR_NOT, ret[0][j]));
           }
           unsigned csize = bv::utils::getSize(last_child);
-          if( csize>1 )
+          if (csize > 1)
           {
-            Node extract = bv::utils::mkExtract(last_child, csize-1, 1);
-            extract = TermUtil::mkNegate(BITVECTOR_NOT,extract);
+            Node extract = bv::utils::mkExtract(last_child, csize - 1, 1);
+            extract = TermUtil::mkNegate(BITVECTOR_NOT, extract);
             children.push_back(extract);
             children.push_back(bv::utils::mkOnes(1));
           }
@@ -1868,7 +1875,7 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
           {
             children.push_back(last_child);
           }
-          new_ret = nm->mkNode(BITVECTOR_CONCAT,children);
+          new_ret = nm->mkNode(BITVECTOR_CONCAT, children);
           debugExtendedRewrite(ret, new_ret, "NEG-odd");
           return new_ret;
         }
@@ -1876,27 +1883,31 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret)
       // negating numbers with msb 1-bits flips all but the last
       // -concat( 1...11, t ) ----> concat( 0...0, -concat(1, t) )
       Node first_child = ret[0][0];
-      if( first_child.isConst() )
+      if (first_child.isConst())
       {
         unsigned csize = bv::utils::getSize(first_child);
-        int i = csize-1;
-        while( i>=0 && bv::utils::getBit(first_child,i) )
+        int i = csize - 1;
+        while (i >= 0 && bv::utils::getBit(first_child, i))
         {
           i--;
         }
-        i = i+2;
-        if( i<=static_cast<int>(csize-1) )
+        i = i + 2;
+        if (i <= static_cast<int>(csize - 1))
         {
-          Assert( i>0 );
-          Node extract_flip = bv::utils::mkExtract(first_child, csize-1, i);
-          extract_flip = TermUtil::mkNegate(BITVECTOR_NOT,extract_flip);
-          std::vector< Node > nchildren;
-          nchildren.push_back(bv::utils::mkExtract(first_child, i-1, 0));
-          for( unsigned j=1, size=ret[0].getNumChildren(); j<size; j++ )
+          Assert(i > 0);
+          Node extract_flip = bv::utils::mkExtract(first_child, csize - 1, i);
+          extract_flip = TermUtil::mkNegate(BITVECTOR_NOT, extract_flip);
+          std::vector<Node> nchildren;
+          nchildren.push_back(bv::utils::mkExtract(first_child, i - 1, 0));
+          for (unsigned j = 1, size = ret[0].getNumChildren(); j < size; j++)
           {
-            nchildren.push_back( ret[0][j] );
+            nchildren.push_back(ret[0][j]);
           }
-          new_ret = nm->mkNode(BITVECTOR_CONCAT,extract_flip, nm->mkNode(BITVECTOR_NEG, nm->mkNode(BITVECTOR_CONCAT,nchildren)));
+          new_ret =
+              nm->mkNode(BITVECTOR_CONCAT,
+                         extract_flip,
+                         nm->mkNode(BITVECTOR_NEG,
+                                    nm->mkNode(BITVECTOR_CONCAT, nchildren)));
           debugExtendedRewrite(ret, new_ret, "NEG-msb-1");
           return new_ret;
         }
@@ -3223,134 +3234,141 @@ void ExtendedRewriter::spliceBv(Node a,
   }
 }
 
-
-int ExtendedRewriter::spliceBvConstBit(Node n1,
-            Node n2,
-            std::vector<Node>& nv)
+int ExtendedRewriter::spliceBvConstBit(Node n1, Node n2, std::vector<Node>& nv)
 {
-  if( n1==n2 )
+  if (n1 == n2)
   {
     return -1;
   }
-  Trace("q-ext-rewrite-debug") << "Splice constant bv bit " << n1 << " " << n2 << std::endl;
+  Trace("q-ext-rewrite-debug")
+      << "Splice constant bv bit " << n1 << " " << n2 << std::endl;
   // splice the children
-  std::vector< Node > rc1;
-  std::vector< Node > rc2;
-  spliceBv(n1,n2,rc1,rc2);
-  Assert( rc1.size()==rc2.size() );
+  std::vector<Node> rc1;
+  std::vector<Node> rc2;
+  spliceBv(n1, n2, rc1, rc2);
+  Assert(rc1.size() == rc2.size());
   int diff_index = -1;
-  for( unsigned r=0; r<rc1.size(); r++ )
+  for (unsigned r = 0; r < rc1.size(); r++)
   {
-    if( rc1[r]!=rc2[r] )
+    if (rc1[r] != rc2[r])
     {
-      if( diff_index>=0 )
+      if (diff_index >= 0)
       {
         // differ at more than one index
-        Trace("q-ext-rewrite-debug") << "...more than one diff component." << std::endl;
+        Trace("q-ext-rewrite-debug")
+            << "...more than one diff component." << std::endl;
         return -1;
       }
       diff_index = r;
     }
   }
-  Assert( diff_index>=0 );
-  if( !rc1[diff_index].isConst() || !rc2[diff_index].isConst() )
+  Assert(diff_index >= 0);
+  if (!rc1[diff_index].isConst() || !rc2[diff_index].isConst())
   {
-    Trace("q-ext-rewrite-debug") << "...non-constant diff components." << std::endl;
+    Trace("q-ext-rewrite-debug")
+        << "...non-constant diff components." << std::endl;
     return -1;
   }
   // insert prefix
-  if( diff_index>0 )
+  if (diff_index > 0)
   {
-    nv.insert(nv.end(),rc1.begin(),rc1.begin()+diff_index);
+    nv.insert(nv.end(), rc1.begin(), rc1.begin() + diff_index);
   }
-  Assert( rc1[diff_index]!=rc2[diff_index] );
+  Assert(rc1[diff_index] != rc2[diff_index]);
   Node c1 = rc1[diff_index];
   Node c2 = rc2[diff_index];
   // do they differ by exactly one bit?
   int bit_diff_index = -1;
   unsigned csize = bv::utils::getSize(c1);
-  for( unsigned i=0; i<csize; i++ )
+  for (unsigned i = 0; i < csize; i++)
   {
-    if( bv::utils::getBit(c1,i)!=bv::utils::getBit(c2,i) )
+    if (bv::utils::getBit(c1, i) != bv::utils::getBit(c2, i))
     {
-      if( bit_diff_index>=0 )
+      if (bit_diff_index >= 0)
       {
         // differ by more than one bit
         nv.clear();
-        Trace("q-ext-rewrite-debug") << "...more than one bit diff." << std::endl;
+        Trace("q-ext-rewrite-debug")
+            << "...more than one bit diff." << std::endl;
         return -1;
       }
       bit_diff_index = i;
     }
   }
-  if( bit_diff_index>=0 )
+  if (bit_diff_index >= 0)
   {
-    std::vector< Node > split;
-    if( bit_diff_index+1<static_cast<int>(csize) )
+    std::vector<Node> split;
+    if (bit_diff_index + 1 < static_cast<int>(csize))
     {
-      Node extract = bv::utils::mkExtract(c1, csize-1, bit_diff_index+1);
+      Node extract = bv::utils::mkExtract(c1, csize - 1, bit_diff_index + 1);
       nv.push_back(Rewriter::rewrite(extract));
     }
-    Node bit = bv::utils::getBit(c1,bit_diff_index) ? bv::utils::mkOnes(1) : bv::utils::mkZero(1);
+    Node bit = bv::utils::getBit(c1, bit_diff_index) ? bv::utils::mkOnes(1)
+                                                     : bv::utils::mkZero(1);
     diff_index = nv.size();
     nv.push_back(bit);
     // remainder
-    if( bit_diff_index>0 )
+    if (bit_diff_index > 0)
     {
-      Node extract = bv::utils::mkExtract(c1, bit_diff_index-1,0);
+      Node extract = bv::utils::mkExtract(c1, bit_diff_index - 1, 0);
       nv.push_back(Rewriter::rewrite(extract));
     }
     // insert suffix
-    if( diff_index<static_cast<int>(rc1.size()) )
+    if (diff_index < static_cast<int>(rc1.size()))
     {
-      nv.insert(nv.end(),rc1.begin()+diff_index+1,rc1.end());
+      nv.insert(nv.end(), rc1.begin() + diff_index + 1, rc1.end());
     }
     return diff_index;
   }
   return -1;
 }
 
-Node ExtendedRewriter::extendBv(Node n, std::vector< Node >& exs)
+Node ExtendedRewriter::extendBv(Node n, std::vector<Node>& exs)
 {
-  std::map< unsigned, Node > ex_map;
-  for( const Node& e : exs )
+  std::map<unsigned, Node> ex_map;
+  for (const Node& e : exs)
   {
     ex_map[bv::utils::getExtractHigh(e)] = e;
   }
-  return extendBv(n,ex_map);
+  return extendBv(n, ex_map);
 }
 
-Node ExtendedRewriter::extendBv(Node n, std::map< unsigned, Node >& ex_map)
+Node ExtendedRewriter::extendBv(Node n, std::map<unsigned, Node>& ex_map)
 {
   Trace("q-ext-rewrite-debug") << "extendBv " << n << std::endl;
-  std::vector< Node > children;
+  std::vector<Node> children;
   int counter = bv::utils::getSize(n) - 1;
-  for( const std::pair< const unsigned, Node >& ep : ex_map )
+  for (const std::pair<const unsigned, Node>& ep : ex_map)
   {
-    Trace("q-ext-rewrite-debug") << "  process " << ep.first << " : " << ep.second << ", counter=" << counter << std::endl;
+    Trace("q-ext-rewrite-debug")
+        << "  process " << ep.first << " : " << ep.second
+        << ", counter=" << counter << std::endl;
     unsigned start = ep.first;
-    Assert( static_cast<int>(start)<=counter );
-    if( static_cast<int>(start)<counter )
+    Assert(static_cast<int>(start) <= counter);
+    if (static_cast<int>(start) < counter)
     {
-      children.push_back( bv::utils::mkExtract(n, counter, start+1) );
+      children.push_back(bv::utils::mkExtract(n, counter, start + 1));
     }
     Node ex = ep.second;
-    children.push_back( ex );
+    children.push_back(ex);
     // update the counter
     unsigned esize = bv::utils::getSize(ex);
-    counter = start-esize;
-    Assert( counter+1>=0 );
+    counter = start - esize;
+    Assert(counter + 1 >= 0);
   }
-  if( counter>=0 )
+  if (counter >= 0)
   {
-    children.push_back( bv::utils::mkExtract(n, counter, 0) );
+    children.push_back(bv::utils::mkExtract(n, counter, 0));
   }
-  Trace("q-ext-rewrite-debug") << "extendBv finish, children = " << children << std::endl;
-  if( children.empty() )
+  Trace("q-ext-rewrite-debug")
+      << "extendBv finish, children = " << children << std::endl;
+  if (children.empty())
   {
     return n;
   }
-  return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( BITVECTOR_CONCAT, children );
+  return children.size() == 1
+             ? children[0]
+             : NodeManager::currentNM()->mkNode(BITVECTOR_CONCAT, children);
 }
 
 void ExtendedRewriter::debugExtendedRewrite(Node n,
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 00228e27c..7b523f0b8 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -309,15 +309,13 @@ class ExtendedRewriter
    *   n2 is equivalent to nv[0] ++ ... ++ (~)nv[i] ++ ... ++ nv[k-1], and
    *   nv[i] is a constant of bit-width one.
    */
-  int spliceBvConstBit(Node n1,
-                       Node n2,
-                       std::vector<Node>& nv);
+  int spliceBvConstBit(Node n1, Node n2, std::vector<Node>& nv);
   /** extend
-   * 
-   * This returns the concatentation node of the form 
+   *
+   * This returns the concatentation node of the form
    */
-  Node extendBv(Node n, std::map< unsigned, Node >& ex_map);
-  Node extendBv(Node n, std::vector< Node >& exs);
+  Node extendBv(Node n, std::map<unsigned, Node>& ex_map);
+  Node extendBv(Node n, std::vector<Node>& exs);
   //--------------------------------------end bit-vectors
 };
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index e3afd2c6e..81e8bbe26 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -105,7 +105,7 @@ void CegConjecture::assign( Node q ) {
   // we now finalize the single invocation module, based on the syntax restrictions
   if (d_qe->getQuantAttributes()->isSygus(q))
   {
-    d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted());
+    d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted());
   }
 
   Assert( d_candidates.empty() );
@@ -125,9 +125,9 @@ void CegConjecture::assign( Node q ) {
   if (options::sygusRepairConst())
   {
     d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates);
-    if( options::sygusConstRepairAbort() )
+    if (options::sygusConstRepairAbort())
     {
-      if( !d_sygus_rconst->isActive() )
+      if (!d_sygus_rconst->isActive())
       {
         // no constant repair is possible: abort
         std::stringstream ss;
@@ -693,7 +693,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
   Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() );
   std::vector<Node> sols;
   std::vector<int> statuses;
-  if( !getSynthSolutionsInternal(sols, statuses, singleInvocation) )
+  if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
   {
     return;
   }
@@ -761,7 +761,7 @@ void CegConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
   TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
   std::vector<Node> sols;
   std::vector<int> statuses;
-  if( !getSynthSolutionsInternal(sols, statuses, singleInvocation) )
+  if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
   {
     return;
   }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 9588757fa..9a6fad52a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -290,7 +290,8 @@ void CegConjectureSingleInv::initialize( Node q ) {
   }
 }
 
-void CegConjectureSingleInv::finishInit( bool syntaxRestricted ) {
+void CegConjectureSingleInv::finishInit(bool syntaxRestricted)
+{
   Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl;
   // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled
   if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && d_single_invocation && syntaxRestricted ){
@@ -570,11 +571,12 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   {
     d_sol->preregisterConjecture( d_orig_conjecture );
     int enumLimit = -1;
-    if( options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_TRY )
+    if (options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_TRY)
     {
       enumLimit = 0;
     }
-    else if( options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_ALL_LIMIT )
+    else if (options::cegqiSingleInvReconstruct()
+             == CEGQI_SI_RCONS_MODE_ALL_LIMIT)
     {
       enumLimit = options::cegqiSingleInvReconstructLimit();
     }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 0fa5c1204..b368a0689 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -189,12 +189,12 @@ class CegConjectureSingleInv {
   // initialize this class for synthesis conjecture q
   void initialize( Node q );
   /** finish initialize
-   * 
+   *
    * This method sets up final decisions about whether to use single invocation
-   * techniques. The argument syntaxRestricted is whether the syntax for 
+   * techniques. The argument syntaxRestricted is whether the syntax for
    * solutions for the initialized conjecture is restricted.
    */
-  void finishInit( bool syntaxRestricted );
+  void finishInit(bool syntaxRestricted);
   //check
   bool check( std::vector< Node >& lems );
   //get solution
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 695ef25c2..44835cc26 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -678,7 +678,7 @@ Node CegConjectureSingleInvSol::reconstructSolution(Node sol,
       Assert(!it->second.empty());
     }
   }
-  if (enumLimit!=0)
+  if (enumLimit != 0)
   {
     int index = 0;
     std::map< TypeNode, bool > active;
@@ -727,7 +727,7 @@ Node CegConjectureSingleInvSol::reconstructSolution(Node sol,
       if( index%100==0 ){
         Trace("csi-rcons-stats") << "Tried " << index << " for each type."  << std::endl;
       }
-    }while( !active.empty() && ( enumLimit<0 || index<enumLimit) );
+    } while (!active.empty() && (enumLimit < 0 || index < enumLimit));
   }
 
   // we ran out of elements, return null
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index 9059531d5..8d18611cf 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -72,7 +72,7 @@ private:
    * This method quickly tries to match sol to the grammar induced by stn. If
    * this fails, we use enumerative techniques to try to repair the solution.
    * The number of iterations for this enumeration is bounded by the argument
-   * enumLimit if it is positive, and unbounded otherwise. 
+   * enumLimit if it is positive, and unbounded otherwise.
    */
   Node reconstructSolution(Node sol,
                            TypeNode stn,
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 9f215f9d4..aeb947bc6 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -29,9 +29,10 @@ void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
 {
   d_conj.clear();
   // simple miniscope
-  if( ( conj.getKind()==AND || conj.getKind()==OR ) && res.isConst() && res.getConst<bool>()==(conj.getKind()==AND) )
+  if ((conj.getKind() == AND || conj.getKind() == OR) && res.isConst()
+      && res.getConst<bool>() == (conj.getKind() == AND))
   {
-    for( const Node& c : conj )
+    for (const Node& c : conj)
     {
       d_conj.push_back(c);
     }
@@ -53,14 +54,14 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
 {
   TNode tnvn = nvn;
   std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
-  for( const Node& c : d_conj )
+  for (const Node& c : d_conj)
   {
     Node conj_subs = c.substitute(d_var, tnvn, cache);
     Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs);
     Trace("sygus-cref-eval2-debug")
         << "  ...check unfolding : " << conj_subs_unfold << std::endl;
-    Trace("sygus-cref-eval2-debug") << "  ......from : " << conj_subs
-                                    << std::endl;
+    Trace("sygus-cref-eval2-debug")
+        << "  ......from : " << conj_subs << std::endl;
     if (conj_subs_unfold != d_result)
     {
       return false;
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index 09b40c2dd..d28a25a4a 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -116,7 +116,7 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest
 
  private:
   /** the formulas we are evaluating */
-  std::vector< Node > d_conj;
+  std::vector<Node> d_conj;
   /** the variable */
   TNode d_var;
   /** the result of the evaluation */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 3061c4035..2ab18eb59 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -411,10 +411,11 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
   if( !enums.empty() ){
     unsigned min_term_size = 0;
     Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
-    std::vector< unsigned > szs;
-    for( unsigned i=0, esize = enums.size(); i<esize; i++ ){
+    std::vector<unsigned> szs;
+    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
+    {
       Trace("sygus-pbe-enum") << "  " << enums[i] << " -> ";
-      TermDbSygus::toStreamSygus("sygus-pbe-enum",enum_values[i]);
+      TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
       Trace("sygus-pbe-enum") << std::endl;
       unsigned sz = d_tds->getSygusTermSize( enum_values[i] );
       szs.push_back(sz);
@@ -423,14 +424,15 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
       }
     }
     unsigned allowDiff = options::sygusUnifPbeMultiFair() ? 0 : 1;
-    std::vector< unsigned > enum_consider;
-    for( unsigned i=0, esize = enums.size(); i<esize; i++ ){
-      if( szs[i]-min_term_size<=allowDiff )
+    std::vector<unsigned> enum_consider;
+    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
+    {
+      if (szs[i] - min_term_size <= allowDiff)
       {
         enum_consider.push_back( i );
       }
     }
-    
+
     // only consider the enumerators that are at minimum size (for fairness)
     Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
     NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index 9b1089a71..3e45f9210 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -77,7 +77,7 @@ class SygusRepairConst
                       const std::vector<Node>& candidate_values,
                       std::vector<Node>& repair_cv,
                       bool useConstantsAsHoles = false);
-  /** 
+  /**
    * Return whether this module has the possibility to repair solutions. This is
    * true if this module has been initialized, and at least one candidate has
    * an "any constant" constructor.
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 8436dd1b4..ef805c844 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -14,11 +14,11 @@
 
 #include "theory/quantifiers/sygus/sygus_unif_io.h"
 
-#include "theory/datatypes/datatypes_rewriter.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/evaluator.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/evaluator.h"
 #include "util/random.h"
 
 using namespace CVC4::kind;
@@ -520,34 +520,34 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
     base_results.push_back(res);
   }
   // get the results for each slave enumerator
-  std::map<Node, std::vector< Node > > srmap;
+  std::map<Node, std::vector<Node>> srmap;
   Evaluator* ev = d_tds->getEvaluator();
   bool tryEval = options::sygusEvalOpt();
-  for( const Node& xs : ei.d_enum_slave )
+  for (const Node& xs : ei.d_enum_slave)
   {
-    Assert( srmap.find(xs)==srmap.end());
+    Assert(srmap.find(xs) == srmap.end());
     EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
     Node templ = eiv.d_template;
-    if( !templ.isNull() )
+    if (!templ.isNull())
     {
       TNode templ_var = eiv.d_template_arg;
-      std::vector< Node > args;
+      std::vector<Node> args;
       args.push_back(templ_var);
-      std::vector< Node > sresults;
-      for( const Node& res : base_results )
+      std::vector<Node> sresults;
+      for (const Node& res : base_results)
       {
         TNode tres = res;
-        std::vector< Node > vals;
+        std::vector<Node> vals;
         vals.push_back(tres);
         Node sres;
         if (tryEval)
         {
           sres = ev->eval(templ, args, vals);
         }
-        if( sres.isNull() )
+        if (sres.isNull())
         {
           // fall back on rewriter
-          sres = templ.substitute(templ_var,tres);
+          sres = templ.substitute(templ_var, tres);
           sres = Rewriter::rewrite(sres);
         }
         sresults.push_back(sres);
@@ -559,11 +559,11 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
       srmap[xs] = base_results;
     }
   }
-  
-  
+
   // is it excluded for domain-specific reason?
   std::vector<Node> exp_exc_vec;
-  if (getExplanationForEnumeratorExclude(e, v, base_results, srmap, true, exp_exc_vec))
+  if (getExplanationForEnumeratorExclude(
+          e, v, base_results, srmap, true, exp_exc_vec))
   {
     Assert(!exp_exc_vec.empty());
     exp_exc = exp_exc_vec.size() == 1
@@ -597,9 +597,9 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
       // evaluate all input/output examples
       std::vector<Node> results;
       std::map<Node, bool> cond_vals;
-      std::map<Node, std::vector< Node > >::iterator itsr = srmap.find(xs);
-      Assert( itsr!=srmap.end());
-      for (unsigned j=0, size=itsr->second.size(); j<size; j++ )
+      std::map<Node, std::vector<Node>>::iterator itsr = srmap.find(xs);
+      Assert(itsr != srmap.end());
+      for (unsigned j = 0, size = itsr->second.size(); j < size; j++)
       {
         Node res = itsr->second[j];
         Assert(res.isConst());
@@ -712,7 +712,8 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   if (exp_exc.isNull())
   {
     std::vector<Node> exp_exc_vec;
-    if (getExplanationForEnumeratorExclude(e, v, base_results, srmap, false, exp_exc_vec))
+    if (getExplanationForEnumeratorExclude(
+            e, v, base_results, srmap, false, exp_exc_vec))
     {
       Assert(!exp_exc_vec.empty());
       exp_exc = exp_exc_vec.size() == 1
@@ -772,9 +773,9 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
       // if we constructed the solution, and we either did not previously have
       // a solution, or the new solution is better (smaller).
       if (!vcc.isNull()
-          && (d_solution.isNull() || (!d_solution.isNull()
-                              && d_tds->getSygusTermSize(vcc)
-                                     < sol_term_size)))
+          && (d_solution.isNull()
+              || (!d_solution.isNull()
+                  && d_tds->getSygusTermSize(vcc) < sol_term_size)))
       {
         Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
                            << std::endl;
@@ -839,19 +840,17 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
   return false;
 }
 
-Node SygusUnifIo::getExclusionInvariancePredicate(Node e, Node v,
-                                                  std::map< Node, std::vector< Node > >& srmap,
-                                                     bool prereg
-                                                 )
+Node SygusUnifIo::getExclusionInvariancePredicate(
+    Node e, Node v, std::map<Node, std::vector<Node>>& srmap, bool prereg)
 {
-  if( prereg )
+  if (prereg)
   {
     return Node::null();
   }
   Node c = d_candidate;
-  std::vector< Node > conj;
+  std::vector<Node> conj;
   NodeManager* nm = NodeManager::currentNM();
-  //if (useStrContainsEnumeratorExclude(e))
+  // if (useStrContainsEnumeratorExclude(e))
   //{
   //}
   bool invariant_eval_role = true;
@@ -860,13 +859,13 @@ Node SygusUnifIo::getExclusionInvariancePredicate(Node e, Node v,
   {
     EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
     EnumRole er = eis.getRole();
-    if( er!=enum_io && er!=enum_ite_condition )
+    if (er != enum_io && er != enum_ite_condition)
     {
       invariant_eval_role = false;
       break;
     }
   }
-  if( invariant_eval_role )
+  if (invariant_eval_role)
   {
     for (const Node& sn : ei.d_enum_slave)
     {
@@ -875,53 +874,56 @@ Node SygusUnifIo::getExclusionInvariancePredicate(Node e, Node v,
       Node templ = eis.d_template;
       TNode templ_var = eis.d_template_arg;
       // get the results
-      std::vector< Node >& sresults = srmap[sn];
-      Assert( d_examples_out.size()==sresults.size() );
+      std::vector<Node>& sresults = srmap[sn];
+      Assert(d_examples_out.size() == sresults.size());
 
-      for( unsigned j=0, size = sresults.size(); j<size; j++ )
+      for (unsigned j = 0, size = sresults.size(); j < size; j++)
       {
-        std::vector< Node > echildren;
+        std::vector<Node> echildren;
         echildren.push_back(e);
-        echildren.insert(echildren.end(),d_examples[j].begin(),d_examples[j].end());
-        Node dte = nm->mkNode( DT_SYGUS_EVAL, echildren );
-        if( !templ.isNull() )
+        echildren.insert(
+            echildren.end(), d_examples[j].begin(), d_examples[j].end());
+        Node dte = nm->mkNode(DT_SYGUS_EVAL, echildren);
+        if (!templ.isNull())
         {
-          dte = templ.substitute(templ_var,dte);
+          dte = templ.substitute(templ_var, dte);
         }
-        Assert( sresults[j].isConst() );
-        if( er==enum_io )
+        Assert(sresults[j].isConst());
+        if (er == enum_io)
         {
           // it is being used as i/o, we must maintain the false examples
-          if( sresults[j]!=d_examples_out[j] )
+          if (sresults[j] != d_examples_out[j])
           {
             conj.push_back(dte.eqNode(d_examples_out[j]).negate());
           }
         }
-        else if( er==enum_ite_condition )
+        else if (er == enum_ite_condition)
         {
           // must remain the same evaluation
-          Assert( dte.getType().isBoolean() );
-          conj.push_back( sresults[j].getConst<bool>() ? dte : dte.negate() );
+          Assert(dte.getType().isBoolean());
+          conj.push_back(sresults[j].getConst<bool>() ? dte : dte.negate());
         }
       }
     }
   }
-  if( !conj.empty() )
+  if (!conj.empty())
   {
-    Node eip = conj.size()==1 ? conj[0] : nm->mkNode( AND, conj );
-    Trace("sygus-io-eip") << "Exclusion invariance predicate for " << v << " is : " << eip << std::endl;
+    Node eip = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
+    Trace("sygus-io-eip") << "Exclusion invariance predicate for " << v
+                          << " is : " << eip << std::endl;
     return eip;
   }
-  
-  return Node::null(); 
+
+  return Node::null();
 }
 
-bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e,
-                                                     Node v,
-                                                     std::vector<Node>& results,
-                                                     std::map< Node, std::vector< Node > >& srmap,
-                                                     bool prereg,
-                                                     std::vector<Node>& exp)
+bool SygusUnifIo::getExplanationForEnumeratorExclude(
+    Node e,
+    Node v,
+    std::vector<Node>& results,
+    std::map<Node, std::vector<Node>>& srmap,
+    bool prereg,
+    std::vector<Node>& exp)
 {
   NodeManager* nm = NodeManager::currentNM();
   if (prereg && useStrContainsEnumeratorExclude(e))
@@ -971,20 +973,20 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e,
       return true;
     }
   }
-  if( options::sygusExcInvPred() )
+  if (options::sygusExcInvPred())
   {
-    Node pred = getExclusionInvariancePredicate(e,v, srmap, prereg);
-    if( !pred.isNull() )
+    Node pred = getExclusionInvariancePredicate(e, v, srmap, prereg);
+    if (!pred.isNull())
     {
       EvalSygusInvarianceTest esit;
-      esit.init(pred,e,nm->mkConst(true));
+      esit.init(pred, e, nm->mkConst(true));
       // construct the generalized explanation
       d_tds->getExplain()->getExplanationFor(e, v, exp, esit);
-      std::vector< Node > triv_exp;
+      std::vector<Node> triv_exp;
       d_tds->getExplain()->getExplanationForEquality(e, v, triv_exp);
-        Trace("sygus-io-eip2")
-            << "Generalized explanation of " << d_tds->sygusToBuiltin(v)
-            << ": " << exp.size() << "/" << triv_exp.size() << std::endl;
+      Trace("sygus-io-eip2")
+          << "Generalized explanation of " << d_tds->sygusToBuiltin(v) << ": "
+          << exp.size() << "/" << triv_exp.size() << std::endl;
       return true;
     }
   }
@@ -1155,7 +1157,7 @@ Node SygusUnifIo::constructSol(
         Assert(incr.find(val_t) == incr.end());
         indent("sygus-sui-dt-debug", ind);
         Trace("sygus-sui-dt-debug") << "increment string values : ";
-        TermDbSygus::toStreamSygus("sygus-sui-dt-debug",val_t);
+        TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t);
         Trace("sygus-sui-dt-debug") << " : ";
         Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
         unsigned tot = 0;
@@ -1210,21 +1212,22 @@ Node SygusUnifIo::constructSol(
           << std::endl;
     }
   }
-  if (!ret_dt.isNull() || einfo.isTemplated() )
+  if (!ret_dt.isNull() || einfo.isTemplated())
   {
     Assert(ret_dt.isNull() || ret_dt.getType() == e.getType());
     indent("sygus-sui-dt", ind);
-    Trace("sygus-sui-dt") << "ConstructPBE: returned (pre-strategy) " << ret_dt << std::endl;
+    Trace("sygus-sui-dt") << "ConstructPBE: returned (pre-strategy) " << ret_dt
+                          << std::endl;
     return ret_dt;
   }
   // we will try a single strategy
   EnumTypeInfoStrat* etis = nullptr;
-  std::map<NodeRole, StrategyNode>::iterator itsn =
-      tinfo.d_snodes.find(nrole);
+  std::map<NodeRole, StrategyNode>::iterator itsn = tinfo.d_snodes.find(nrole);
   if (itsn == tinfo.d_snodes.end())
   {
     indent("sygus-sui-dt", ind);
-    Trace("sygus-sui-dt") << "ConstructPBE: returned (no-strategy) " << ret_dt << std::endl;
+    Trace("sygus-sui-dt") << "ConstructPBE: returned (no-strategy) " << ret_dt
+                          << std::endl;
     return ret_dt;
   }
   // strategy info
@@ -1234,7 +1237,8 @@ Node SygusUnifIo::constructSol(
     // already visited and context not changed (notice d_visit_role is cleared
     // when the context changes).
     indent("sygus-sui-dt", ind);
-    Trace("sygus-sui-dt") << "ConstructPBE: returned (already visited) " << ret_dt << std::endl;
+    Trace("sygus-sui-dt") << "ConstructPBE: returned (already visited) "
+                          << ret_dt << std::endl;
     return ret_dt;
   }
   x.d_visit_role[e][nrole] = true;
@@ -1247,27 +1251,27 @@ Node SygusUnifIo::constructSol(
   // the reasoning is that splitting on conditions only subdivides the problem
   // and cannot be the source of failure, whereas the wrong choice for a
   // concatenation term may lead to failure
-  if( d_solution.isNull() )
+  if (d_solution.isNull())
   {
-    for( unsigned i=0; i<snode.d_strats.size(); i++ )
+    for (unsigned i = 0; i < snode.d_strats.size(); i++)
     {
-      if( snode.d_strats[i]->d_this==strat_ITE )
+      if (snode.d_strats[i]->d_this == strat_ITE)
       {
         // flip the two
-        EnumTypeInfoStrat * etis = snode.d_strats[i];
+        EnumTypeInfoStrat* etis = snode.d_strats[i];
         snode.d_strats[i] = snode.d_strats[0];
         snode.d_strats[0] = etis;
         break;
       }
     }
   }
-  
+
   // iterate over the strategies
   unsigned sindex = 0;
   bool did_recurse = false;
   while (ret_dt.isNull() && !did_recurse && sindex < snode.d_strats.size())
   {
-    if( snode.d_strats[sindex]->isValid(x) )
+    if (snode.d_strats[sindex]->isValid(x))
     {
       etis = snode.d_strats[sindex];
       Assert(etis != nullptr);
@@ -1311,7 +1315,7 @@ Node SygusUnifIo::constructSol(
             EnumCache& ecache_cond = d_ecache[split_cond_enum];
             Assert(split_cond_res_index >= 0);
             Assert(split_cond_res_index
-                    < (int)ecache_cond.d_enum_vals_res.size());
+                   < (int)ecache_cond.d_enum_vals_res.size());
             prev = x.d_vals;
             bool ret = x.updateContext(
                 this,
@@ -1335,10 +1339,10 @@ Node SygusUnifIo::constructSol(
                 x.d_uinfo[ce].clear();
                 Trace("sygus-sui-dt-debug2")
                     << "  reg : PBE: Look for direct solutions for conditional "
-                        "enumerator "
+                       "enumerator "
                     << ce << " ... " << std::endl;
                 Assert(ecache_child.d_enum_vals.size()
-                        == ecache_child.d_enum_vals_res.size());
+                       == ecache_child.d_enum_vals_res.size());
                 for (unsigned i = 1; i <= 2; i++)
                 {
                   std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
@@ -1348,8 +1352,8 @@ Node SygusUnifIo::constructSol(
                   // for each condition, get terms that satisfy it in this
                   // branch
                   for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
-                        k < size;
-                        k++)
+                       k < size;
+                       k++)
                   {
                     Node cond = ecache_child.d_enum_vals[k];
                     std::vector<Node> solved;
@@ -1458,18 +1462,18 @@ Node SygusUnifIo::constructSol(
               // types?
               indent("sygus-sui-dt", ind);
               Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
-                                        "cannot find a distinguishable condition"
+                                       "cannot find a distinguishable condition"
                                     << std::endl;
             }
             if (!rec_c.isNull())
             {
               Assert(ecache_child.d_enum_val_to_index.find(rec_c)
-                      != ecache_child.d_enum_val_to_index.end());
+                     != ecache_child.d_enum_val_to_index.end());
               split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
               split_cond_enum = ce;
               Assert(split_cond_res_index >= 0);
               Assert(split_cond_res_index
-                      < (int)ecache_child.d_enum_vals_res.size());
+                     < (int)ecache_child.d_enum_vals_res.size());
             }
           }
           else
@@ -1501,9 +1505,9 @@ Node SygusUnifIo::constructSol(
         // dt_children );
         ret_dt = etis->d_sol_templ;
         ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
-                                    etis->d_sol_templ_args.end(),
-                                    dt_children_cons.begin(),
-                                    dt_children_cons.end());
+                                   etis->d_sol_templ_args.end(),
+                                   dt_children_cons.begin(),
+                                   dt_children_cons.end());
         indent("sygus-sui-dt-debug", ind);
         Trace("sygus-sui-dt-debug")
             << "PBE: success : constructed for strategy " << strat << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index a499ba284..35306de01 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -415,15 +415,17 @@ class SygusUnifIo : public SygusUnif
    * exp : if this function returns true, then exp contains a (possibly
    * generalize) explanation for why v can be excluded.
    */
-  bool getExplanationForEnumeratorExclude(Node e,
-                                          Node v,
-                                          std::vector<Node>& results,
-                                                     std::map< Node, std::vector< Node > >& srmap,
-                                                     bool prereg,
-                                          std::vector<Node>& exp);
-  Node getExclusionInvariancePredicate(Node e, Node v,
-                                       std::map< Node, std::vector< Node > >& srmap,
-                                                     bool prereg);
+  bool getExplanationForEnumeratorExclude(
+      Node e,
+      Node v,
+      std::vector<Node>& results,
+      std::map<Node, std::vector<Node>>& srmap,
+      bool prereg,
+      std::vector<Node>& exp);
+  Node getExclusionInvariancePredicate(Node e,
+                                       Node v,
+                                       std::map<Node, std::vector<Node>>& srmap,
+                                       bool prereg);
   /** returns true if we can exlude values of e based on negative str.contains
    *
    * Values v for e may be excluded if we realize that the value of v under the
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 0f14eebac..883aae070 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -758,7 +758,7 @@ bool SygusUnifStrategy::isTrivial()
   TypeNode etn = root_e.getType();
   EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
   StrategyNode& snode = tinfo.getStrategyNode(role_equal);
-  if( snode.d_strats.empty() )
+  if (snode.d_strats.empty())
   {
     return true;
   }
@@ -768,8 +768,8 @@ bool SygusUnifStrategy::isTrivial()
 bool SygusUnifStrategy::isNonDeterministic()
 {
   std::map<Node, std::map<NodeRole, bool>> visited;
-  std::vector< Node > visit;
-  std::vector< NodeRole > visit_role;
+  std::vector<Node> visit;
+  std::vector<NodeRole> visit_role;
   visit.push_back(getRootEnumerator());
   visit_role.push_back(role_equal);
   Node e;
@@ -790,18 +790,18 @@ bool SygusUnifStrategy::isNonDeterministic()
       {
         EnumTypeInfoStrat* etis = snode.d_strats[j];
         StrategyType strat = etis->d_this;
-        if( strat==strat_CONCAT_PREFIX || strat==strat_CONCAT_SUFFIX )
+        if (strat == strat_CONCAT_PREFIX || strat == strat_CONCAT_SUFFIX)
         {
           return true;
         }
         for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
         {
-          visit.push_back( cec.first );
-          visit_role.push_back( cec.second );
+          visit.push_back(cec.first);
+          visit_role.push_back(cec.second);
         }
       }
     }
-  }while( !visit.empty() );
+  } while (!visit.empty());
   return false;
 }
 
@@ -838,7 +838,7 @@ TypeNode SygusUnifStrategy::getStrategyType()
       TypeNode etn = e.getType();
       EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
       StrategyNode& snode = tinfo.getStrategyNode(erole);
-      
+
       // process=1 --> building a sygus datatype
       std::stringstream dname;
       dname << "strategy_" << e << "_" << erole;
@@ -855,7 +855,7 @@ TypeNode SygusUnifStrategy::getStrategyType()
           NodeRole cnr = cec.second;
           if( process==1 )
           {
-            // get the child sygus datatype 
+            // get the child sygus datatype
             Assert( visitedt[cn].find(cnr)!=visitedt[cn].end());
             TypeNode childt = visitedt[cn][cnr];
             childArgTypes.push_back(childt.toType());
@@ -874,7 +874,7 @@ TypeNode SygusUnifStrategy::getStrategyType()
       }
     }
   }while( !visit.empty() );
-  
+
   return visited[root_e][role_equal];
 }
 */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index eea0be944..930ccd65f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -326,11 +326,11 @@ class SygusUnifStrategy
   bool isTrivial();
   /** is non-deterministic? */
   bool isNonDeterministic();
-  /** get strategy type 
-   * 
+  /** get strategy type
+   *
    * TODO: build type that summarizes shapes?
    */
-  //TypeNode getStrategyType();
+  // TypeNode getStrategyType();
 
   /** debug print this strategy on Trace c */
   void debugPrint(const char* c);
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 4c1dcc39a..a6b2b617c 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -15,15 +15,15 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 #include "base/cvc4_check.h"
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "printer/printer.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "options/base_options.h"
-#include "printer/printer.h"
 
 using namespace CVC4::kind;
 
@@ -362,11 +362,13 @@ public:
     if( d_req_kind!=UNDEFINED_KIND ){
       Trace("sygus-sb-debug") << "- check if " << tn << " has " << d_req_kind
                               << std::endl;
-      std::vector< TypeNode > argts;
-      if( tdb->canConstructKind(tn, d_req_kind, argts ) ){
+      std::vector<TypeNode> argts;
+      if (tdb->canConstructKind(tn, d_req_kind, argts))
+      {
         bool ret = true;
         for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
-          if( it->first<argts.size() ){
+          if (it->first < argts.size())
+          {
             TypeNode tnc = argts[it->first];
             if( !it->second.satisfiedBy( tdb, tnc ) ){
               return false;
@@ -1037,9 +1039,9 @@ TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
   return d_register[tn];
 }
 
-void TermDbSygus::toStreamSygus( const char * c, Node n )
+void TermDbSygus::toStreamSygus(const char* c, Node n)
 {
-  if( Trace.isOn(c) )
+  if (Trace.isOn(c))
   {
     std::stringstream ss;
     Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n);
@@ -1315,65 +1317,74 @@ bool TermDbSygus::isSymbolicConsApp(Node n) const
   return sygusOp.getAttribute(SygusAnyConstAttribute());
 }
 
-bool TermDbSygus::canConstructKind( TypeNode tn, Kind k, std::vector< TypeNode >& argts, bool aggr )
+bool TermDbSygus::canConstructKind(TypeNode tn,
+                                   Kind k,
+                                   std::vector<TypeNode>& argts,
+                                   bool aggr)
 {
-  int c = getKindConsNum( tn, k );
+  int c = getKindConsNum(tn, k);
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  if( c!=-1 )
+  if (c != -1)
   {
-    for( unsigned i=0, nargs=dt[c].getNumArgs(); i<nargs; i++ )
+    for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
     {
       argts.push_back(TypeNode::fromType(dt[c].getArgType(i)));
     }
     return true;
   }
-  if( !options::sygusSymBreakAgg() )
+  if (!options::sygusSymBreakAgg())
   {
     return false;
   }
   if (sygusToBuiltinType(tn).isBoolean())
   {
-    if( k==ITE )
+    if (k == ITE)
     {
       // ite( b1, b2, b3 ) <---- and( or( ~b1, b2 ), or( b1, b3 ) )
-      std::vector< TypeNode > conj_types;
-      if( canConstructKind( tn, AND, conj_types, true ) && conj_types.size()==2 )
+      std::vector<TypeNode> conj_types;
+      if (canConstructKind(tn, AND, conj_types, true) && conj_types.size() == 2)
       {
         bool success = true;
-        std::vector< TypeNode > disj_types[2];
-        for( unsigned c=0; c<2; c++ )
+        std::vector<TypeNode> disj_types[2];
+        for (unsigned c = 0; c < 2; c++)
         {
-          if( !canConstructKind( conj_types[c], OR, disj_types[c], true ) || disj_types[c].size()!=2 )
+          if (!canConstructKind(conj_types[c], OR, disj_types[c], true)
+              || disj_types[c].size() != 2)
           {
             success = false;
             break;
           }
         }
-        if( success )
+        if (success)
         {
-          for( unsigned r=0; r<2; r++ )
+          for (unsigned r = 0; r < 2; r++)
           {
-            for( unsigned d=0, size=disj_types[r].size(); d<size; d++ )
+            for (unsigned d = 0, size = disj_types[r].size(); d < size; d++)
             {
               TypeNode dtn = disj_types[r][d];
               // must have negation that occurs in the other conjunct
-              std::vector< TypeNode > ntypes;
-              if( canConstructKind( dtn, NOT, ntypes ) && ntypes.size()==1 )
+              std::vector<TypeNode> ntypes;
+              if (canConstructKind(dtn, NOT, ntypes) && ntypes.size() == 1)
               {
                 TypeNode ntn = ntypes[0];
-                for( unsigned dd=0, size=disj_types[1-r].size(); dd<size; dd++ )
+                for (unsigned dd = 0, size = disj_types[1 - r].size();
+                     dd < size;
+                     dd++)
                 {
-                  if( disj_types[1-r][dd]==ntn )
+                  if (disj_types[1 - r][dd] == ntn)
                   {
                     argts.push_back(ntn);
                     argts.push_back(disj_types[r][d]);
-                    argts.push_back(disj_types[1-r][1-dd]);
-                    if( Trace.isOn("sygus-cons-kind") )
+                    argts.push_back(disj_types[1 - r][1 - dd]);
+                    if (Trace.isOn("sygus-cons-kind"))
                     {
-                      Trace("sygus-cons-kind") << "Can construct kind " << k << " in " << tn << " via child types:" << std::endl;
-                      for( unsigned i=0; i<3; i++ )
+                      Trace("sygus-cons-kind")
+                          << "Can construct kind " << k << " in " << tn
+                          << " via child types:" << std::endl;
+                      for (unsigned i = 0; i < 3; i++)
                       {
-                        Trace("sygus-cons-kind") << "  " << argts[i] << std::endl;
+                        Trace("sygus-cons-kind")
+                            << "  " << argts[i] << std::endl;
                       }
                     }
                     return true;
@@ -1398,7 +1409,7 @@ bool TermDbSygus::canConstructKind( TypeNode tn, Kind k, std::vector< TypeNode >
         // (and b1 b2) <---- (not (or (not b1) (not b2)))
         // (or b1 b2)  <---- (not (and (not b1) (not b2)))
         std::vector< Node > ctypes;
-        
+
       }
     }
   }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index efb7d162e..5b528e7ed 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -230,9 +230,10 @@ class TermDbSygus {
    */
   TypeNode sygusToBuiltinType(TypeNode tn);
   //-----------------------------end conversion from sygus to builtin
-  
+
   /** print to sygus stream n on trace c */
-  static void toStreamSygus( const char * c, Node n );
+  static void toStreamSygus(const char* c, Node n);
+
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -393,24 +394,27 @@ class TermDbSygus {
   bool hasSubtermSymbolicCons(TypeNode tn) const;
   /** return whether n is an application of a symbolic constructor */
   bool isSymbolicConsApp(Node n) const;
-  /** can construct kind 
-   * 
+  /** can construct kind
+   *
    * Given a sygus datatype type tn, if this method returns true, then there
    * exists values of tn whose builtin analog is equivalent to
    * <k>( t1, ..., tn ). The sygus types of t1...tn are added to arg_types.
-   * 
+   *
    * For example, if:
    *   A -> A+A | ite( B, A, A ) | x | 1 | 0
    *   B -> and( B, B ) | not( B ) | or( B, B ) | A = A
    * - canConstructKind( A, +, ... ) returns true and adds {A,A} to arg_types,
    * - canConstructKind( B, not, ... ) returns true and adds { B } to arg types.
-   * 
+   *
    * We also may infer that operator is constructable. For example,
    * - canConstructKind( B, ite, ... ) may return true, adding { B, B, B } to
-   * arg_types, noting that the term 
+   * arg_types, noting that the term
    *   (and (or (not b1) b2) (or b1 b3)) is equivalent to (ite b1 b2 b3)
    */
-  bool canConstructKind( TypeNode tn, Kind k, std::vector< TypeNode >& argts, bool aggr = false );
+  bool canConstructKind(TypeNode tn,
+                        Kind k,
+                        std::vector<TypeNode>& argts,
+                        bool aggr = false);
 
   TypeNode getSygusTypeForVar( Node v );
   Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f0fc939a1..eecd87261 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1166,13 +1166,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         }
         retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
       }
-    }else if( node[0].getKind()==STRING_STRREPL ){
+    }
+    else if (node[0].getKind() == STRING_STRREPL)
+    {
       Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
       Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
-      if( len1==len2 )
+      if (len1 == len2)
       {
         // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x )
-        retNode = nm->mkNode( STRING_LENGTH, node[0][0] );
+        retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
       }
     }
   }else if( node.getKind() == kind::STRING_CHARAT ){
@@ -2156,19 +2158,19 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       return returnRewrite(node, ret, "rpl-const-find");
     }
   }
-  
-  if( node[0].isConst() )
+
+  if (node[0].isConst())
   {
     // str.replace( "", x, t ) ---> str.replace( "", x, t{x->""} )
     CVC4::String s = node[0].getConst<String>();
-    if( s.empty() )
+    if (s.empty())
     {
       TNode v = node[1];
       TNode s = node[0];
-      Node sn2 = node[2].substitute(v,s);
-      if( sn2!=node[2] )
+      Node sn2 = node[2].substitute(v, s);
+      if (sn2 != node[2])
       {
-        Node ret = nm->mkNode( STRING_STRREPL, node[0], node[1], sn2 );
+        Node ret = nm->mkNode(STRING_STRREPL, node[0], node[1], sn2);
         return returnRewrite(node, ret, "repl-empty-subs");
       }
     }
@@ -2301,19 +2303,19 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       return returnRewrite(node, res, "repl-subst-idx");
     }
   }
-  if( node[1].getKind()==STRING_STRREPL )
+  if (node[1].getKind() == STRING_STRREPL)
   {
-    if( node[1][0]==node[0] )
+    if (node[1][0] == node[0])
     {
-      if( node[1][0]==node[1][2] && node[1][0]==node[2] )
+      if (node[1][0] == node[1][2] && node[1][0] == node[2])
       {
         // str.replace( x, str.replace( x, y, x ), x ) ---> x
         return returnRewrite(node, node[0], "repl-repl2-inv-id");
       }
       bool dualReplIteSuccess = false;
       Node cmp_con = nm->mkNode(STRING_STRCTN, node[1][0], node[1][2]);
-      cmp_con = Rewriter::rewrite( cmp_con );
-      if( cmp_con.isConst() && !cmp_con.getConst<bool>() )
+      cmp_con = Rewriter::rewrite(cmp_con);
+      if (cmp_con.isConst() && !cmp_con.getConst<bool>())
       {
         // str.contains( x, z ) ---> false
         //   implies
@@ -2328,39 +2330,42 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
         // str.replace( x, str.replace( x, y, z ), w ) --->
         // ite( str.contains( x, y ), x, w )
         cmp_con = nm->mkNode(STRING_STRCTN, node[1][1], node[1][2]);
-        cmp_con = Rewriter::rewrite( cmp_con );
-        if( cmp_con.isConst() && !cmp_con.getConst<bool>() )
+        cmp_con = Rewriter::rewrite(cmp_con);
+        if (cmp_con.isConst() && !cmp_con.getConst<bool>())
         {
           cmp_con = nm->mkNode(STRING_STRCTN, node[1][2], node[1][1]);
-          cmp_con = Rewriter::rewrite( cmp_con );
-          if( cmp_con.isConst() && !cmp_con.getConst<bool>() )
+          cmp_con = Rewriter::rewrite(cmp_con);
+          if (cmp_con.isConst() && !cmp_con.getConst<bool>())
           {
             dualReplIteSuccess = true;
           }
         }
       }
-      if( dualReplIteSuccess )
+      if (dualReplIteSuccess)
       {
-        Node res = nm->mkNode( ITE, nm->mkNode(STRING_STRCTN,node[0],node[1][1]), node[0], node[2] );
+        Node res = nm->mkNode(ITE,
+                              nm->mkNode(STRING_STRCTN, node[0], node[1][1]),
+                              node[0],
+                              node[2]);
         return returnRewrite(node, res, "repl-dual-repl-ite");
       }
     }
-    
+
     bool invSuccess = false;
-    if( node[1][1]==node[0] )
+    if (node[1][1] == node[0])
     {
-      if( node[1][0]==node[1][2] )
+      if (node[1][0] == node[1][2])
       {
         // str.replace(x, str.replace(y, x, y), w) ---> str.replace(x, y, w)
         invSuccess = true;
       }
-      else if( node[1][1]==node[2] || node[1][0]==node[2] )
+      else if (node[1][1] == node[2] || node[1][0] == node[2])
       {
         // str.contains(y, z) ----> false and ( y == w or x == w ) implies
         //   implies
         // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w)
         Node cmp_con = nm->mkNode(STRING_STRCTN, node[1][0], node[1][2]);
-        cmp_con = Rewriter::rewrite( cmp_con );
+        cmp_con = Rewriter::rewrite(cmp_con);
         invSuccess = cmp_con.isConst() && !cmp_con.getConst<bool>();
       }
     }
@@ -2370,45 +2375,39 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       //   implies
       // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u)
       Node cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[1][1]);
-      cmp_con = Rewriter::rewrite( cmp_con );
-      if( cmp_con.isConst() && !cmp_con.getConst<bool>() )
+      cmp_con = Rewriter::rewrite(cmp_con);
+      if (cmp_con.isConst() && !cmp_con.getConst<bool>())
       {
         cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[1][2]);
-        cmp_con = Rewriter::rewrite( cmp_con );
+        cmp_con = Rewriter::rewrite(cmp_con);
         invSuccess = cmp_con.isConst() && !cmp_con.getConst<bool>();
       }
     }
-    if( invSuccess )
+    if (invSuccess)
     {
-      Node res = nm->mkNode(kind::STRING_STRREPL,
-                            node[0],
-                            node[1][0],
-                            node[2]);
+      Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1][0], node[2]);
       return returnRewrite(node, res, "repl-repl2-inv");
     }
-
   }
-  if( node[2].getKind()==STRING_STRREPL )
+  if (node[2].getKind() == STRING_STRREPL)
   {
-    if( node[2][1]==node[0] )
+    if (node[2][1] == node[0])
     {
       // str.contains( z, w ) ----> false implies
       // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z )
       Node cmp_con = nm->mkNode(STRING_STRCTN, node[1], node[2][0]);
-      cmp_con = Rewriter::rewrite( cmp_con );
+      cmp_con = Rewriter::rewrite(cmp_con);
       if (cmp_con.isConst() && !cmp_con.getConst<bool>())
       {
-        Node res = nm->mkNode(kind::STRING_STRREPL,
-                              node[0],
-                              node[1],
-                              node[2][0]);
+        Node res =
+            nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]);
         return returnRewrite(node, res, "repl-repl3-inv");
       }
     }
-    if( node[2][0]==node[1] )
+    if (node[2][0] == node[1])
     {
       bool success = false;
-      if( node[2][0]==node[2][2] && node[2][1]==node[0] )
+      if (node[2][0] == node[2][2] && node[2][1] == node[0])
       {
         // str.replace( x, y, str.replace( y, x, y ) ) ---> x
         success = true;
@@ -2418,10 +2417,10 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
         // str.contains( x, z ) ----> false implies
         // str.replace( x, y, str.replace( y, z, w ) ) ---> x
         cmp_con = nm->mkNode(STRING_STRCTN, node[0], node[2][1]);
-        cmp_con = Rewriter::rewrite( cmp_con );
+        cmp_con = Rewriter::rewrite(cmp_con);
         success = cmp_con.isConst() && !cmp_con.getConst<bool>();
       }
-      if( success )
+      if (success)
       {
         return returnRewrite(node, node[0], "repl-repl3-inv-id");
       }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 584ccfe00..50db11c10 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -232,19 +232,22 @@ std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() cons
   return currentlyShared;
 }
 
-
-void Theory::collectTerms(TNode n, set<Kind>& irr_kinds, set<Node>& termSet) const
+void Theory::collectTerms(TNode n,
+                          set<Kind>& irr_kinds,
+                          set<Node>& termSet) const
 {
   if (termSet.find(n) != termSet.end()) {
     return;
   }
   Kind nk = n.getKind();
-  if( irr_kinds.find(nk)==irr_kinds.end() )
+  if (irr_kinds.find(nk) == irr_kinds.end())
   {
-    Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
+    Trace("theory::collectTerms")
+        << "Theory::collectTerms: adding " << n << endl;
     termSet.insert(n);
   }
-  if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n)) {
+  if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
+  {
     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
       collectTerms(*child_it, irr_kinds, termSet);
     }
@@ -255,10 +258,12 @@ void Theory::collectTerms(TNode n, set<Kind>& irr_kinds, set<Node>& termSet) con
 void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
 {
   set<Kind> irr_kinds;
-  computeRelevantTerms(termSet,irr_kinds,includeShared);
+  computeRelevantTerms(termSet, irr_kinds, includeShared);
 }
 
-void Theory::computeRelevantTerms(set<Node>& termSet, set<Kind>& irr_kinds, bool includeShared) const
+void Theory::computeRelevantTerms(set<Node>& termSet,
+                                  set<Kind>& irr_kinds,
+                                  bool includeShared) const
 {
   // Collect all terms appearing in assertions
   irr_kinds.insert(kind::EQUAL);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index f5bf068d2..a05779c76 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -161,7 +161,9 @@ private:
   /**
    * Helper function for computeRelevantTerms
    */
-  void collectTerms(TNode n, std::set<Kind>& irr_kinds, std::set<Node>& termSet) const;
+  void collectTerms(TNode n,
+                    std::set<Kind>& irr_kinds,
+                    std::set<Node>& termSet) const;
 
   /**
    * Scans the current set of assertions and shared terms top-down
@@ -169,7 +171,9 @@ private:
    * termSet.  This is used by collectModelInfo to delimit the set of
    * terms that should be used when constructing a model
    */
-  void computeRelevantTerms(std::set<Node>& termSet, std::set<Kind>& irr_kinds, bool includeShared = true) const;
+  void computeRelevantTerms(std::set<Node>& termSet,
+                            std::set<Kind>& irr_kinds,
+                            bool includeShared = true) const;
   void computeRelevantTerms(std::set<Node>& termSet, bool includeShared = true) const;
 
   /**