Sygus query generator (#2465)

9 files changed, 621 insertions, 3 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e353d53c5..676943b11 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -512,6 +512,8 @@ libcvc4_add_sources(
   theory/quantifiers/quantifiers_attributes.h
   theory/quantifiers/quantifiers_rewriter.cpp
   theory/quantifiers/quantifiers_rewriter.h
+  theory/quantifiers/query_generator.cpp
+  theory/quantifiers/query_generator.h
   theory/quantifiers/relevant_domain.cpp
   theory/quantifiers/relevant_domain.h
   theory/quantifiers/rewrite_engine.cpp
diff --git a/src/Makefile.am b/src/Makefile.am
index 8c1c0871d..d29dcd172 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -524,6 +524,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/quantifiers_attributes.h \
 	theory/quantifiers/quantifiers_rewriter.cpp \
 	theory/quantifiers/quantifiers_rewriter.h \
+	theory/quantifiers/query_generator.cpp \
+	theory/quantifiers/query_generator.h \
 	theory/quantifiers/relevant_domain.cpp \
 	theory/quantifiers/relevant_domain.h \
 	theory/quantifiers/rewrite_engine.cpp \
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 07c11d73a..1c2405449 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1364,6 +1364,38 @@ header = "options/quantifiers_options.h"
   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
 
 [[option]]
+  name       = "sygusQueryGen"
+  category   = "regular"
+  long       = "sygus-query-gen"
+  type       = "bool"
+  default    = "false"
+  help       = "use sygus to enumerate interesting satisfiability queries"
+
+[[option]]
+  name       = "sygusQueryGenThresh"
+  category   = "regular"
+  long       = "sygus-query-gen-thresh=N"
+  type       = "unsigned"
+  default    = "5"
+  help       = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen"
+
+[[option]]
+  name       = "sygusQueryGenCheck"
+  category   = "regular"
+  long       = "sygus-query-gen-check"
+  type       = "bool"
+  default    = "true"
+  help       = "use interesting satisfiability queries to check soundness of CVC4"
+
+[[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"
+
+[[option]]
   name       = "sygusExprMinerCheckUseExport"
   category   = "expert"
   long       = "sygus-expr-miner-check-use-export"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 38c9e7ee2..196da6b9c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1876,7 +1876,8 @@ void SmtEngine::setDefaults() {
         options::sygusExtRew.set(false);
       }
     }
-    if (options::sygusRewSynth() || options::sygusRewVerify())
+    if (options::sygusRewSynth() || options::sygusRewVerify()
+        || options::sygusQueryGen())
     {
       // rewrite rule synthesis implies that sygus stream must be true
       options::sygusStream.set(true);
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp
index 8c116781d..010b5a4ab 100644
--- a/src/theory/quantifiers/expr_miner_manager.cpp
+++ b/src/theory/quantifiers/expr_miner_manager.cpp
@@ -13,6 +13,7 @@
  **/
 
 #include "theory/quantifiers/expr_miner_manager.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -20,6 +21,7 @@ namespace quantifiers {
 
 ExpressionMinerManager::ExpressionMinerManager()
     : d_doRewSynth(false),
+      d_doQueryGen(false),
       d_use_sygus_type(false),
       d_qe(nullptr),
       d_tds(nullptr)
@@ -32,6 +34,7 @@ void ExpressionMinerManager::initialize(const std::vector<Node>& vars,
                                         bool unique_type_ids)
 {
   d_doRewSynth = false;
+  d_doQueryGen = false;
   d_sygus_fun = Node::null();
   d_use_sygus_type = false;
   d_qe = nullptr;
@@ -46,6 +49,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
                                              bool useSygusType)
 {
   d_doRewSynth = false;
+  d_doQueryGen = false;
   d_sygus_fun = f;
   d_use_sygus_type = useSygusType;
   d_qe = qe;
@@ -78,11 +82,45 @@ void ExpressionMinerManager::enableRewriteRuleSynth()
   d_crd.setSilent(false);
 }
 
+void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh)
+{
+  if (d_doQueryGen)
+  {
+    // already enabled
+    return;
+  }
+  d_doQueryGen = true;
+  std::vector<Node> vars;
+  d_sampler.getVariables(vars);
+  // must also enable rewrite rule synthesis
+  if (!d_doRewSynth)
+  {
+    // initialize the candidate rewrite database, in silent mode
+    enableRewriteRuleSynth();
+    d_crd.setSilent(true);
+  }
+  // initialize the query generator
+  d_qg.initialize(vars, &d_sampler);
+  d_qg.setThreshold(deqThresh);
+}
+
 bool ExpressionMinerManager::addTerm(Node sol,
                                      std::ostream& out,
                                      bool& rew_print)
 {
-  return d_crd.addTerm(sol, out, rew_print);
+  bool ret = d_crd.addTerm(sol, out, rew_print);
+  if (ret && d_doQueryGen)
+  {
+    // use the builtin version if d_use_sygus_type is true
+    Node solb = sol;
+    if (d_use_sygus_type)
+    {
+      solb = d_tds->sygusToBuiltin(sol);
+    }
+    // a unique term, let's try the query generator
+    d_qg.addTerm(solb, out);
+  }
+  return ret;
 }
 
 bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out)
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index 668d04beb..d15b69cb5 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -20,6 +20,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers/query_generator.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers_engine.h"
 
@@ -67,6 +68,8 @@ class ExpressionMinerManager
                        bool useSygusType);
   /** enable rewrite rule synthesis (--sygus-rr-synth) */
   void enableRewriteRuleSynth();
+  /** enable query generation (--sygus-query-gen) */
+  void enableQueryGeneration(unsigned deqThresh);
   /** add term
    *
    * Expression miners may print information on the output stream out, for
@@ -84,6 +87,8 @@ class ExpressionMinerManager
  private:
   /** whether we are doing rewrite synthesis */
   bool d_doRewSynth;
+  /** whether we are doing query generation */
+  bool d_doQueryGen;
   /** the sygus function passed to initializeSygus, if any */
   Node d_sygus_fun;
   /** whether we are using sygus types */
@@ -94,6 +99,8 @@ class ExpressionMinerManager
   TermDbSygus* d_tds;
   /** candidate rewrite database */
   CandidateRewriteDatabase d_crd;
+  /** query generator */
+  QueryGenerator d_qg;
   /** sygus sampler object */
   SygusSampler d_sampler;
   /** extended rewriter object */
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
new file mode 100644
index 000000000..e62f3513c
--- /dev/null
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -0,0 +1,416 @@
+/*********************                                                        */
+/*! \file query_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of a class for mining interesting satisfiability
+ ** queries from a stream of generated expressions.
+ **/
+
+#include "theory/quantifiers/query_generator.h"
+
+#include <fstream>
+#include "options/quantifiers_options.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "util/random.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QueryGenerator::QueryGenerator() : d_queryCount(0) {}
+void QueryGenerator::initialize(const std::vector<Node>& vars, SygusSampler* ss)
+{
+  Assert(ss != nullptr);
+  d_queryCount = 0;
+  ExprMiner::initialize(vars, ss);
+}
+
+void QueryGenerator::setThreshold(unsigned deqThresh)
+{
+  d_deqThresh = deqThresh;
+}
+
+bool QueryGenerator::addTerm(Node n, std::ostream& out)
+{
+  Node nn = n.getKind() == NOT ? n[0] : n;
+  if (d_terms.find(nn) != d_terms.end())
+  {
+    return false;
+  }
+  d_terms.insert(nn);
+
+  Trace("sygus-qgen") << "QueryGenerator::addTerm : " << n << std::endl;
+  unsigned npts = d_sampler->getNumSamplePoints();
+  TypeNode tn = n.getType();
+  // TODO : as an optimization, use a shared lazy trie?
+
+  // the queries we generate on this round
+  std::vector<Node> queries;
+  // For each query in the above vector, this stores the indices of the points
+  // for which that query evaluated to true on.
+  std::vector<std::vector<unsigned>> queriesPtTrue;
+  // the sample point indices for which the above queries are true
+  std::unordered_set<unsigned> indices;
+
+  // collect predicate queries (if n is Boolean)
+  if (tn.isBoolean())
+  {
+    std::map<Node, std::vector<unsigned>> ev_to_pt;
+    unsigned index = 0;
+    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)
+      {
+        threshCount++;
+      }
+      index++;
+    }
+    if (threshCount < 2)
+    {
+      for (const std::pair<Node, std::vector<unsigned>>& etp : ev_to_pt)
+      {
+        if (etp.second.size() < d_deqThresh)
+        {
+          indices.insert(etp.second.begin(), etp.second.end());
+          Node qy = nn;
+          Assert(etp.first.isConst());
+          if (!etp.first.getConst<bool>())
+          {
+            qy = qy.negate();
+          }
+          queries.push_back(qy);
+          queriesPtTrue.push_back(etp.second);
+        }
+      }
+    }
+  }
+
+  // collect equality queries
+  findQueries(nn, queries, queriesPtTrue);
+  Assert(queries.size() == queriesPtTrue.size());
+  if (queries.empty())
+  {
+    return true;
+  }
+  Trace("sygus-qgen-debug")
+      << "query: Check " << queries.size() << " queries..." << std::endl;
+  // literal queries
+  for (unsigned i = 0, nqueries = queries.size(); i < nqueries; i++)
+  {
+    Node qy = queries[i];
+    std::vector<unsigned>& tIndices = queriesPtTrue[i];
+    // we have an interesting query
+    out << "(query " << qy << ")  ; " << tIndices.size() << "/" << npts
+        << std::endl;
+    AlwaysAssert(!tIndices.empty());
+    checkQuery(qy, tIndices[0]);
+    // add information
+    for (unsigned& ti : tIndices)
+    {
+      d_ptToQueries[ti].push_back(qy);
+      d_qysToPoints[qy].push_back(ti);
+      indices.insert(ti);
+    }
+  }
+  // for each new index, we may have a new conjunctive query
+  NodeManager* nm = NodeManager::currentNM();
+  for (const unsigned& i : indices)
+  {
+    std::vector<Node>& qsi = d_ptToQueries[i];
+    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);
+    }
+  }
+  Trace("sygus-qgen-check") << "...finished." << std::endl;
+  return true;
+}
+
+void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
+{
+  // external query
+  if (options::sygusQueryGenDumpFiles())
+  {
+    // 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();
+  }
+
+  if (options::sygusQueryGenCheck())
+  {
+    Trace("sygus-qgen-check") << "  query: check " << qy << "..." << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
+    // make the satisfiability query
+    bool needExport = false;
+    ExprManagerMapCollection varMap;
+    ExprManager em(nm->getOptions());
+    std::unique_ptr<SmtEngine> queryChecker;
+    initializeChecker(queryChecker, em, varMap, qy, needExport);
+    Result r = queryChecker->checkSat();
+    Trace("sygus-qgen-check") << "  query: ...got : " << r << std::endl;
+    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
+      std::stringstream ss;
+      ss << "--sygus-rr-query-gen detected unsoundness in CVC4 on input " << qy
+         << "!" << std::endl;
+      ss << "This query has a model : " << std::endl;
+      std::vector<Node> pt;
+      d_sampler->getSamplePoint(spIndex, pt);
+      Assert(pt.size() == d_vars.size());
+      for (unsigned i = 0, size = pt.size(); i < size; i++)
+      {
+        ss << "  " << d_vars[i] << " -> " << pt[i] << std::endl;
+      }
+      ss << "but CVC4 answered unsat!" << std::endl;
+      AlwaysAssert(false, ss.str().c_str());
+    }
+  }
+
+  d_queryCount++;
+}
+
+void QueryGenerator::findQueries(
+    Node n,
+    std::vector<Node>& queries,
+    std::vector<std::vector<unsigned>>& queriesPtTrue)
+{
+  // At a high level, this method traverses the LazyTrie for the type of n
+  // and tries to find paths to leafs that contain terms n' such that n = n'
+  // or n != n' is an interesting query, i.e. satisfied for a small number of
+  // points.
+  TypeNode tn = n.getType();
+  LazyTrie* lt = &d_qgtTrie[tn];
+  // These vectors are the set of indices of sample points for which the current
+  // node we are considering are { equal, disequal } from n.
+  std::vector<unsigned> eqIndex[2];
+  Trace("sygus-qgen-debug") << "Compute queries for " << n << "...\n";
+
+  LazyTrieEvaluator* ev = d_sampler;
+  unsigned ntotal = d_sampler->getNumSamplePoints();
+  unsigned index = 0;
+  bool exact = true;
+  bool pushEq[2] = {false, false};
+  bool pre = true;
+  // The following parallel vectors describe the state of the locations in the
+  // trie we are currently visiting.
+  // Reference to the location in the trie
+  std::vector<LazyTrie*> visitTr;
+  // The index of the sample point we are testing
+  std::vector<unsigned> currIndex;
+  // Whether the path to this location exactly matches the evaluation of n
+  std::vector<bool> currExact;
+  // Whether we are adding to the points that are { equal, disequal } by
+  // traversing to this location.
+  std::vector<bool> pushIndex[2];
+  // Whether we are in a pre-traversal for this location.
+  std::vector<bool> preVisit;
+  visitTr.push_back(lt);
+  currIndex.push_back(0);
+  currExact.push_back(true);
+  pushIndex[0].push_back(false);
+  pushIndex[1].push_back(false);
+  preVisit.push_back(true);
+  do
+  {
+    lt = visitTr.back();
+    index = currIndex.back();
+    exact = currExact.back();
+    for (unsigned r = 0; r < 2; r++)
+    {
+      pushEq[r] = pushIndex[r].back();
+    }
+    pre = preVisit.back();
+    if (!pre)
+    {
+      visitTr.pop_back();
+      currIndex.pop_back();
+      currExact.pop_back();
+      preVisit.pop_back();
+      // clean up the indices of points that are { equal, disequal }
+      for (unsigned r = 0; r < 2; r++)
+      {
+        if (pushEq[r])
+        {
+          eqIndex[r].pop_back();
+        }
+        pushIndex[r].pop_back();
+      }
+    }
+    else
+    {
+      preVisit[preVisit.size() - 1] = false;
+      // add to the indices of points that are { equal, disequal }
+      for (unsigned r = 0; r < 2; r++)
+      {
+        if (pushEq[r])
+        {
+          eqIndex[r].push_back(index - 1);
+        }
+      }
+      int eqAllow = d_deqThresh - eqIndex[0].size();
+      int deqAllow = d_deqThresh - eqIndex[1].size();
+      Trace("sygus-qgen-debug")
+          << "Find queries " << n << " " << index << "/" << ntotal
+          << ", deq/eq allow = " << deqAllow << "/" << eqAllow
+          << ", exact = " << exact << std::endl;
+      if (index == ntotal)
+      {
+        if (exact)
+        {
+          // add to the trie
+          lt->d_lazy_child = n;
+        }
+        else
+        {
+          Node nAlmostEq = lt->d_lazy_child;
+          // if made it here, we still should have either a equality or
+          // a disequality that is allowed.
+          Assert(deqAllow >= 0 || eqAllow >= 0);
+          Node query = n.eqNode(nAlmostEq);
+          std::vector<unsigned> tIndices;
+          if (eqAllow >= 0)
+          {
+            tIndices.insert(
+                tIndices.end(), eqIndex[0].begin(), eqIndex[0].end());
+          }
+          else if (deqAllow >= 0)
+          {
+            query = query.negate();
+            tIndices.insert(
+                tIndices.end(), eqIndex[1].begin(), eqIndex[1].end());
+          }
+          AlwaysAssert(tIndices.size() <= d_deqThresh);
+          if (!tIndices.empty())
+          {
+            queries.push_back(query);
+            queriesPtTrue.push_back(tIndices);
+          }
+        }
+      }
+      else
+      {
+        if (!lt->d_lazy_child.isNull())
+        {
+          // if there is a lazy child here, push
+          Node e_lc = ev->evaluate(lt->d_lazy_child, index);
+          // store at next level
+          lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
+          // replace
+          lt->d_lazy_child = Node::null();
+        }
+        // compute
+        Node e_this = ev->evaluate(n, index);
+
+        if (deqAllow >= 0)
+        {
+          // recursing on disequal points
+          deqAllow--;
+          // if there is use continuing
+          if (deqAllow >= 0 || eqAllow >= 0)
+          {
+            for (std::pair<const Node, LazyTrie>& ltc : lt->d_children)
+            {
+              if (ltc.first != e_this)
+              {
+                visitTr.push_back(&ltc.second);
+                currIndex.push_back(index + 1);
+                currExact.push_back(false);
+                pushIndex[0].push_back(false);
+                pushIndex[1].push_back(true);
+                preVisit.push_back(true);
+              }
+            }
+          }
+          deqAllow++;
+        }
+        bool pushEqNext = false;
+        if (eqAllow >= 0)
+        {
+          // below, we try recursing (if at all) on equal nodes.
+          eqAllow--;
+          pushEqNext = true;
+        }
+        // if we are on the exact path of n
+        if (exact)
+        {
+          if (lt->d_children.empty())
+          {
+            // if no one has been here before, we are done
+            lt->d_lazy_child = n;
+          }
+          else
+          {
+            // otherwise, we recurse on the equal point
+            visitTr.push_back(&(lt->d_children[e_this]));
+            currIndex.push_back(index + 1);
+            currExact.push_back(true);
+            pushIndex[0].push_back(pushEqNext);
+            pushIndex[1].push_back(false);
+            preVisit.push_back(true);
+          }
+        }
+        else if (deqAllow >= 0 || eqAllow >= 0)
+        {
+          // recurse on the equal point if it exists
+          std::map<Node, LazyTrie>::iterator iteq = lt->d_children.find(e_this);
+          if (iteq != lt->d_children.end())
+          {
+            visitTr.push_back(&(iteq->second));
+            currIndex.push_back(index + 1);
+            currExact.push_back(false);
+            pushIndex[0].push_back(pushEqNext);
+            pushIndex[1].push_back(false);
+            preVisit.push_back(true);
+          }
+        }
+      }
+    }
+  } while (!visitTr.empty());
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h
new file mode 100644
index 000000000..f0b3fa565
--- /dev/null
+++ b/src/theory/quantifiers/query_generator.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file query_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class for mining interesting satisfiability queries from a stream
+ ** of generated expressions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+
+#include <map>
+#include <unordered_set>
+#include "expr/node.h"
+#include "theory/quantifiers/expr_miner.h"
+#include "theory/quantifiers/lazy_trie.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** QueryGenerator
+ *
+ * This module is used for finding satisfiable queries that are maximally
+ * likely to trigger an unsound response in an SMT solver. These queries are
+ * mined from a stream of enumerated expressions. We judge likelihood of
+ * triggering unsoundness by the frequency at which the query is satisfied.
+ *
+ * In detail, given a stream of expressions t_1, ..., t_{n-1}, upon generating
+ * term t_n, we consider a query (not) t_n = t_i to be an interesting query
+ * if it is satisfied by at most D points, where D is a predefined threshold
+ * given by options::sygusQueryGenThresh(). If t_n has type Bool, we
+ * additionally consider the case where t_n is satisfied (or not satisfied) by
+ * fewer than D points.
+ *
+ * In addition to generating single literal queries, this module also generates
+ * conjunctive queries, for instance, by remembering that literals L1 and L2
+ * were both satisfied by the same point, and thus L1 ^ L2 is an interesting
+ * query as well.
+ */
+class QueryGenerator : public ExprMiner
+{
+ public:
+  QueryGenerator();
+  ~QueryGenerator() {}
+  /** initialize */
+  void initialize(const std::vector<Node>& vars,
+                  SygusSampler* ss = nullptr) override;
+  /**
+   * Add term to this module. This may trigger the printing and/or checking of
+   * new queries.
+   */
+  bool addTerm(Node n, std::ostream& out) override;
+  /**
+   * Set the threshold value. This is the maximal number of sample points that
+   * each query we generate is allowed to be satisfied by.
+   */
+  void setThreshold(unsigned deqThresh);
+
+ private:
+  /** cache of all terms registered to this generator */
+  std::unordered_set<Node, NodeHashFunction> d_terms;
+  /** the threshold used by this module for maximum number of sat points */
+  unsigned d_deqThresh;
+  /**
+   * For each type, a lazy trie storing the evaluation of all added terms on
+   * sample points.
+   */
+  std::map<TypeNode, LazyTrie> d_qgtTrie;
+  /** total number of queries generated by this class */
+  unsigned d_queryCount;
+  /** find queries
+   *
+   * This function traverses the lazy trie for the type of n, finding equality
+   * and disequality queries between n and other terms in the trie. The argument
+   * queries collects the newly generated queries, and the argument
+   * queriesPtTrue collects the indices of points that each query was satisfied
+   * by (these indices are the indices of the points in the sampler used by this
+   * class).
+   */
+  void findQueries(Node n,
+                   std::vector<Node>& queries,
+                   std::vector<std::vector<unsigned>>& queriesPtTrue);
+  /**
+   * Maps the index of each sample point to the list of queries that it
+   * satisfies, and that were generated by the above function. This map is used
+   * for generating conjunctive queries.
+   */
+  std::map<unsigned, std::vector<Node>> d_ptToQueries;
+  /**
+   * Map from queries to the indices of the points that satisfy them.
+   */
+  std::map<Node, std::vector<unsigned>> d_qysToPoints;
+  /**
+   * 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);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS___H */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 7955d59a8..32342a9ba 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -981,7 +981,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
 
       bool is_unique_term = true;
 
-      if (status != 0 && options::sygusRewSynth())
+      if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen()))
       {
         std::map<Node, ExpressionMinerManager>::iterator its =
             d_exprm.find(prog);
@@ -993,6 +993,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
           {
             d_exprm[prog].enableRewriteRuleSynth();
           }
+          if (options::sygusQueryGen())
+          {
+            d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
+          }
           its = d_exprm.find(prog);
         }
         bool rew_print = false;