sygusComp2018: update policies for solution reconstruction (#2109)

4 files changed, 119 insertions, 15 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2b1d72802..8f179531b 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -489,6 +489,30 @@ all \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_cegqiSingleInvRconsHelp =
+    "\
+Modes for reconstruction solutions while using single invocation techniques,\
+supported by --cegqi-si-rcons:\n\
+\n\
+none \n\
++ Do not try to reconstruct solutions in the original (user-provided) grammar\
+  when using single invocation techniques. In this mode, solutions produced by\
+  CVC4 may violate grammar restrictions.\n\
+\n\
+try \n\
++ Try to reconstruct solutions in the original grammar when using single\
+  invocation techniques in an incomplete (fail-fast) manner.\n\
+\n\
+all-limit \n\
++ Try to reconstruct solutions in the original grammar, but termintate if a\
+  maximum number of rounds for reconstruction is exceeded.\n\
+\n\
+all \n\
++ Try to reconstruct solutions in the original grammar. In this mode,\
+  we do not terminate until a solution is successfully reconstructed. \n\
+\n\
+";
+
 const std::string OptionsHandler::s_cegisSampleHelp =
     "\
 Modes for sampling with counterexample-guided inductive synthesis (CEGIS),\
@@ -878,8 +902,6 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option,
     return theory::quantifiers::CEGQI_SI_MODE_NONE;
   } else if(optarg == "use" || optarg == "default") {
     return theory::quantifiers::CEGQI_SI_MODE_USE;
-  } else if(optarg == "all-abort") {
-    return theory::quantifiers::CEGQI_SI_MODE_ALL_ABORT;
   } else if(optarg == "all") {
     return theory::quantifiers::CEGQI_SI_MODE_ALL;
   } else if(optarg ==  "help") {
@@ -891,6 +913,38 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option,
   }
 }
 
+theory::quantifiers::CegqiSingleInvRconsMode
+OptionsHandler::stringToCegqiSingleInvRconsMode(std::string option,
+                                                std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return theory::quantifiers::CEGQI_SI_RCONS_MODE_NONE;
+  }
+  else if (optarg == "try")
+  {
+    return theory::quantifiers::CEGQI_SI_RCONS_MODE_TRY;
+  }
+  else if (optarg == "all")
+  {
+    return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL;
+  }
+  else if (optarg == "all-limit")
+  {
+    return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT;
+  }
+  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.");
+  }
+}
+
 theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode(
     std::string option, std::string optarg)
 {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 4cdd445ed..ab107ae78 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -108,6 +108,8 @@ public:
       std::string option, std::string optarg);
   theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(
       std::string option, std::string optarg);
+  theory::quantifiers::CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode(
+      std::string option, std::string optarg);
   theory::quantifiers::CegisSampleMode stringToCegisSampleMode(
       std::string option, std::string optarg);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(
@@ -245,6 +247,7 @@ public:
   static const std::string s_sygusSolutionOutModeHelp;
   static const std::string s_cbqiBvIneqModeHelp;
   static const std::string s_cegqiSingleInvHelp;
+  static const std::string s_cegqiSingleInvRconsHelp;
   static const std::string s_cegisSampleHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_termDbModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index a949b97be..afb54002c 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -208,12 +208,41 @@ enum CegqiSingleInvMode {
   CEGQI_SI_MODE_NONE,
   /** use single invocation techniques */
   CEGQI_SI_MODE_USE,
-  /** always use single invocation techniques, abort if solution reconstruction will fail */
-  CEGQI_SI_MODE_ALL_ABORT,
   /** always use single invocation techniques */
   CEGQI_SI_MODE_ALL,
 };
 
+/** 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
+{
+  /**
+   * Do not try to reconstruct solutions to single invocation conjectures. With
+   * 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.
+   */
+  CEGQI_SI_RCONS_MODE_TRY,
+  /**
+   * Reconstruct solutions to single invocation conjectures, but fail if we
+   * reach an upper limit on number of iterations in the enumeration
+   */
+  CEGQI_SI_RCONS_MODE_ALL_LIMIT,
+  /**
+   * Reconstruct solutions to single invocation conjectures. This method
+   * relies on an expensive enumeration technique which only terminates when
+   * we succesfully reconstruct the solution, although it may not terminate.
+   */
+  CEGQI_SI_RCONS_MODE_ALL,
+};
+
 enum CegisSampleMode
 {
   /** do not use samples for CEGIS */
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index ecdf87a47..bf514ada7 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -917,11 +917,30 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "cegqiSingleInvReconstruct"
   category   = "regular"
-  long       = "cegqi-si-reconstruct"
+  long       = "cegqi-si-rcons=MODE"
+  type       = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode"
+  default    = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT"
+  handler    = "stringToCegqiSingleInvRconsMode"
+  includes   = ["options/quantifiers_modes.h"]
+  help       = "policy for reconstructing solutions for single invocation conjectures"
+
+[[option]]
+  name       = "cegqiSingleInvReconstructLimit"
+  category   = "regular"
+  long       = "cegqi-si-rcons-limit=N"
+  type       = "int"
+  default    = "10000"
+  read_only  = true
+  help       = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)"
+
+[[option]]
+  name       = "cegqiSingleInvReconstructConst"
+  category   = "regular"
+  long       = "cegqi-si-reconstruct-const"
   type       = "bool"
   default    = "true"
   read_only  = true
-  help       = "reconstruct solutions for single invocation conjectures in original grammar"
+  help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
 
 [[option]]
   name       = "cegqiSolMinCore"
@@ -942,15 +961,6 @@ header = "options/quantifiers_options.h"
   help       = "minimize individual instantiations for single invocation conjectures based on unsat core"
 
 [[option]]
-  name       = "cegqiSingleInvReconstructConst"
-  category   = "regular"
-  long       = "cegqi-si-reconstruct-const"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
-
-[[option]]
   name       = "cegqiSingleInvAbort"
   category   = "regular"
   long       = "cegqi-si-abort"
@@ -1119,6 +1129,14 @@ header = "options/quantifiers_options.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"
+  
+[[option]]
   name       = "sygusEvalOpt"
   category   = "regular"
   long       = "sygus-eval-opt"