Sygus streaming non-implied predicates (#2660)

10 files changed, 224 insertions, 19 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4cf8412f0..10db1dc86 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -522,6 +522,8 @@ libcvc4_add_sources(
   theory/quantifiers/single_inv_partition.h
   theory/quantifiers/skolemize.cpp
   theory/quantifiers/skolemize.h
+  theory/quantifiers/solution_filter.cpp
+  theory/quantifiers/solution_filter.h
   theory/quantifiers/sygus/ce_guided_single_inv.cpp
   theory/quantifiers/sygus/ce_guided_single_inv.h
   theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 1c2405449..0762622f0 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1094,7 +1094,6 @@ header = "options/quantifiers_options.h"
   default    = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
   handler    = "stringToSygusInvTemplMode"
   includes   = ["options/quantifiers_modes.h"]
-  read_only  = true
   help       = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
 
 [[option]]
@@ -1396,6 +1395,14 @@ header = "options/quantifiers_options.h"
   help       = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen"
 
 [[option]]
+  name       = "sygusSolFilterImplied"
+  category   = "regular"
+  long       = "sygus-sol-filter-implied"
+  type       = "bool"
+  default    = "false"
+  help       = "use sygus to enumerate interesting satisfiability queries"
+
+[[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 e5db42a22..149d8bb35 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1927,7 +1927,9 @@ void SmtEngine::setDefaults() {
     }
     if (options::sygusStream())
     {
-      // PBE and streaming modes are incompatible
+      // Streaming is incompatible with techniques that focus the search towards
+      // finding a single solution. This currently includes the PBE solver and
+      // static template inference for invariant synthesis.
       if (!options::sygusSymBreakPbe.wasSetByUser())
       {
         options::sygusSymBreakPbe.set(false);
@@ -1936,6 +1938,10 @@ void SmtEngine::setDefaults() {
       {
         options::sygusUnifPbe.set(false);
       }
+      if (!options::sygusInvTemplMode.wasSetByUser())
+      {
+        options::sygusInvTemplMode.set(quantifiers::SYGUS_INV_TEMPL_MODE_NONE);
+      }
     }
     //do not allow partial functions
     if( !options::bitvectorDivByZeroConst.wasSetByUser() ){
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp
index 010b5a4ab..cc97888e3 100644
--- a/src/theory/quantifiers/expr_miner_manager.cpp
+++ b/src/theory/quantifiers/expr_miner_manager.cpp
@@ -22,6 +22,7 @@ namespace quantifiers {
 ExpressionMinerManager::ExpressionMinerManager()
     : d_doRewSynth(false),
       d_doQueryGen(false),
+      d_doFilterImplied(false),
       d_use_sygus_type(false),
       d_qe(nullptr),
       d_tds(nullptr)
@@ -35,6 +36,7 @@ void ExpressionMinerManager::initialize(const std::vector<Node>& vars,
 {
   d_doRewSynth = false;
   d_doQueryGen = false;
+  d_doFilterImplied = false;
   d_sygus_fun = Node::null();
   d_use_sygus_type = false;
   d_qe = nullptr;
@@ -50,6 +52,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
 {
   d_doRewSynth = false;
   d_doQueryGen = false;
+  d_doFilterImplied = false;
   d_sygus_fun = f;
   d_use_sygus_type = useSygusType;
   d_qe = qe;
@@ -104,22 +107,43 @@ void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh)
   d_qg.setThreshold(deqThresh);
 }
 
+void ExpressionMinerManager::enableFilterImpliedSolutions()
+{
+  d_doFilterImplied = true;
+  std::vector<Node> vars;
+  d_sampler.getVariables(vars);
+  d_solf.initialize(vars, &d_sampler);
+}
+
 bool ExpressionMinerManager::addTerm(Node sol,
                                      std::ostream& out,
                                      bool& rew_print)
 {
-  bool ret = d_crd.addTerm(sol, out, rew_print);
+  // set the builtin version
+  Node solb = sol;
+  if (d_use_sygus_type)
+  {
+    solb = d_tds->sygusToBuiltin(sol);
+  }
+
+  // add to the candidate rewrite rule database
+  bool ret = true;
+  if (d_doRewSynth)
+  {
+    ret = d_crd.addTerm(sol, out, rew_print);
+  }
+
+  // a unique term, let's try the query generator
   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);
   }
+
+  // filter if it's implied
+  if (ret && d_doFilterImplied)
+  {
+    ret = d_solf.addTerm(solb, out);
+  }
   return ret;
 }
 
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index d15b69cb5..d8e6ae651 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/extended_rewrite.h"
 #include "theory/quantifiers/query_generator.h"
+#include "theory/quantifiers/solution_filter.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers_engine.h"
 
@@ -70,6 +71,8 @@ class ExpressionMinerManager
   void enableRewriteRuleSynth();
   /** enable query generation (--sygus-query-gen) */
   void enableQueryGeneration(unsigned deqThresh);
+  /** filter implied solutions (--sygus-sol-filter-implied) */
+  void enableFilterImpliedSolutions();
   /** add term
    *
    * Expression miners may print information on the output stream out, for
@@ -89,6 +92,8 @@ class ExpressionMinerManager
   bool d_doRewSynth;
   /** whether we are doing query generation */
   bool d_doQueryGen;
+  /** whether we are filtering implied candidates */
+  bool d_doFilterImplied;
   /** the sygus function passed to initializeSygus, if any */
   Node d_sygus_fun;
   /** whether we are using sygus types */
@@ -101,6 +106,8 @@ class ExpressionMinerManager
   CandidateRewriteDatabase d_crd;
   /** query generator */
   QueryGenerator d_qg;
+  /** solution filter */
+  SolutionFilter d_solf;
   /** sygus sampler object */
   SygusSampler d_sampler;
   /** extended rewriter object */
diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
new file mode 100644
index 000000000..bea3356d1
--- /dev/null
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -0,0 +1,92 @@
+/*********************                                                        */
+/*! \file solution_filter.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 Utilities for filtering solutions.
+ **/
+
+#include "theory/quantifiers/solution_filter.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 CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SolutionFilter::SolutionFilter() {}
+void SolutionFilter::initialize(const std::vector<Node>& vars, SygusSampler* ss)
+{
+  ExprMiner::initialize(vars, ss);
+}
+
+bool SolutionFilter::addTerm(Node n, std::ostream& out)
+{
+  if (!n.getType().isBoolean())
+  {
+    // currently, should not register non-Boolean terms here
+    Assert(false);
+    return true;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node imp = d_conj.isNull() ? n.negate() : nm->mkNode(AND, d_conj, n.negate());
+  imp = Rewriter::rewrite(imp);
+  bool success = false;
+  if (imp.isConst())
+  {
+    if (!imp.getConst<bool>())
+    {
+      // if the implication rewrites to false, we filter
+      Trace("sygus-sol-implied-filter") << "Filtered (by rewriting) : " << n
+                                        << std::endl;
+      return false;
+    }
+    else
+    {
+      // if the implication rewrites to true, it is trivial
+      success = true;
+    }
+  }
+  if (!success)
+  {
+    Trace("sygus-sol-implied") << "  implies: check " << imp << "..."
+                               << std::endl;
+    // make the satisfiability query
+    bool needExport = false;
+    ExprManagerMapCollection varMap;
+    ExprManager em(nm->getOptions());
+    std::unique_ptr<SmtEngine> queryChecker;
+    initializeChecker(queryChecker, em, varMap, imp, needExport);
+    Result r = queryChecker->checkSat();
+    Trace("sygus-sol-implied") << "  implies: ...got : " << r << std::endl;
+    if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+    {
+      success = true;
+    }
+  }
+  if (success)
+  {
+    d_conj = d_conj.isNull() ? n : nm->mkNode(AND, d_conj, n);
+    d_conj = Rewriter::rewrite(d_conj);
+    // note if d_conj is false, we could terminate here
+    return true;
+  }
+  Trace("sygus-sol-implied-filter") << "Filtered : " << n << std::endl;
+  return false;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h
new file mode 100644
index 000000000..9f098cf69
--- /dev/null
+++ b/src/theory/quantifiers/solution_filter.h
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file solution_filter.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 Utility for filtering sygus solutions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
+#define __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_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 {
+
+/**
+ * This class is used to filter solutions based on some criteria.
+ *
+ * Currently, it is used to filter predicate solutions that are collectively
+ * entailed by the previous predicate solutions.
+ */
+class SolutionFilter : public ExprMiner
+{
+ public:
+  SolutionFilter();
+  ~SolutionFilter() {}
+  /** initialize */
+  void initialize(const std::vector<Node>& vars,
+                  SygusSampler* ss = nullptr) override;
+  /**
+   * Add term to this module. It is expected that n has Boolean type.
+   * If this method returns false, then the entailment n_1 ^ ... ^ n_m |= n
+   * holds, where n_1, ..., n_m are the terms previously registered to this
+   * class.
+   */
+  bool addTerm(Node n, std::ostream& out) override;
+
+ private:
+  /** conjunction of all (non-implied) terms registered to this class */
+  Node d_conj;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 32342a9ba..adc20008e 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -955,7 +955,7 @@ void SynthConjecture::printAndContinueStream()
 
 void SynthConjecture::printSynthSolution(std::ostream& out)
 {
-  Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
+  Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
   Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
   std::vector<Node> sols;
   std::vector<int> statuses;
@@ -981,8 +981,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
 
       bool is_unique_term = true;
 
-      if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen()))
+      if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen()
+                          || options::sygusSolFilterImplied()))
       {
+        Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
         std::map<Node, ExpressionMinerManager>::iterator its =
             d_exprm.find(prog);
         if (its == d_exprm.end())
@@ -997,6 +999,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
           {
             d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
           }
+          if (options::sygusSolFilterImplied())
+          {
+            d_exprm[prog].enableFilterImpliedSolutions();
+          }
           its = d_exprm.find(prog);
         }
         bool rew_print = false;
@@ -1007,7 +1013,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
         }
         if (!is_unique_term)
         {
-          ++(cei->d_statistics.d_candidate_rewrites);
+          ++(cei->d_statistics.d_filtered_solutions);
         }
       }
       if (is_unique_term)
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index ba227bc8f..479cfa535 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -426,17 +426,16 @@ SynthEngine::Statistics::Statistics()
       d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0),
       d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0),
       d_solutions("SynthConjecture::solutions", 0),
-      d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print",
-                                 0),
-      d_candidate_rewrites("SynthConjecture::candidate_rewrites", 0)
+      d_filtered_solutions("SynthConjecture::filtered_solutions", 0),
+      d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", 0)
 
 {
   smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce);
   smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
   smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
   smtStatisticsRegistry()->registerStat(&d_solutions);
+  smtStatisticsRegistry()->registerStat(&d_filtered_solutions);
   smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print);
-  smtStatisticsRegistry()->registerStat(&d_candidate_rewrites);
 }
 
 SynthEngine::Statistics::~Statistics()
@@ -445,8 +444,8 @@ SynthEngine::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_solutions);
+  smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions);
   smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print);
-  smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites);
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 8f0eea58f..a7346b888 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -100,8 +100,8 @@ class SynthEngine : public QuantifiersModule
     IntStat d_cegqi_lemmas_refine;
     IntStat d_cegqi_si_lemmas;
     IntStat d_solutions;
+    IntStat d_filtered_solutions;
     IntStat d_candidate_rewrites_print;
-    IntStat d_candidate_rewrites;
     Statistics();
     ~Statistics();
   }; /* class SynthEngine::Statistics */