Format

5 files changed, 167 insertions, 141 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 16f229f89..fe208658b 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -294,7 +294,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n";
   unsigned max_depth = ssz>=d ? ssz-d : 0;
   unsigned min_depth = d_simple_proc[exp];
-  NodeManager * nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   if( min_depth<=max_depth ){
     TNode x = getFreeVar( ntn );
     std::vector<Node> sb_lemmas;
@@ -328,12 +328,12 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
     // add the above symmetry breaking predicates to lemmas
     std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
     Node rlv = getRelevancyCondition(n);
-    for( const Node& slem : sb_lemmas )
+    for (const Node& slem : sb_lemmas)
     {
       Node sslem = slem.substitute(x, n, cache);
-      if( !rlv.isNull() )
+      if (!rlv.isNull())
       {
-        sslem = nm->mkNode(OR,rlv,sslem);
+        sslem = nm->mkNode(OR, rlv, sslem);
       }
       lemmas.push_back(sslem);
     }
@@ -383,18 +383,20 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) {
         }
         Assert( !disj.empty() );
         if( excl ){
-          cond = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::AND, disj );
+          cond = disj.size() == 1
+                     ? disj[0]
+                     : NodeManager::currentNM()->mkNode(kind::AND, disj);
         }
       }else{
         int sindex = Datatype::cindexOf( selExpr );
         Assert( sindex!=-1 );
-        cond = DatatypesRewriter::mkTester( n[0], sindex, dt ).negate();
+        cond = DatatypesRewriter::mkTester(n[0], sindex, dt).negate();
       }
       Node c1 = getRelevancyCondition( n[0] );
       if( cond.isNull() ){
         cond = c1;
       }else if( !c1.isNull() ){
-        cond = NodeManager::currentNM()->mkNode( kind::OR, cond, c1 );
+        cond = NodeManager::currentNM()->mkNode(kind::OR, cond, c1);
       }
     }
     Trace("sygus-sb-debug2") << "Relevancy condition for " << n << " is " << cond << std::endl;
@@ -990,18 +992,18 @@ void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz
   TNode x = getFreeVar( tn );
   unsigned csz = getSearchSizeForAnchor( a );
   int max_depth = ((int)csz)-((int)sz);
-  NodeManager * nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   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)
       {
         if( !options::sygusSymBreakLazy() || d_active_terms.find( t )!=d_active_terms.end() ){
-          Node slem = lem.substitute(x,t);
-          Node rlv = getRelevancyCondition( t );
-          if( !rlv.isNull() )
+          Node slem = lem.substitute(x, t);
+          Node rlv = getRelevancyCondition(t);
+          if (!rlv.isNull())
           {
-            slem = nm->mkNode( OR, rlv, slem );
+            slem = nm->mkNode(OR, rlv, slem);
           }
           lemmas.push_back(slem);
         }
@@ -1021,8 +1023,8 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No
   Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d
                            << " " << a << std::endl;
   std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn );
-  Node rlv = getRelevancyCondition( t );
-  NodeManager * nm = NodeManager::currentNM();
+  Node rlv = getRelevancyCondition(t);
+  NodeManager* nm = NodeManager::currentNM();
   if( its != d_cache[a].d_sb_lemmas.end() ){
     TNode x = getFreeVar( tn );
     //get symmetry breaking lemmas for this term 
@@ -1036,11 +1038,11 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No
       if( (int)it->first<=max_sz ){
         for (const Node& lem : it->second)
         {
-          Node slem = lem.substitute(x,t,cache);
+          Node slem = lem.substitute(x, t, cache);
           // add the relevancy condition for t
-          if( !rlv.isNull() )
+          if (!rlv.isNull())
           {
-            slem = nm->mkNode( OR, rlv, slem );
+            slem = nm->mkNode(OR, rlv, slem);
           }
           lemmas.push_back(slem);
         }
@@ -1179,7 +1181,7 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >&
   Assert( itsz!=d_szinfo.end() );
   itsz->second->d_curr_search_size++;
   Trace("sygus-fair") << "  register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl;
-  NodeManager * nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   for( std::map< Node, SearchCache >::iterator itc = d_cache.begin(); itc != d_cache.end(); ++itc ){
     Node a = itc->first;
     Trace("sygus-fair-debug") << "  look at anchor " << a << "..." << std::endl;
@@ -1195,24 +1197,29 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >&
           int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz);
           std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth );
           if( itt!=itc->second.d_search_terms[tn].end() ){
-            for( const TNode& t : itt->second ){
-              if( !options::sygusSymBreakLazy() || d_active_terms.find( t )!=d_active_terms.end() && !it->second.empty() ){
-                std::vector< Node > slemmas;
+            for (const TNode& t : itt->second)
+            {
+              if (!options::sygusSymBreakLazy()
+                  || d_active_terms.find(t) != d_active_terms.end()
+                         && !it->second.empty())
+              {
+                std::vector<Node> slemmas;
                 std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
                 for (const Node& lem : it->second)
                 {
-                  slemmas.push_back(lem.substitute(x,t,cache));
+                  slemmas.push_back(lem.substitute(x, t, cache));
                 }
-                if( !slemmas.empty() )
+                if (!slemmas.empty())
                 {
-                  Node slem = slemmas.size()==1 ? slemmas[0] : nm->mkNode( AND, slemmas );
+                  Node slem = slemmas.size() == 1 ? slemmas[0]
+                                                  : nm->mkNode(AND, slemmas);
                   // add the relevancy condition
-                  Node rlv = getRelevancyCondition( t );
-                  if( !rlv.isNull() )
+                  Node rlv = getRelevancyCondition(t);
+                  if (!rlv.isNull())
                   {
-                    slem = nm->mkNode( OR, rlv, slem );
+                    slem = nm->mkNode(OR, rlv, slem);
                   }
-                  lemmas.push_back( slem );
+                  lemmas.push_back(slem);
                 }
               }
             }
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 27c062cdc..ea5a75705 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -446,7 +446,6 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
   return new_ret;
 }
 
-
 Node ExtendedRewriter::extendedRewriteAndOr(Node n)
 {
   Node new_ret;
@@ -458,17 +457,16 @@ Node ExtendedRewriter::extendedRewriteAndOr(Node n)
     debugExtendedRewrite(n, new_ret, "Bool bcp");
     return new_ret;
   }
-  // factoring 
-  new_ret = extendedRewriteFactoring(AND,OR,NOT,n);
-  if(!new_ret.isNull())
+  // factoring
+  new_ret = extendedRewriteFactoring(AND, OR, NOT, n);
+  if (!new_ret.isNull())
   {
     debugExtendedRewrite(n, new_ret, "Bool factoring");
     return new_ret;
   }
-  
+
   // equality resolution
-  new_ret =
-      extendedRewriteEqRes(AND, OR, EQUAL, NOT, bcp_kinds, n, false);
+  new_ret = extendedRewriteEqRes(AND, OR, EQUAL, NOT, bcp_kinds, n, false);
   debugExtendedRewrite(n, new_ret, "Bool eq res");
   return new_ret;
 }
@@ -795,24 +793,26 @@ Node ExtendedRewriter::extendedRewriteBcp(
   return Node::null();
 }
 
-Node ExtendedRewriter::extendedRewriteFactoring(
-    Kind andk, Kind ork, Kind notk, Node n)
+Node ExtendedRewriter::extendedRewriteFactoring(Kind andk,
+                                                Kind ork,
+                                                Kind notk,
+                                                Node n)
 {
   Trace("ext-rew-factoring") << "Factoring: *** INPUT: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
 
   Kind nk = n.getKind();
-  Assert( nk==andk || nk==ork );
-  Kind onk = nk==andk ? ork : andk;
+  Assert(nk == andk || nk == ork);
+  Kind onk = nk == andk ? ork : andk;
   // count the number of times atoms occur
-  std::map< Node, std::vector< Node > > lit_to_cl;
-  std::map< Node, std::vector< Node > > cl_to_lits;
-  for( const Node& nc : n )
+  std::map<Node, std::vector<Node> > lit_to_cl;
+  std::map<Node, std::vector<Node> > cl_to_lits;
+  for (const Node& nc : n)
   {
     Kind nck = nc.getKind();
-    if( nck==onk )
+    if (nck == onk)
     {
-      for( const Node& ncl : nc )
+      for (const Node& ncl : nc)
       {
         lit_to_cl[ncl].push_back(nc);
         cl_to_lits[nc].push_back(ncl);
@@ -827,47 +827,48 @@ Node ExtendedRewriter::extendedRewriteFactoring(
   // get the maximum shared literal to factor
   unsigned max_size = 0;
   Node flit;
-  for( const std::pair< const Node, std::vector< Node > >& ltc : lit_to_cl )
+  for (const std::pair<const Node, std::vector<Node> >& ltc : lit_to_cl)
   {
-    if( ltc.second.size()>max_size )
+    if (ltc.second.size() > max_size)
     {
       max_size = ltc.second.size();
       flit = ltc.first;
     }
   }
-  if( max_size>1 )
+  if (max_size > 1)
   {
     // do the factoring
-    std::vector< Node > children;
-    std::vector< Node > fchildren;
-    std::map< Node, std::vector< Node > >::iterator itl = lit_to_cl.find(flit);
-    std::vector< Node >& cls = itl->second;
-    for( const Node& nc : n )
+    std::vector<Node> children;
+    std::vector<Node> fchildren;
+    std::map<Node, std::vector<Node> >::iterator itl = lit_to_cl.find(flit);
+    std::vector<Node>& cls = itl->second;
+    for (const Node& nc : n)
     {
-      if( std::find( cls.begin(), cls.end(), nc )==cls.end() )
+      if (std::find(cls.begin(), cls.end(), nc) == cls.end())
       {
-        children.push_back( nc );
+        children.push_back(nc);
       }
       else
       {
         // rebuild
-        std::vector< Node >& lits = cl_to_lits[nc];
-        std::vector< Node >::iterator itlfl = std::find( lits.begin(), lits.end(), flit );
-        Assert( itlfl!=lits.end() );
-        lits.erase( itlfl );
+        std::vector<Node>& lits = cl_to_lits[nc];
+        std::vector<Node>::iterator itlfl =
+            std::find(lits.begin(), lits.end(), flit);
+        Assert(itlfl != lits.end());
+        lits.erase(itlfl);
         // rebuild
-        if( !lits.empty() )
+        if (!lits.empty())
         {
-          Node new_cl = lits.size()==1 ? lits[0] : nm->mkNode( onk, lits );
+          Node new_cl = lits.size() == 1 ? lits[0] : nm->mkNode(onk, lits);
           fchildren.push_back(new_cl);
         }
       }
     }
     // rebuild the factored children
-    Assert( !fchildren.empty() );
-    Node fcn = fchildren.size()==1 ? fchildren[0] : nm->mkNode(nk,fchildren);
-    children.push_back(nm->mkNode(onk,flit,fcn));
-    Node ret = children.size()==1 ? children[0] : nm->mkNode(nk,children);
+    Assert(!fchildren.empty());
+    Node fcn = fchildren.size() == 1 ? fchildren[0] : nm->mkNode(nk, fchildren);
+    children.push_back(nm->mkNode(onk, flit, fcn));
+    Node ret = children.size() == 1 ? children[0] : nm->mkNode(nk, children);
     Trace("ext-rew-factoring") << "Factoring: *** OUTPUT: " << ret << std::endl;
     return ret;
   }
@@ -964,48 +965,50 @@ Node ExtendedRewriter::extendedRewriteEqRes(Kind andk,
   return Node::null();
 }
 
-bool sortPairSecond(const std::pair<Node,unsigned> &a,
-               const std::pair<Node,unsigned> &b)
+bool sortPairSecond(const std::pair<Node, unsigned>& a,
+                    const std::pair<Node, unsigned>& b)
 {
-    return (a.second < b.second);
+  return (a.second < b.second);
 }
 
-
 class SimpSubsumeTrie
 {
  public:
-  std::map< Node, SimpSubsumeTrie > d_children;
+  std::map<Node, SimpSubsumeTrie> d_children;
   Node d_data;
-  void addTerm( Node c, std::vector< Node >& alist, std::vector< Node >& subsumes, unsigned index=0, bool doAdd = true )
+  void addTerm(Node c,
+               std::vector<Node>& alist,
+               std::vector<Node>& subsumes,
+               unsigned index = 0,
+               bool doAdd = true)
   {
-    if( !d_data.isNull() )
+    if (!d_data.isNull())
     {
       subsumes.push_back(d_data);
     }
-    if( doAdd )
+    if (doAdd)
     {
-      if( index==alist.size() )
+      if (index == alist.size())
       {
         d_data = c;
         return;
       }
     }
     // try all children where we have this atom
-    for( std::pair<const Node, SimpSubsumeTrie >& cp : d_children )
+    for (std::pair<const Node, SimpSubsumeTrie>& cp : d_children)
     {
-      if(std::find(alist.begin(),alist.end(),cp.first)!=alist.end() )
+      if (std::find(alist.begin(), alist.end(), cp.first) != alist.end())
       {
-        cp.second.addTerm(c,alist,subsumes,0,false);
+        cp.second.addTerm(c, alist, subsumes, 0, false);
       }
     }
-    if( doAdd )
+    if (doAdd)
     {
-      d_children[alist[index]].addTerm(c,alist,subsumes,index+1,doAdd);
+      d_children[alist[index]].addTerm(c, alist, subsumes, index + 1, doAdd);
     }
   }
 };
 
-
 Node ExtendedRewriter::extendedRewriteEqChain(
     Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor)
 {
@@ -1071,12 +1074,12 @@ Node ExtendedRewriter::extendedRewriteEqChain(
   // compute the atoms of each child
   Trace("ext-rew-eqchain") << "eqchain-simplify: begin\n";
   Trace("ext-rew-eqchain") << "  eqchain-simplify: get atoms...\n";
-  std::map< Node, std::map< Node, bool > > atoms;
-  std::map< Node, std::vector< Node > > alist;
-  std::vector< std::pair< Node, unsigned > > atom_count;
+  std::map<Node, std::map<Node, bool> > atoms;
+  std::map<Node, std::vector<Node> > alist;
+  std::vector<std::pair<Node, unsigned> > atom_count;
   for (std::pair<const Node, bool>& cp : cstatus)
   {
-    if( !cp.second )
+    if (!cp.second)
     {
       // already eliminated
       continue;
@@ -1085,19 +1088,19 @@ Node ExtendedRewriter::extendedRewriteEqChain(
     Kind ck = c.getKind();
     if (ck == andk || ck == ork)
     {
-      for(unsigned j=0, nchild = c.getNumChildren(); j<nchild; j++ )
+      for (unsigned j = 0, nchild = c.getNumChildren(); j < nchild; j++)
       {
         Node cl = c[j];
         bool pol = cl.getKind() != notk;
         Node ca = pol ? cl : cl[0];
-        Assert( atoms[c].find(ca)==atoms[c].end() );
+        Assert(atoms[c].find(ca) == atoms[c].end());
         // polarity is flipped when we are AND
-        atoms[c][ca] = pol==(ck==ork); 
+        atoms[c][ca] = pol == (ck == ork);
         alist[c].push_back(ca);
-        
+
         // if this already exists as a child of the equality chain, eliminate.
         // this catches cases like ( x & y ) = ( ( x & y ) | z ), where we
-        // consider ( x & y ) a unit, whereas below it is expanded to 
+        // consider ( x & y ) a unit, whereas below it is expanded to
         // ~( ~x | ~y ).
         std::map<Node, bool>::iterator itc = cstatus.find(ca);
         if (itc != cstatus.end() && itc->second)
@@ -1121,7 +1124,7 @@ Node ExtendedRewriter::extendedRewriteEqChain(
           Node nc[2];
           nc[0] = c[j];
           nc[1] = new_children.size() == 1 ? new_children[0]
-                                            : nm->mkNode(ck, new_children);
+                                           : nm->mkNode(ck, new_children);
           // negate the proper child
           unsigned nindex = (ck == andk) == pol ? 0 : 1;
           nc[nindex] = TermUtil::mkNegate(notk, nc[nindex]);
@@ -1143,53 +1146,58 @@ Node ExtendedRewriter::extendedRewriteEqChain(
       atoms[c][ca] = pol;
       alist[c].push_back(ca);
     }
-    atom_count.push_back(std::pair<Node,unsigned>(c,alist[c].size()));
+    atom_count.push_back(std::pair<Node, unsigned>(c, alist[c].size()));
   }
-  // check subsumptions 
+  // check subsumptions
   // sort by #atoms
-  std::sort(atom_count.begin(),atom_count.end(),sortPairSecond);
-  for( const std::pair< Node, unsigned >& ac : atom_count )
+  std::sort(atom_count.begin(), atom_count.end(), sortPairSecond);
+  for (const std::pair<Node, unsigned>& ac : atom_count)
   {
-    Trace("ext-rew-eqchain") << "  eqchain-simplify: " << ac.first << " has " << ac.second << " atoms." << std::endl;
+    Trace("ext-rew-eqchain") << "  eqchain-simplify: " << ac.first << " has "
+                             << ac.second << " atoms." << std::endl;
   }
   Trace("ext-rew-eqchain") << "  eqchain-simplify: compute subsumptions...\n";
   SimpSubsumeTrie sst;
   for (std::pair<const Node, bool>& cp : cstatus)
   {
-    if( !cp.second )
+    if (!cp.second)
     {
       // already eliminated
       continue;
     }
     Node c = cp.first;
-    Trace("ext-rew-eqchain") << "  - add term " << c << " with atom list " << alist[c] << "...\n";
-    std::vector< Node > subsumes;
-    sst.addTerm(c,alist[c], subsumes);
-    for( const Node& cc : subsumes )
+    Trace("ext-rew-eqchain")
+        << "  - add term " << c << " with atom list " << alist[c] << "...\n";
+    std::vector<Node> subsumes;
+    sst.addTerm(c, alist[c], subsumes);
+    for (const Node& cc : subsumes)
     {
-      if( !cstatus[cc] )
+      if (!cstatus[cc])
       {
         // subsumes a child that was already eliminated
         continue;
       }
-      Trace("ext-rew-eqchain") << "  eqchain-simplify: " << c << " subsumes " << cc << std::endl;
+      Trace("ext-rew-eqchain")
+          << "  eqchain-simplify: " << c << " subsumes " << cc << std::endl;
       // for each of the atoms in cc
-      std::map< Node, std::map< Node, bool > >::iterator itc = atoms.find(c);
-      Assert( itc!=atoms.end() );
-      std::map< Node, std::map< Node, bool > >::iterator itcc = atoms.find(cc);
-      Assert( itcc!=atoms.end() );
-      std::vector< Node > common_children;
-      std::vector< Node > diff_children;
-      for( const std::pair< const Node, bool > & ap : itcc->second )
+      std::map<Node, std::map<Node, bool> >::iterator itc = atoms.find(c);
+      Assert(itc != atoms.end());
+      std::map<Node, std::map<Node, bool> >::iterator itcc = atoms.find(cc);
+      Assert(itcc != atoms.end());
+      std::vector<Node> common_children;
+      std::vector<Node> diff_children;
+      for (const std::pair<const Node, bool>& ap : itcc->second)
       {
         // compare the polarity
         Node a = ap.first;
         bool polcc = ap.second;
-        Assert( itc->second.find(a)!=itc->second.end() );
+        Assert(itc->second.find(a) != itc->second.end());
         bool polc = itc->second[a];
-        Trace("ext-rew-eqchain") << "    eqchain-simplify: atom " << a << " has polarities : " << polc << " " << polcc << "\n";
-        Node lit = polc ? a : TermUtil::mkNegate( notk,a );
-        if( polc!=polcc )
+        Trace("ext-rew-eqchain")
+            << "    eqchain-simplify: atom " << a
+            << " has polarities : " << polc << " " << polcc << "\n";
+        Node lit = polc ? a : TermUtil::mkNegate(notk, a);
+        if (polc != polcc)
         {
           diff_children.push_back(lit);
         }
@@ -1198,19 +1206,22 @@ Node ExtendedRewriter::extendedRewriteEqChain(
           common_children.push_back(lit);
         }
       }
-      std::vector< Node > rem_children;
-      for( const std::pair< const Node, bool > & ap : itc->second )
+      std::vector<Node> rem_children;
+      for (const std::pair<const Node, bool>& ap : itc->second)
       {
         Node a = ap.first;
-        if( atoms[cc].find(a)==atoms[cc].end() )
+        if (atoms[cc].find(a) == atoms[cc].end())
         {
           bool polc = ap.second;
-          rem_children.push_back(polc ? a : TermUtil::mkNegate( notk,a ));
+          rem_children.push_back(polc ? a : TermUtil::mkNegate(notk, a));
         }
       }
-      Trace("ext-rew-eqchain") << "    #common/diff/rem: " << common_children.size() << "/" << diff_children.size() << "/" << rem_children.size() << "\n";
+      Trace("ext-rew-eqchain")
+          << "    #common/diff/rem: " << common_children.size() << "/"
+          << diff_children.size() << "/" << rem_children.size() << "\n";
       bool do_rewrite = false;
-      if( common_children.empty() && itc->second.size()==itcc->second.size() && itcc->second.size()==2 )
+      if (common_children.empty() && itc->second.size() == itcc->second.size()
+          && itcc->second.size() == 2)
       {
         // x | y = ~x | ~y ---> ~( x = y )
         do_rewrite = true;
@@ -1219,25 +1230,29 @@ Node ExtendedRewriter::extendedRewriteEqChain(
         gpol = !gpol;
         Trace("ext-rew-eqchain") << "    apply 2-child all-diff\n";
       }
-      else if( common_children.empty() && diff_children.size()==1 )
+      else if (common_children.empty() && diff_children.size() == 1)
       {
         do_rewrite = true;
         // x = ( ~x | y ) ---> ~( ~x | ~y )
-        Node remn = rem_children.size()==1 ? rem_children[0] : nm->mkNode( ork, rem_children );
-        remn = TermUtil::mkNegate( notk, remn );
-        children.push_back(nm->mkNode(ork,diff_children[0],remn));
+        Node remn = rem_children.size() == 1 ? rem_children[0]
+                                             : nm->mkNode(ork, rem_children);
+        remn = TermUtil::mkNegate(notk, remn);
+        children.push_back(nm->mkNode(ork, diff_children[0], remn));
         if (!isXor)
         {
           gpol = !gpol;
         }
         Trace("ext-rew-eqchain") << "    apply unit resolution\n";
       }
-      else if( diff_children.size()==1 && itc->second.size()==itcc->second.size() )
+      else if (diff_children.size() == 1
+               && itc->second.size() == itcc->second.size())
       {
         // ( x | y | z ) = ( x | ~y | z ) ---> ( x | z )
         do_rewrite = true;
-        Assert( !common_children.empty() );
-        Node comn = common_children.size()==1 ? common_children[0] : nm->mkNode(ork, common_children);
+        Assert(!common_children.empty());
+        Node comn = common_children.size() == 1
+                        ? common_children[0]
+                        : nm->mkNode(ork, common_children);
         children.push_back(comn);
         if (isXor)
         {
@@ -1245,10 +1260,10 @@ Node ExtendedRewriter::extendedRewriteEqChain(
         }
         Trace("ext-rew-eqchain") << "    apply resolution\n";
       }
-      else if( diff_children.empty() )
+      else if (diff_children.empty())
       {
         do_rewrite = true;
-        if( rem_children.empty() )
+        if (rem_children.empty())
         {
           // x | y = x | y ---> true
           // this can happen if we have ( ~x & ~y ) = ( x | y )
@@ -1262,10 +1277,13 @@ Node ExtendedRewriter::extendedRewriteEqChain(
         else
         {
           // x | y = ( x | y | z ) ---> ( x | y | ~z )
-          Node remn = rem_children.size()==1 ? rem_children[0] : nm->mkNode( ork, rem_children );
-          remn = TermUtil::mkNegate( notk, remn );
-          Node comn = common_children.size()==1 ? common_children[0] : nm->mkNode(ork, common_children);
-          children.push_back(nm->mkNode(ork,comn,remn));
+          Node remn = rem_children.size() == 1 ? rem_children[0]
+                                               : nm->mkNode(ork, rem_children);
+          remn = TermUtil::mkNegate(notk, remn);
+          Node comn = common_children.size() == 1
+                          ? common_children[0]
+                          : nm->mkNode(ork, common_children);
+          children.push_back(nm->mkNode(ork, comn, remn));
           if (isXor)
           {
             gpol = !gpol;
@@ -1273,14 +1291,14 @@ Node ExtendedRewriter::extendedRewriteEqChain(
           Trace("ext-rew-eqchain") << "    apply subsume\n";
         }
       }
-      if( do_rewrite )
+      if (do_rewrite)
       {
         // eliminate the children, reverse polarity as needed
-        for( unsigned r=0; r<2; r++ )
+        for (unsigned r = 0; r < 2; r++)
         {
-          Node c_rem = r==0 ? c : cc;
+          Node c_rem = r == 0 ? c : cc;
           cstatus[c_rem] = false;
-          if( c_rem.getKind()==andk )
+          if (c_rem.getKind() == andk)
           {
             gpol = !gpol;
           }
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index d4ea92a58..00ac47ecd 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -132,11 +132,10 @@ class ExtendedRewriter
   Node extendedRewriteBcp(
       Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node n);
   /** (type-independent) factoring, for example:
-   * 
+   *
    */
-  
-  Node extendedRewriteFactoring(
-      Kind andk, Kind ork, Kind notk, Node n);
+
+  Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n);
   /** (type-independent) equality resolution, for example:
    *
    *   ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B )
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index fa39f28b7..ae9c79f1c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -293,7 +293,8 @@ void CegConjectureSingleInv::initialize( Node q ) {
 
 void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) {
   d_has_ites = hasItes;
-  Trace("cegqi-si-debug") << "Single invocation, finish init, has ITEs = " << d_has_ites << std::endl;
+  Trace("cegqi-si-debug") << "Single invocation, finish init, has ITEs = "
+                          << d_has_ites << 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 ){
     d_single_invocation = false;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 88a8f258c..3efad5ab4 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -247,7 +247,8 @@ Node CegGrammarConstructor::process(Node q,
     }
     d_qe->getTermDatabaseSygus()->registerSygusType( tn );
     // check grammar restrictions
-    if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
+    if (!d_qe->getTermDatabaseSygus()->hasKind(tn, ITE))
+    {
       d_has_ite = false;
     }
     Assert( tn.isDatatype() );