From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 25 Jan 2022 17:15:51 +0000 (-0600)
Subject: Fixes and improvements to sygus satisfiable query generation (#7980)
X-Git-Tag: cvc5-1.0.0~508
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b022fb999107870c07fad71944d916cfb6332f41;p=cvc5.git

Fixes and improvements to sygus satisfiable query generation (#7980)

Fixes issues related to the use of partial functions. Also ensures we avoid duplicate queries.
---

diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index c7cc6d442..05cc4c46b 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -69,14 +69,20 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
   {
     std::map<Node, std::vector<unsigned>> ev_to_pt;
     unsigned index = 0;
+    // the number of {true,false} for which the #points evaluated to that
+    // constant is greater than the threshold.
     unsigned threshCount = 0;
     while (index < npts && threshCount < 2)
     {
       Node v = d_sampler->evaluate(nn, index);
-      ev_to_pt[v].push_back(index);
-      if (ev_to_pt[v].size() == d_deqThresh + 1)
+      // it may not evaluate, in which case we ignore the point
+      if (v.isConst())
       {
-        threshCount++;
+        ev_to_pt[v].push_back(index);
+        if (ev_to_pt[v].size() == d_deqThresh + 1)
+        {
+          threshCount++;
+        }
       }
       index++;
     }
@@ -115,10 +121,10 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
     Node qy = queries[i];
     std::vector<unsigned>& tIndices = queriesPtTrue[i];
     // we have an interesting query
-    out << "(query " << qy << ")  ; " << tIndices.size() << "/" << npts
-        << std::endl;
+    Trace("sygus-qgen-debug")
+        << "; " << tIndices.size() << "/" << npts << std::endl;
     AlwaysAssert(!tIndices.empty());
-    checkQuery(qy, tIndices[0]);
+    checkQuery(qy, tIndices[0], out);
     // add information
     for (unsigned& ti : tIndices)
     {
@@ -135,17 +141,28 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
     if (qsi.size() > 1)
     {
       // take two random queries
-      std::shuffle(qsi.begin(), qsi.end(), Random::getRandom());
-      Node qy = nm->mkNode(AND, qsi[0], qsi[1]);
-      checkQuery(qy, i);
+      size_t rindex = Random::getRandom().pick(0, qsi.size() - 1);
+      size_t rindex2 = Random::getRandom().pick(0, qsi.size() - 2);
+      if (rindex2 >= rindex)
+      {
+        rindex2 = rindex2 + 1;
+      }
+      Node qy = nm->mkNode(AND, qsi[rindex], qsi[rindex2]);
+      checkQuery(qy, i, out);
     }
   }
   Trace("sygus-qgen-check") << "...finished." << std::endl;
   return true;
 }
 
-void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
+void QueryGenerator::checkQuery(Node qy, unsigned spIndex, std::ostream& out)
 {
+  if (d_allQueries.find(qy) != d_allQueries.end())
+  {
+    return;
+  }
+  d_allQueries.insert(qy);
+  out << "(query " << qy << ")" << std::endl;
   // external query
   if (options().quantifiers.sygusQueryGenDumpFiles
       == options::SygusQueryDumpFilesMode::ALL)
diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h
index 952966adc..750459588 100644
--- a/src/theory/quantifiers/query_generator.h
+++ b/src/theory/quantifiers/query_generator.h
@@ -102,12 +102,14 @@ class QueryGenerator : public ExprMiner
    * Map from queries to the indices of the points that satisfy them.
    */
   std::map<Node, std::vector<unsigned>> d_qysToPoints;
+  /** Set of all queries generated */
+  std::unordered_set<Node> d_allQueries;
   /**
    * Check query qy, which is satisfied by (at least) sample point spIndex,
    * using a separate copy of the SMT engine. Throws an exception if qy is
    * reported to be unsatisfiable.
    */
-  void checkQuery(Node qy, unsigned spIndex);
+  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).