Min synth sol option.

5 files changed, 19 insertions, 13 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 466a1a3de..877af3967 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1142,6 +1142,14 @@ header = "options/quantifiers_options.h"
   includes   = ["options/quantifiers_modes.h"]
   help       = "mode for using samples in the counterexample-guided inductive synthesis loop"
 
+[[option]]
+  name       = "minSynthSol"
+  category   = "regular"
+  long       = "min-synth-sol"
+  type       = "bool"
+  default    = "true"
+  help       = "Minimize synthesis solutions"
+
 # Internal uses of sygus
 
 [[option]]
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9ae1fb062..c28a3c30e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1315,6 +1315,12 @@ void SmtEngine::setDefaults() {
     {
       options::cbqiMidpoint.set(true);
     }
+    if( options::sygusRepairConst() )
+    {
+      if( !options::cbqi.wasSetByUser() ){
+        options::cbqi.set( true );
+      }
+    }
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index d4547ca7d..f279b4ff4 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -727,7 +727,6 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         out << dt.getSygusType() << " ";
         if (status == 0)
         {
-          sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
           out << sol;
         }
         else
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index e10219fdd..b2c5c6ee7 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -458,13 +459,6 @@ struct sortSiInstanceIndices {
 
 
 Node CegConjectureSingleInv::postProcessSolution( Node n ){
-  ////remove boolean ITE (not allowed for sygus comp 2015)
-  //if( n.getKind()==ITE && n.getType().isBoolean() ){
-  //  Node n1 = postProcessSolution( n[1] );
-  //  Node n2 = postProcessSolution( n[2] );
-  //  return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ),
-  //                                               NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) );
-  //}else{
   bool childChanged = false;
   Kind k = n.getKind();
   if( n.getKind()==INTS_DIVISION_TOTAL ){
@@ -488,7 +482,6 @@ Node CegConjectureSingleInv::postProcessSolution( Node n ){
   }else{
     return n;
   }
-  //}
 }
 
 
@@ -582,6 +575,10 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   }else{
     Trace("csi-sol") << "Post-process solution..." << std::endl;
     Node prev = d_solution;
+    if( options::minSynthSol() )
+    {
+      d_solution = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(d_solution);
+    }
     d_solution = postProcessSolution( d_solution );
     if( prev!=d_solution ){
       Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl;
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 83fb6f253..2b17d6d79 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -474,10 +474,6 @@ void CegisUnifEnumManager::incrementNumEnumerators()
                                  << " to strategy point " << ci.second.d_pt
                                  << "\n";
         d_tds->registerEnumerator(e, ci.second.d_pt, d_parent, false, index==0 ? options::sygusUnifRepairRet() : options::sygusUnifRepairCond());
-        // TODO symmetry breaking for making
-        //   e distinct from ei : (ci.second.d_enums[index] \ {e})
-        // if its respective type has had at least
-        // ci.second.d_enums[index].size() distinct values enumerated
       }
     }
     // register the evaluation points at the new value