Format

8 files changed, 92 insertions, 59 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 1606a462c..09b4d4850 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -492,7 +492,8 @@ all \n\
 \n\
 ";
 
-const std::string OptionsHandler::s_cegqiSingleInvRconsHelp = "\
+const std::string OptionsHandler::s_cegqiSingleInvRconsHelp =
+    "\
 Modes for reconstruction solutions while using single invocation techniques, supported by --cegqi-si-rcons:\n\
 \n\
 none \n\
@@ -915,20 +916,29 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option,
 
 theory::quantifiers::CegqiSingleInvRconsMode
 OptionsHandler::stringToCegqiSingleInvRconsMode(std::string option,
-                                           std::string optarg)
+                                                std::string optarg)
 {
-  if(optarg == "none" ) {
+  if (optarg == "none")
+  {
     return theory::quantifiers::CEGQI_SI_RCONS_MODE_NONE;
-  } else if(optarg == "try") {
+  }
+  else if (optarg == "try")
+  {
     return theory::quantifiers::CEGQI_SI_RCONS_MODE_TRY;
-  } else if(optarg == "all") {
+  }
+  else if (optarg == "all")
+  {
     return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL;
-  } else if(optarg ==  "help") {
+  }
+  else if (optarg == "help")
+  {
     puts(s_cegqiSingleInvRconsHelp.c_str());
     exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --cegqi-si-rcons: `") +
-                          optarg + "'.  Try --cegqi-si-rcons help.");
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --cegqi-si-rcons: `")
+                          + optarg + "'.  Try --cegqi-si-rcons help.");
   }
 }
 
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 1bbad28bd..2275705fb 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -216,24 +216,25 @@ enum CegqiSingleInvMode {
   CEGQI_SI_MODE_ALL,
 };
 
-/** Solution reconstruction modes for single invocation conjectures 
- * 
+/** Solution reconstruction modes for single invocation conjectures
+ *
  * These modes indicate the policy when CVC4 solves a synthesis conjecture using
  * single invocation techniques for a sygus problem with a user-specified
  * grammar.
  */
