Format

19 files changed, 142 insertions, 116 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 169bef7a5..6b382a012 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1219,7 +1219,8 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt,
 }
 
 const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
-  for( unsigned i=0, size = d_sygusInvVars.size(); i<size; i++ ){
+  for (unsigned i = 0, size = d_sygusInvVars.size(); i < size; i++)
+  {
     Expr v = d_sygusInvVars[i];
     std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
     if( it!=d_sygusVarPrimed.end() ){
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 7d2fc1ace..4e169ee82 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -62,7 +62,8 @@ private:
   std::unordered_map<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
   // for sygus
-  std::vector<Expr> d_sygusVars, d_sygusInvVars, d_sygusConstraints, d_sygusFunSymbols;
+  std::vector<Expr> d_sygusVars, d_sygusInvVars, d_sygusConstraints,
+      d_sygusFunSymbols;
   std::map< Expr, bool > d_sygusVarPrimed;
 
 protected:
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c28a3c30e..4dfe8ec57 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1315,10 +1315,11 @@ void SmtEngine::setDefaults() {
     {
       options::cbqiMidpoint.set(true);
     }
-    if( options::sygusRepairConst() )
+    if (options::sygusRepairConst())
     {
-      if( !options::cbqi.wasSetByUser() ){
-        options::cbqi.set( true );
+      if (!options::cbqi.wasSetByUser())
+      {
+        options::cbqi.set(true);
       }
     }
   }
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 15fb9aac3..28707bfe3 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -790,14 +790,17 @@ Node SygusSymBreakNew::registerSearchValue(
   Node cnv = d_tds->canonizeBuiltin(nv, var_count);
   Trace("sygus-sb-debug") << "  ...canonized value is " << cnv << std::endl;
   // must do this for all nodes, regardless of top-level
-  if( d_cache[a].d_search_val_proc.find( cnv )==d_cache[a].d_search_val_proc.end() ){
+  if (d_cache[a].d_search_val_proc.find(cnv)
+      == d_cache[a].d_search_val_proc.end())
+  {
     d_cache[a].d_search_val_proc.insert(cnv);
     // get the root (for PBE symmetry breaking)
     Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end());
     quantifiers::CegConjecture* aconj = d_anchor_to_conj[a];
     Assert(aconj != NULL);
-    Trace("sygus-sb-debug") << "  ...register search value " << cnv << ", type=" << tn << std::endl;
-    Node bv = d_tds->sygusToBuiltin( cnv, tn );
+    Trace("sygus-sb-debug")
+        << "  ...register search value " << cnv << ", type=" << tn << std::endl;
+    Node bv = d_tds->sygusToBuiltin(cnv, tn);
     Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
     Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
     Trace("sygus-sb-debug") << "  ......rewrites to " << bvr << std::endl;
@@ -805,8 +808,10 @@ Node SygusSymBreakNew::registerSearchValue(
     unsigned sz = d_tds->getSygusTermSize( nv );      
     if( d_tds->involvesDivByZero( bvr ) ){
       quantifiers::DivByZeroSygusInvarianceTest dbzet;
-      Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " << bv << std::endl;
-      registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), var_count, lemmas);
+      Trace("sygus-sb-mexp-debug")
+          << "Minimize explanation for div-by-zero in " << bv << std::endl;
+      registerSymBreakLemmaForValue(
+          a, nv, dbzet, Node::null(), var_count, lemmas);
       return Node::null();
     }else{
       std::unordered_map<Node, Node, NodeHashFunction>::iterator itsv =
@@ -941,7 +946,8 @@ Node SygusSymBreakNew::registerSearchValue(
         eset.init(d_tds, tn, aconj, a, bvr);
 
         Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl;
-        registerSymBreakLemmaForValue(a, bad_val, eset, bad_val_o, var_count, lemmas);
+        registerSymBreakLemmaForValue(
+            a, bad_val, eset, bad_val_o, var_count, lemmas);
         return Node::null();
       }
     }
@@ -985,7 +991,8 @@ void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz
   for( int d=0; d<=max_depth; d++ ){
     std::map< unsigned, std::vector< Node > >::iterator itt = d_cache[a].d_search_terms[tn].find( d );
     if( itt!=d_cache[a].d_search_terms[tn].end() ){
-      for( const TNode& t : itt->second ){
+      for (const TNode& t : itt->second)
+      {
         if( !options::sygusSymBreakLazy() || d_active_terms.find( t )!=d_active_terms.end() ){
           std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
           addSymBreakLemma(lem, x, t, lemmas, cache);
@@ -1017,7 +1024,7 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No
     std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
     for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){
       if( (int)it->first<=max_sz ){
-        for( const Node& lem : it->second )
+        for (const Node& lem : it->second)
         {
           addSymBreakLemma(lem, x, t, lemmas, cache);
         }
@@ -1027,15 +1034,16 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No
   Trace("sygus-sb-debug2") << "...finished." << std::endl;
 }
 
-void SygusSymBreakNew::addSymBreakLemma(Node lem,
-                                        TNode x,
-                                        TNode n,
-                                        std::vector<Node>& lemmas, 
-                                        std::unordered_map<TNode, TNode, TNodeHashFunction>& cache)
+void SygusSymBreakNew::addSymBreakLemma(
+    Node lem,
+    TNode x,
+    TNode n,
+    std::vector<Node>& lemmas,
+    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache)
 {
   Assert( !options::sygusSymBreakLazy() || d_active_terms.find( n )!=d_active_terms.end() );
   // apply lemma
-  Node slem = lem.substitute( x, n, cache );
+  Node slem = lem.substitute(x, n, cache);
   Trace("sygus-sb-exc-debug") << "SymBreak lemma : " << slem << std::endl;
   Node rlv = getRelevancyCondition( n );
   if( !rlv.isNull() ){
@@ -1192,7 +1200,7 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >&
               TNode t = itt->second[k];
               if( !options::sygusSymBreakLazy() || d_active_terms.find( t )!=d_active_terms.end() ){
                 std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
-                for( const Node& lem : it->second )
+                for (const Node& lem : it->second)
                 {
                   addSymBreakLemma(lem, x, t, lemmas, cache);
                 }
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 9819803b2..51794e641 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -369,8 +369,12 @@ private:
    * the substitution { x -> n } has been applied, and is passed to the
    * underlying substitute call.
    */
-  void addSymBreakLemma(Node lem, TNode x, TNode n, std::vector<Node>& lemmas, 
-                                        std::unordered_map<TNode, TNode, TNodeHashFunction>& cache);
+  void addSymBreakLemma(
+      Node lem,
+      TNode x,
+      TNode n,
+      std::vector<Node>& lemmas,
+      std::unordered_map<TNode, TNode, TNodeHashFunction>& cache);
   //------------------------end dynamic symmetry breaking
 
   /** Get relevancy condition
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 50ba22229..b67e6ef73 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -2270,7 +2270,7 @@ void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
             addedFirst = true;
             termSet.insert(first);
           }
-          termSet.insert( n );
+          termSet.insert(n);
         }
         ++eqc_i;
       }
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 6ef66f6e4..0d46ba445 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -325,16 +325,16 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
   }
   // Boolean true/false return
   TypeNode tn = n.getType();
-  if( tn.isBoolean() )
+  if (tn.isBoolean())
   {
-    for( unsigned i=1; i<=2; i++ )
+    for (unsigned i = 1; i <= 2; i++)
     {
-      if( n[i].isConst() )
+      if (n[i].isConst())
       {
-        Node cond = i==1 ? n[0] : n[0].negate();
-        Node other = n[i==1 ? 2 : 1];
+        Node cond = i == 1 ? n[0] : n[0].negate();
+        Node other = n[i == 1 ? 2 : 1];
         Kind retk = AND;
-        if( n[i].getConst<bool>() )
+        if (n[i].getConst<bool>())
         {
           retk = OR;
         }
@@ -342,7 +342,7 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
         {
           cond = cond.negate();
         }
-        Node new_ret = nm->mkNode( retk, cond, other );
+        Node new_ret = nm->mkNode(retk, cond, other);
         if (full)
         {
           debugExtendedRewrite(n, new_ret, "ITE const return");
@@ -1250,20 +1250,20 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret, bool& pol)
           nconst_count++;
           nconst_index = i;
         }
-        for( unsigned j=0; j<2; j++ )
+        for (unsigned j = 0; j < 2; j++)
         {
-          Node v = j==0 ? v1[i] : v2[i];
-          Node vo = j==0 ? v2[i] : v1[i];
+          Node v = j == 0 ? v1[i] : v2[i];
+          Node vo = j == 0 ? v2[i] : v1[i];
           // should we negate both?
-          if( v.getKind()==BITVECTOR_NOT && vo.isConst() )
+          if (v.getKind() == BITVECTOR_NOT && vo.isConst())
           {
             v = v[0];
-            vo = TermUtil::mkNegate(BITVECTOR_NOT, vo );
-            vo = Rewriter::rewrite( vo );
+            vo = TermUtil::mkNegate(BITVECTOR_NOT, vo);
+            vo = Rewriter::rewrite(vo);
             vs_changed = true;
           }
-          v1[i] = j==0 ? v : vo;
-          v2[i] = j==0 ? vo : v;
+          v1[i] = j == 0 ? v : vo;
+          v2[i] = j == 0 ? vo : v;
         }
       }
       if (nconst_count == 1)
@@ -1272,10 +1272,10 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret, bool& pol)
         debugExtendedRewrite(ret, new_ret, "CONCAT eq true");
         return new_ret;
       }
-      if( vs_changed )
+      if (vs_changed)
       {
-        Node v1n = nm->mkNode(BITVECTOR_CONCAT,v1);
-        Node v2n = nm->mkNode(BITVECTOR_CONCAT,v2);
+        Node v1n = nm->mkNode(BITVECTOR_CONCAT, v1);
+        Node v2n = nm->mkNode(BITVECTOR_CONCAT, v2);
         new_ret = v1n.eqNode(v2n);
         debugExtendedRewrite(ret, new_ret, "CONCAT mod component");
         return new_ret;
@@ -2232,7 +2232,7 @@ bool ExtendedRewriter::bitVectorDisjoint(Node a, Node b)
       break;
     }
   }
-  if( dualSubsumeSuccess )
+  if (dualSubsumeSuccess)
   {
     return true;
   }
@@ -2255,31 +2255,27 @@ bool ExtendedRewriter::bitVectorDisjoint(Node a, Node b)
 void bitVectorIntervalSetIndices(Node a, unsigned& min_i, unsigned& max_i)
 {
   unsigned size = bv::utils::getSize(a);
-  Assert( size>0 );
+  Assert(size > 0);
   min_i = 0;
-  max_i = size-1;
-  if( a.isConst() )
+  max_i = size - 1;
+  if (a.isConst())
   {
-    
-    for( unsigned i=0; i<size; i++ )
+    for (unsigned i = 0; i < size; i++)
     {
-      
     }
   }
   Kind ak = a.getKind();
-  if( ak==BITVECTOR_SHL || ak==BITVECTOR_LSHR  )
+  if (ak == BITVECTOR_SHL || ak == BITVECTOR_LSHR)
   {
     // constant shift
-    if( a[1].isConst() )
+    if (a[1].isConst())
     {
-      
     }
   }
-  else if( ak==BITVECTOR_AND || ak==BITVECTOR_OR )
+  else if (ak == BITVECTOR_AND || ak == BITVECTOR_OR)
   {
-
   }
-  else if( ak==MULT )
+  else if (ak == MULT)
   {
     // powers of two combine
   }
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index f279b4ff4..67508633e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -274,10 +274,10 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
         Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
         fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
       }
-      if( Trace.isOn("cegqi-check") )
+      if (Trace.isOn("cegqi-check"))
       {
         Trace("cegqi-check") << "CegConjuncture : repair previous solution ";
-        for( const Node& fc : fail_cvs )
+        for (const Node& fc : fail_cvs)
         {
           std::stringstream ss;
           Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc);
@@ -362,7 +362,8 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
         Node sk = nm->mkSkolem("rsk", v.getType());
         sks.push_back(sk);
         vars.push_back(v);
-        Trace("cegqi-check-debug") << "  introduce skolem " << sk << " for " << v << "\n";
+        Trace("cegqi-check-debug")
+            << "  introduce skolem " << sk << " for " << v << "\n";
       }
       lem = inst[0][1].substitute(
           vars.begin(), vars.end(), sks.begin(), sks.end());
@@ -403,7 +404,7 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
     // either this conjecture does not have a solution, or candidate_values
     // is a solution for this conjecture.
     lem = nm->mkNode(OR, d_quant.negate(), query);
-    if( options::sygusVerifySubcall() )
+    if (options::sygusVerifySubcall())
     {
       Trace("cegqi-engine") << "  *** Direct verify..." << std::endl;
       SmtEngine verifySmt(nm->toExprManager());
@@ -424,7 +425,7 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
         Trace("cegqi-engine") << std::endl;
         return;
       }
-      else if(r.asSatisfiabilityResult().isSat() == Result::UNSAT )
+      else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
         // if the result in the subcall was unsatisfiable, we avoid
         // rechecking, hence we drop "query" from the verification lemma
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index b2c5c6ee7..e16e696b5 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -17,9 +17,9 @@
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -575,9 +575,11 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   }else{
     Trace("csi-sol") << "Post-process solution..." << std::endl;
     Node prev = d_solution;
-    if( options::minSynthSol() )
+    if (options::minSynthSol())
     {
-      d_solution = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(d_solution);
+      d_solution =
+          d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(
+              d_solution);
     }
     d_solution = postProcessSolution( d_solution );
     if( prev!=d_solution ){
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 2b17d6d79..07e4c887d 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -52,7 +52,8 @@ bool CegisUnif::processInitialize(Node n,
     if (!d_sygus_unif.usingUnif(f))
     {
       Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
-      d_tds->registerEnumerator(f, f, d_parent, false, options::sygusRepairConst());
+      d_tds->registerEnumerator(
+          f, f, d_parent, false, options::sygusRepairConst());
       d_non_unif_candidates.push_back(f);
     }
     else
@@ -270,10 +271,7 @@ Node CegisUnif::getNextDecisionRequest(unsigned& priority)
   return d_u_enum_manager.getNextDecisionRequest(priority);
 }
 
-bool CegisUnif::usingRepairConst() 
-{
-  return false;
-}
+bool CegisUnif::usingRepairConst() { return false; }
 
 CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
                                            CegConjecture* parent)
@@ -473,7 +471,12 @@ void CegisUnifEnumManager::incrementNumEnumerators()
         Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                                  << " to strategy point " << ci.second.d_pt
                                  << "\n";
-        d_tds->registerEnumerator(e, ci.second.d_pt, d_parent, false, index==0 ? options::sygusUnifRepairRet() : options::sygusUnifRepairCond());
+        d_tds->registerEnumerator(e,
+                                  ci.second.d_pt,
+                                  d_parent,
+                                  false,
+                                  index == 0 ? options::sygusUnifRepairRet()
+                                             : options::sygusUnifRepairCond());
       }
     }
     // register the evaluation points at the new value
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index b05193f35..a0e5006b9 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -237,6 +237,7 @@ class CegisUnif : public Cegis
 
   /** using repair const */
   bool usingRepairConst() override;
+
  private:
   /** do cegis-implementation-specific intialization for this class */
   bool processInitialize(Node n,
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 93dbf79e8..a942da909 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -285,7 +285,7 @@ void SygusExplain::getExplanationFor(Node n,
                                      unsigned& sz)
 {
   std::map<TypeNode, int> var_count;
-  return getExplanationFor(n,vn,exp,et,vnr,var_count,sz);
+  return getExplanationFor(n, vn, exp, et, vnr, var_count, sz);
 }
 
 void SygusExplain::getExplanationFor(Node n,
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index be2f4d22d..435530f46 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -459,11 +459,12 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
       // beneath the same application
       // we set its weight to zero since it should be considered at the
       // same level as constants.
-      to.d_ops.insert(to.d_ops.begin(),av.toExpr());
-      to.d_cons_names.insert(to.d_cons_names.begin(),cname);
-      to.d_cons_args_t.insert(to.d_cons_args_t.begin(),builtin_arg);
-      to.d_pc.insert(to.d_pc.begin(),printer::SygusEmptyPrintCallback::getEmptyPC());
-      to.d_weight.insert(to.d_weight.begin(),0);
+      to.d_ops.insert(to.d_ops.begin(), av.toExpr());
+      to.d_cons_names.insert(to.d_cons_names.begin(), cname);
+      to.d_cons_args_t.insert(to.d_cons_args_t.begin(), builtin_arg);
+      to.d_pc.insert(to.d_pc.begin(),
+                     printer::SygusEmptyPrintCallback::getEmptyPC());
+      to.d_weight.insert(to.d_weight.begin(), 0);
     }
   }
   /* Build normalize datatype */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 0792c595c..5e578d70b 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -459,7 +459,8 @@ void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
   getLeavesInternal(vals, pol, v, 0, -2);
 }
 
-SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0), d_sol_cons_nondet(false)
+SygusUnifIo::SygusUnifIo()
+    : d_check_sol(false), d_cond_count(0), d_sol_cons_nondet(false)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -730,7 +731,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
         Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
         vc = vcc;
       }
-      else if( !d_sol_cons_nondet )
+      else if (!d_sol_cons_nondet)
       {
         break;
       }
@@ -854,7 +855,7 @@ void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
 }
 
 void SygusUnifIo::initializeConstructSol()
-{ 
+{
   d_context.initialize(this);
   d_sol_cons_nondet = false;
 }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index e613883a7..0aca9ebe2 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -310,13 +310,13 @@ class SygusUnifIo : public SygusUnif
   unsigned d_cond_count;
   /** The solution for the function of this class, if one has been found */
   Node d_solution;
-  /** 
-   * This flag is set to true if the solution construction was 
+  /**
+   * This flag is set to true if the solution construction was
    * non-deterministic with respect to failure/success.
-   * 
-   * The solution construction for the string concatenation strategy is 
+   *
+   * The solution construction for the string concatenation strategy is
    * non-deterministic with respect to success/failure. That is, choosing
-   * a particular string may lead to being unsolvable in the recursive calls, 
+   * a particular string may lead to being unsolvable in the recursive calls,
    * whereas others may not. For example, if our pool of enumerated strings is:
    *   { "A", x, "B" }
    * and our I/O example is:
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 77e4128c1..45167efb2 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -674,7 +674,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
           << "  add condition (" << c_counter << "/" << d_conds.size()
           << "): " << ce << " -> " << ss.str() << std::endl;
     }
-    cv = repairConditionToSeparate(ce, cv,e,er);
+    cv = repairConditionToSeparate(ce, cv, e, er);
     d_conds[c_counter] = cv;
     // cache the separation class
     std::vector<Node> prev_sep_c = d_pt_sep.d_trie.d_rep_to_class[er];
@@ -828,52 +828,57 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
   return cache[root];
 }
 
-Node SygusUnifRl::DecisionTreeInfo::repairConditionToSeparate( Node ce, Node cv, Node e1, Node e2 )
+Node SygusUnifRl::DecisionTreeInfo::repairConditionToSeparate(Node ce,
+                                                              Node cv,
+                                                              Node e1,
+                                                              Node e2)
 {
   // repair condition
-  if( options::sygusUnifRepairCond() )
+  if (options::sygusUnifRepairCond())
   {
-    if( SygusRepairConst::mustRepair(cv) )
+    if (SygusRepairConst::mustRepair(cv))
     {
       SygusRepairConst src(d_unif->d_qe);
       Node t[2];
-      for( unsigned i=0; i<2; i++ )
+      for (unsigned i = 0; i < 2; i++)
       {
-        Node ei = i==0 ? e1 : e2;
-        std::map<Node, std::vector<Node>>::iterator it = d_unif->d_hd_to_pt.find(ei);
-        Assert( it != d_unif->d_hd_to_pt.end() );
-        std::vector< Node > children;
+        Node ei = i == 0 ? e1 : e2;
+        std::map<Node, std::vector<Node>>::iterator it =
+            d_unif->d_hd_to_pt.find(ei);
+        Assert(it != d_unif->d_hd_to_pt.end());
+        std::vector<Node> children;
         children.push_back(ce);
-        children.insert(children.end(),it->second.begin(),it->second.end());
+        children.insert(children.end(), it->second.begin(), it->second.end());
         t[i] = datatypes::DatatypesRewriter::mkSygusEvalApp(children);
       }
       Node deq = t[0].eqNode(t[1]).negate();
-      Trace("sygus-unif-sol") << "Try to repair to satisfy : " << deq << std::endl;
-      std::vector< Node > candidate;
+      Trace("sygus-unif-sol")
+          << "Try to repair to satisfy : " << deq << std::endl;
+      std::vector<Node> candidate;
       candidate.push_back(ce);
-      std::vector< Node > candidate_value;
+      std::vector<Node> candidate_value;
       candidate_value.push_back(cv);
-      src.initialize(deq,candidate);
-      std::vector< Node > repair_cv;
-      if(src.repairSolution(candidate,candidate_value,repair_cv))
+      src.initialize(deq, candidate);
+      std::vector<Node> repair_cv;
+      if (src.repairSolution(candidate, candidate_value, repair_cv))
       {
-        Assert(repair_cv.size()==1);
+        Assert(repair_cv.size() == 1);
         Node cvr = repair_cv[0];
-        if(Trace.isOn("sygus-unif-sol"))
+        if (Trace.isOn("sygus-unif-sol"))
         {
           Trace("sygus-unif-sol") << "Repaired ";
           std::stringstream ss;
-          Printer::getPrinter(options::outputLanguage())
-              ->toStreamSygus(ss, cv);
+          Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, cv);
           Trace("sygus-unif-sol") << ss.str() << " to ";
           std::stringstream ssr;
           Printer::getPrinter(options::outputLanguage())
               ->toStreamSygus(ssr, cvr);
           Trace("sygus-unif-sol") << ssr.str() << " to separate points:\n";
-          for( unsigned i=0; i<2; i++ )
+          for (unsigned i = 0; i < 2; i++)
           {
-            Node ei = i==0 ? e1 : e2;
-            std::map<Node, std::vector<Node>>::iterator it = d_unif->d_hd_to_pt.find(ei);
+            Node ei = i == 0 ? e1 : e2;
+            std::map<Node, std::vector<Node>>::iterator it =
+                d_unif->d_hd_to_pt.find(ei);
             Trace("sygus-unif-sol") << "  " << it->second << std::endl;
           }
         }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 0b1b94dd2..16f04e0c8 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -280,7 +280,7 @@ class SygusUnifRl : public SygusUnif
       DecisionTreeInfo* d_dt;
     };
     /** repair condition to separate */
-    Node repairConditionToSeparate( Node ce, Node cv, Node e1, Node e2 );
+    Node repairConditionToSeparate(Node ce, Node cv, Node e1, Node e2);
     /**
      * Utility for determining how evaluation points are separated by currently
      * enumerated condiotion values
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 40a76de63..d5168a905 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -118,7 +118,7 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
   {
     int anyC = getAnyConstantConsNum(tn);
     Node k;
-    if( anyC==-1 )
+    if (anyC == -1)
     {
       k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy");
       SygusPrintProxyAttribute spa;
@@ -127,7 +127,8 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
     else
     {
       const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-      k = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[anyC].getConstructor() ), c );
+      k = NodeManager::currentNM()->mkNode(
+          APPLY_CONSTRUCTOR, Node::fromExpr(dt[anyC].getConstructor()), c);
     }
     d_proxy_vars[tn][c] = k;
     return k;
@@ -193,8 +194,7 @@ Node TermDbSygus::canonizeBuiltin(Node n)
   return canonizeBuiltin(n, var_count);
 }
 
-Node TermDbSygus::canonizeBuiltin(Node n,
-                                  std::map<TypeNode, int>& var_count)
+Node TermDbSygus::canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count)
 {
   // has it already been computed?
   if (var_count.empty() && n.hasAttribute(CanonizeBuiltinAttribute()))
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 4b00a9451..eff46d23a 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -47,17 +47,18 @@ public:
     if(node.getKind() == kind::APPLY_UF) {
       if( node.getOperator().getKind() == kind::LAMBDA ){
         TNode lambda = node.getOperator();
-        std::vector< TNode > vars;
-        std::vector< TNode > subs;
-        for( const TNode& v : lambda[0] )
+        std::vector<TNode> vars;
+        std::vector<TNode> subs;
+        for (const TNode& v : lambda[0])
         {
-          vars.push_back( v );
+          vars.push_back(v);
         }
-        for( const TNode& s : node )
+        for (const TNode& s : node)
         {
           subs.push_back(s);
         }
-        Node ret = lambda[1].substitute(vars.begin(),vars.end(),subs.begin(),subs.end());
+        Node ret = lambda[1].substitute(
+            vars.begin(), vars.end(), subs.begin(), subs.end());
         return RewriteResponse(REWRITE_AGAIN_FULL, ret);
       }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){
         return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));