Merge branch 'sygusComp2018-2' into replaceSubstitutereplaceSubstitute

37 files changed, 298 insertions, 253 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index dfbd5fb3e..81e8bbe26 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -2,9 +2,9 @@
 /*! \file ce_guided_conjecture.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index a874ad048..0b6f0e1a8 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -2,9 +2,9 @@
 /*! \file ce_guided_conjecture.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Tim King, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 031507c11..f877bcefd 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
index e461a08d5..502244d25 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
@@ -2,9 +2,9 @@
 /*! \file ce_guided_instantiation.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Mathias Preiner, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 5fc22b002..9a6fad52a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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 e19d749ad..b368a0689 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -2,9 +2,9 @@
 /*! \file ce_guided_single_inv.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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 5abed96e6..44835cc26 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -2,9 +2,9 @@
 /*! \file ce_guided_single_inv_sol.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng, Tim King
+ **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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 4f85fe14f..8d18611cf 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -2,9 +2,9 @@
 /*! \file ce_guided_single_inv_sol.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index fcb81ce5f..37ee01370 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -2,9 +2,9 @@
 /*! \file cegis.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 856219b73..f094b9490 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -2,9 +2,9 @@
 /*! \file cegis.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -42,7 +42,7 @@ class Cegis : public SygusModule
 {
  public:
   Cegis(QuantifiersEngine* qe, CegConjecture* p);
-  ~Cegis() {}
+  ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node n,
                           const std::vector<Node>& candidates,
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 07e4c887d..5ad4cec11 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -2,7 +2,7 @@
 /*! \file cegis_unif.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa, Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index a0e5006b9..530f68c8b 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -2,7 +2,7 @@
 /*! \file cegis_unif.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa, Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -200,7 +200,7 @@ class CegisUnif : public Cegis
 {
  public:
   CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
-  ~CegisUnif();
+  ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
    * Non-unification candidates have themselves as enumerators, while for
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index a942da909..ddf52001e 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index aa28d4693..4efc171d3 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index c0f285c7e..efffa046f 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_grammar_cons.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 9c2d76733..c99c431ea 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 435530f46..8a415cc10 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_grammar_norm.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index f72a83e5a..a0f81dcf3 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -2,9 +2,9 @@
 /*! \file sygus_grammar_norm.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 939788e4d..24aa74c9e 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index d0484aa57..ce83402c9 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 277a443c5..aeb947bc6 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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 d9ff98c2a..d28a25a4a 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -2,9 +2,9 @@
 /*! \file sygus_invariance.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 11747830d..b36fe4281 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index b01f8e1d0..52b6aea0a 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -2,9 +2,9 @@
 /*! \file sygus_module.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -49,7 +49,7 @@ class SygusModule
 {
  public:
   SygusModule(QuantifiersEngine* qe, CegConjecture* p);
-  ~SygusModule() {}
+  virtual ~SygusModule() {}
   /** initialize
    *
    * n is the "base instantiation" of the deep-embedding version of the
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 7c7659fde..2ab18eb59 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file ce_guided_pbe.cpp
+/*! \file sygus_pbe.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index dc61f459b..49d853248 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file ce_guided_pbe.h
+/*! \file sygus_pbe.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index ef530e722..76e484549 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_process_conj.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index 0b9a25532..b16118b2e 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -2,9 +2,9 @@
 /*! \file sygus_process_conj.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
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.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 76ca94e05..d0f156811 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_unif.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index a19f8e41b..dd6922351 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -2,9 +2,9 @@
 /*! \file sygus_unif.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 228a501ac..ef805c844 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_unif_io.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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;
@@ -177,9 +177,14 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
         Trace("sygus-sui-dt-debug") << "X";
         return false;
       }
+      Trace("sygus-sui-dt-debug") << ival;
+      tot += ival;
+    }
+    else
+    {
+      // inactive in this context
+      Trace("sygus-sui-dt-debug") << "-";
     }
-    Trace("sygus-sui-dt-debug") << ival;
-    tot += ival;
     inc.push_back(ival);
   }
   return true;
@@ -515,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);
@@ -554,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
@@ -592,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());
@@ -707,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
@@ -754,7 +760,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
     d_check_sol = false;
     // try multiple times if we have done multiple conditions, due to
     // non-determinism
-    Node vc;
+    unsigned sol_term_size = 0;
     for (unsigned i = 0; i <= d_cond_count; i++)
     {
       Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
@@ -767,24 +773,24 @@ 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()
-          && (vc.isNull() || (!vc.isNull()
-                              && d_tds->getSygusTermSize(vcc)
-                                     < d_tds->getSygusTermSize(vc))))
+          && (d_solution.isNull()
+              || (!d_solution.isNull()
+                  && d_tds->getSygusTermSize(vcc) < sol_term_size)))
       {
         Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
                            << std::endl;
         Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
-        vc = vcc;
+        d_solution = vcc;
+        sol_term_size = d_tds->getSygusTermSize(vcc);
       }
       else if (!d_sol_cons_nondet)
       {
         break;
       }
     }
-    if (!vc.isNull())
+    if (!d_solution.isNull())
     {
-      d_solution = vc;
-      return vc;
+      return d_solution;
     }
     Trace("sygus-pbe") << "...failed to solve." << std::endl;
   }
@@ -834,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;
@@ -855,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)
     {
@@ -870,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))
@@ -966,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;
     }
   }
@@ -1150,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;
@@ -1205,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
@@ -1229,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;
@@ -1238,15 +1247,31 @@ Node SygusUnifIo::constructSol(
   {
     std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
   }
-  // TODO: ITE always first, if possible
-  
-  
+  // ITE always first if we have not yet solved
+  // 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())
+  {
+    for (unsigned i = 0; i < snode.d_strats.size(); i++)
+    {
+      if (snode.d_strats[i]->d_this == strat_ITE)
+      {
+        // flip the two
+        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);
@@ -1290,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,
@@ -1314,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];
@@ -1327,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;
@@ -1437,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
@@ -1480,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 90612cfaf..35306de01 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -2,9 +2,9 @@
 /*! \file sygus_unif_io.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -310,6 +310,8 @@ class SygusUnifIo : public SygusUnif
    * register a new value for an enumerator.
    */
   bool d_check_sol;
