Add option to only dump unsolved queries for --sygus-query-gen (#3173)

4 files changed, 63 insertions, 5 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index b0a1cd1ad..874c57629 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -504,6 +504,21 @@ trust  \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_sygusQueryDumpFileHelp =
+    "\
+Query file options supported by --sygus-query-gen-dump-files:\n\
+\n\
+none (default) \n\
++ Do not dump query files when using --sygus-query-gen.\n\
+\n\
+all \n\
++ Dump all query files.\n\
+\n\
+unsolved \n\
++ Dump query files that the subsolver did not solve.\n\
+\n\
+";
+
 const std::string OptionsHandler::s_sygusFilterSolHelp =
     "\
 Modes for filtering sygus solutions supported by --sygus-filter-sol:\n\
@@ -959,6 +974,34 @@ theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode(
   }
 }
 
+theory::quantifiers::SygusQueryDumpFilesMode
+OptionsHandler::stringToSygusQueryDumpFilesMode(std::string option,
+                                                std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return theory::quantifiers::SYGUS_QUERY_DUMP_NONE;
+  }
+  else if (optarg == "all")
+  {
+    return theory::quantifiers::SYGUS_QUERY_DUMP_ALL;
+  }
+  else if (optarg == "unsolved")
+  {
+    return theory::quantifiers::SYGUS_QUERY_DUMP_UNSOLVED;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_sygusQueryDumpFileHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(
+        std::string("unknown option for --sygus-query-gen-dump-files: `")
+        + optarg + "'.  Try --sygus-query-gen-dump-files help.");
+  }
+}
 theory::quantifiers::SygusFilterSolMode
 OptionsHandler::stringToSygusFilterSolMode(std::string option,
                                            std::string optarg)
@@ -977,7 +1020,7 @@ OptionsHandler::stringToSygusFilterSolMode(std::string option,
   }
   else if (optarg == "help")
   {
-    puts(s_cegisSampleHelp.c_str());
+    puts(s_sygusFilterSolHelp.c_str());
     exit(1);
   }
   else
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 9a596ddfc..84b7002e3 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -114,6 +114,8 @@ public:
       std::string option, std::string optarg);
   theory::quantifiers::CegisSampleMode stringToCegisSampleMode(
       std::string option, std::string optarg);
+  theory::quantifiers::SygusQueryDumpFilesMode stringToSygusQueryDumpFilesMode(
+      std::string option, std::string optarg);
   theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode(
       std::string option, std::string optarg);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(
@@ -269,6 +271,7 @@ public:
   static const std::string s_cegqiSingleInvHelp;
   static const std::string s_cegqiSingleInvRconsHelp;
   static const std::string s_cegisSampleHelp;
+  static const std::string s_sygusQueryDumpFileHelp;
   static const std::string s_sygusFilterSolHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_sygusActiveGenHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index c9aeda154..049cdef1c 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -272,6 +272,16 @@ enum SygusActiveGenMode
   SYGUS_ACTIVE_GEN_AUTO,
 };
 
+enum SygusQueryDumpFilesMode
+{
+  /** do not dump query files */
+  SYGUS_QUERY_DUMP_NONE,
+  /** dump all query files */
+  SYGUS_QUERY_DUMP_ALL,
+  /** dump query files that were not solved by the subsolver */
+  SYGUS_QUERY_DUMP_UNSOLVED,
+};
+
 enum SygusFilterSolMode
 {
   /** do not filter solutions */
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 8792fb56b..717ee9dae 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1414,10 +1414,12 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "sygusQueryGenDumpFiles"
   category   = "regular"
-  long       = "sygus-query-gen-dump-files"
-  type       = "bool"
-  default    = "false"
-  help       = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen"
+  long       = "sygus-query-gen-dump-files=MODE"
+  type       = "CVC4::theory::quantifiers::SygusQueryDumpFilesMode"
+  default    = "CVC4::theory::quantifiers::SYGUS_QUERY_DUMP_NONE"
+  handler    = "stringToSygusQueryDumpFilesMode"
+  includes   = ["options/quantifiers_modes.h"]
+  help       = "mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen"
 
 [[option]]
   name       = "sygusFilterSolMode"