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

6 files changed, 110 insertions, 35 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"
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index bc7538c1f..742b3000b 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -146,37 +146,9 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
 void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
 {
   // external query
-  if (options::sygusQueryGenDumpFiles())
+  if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_ALL)
   {
-    // Print the query and the query + its model (commented) to queryN.smt2
-    std::vector<Node> pt;
-    d_sampler->getSamplePoint(spIndex, pt);
-    unsigned nvars = d_vars.size();
-    AlwaysAssert(pt.size() == d_vars.size());
-    std::stringstream fname;
-    fname << "query" << d_queryCount << ".smt2";
-    std::ofstream fs(fname.str(), std::ofstream::out);
-    fs << "(set-logic ALL)" << std::endl;
-    for (unsigned i = 0; i < 2; i++)
-    {
-      for (unsigned j = 0; j < nvars; j++)
-      {
-        Node x = d_vars[j];
-        if (i == 0)
-        {
-          fs << "(declare-fun " << x << " () " << x.getType() << ")";
-        }
-        else
-        {
-          fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j]
-             << ")";
-        }
-        fs << std::endl;
-      }
-    }
-    fs << "(assert " << qy << ")" << std::endl;
-    fs << "(check-sat)" << std::endl;
-    fs.close();
+    dumpQuery(qy, spIndex);
   }
 
   if (options::sygusQueryGenCheck())
@@ -207,11 +179,51 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
       ss << "but CVC4 answered unsat!" << std::endl;
       AlwaysAssert(false, ss.str().c_str());
     }
+    if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_UNSOLVED)
+    {
+      if (r.asSatisfiabilityResult().isSat() != Result::SAT)
+      {
+        dumpQuery(qy, spIndex);
+      }
+    }
   }
 
   d_queryCount++;
 }
 
+void QueryGenerator::dumpQuery(Node qy, unsigned spIndex)
+{
+  // Print the query and the query + its model (commented) to queryN.smt2
+  std::vector<Node> pt;
+  d_sampler->getSamplePoint(spIndex, pt);
+  size_t nvars = d_vars.size();
+  AlwaysAssert(pt.size() == d_vars.size());
+  std::stringstream fname;
+  fname << "query" << d_queryCount << ".smt2";
+  std::ofstream fs(fname.str(), std::ofstream::out);
+  fs << "(set-logic ALL)" << std::endl;
+  for (unsigned i = 0; i < 2; i++)
+  {
+    for (size_t j = 0; j < nvars; j++)
+    {
+      Node x = d_vars[j];
+      if (i == 0)
+      {
+        fs << "(declare-fun " << x << " () " << x.getType() << ")";
+      }
+      else
+      {
+        fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j]
+           << ")";
+      }
+      fs << std::endl;
+    }
+  }
+  fs << "(assert " << qy << ")" << std::endl;
+  fs << "(check-sat)" << std::endl;
+  fs.close();
+}
+
 void QueryGenerator::findQueries(
     Node n,
     std::vector<Node>& queries,
diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h
index 749c78c85..8cb7b2785 100644
--- a/src/theory/quantifiers/query_generator.h
+++ b/src/theory/quantifiers/query_generator.h
@@ -107,6 +107,11 @@ class QueryGenerator : public ExprMiner
    * reported to be unsatisfiable.
    */
   void checkQuery(Node qy, unsigned spIndex);
+  /**
+   * Dumps query qy to the a file queryN.smt2 for the current counter N;
+   * spIndex specifies the sample point that satisfies it (for debugging).
+   */
+  void dumpQuery(Node qy, unsigned spIndex);
 };
 
 }  // namespace quantifiers