+  /** whether we have solved the overall conjecture */
+  bool d_solved;
   /** The number of values we have enumerated for all enumerators. */
   unsigned d_cond_count;
   /** The solution for the function of this class, if one has been found */
@@ -413,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 f23e4318a..883aae070 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_unif_strat.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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 7431136ac..930ccd65f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -2,9 +2,9 @@
 /*! \file sygus_unif_strat.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -93,6 +93,8 @@ std::ostream& operator<<(std::ostream& os, StrategyType st);
 class UnifContext
 {
  public:
+  virtual ~UnifContext() {}
+
   /** Get the current role
    *
    * In a particular context when constructing solutions in synthesis by
@@ -324,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 14941520f..5e2187e7a 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -2,9 +2,9 @@
 /*! \file term_database_sygus.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -15,7 +15,9 @@
 #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"
@@ -362,11 +364,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 +1041,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 +1319,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 +1411,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;
-        
+
       }
     }
   }
@@ -1750,14 +1763,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
     }
     if (!res.isNull())
     {
-      /*
-      std::cout << bn << std::endl;
-      std::cout << res << std::endl;
-      std::cout << Rewriter::rewrite(bn.substitute(it->second.begin(),
-                                                it->second.end(),
-                                                args.begin(),
-                                                args.end())) << std::endl;
-                                                */
       Assert(res
              == Rewriter::rewrite(bn.substitute(it->second.begin(),
                                                 it->second.end(),
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index a51de1b1f..5b528e7ed 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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 );