More fixes and improvements for query generator (#7988)

Includes proper printing of dumped benchmarks.

diff --git a/src/smt/print_benchmark.cpp b/src/smt/print_benchmark.cpp
index 778a431ab3f622556a6bd43f86fb29b7c0ad3541..e16b661399627047b688559a7d1410a9171fe8df 100644 (file)
--- a/src/smt/print_benchmark.cpp
+++ b/src/smt/print_benchmark.cpp
@@ -36,6 +36,7 @@ void PrintBenchmark::printAssertions(std::ostream& out,
   }
   for (const Node& a : assertions)
   {
+    Assert(!expr::hasFreeVar(a));
     expr::getTypes(a, types, typeVisited);
   }
   // print the declared types first

diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 05cc4c46b5888e01f59626f6ec248a7bd8647d95..d9e6954f64b5b5a9ab7853f4e73edaf525168648 100644 (file)
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -20,6 +20,8 @@
 #include <sstream>
 
 #include "options/quantifiers_options.h"
+#include "smt/env.h"
+#include "smt/print_benchmark.h"
 #include "util/random.h"
 
 using namespace std;
@@ -167,7 +169,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex, std::ostream& out)
   if (options().quantifiers.sygusQueryGenDumpFiles
       == options::SygusQueryDumpFilesMode::ALL)
   {
-    dumpQuery(qy, spIndex);
+    dumpQuery(qy);
   }
 
   if (options().quantifiers.sygusQueryGenCheck)
@@ -199,7 +201,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex, std::ostream& out)
     {
       if (r.asSatisfiabilityResult().isSat() != Result::SAT)
       {
-        dumpQuery(qy, spIndex);
+        dumpQuery(qy);
       }
     }
   }
@@ -207,36 +209,15 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex, std::ostream& out)
   d_queryCount++;
 }
 
-void QueryGenerator::dumpQuery(Node qy, unsigned spIndex)
+void QueryGenerator::dumpQuery(Node qy)
 {
-  // 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());
+  Node kqy = convertToSkolem(qy);
+  // Print the query to to queryN.smt2
   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;
+  smt::PrintBenchmark pb(&d_env.getPrinter());
+  pb.printBenchmark(fs, d_env.getLogicInfo().getLogicString(), {}, {kqy});
   fs.close();
 }
 

diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h
index 75045958879f319fa9cff63ec14aa0fb4c5c994d..38c99b6f99e242e8b28f8351d6868c50d30dadc2 100644 (file)
--- a/src/theory/quantifiers/query_generator.h
+++ b/src/theory/quantifiers/query_generator.h
@@ -111,10 +111,9 @@ class QueryGenerator : public ExprMiner
    */
   void checkQuery(Node qy, unsigned spIndex, std::ostream& out);
   /**
-   * Dumps query qy to the a file queryN.smt2 for the current counter N;
-   * spIndex specifies the sample point that satisfies it (for debugging).
+   * Dumps query qy to the a file queryN.smt2 for the current counter N
    */
-  void dumpQuery(Node qy, unsigned spIndex);
+  void dumpQuery(Node qy);
 };
 
 }  // namespace quantifiers