-enum CegqiSingleInvRconsMode {
-  /** 
+enum CegqiSingleInvRconsMode
+{
+  /**
    * Do not try to reconstruct solutions to single invocation conjectures. With
-   * this mode, solutions produced by CVC4 may violate grammar restrictions. 
+   * this mode, solutions produced by CVC4 may violate grammar restrictions.
    */
   CEGQI_SI_RCONS_MODE_NONE,
-  /** 
-   * Try to reconstruct solution to single invocation conjectures in an 
-   * incomplete (fail fast) way. 
+  /**
+   * Try to reconstruct solution to single invocation conjectures in an
+   * incomplete (fail fast) way.
    */
   CEGQI_SI_RCONS_MODE_TRY,
-  /** 
+  /**
    * Reconsturct solutions to single invocation conjectures. This method
    * relies on an expensive enumeration technique which only terminate when
    * we succesfully reconstruct the solution, although it may not terminate.
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index b6b24a3ff..2ff8ae701 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -568,10 +568,14 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
-  if( options::cegqiSingleInvReconstruct()!=CEGQI_SI_RCONS_MODE_NONE && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus ){
+  if (options::cegqiSingleInvReconstruct() != CEGQI_SI_RCONS_MODE_NONE
+      && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus)
+  {
     d_sol->preregisterConjecture( d_orig_conjecture );
-    bool tryEnum = options::cegqiSingleInvReconstruct()==CEGQI_SI_RCONS_MODE_ALL;
-    d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed, tryEnum );
+    bool tryEnum =
+        options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_ALL;
+    d_sygus_solution =
+        d_sol->reconstructSolution(s, stn, reconstructed, tryEnum);
     if( reconstructed==1 ){
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
     }
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 1ca4b1932..321071272 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -639,7 +639,11 @@ void CegConjectureSingleInvSol::preregisterConjecture( Node q ) {
   registerEquivalentTerms( n );
 }
 
-Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed, bool tryEnum ) {
+Node CegConjectureSingleInvSol::reconstructSolution(Node sol,
+                                                    TypeNode stn,
+                                                    int& reconstructed,
+                                                    bool tryEnum)
+{
   Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
   int status;
   d_root_id = collectReconstructNodes( sol, stn, status );
@@ -650,22 +654,31 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
     reconstructed = 1;
     return ret;
   }
-  //Trace("csi-debug-sol") << "Induced solution template is : " << d_templ_solution << std::endl;
-  if( Trace.isOn("csi-rcons") ){
-    for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
+  if (Trace.isOn("csi-rcons"))
+  {
+    for (std::map<TypeNode, std::map<Node, int> >::iterator it =
+             d_rcons_to_id.begin();
+         it != d_rcons_to_id.end();
+         ++it)
+    {
       TypeNode tn = it->first;
-      Assert( tn.isDatatype() );
+      Assert(tn.isDatatype());
       const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-      Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl;
-      for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        if( d_reconstruct.find( it2->second )==d_reconstruct.end() ){
+      Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName()
+                         << " : " << std::endl;
+      for (std::map<Node, int>::iterator it2 = it->second.begin();
+           it2 != it->second.end();
+           ++it2)
+      {
+        if (d_reconstruct.find(it2->second) == d_reconstruct.end())
+        {
           Trace("csi-rcons") << "  " << it2->first << std::endl;
         }
       }
-      Assert( !it->second.empty() );
+      Assert(!it->second.empty());
     }
   }
-  if( tryEnum )
+  if (tryEnum)
   {
     unsigned index = 0;
     std::map< TypeNode, bool > active;
@@ -719,7 +732,8 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
 
   // we ran out of elements, return null
   reconstructed = -1;
-  Warning() << CommandFailure("Cannot get synth function: reconstruction to syntax failed.");
+  Warning() << CommandFailure(
+      "Cannot get synth function: reconstruction to syntax failed.");
   // could return sol here, however, we choose to fail by returning null, since
   // it indicates a failure.
   return Node::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 858b7f67a..32870a420 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -67,13 +67,16 @@ private:
    * Returns (if possible) a node that is equivalent to sol those syntax
    * matches the grammar corresponding to sygus datatype stn.
    * The value reconstructed is set to 1 if we successfully return a node,
-   * otherwise it is set to -1. 
-   * 
+   * otherwise it is set to -1.
+   *
    * This method quickly tries to match sol to the grammar induced by stn. If
-   * this fails and tryEnum is true, we use non-terminating enumerative 
+   * this fails and tryEnum is true, we use non-terminating enumerative
    * techniques to try to repair the solution.
    */
-  Node reconstructSolution(Node sol, TypeNode stn, int& reconstructed, bool tryEnum);
+  Node reconstructSolution(Node sol,
+                           TypeNode stn,
+                           int& reconstructed,
+                           bool tryEnum);
   /** preregister conjecture
    *
    * q : the synthesis conjecture this class is for.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 81784d27e..957c4acad 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -198,7 +198,7 @@ Node CegGrammarConstructor::process(Node q,
   std::vector<Node> qchildren;
   Node qbody_subs = q[1];
   std::map<Node, Node> synth_fun_vars;
-  TermDbSygus * tds = d_qe->getTermDatabaseSygus();
+  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
   {
     Node sf = q[0][i];
@@ -246,42 +246,42 @@ Node CegGrammarConstructor::process(Node q,
         Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
       }
     }
-    tds->registerSygusType( tn );
-    Assert( tn.isDatatype() );
+    tds->registerSygusType(tn);
+    Assert(tn.isDatatype());
     const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-    Assert( dt.isSygus() );
+    Assert(dt.isSygus());
     // check grammar restrictions
     if (!tds->hasKind(tn, ITE))
     {
       d_has_ite = false;
-      // can maybe (fully) simulate the ITE 
-      if( tds->sygusToBuiltinType( tn ).isBoolean() )
+      // can maybe (fully) simulate the ITE
+      if (tds->sygusToBuiltinType(tn).isBoolean())
       {
         // if it has a recursive AND or OR, and NOT.
         bool success = true;
-        for( unsigned j=0; j<3; j++ )
+        for (unsigned j = 0; j < 3; j++)
         {
-          Assert( success );
-          Kind k = i==0 ? NOT : ( i==1 ? AND : OR );
+          Assert(success);
+          Kind k = i == 0 ? NOT : (i == 1 ? AND : OR);
           // do we have the required kind?
-          int cn = tds->getKindConsNum(tn,k);
-          success = cn>=0;
-          if( success )
+          int cn = tds->getKindConsNum(tn, k);
+          success = cn >= 0;
+          if (success)
           {
             // check whether we are recursive on types
-            for( unsigned a=0, nargs=dt[cn].getNumArgs(); a<nargs; a++ )
+            for (unsigned a = 0, nargs = dt[cn].getNumArgs(); a < nargs; a++)
             {
               TypeNode tna = TypeNode::fromType(dt[cn].getArgType(a));
-              if( tna!=tn )
+              if (tna != tn)
               {
                 success = false;
                 break;
               }
             }
           }
-          if( !success )
+          if (!success)
           {
-            if( j!=1 )
+            if (j != 1)
             {
               break;
             }
@@ -289,7 +289,7 @@ Node CegGrammarConstructor::process(Node q,
             success = true;
           }
         }
-        if( success )
+        if (success)
         {
           d_has_ite = true;
         }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index c32ce2471..416e9825b 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -867,10 +867,10 @@ void TermDbSygus::registerEnumerator(Node e,
   d_enum_to_using_sym_cons[e] = useSymbolicCons;
   // depending on if we are using symbolic constructors, introduce symmetry
   // breaking lemma templates for each relevant subtype of the grammar
-  std::vector< TypeNode > sf_types;
-  getSubfieldTypes(et,sf_types);
+  std::vector<TypeNode> sf_types;
+  getSubfieldTypes(et, sf_types);
   // for each type of subfield type of this enumerator
-  for( unsigned i=0, ntypes = sf_types.size(); i<ntypes; i++ )
+  for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
   {
     std::vector<unsigned> rm_indices;
     TypeNode stn = sf_types[i];
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 00f8a9a8b..9ebf6182b 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -341,14 +341,15 @@ class TermDbSygus {
   unsigned getMinConsTermSize( TypeNode tn, unsigned cindex );
   /** get the weight of the selector, where tn is the domain of sel */
   unsigned getSelectorWeight(TypeNode tn, Node sel);
-  /** get subfield types 
-   * 
+  /** get subfield types
+   *
    * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
-   * type of tn if there exists a selector chain S1( ... Sn( x )...) that has 
+   * type of tn if there exists a selector chain S1( ... Sn( x )...) that has
    * type tnc, where x has type tn. In other words, tnc is the type of some
    * subfield of terms of type tn, at any depth.
    */
   void getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types);
+
  public:
   int getKindConsNum( TypeNode tn, Kind k );
   int getConstConsNum( TypeNode tn, Node n );