Generalize sygus stream solution filtering to logical strength (#2697)

11 files changed, 215 insertions, 71 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 565f28334..bd5b00728 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -508,6 +508,21 @@ trust  \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_sygusFilterSolHelp =
+    "\
+Modes for filtering sygus solutions supported by --sygus-filter-sol:\n\
+\n\
+none (default) \n\
++ Do not filter sygus solutions.\n\
+\n\
+strong \n\
++ Filter solutions that are logically stronger than others.\n\
+\n\
+weak \n\
++ Filter solutions that are logically weaker than others.\n\
+\n\
+";
+
 const std::string OptionsHandler::s_sygusInvTemplHelp = "\
 Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
 \n\
@@ -951,6 +966,35 @@ theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode(
   }
 }
 
+theory::quantifiers::SygusFilterSolMode
+OptionsHandler::stringToSygusFilterSolMode(std::string option,
+                                           std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return theory::quantifiers::SYGUS_FILTER_SOL_NONE;
+  }
+  else if (optarg == "strong")
+  {
+    return theory::quantifiers::SYGUS_FILTER_SOL_STRONG;
+  }
+  else if (optarg == "weak")
+  {
+    return theory::quantifiers::SYGUS_FILTER_SOL_WEAK;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_cegisSampleHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(
+        std::string("unknown option for --sygus-filter-sol: `") + optarg
+        + "'.  Try --sygus-filter-sol help.");
+  }
+}
+
 theory::quantifiers::SygusInvTemplMode
 OptionsHandler::stringToSygusInvTemplMode(std::string option,
                                           std::string optarg)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 3078db0f8..53e317895 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -112,6 +112,8 @@ public:
       std::string option, std::string optarg);
   theory::quantifiers::CegisSampleMode stringToCegisSampleMode(
       std::string option, std::string optarg);
+  theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode(
+      std::string option, std::string optarg);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(
       std::string option, std::string optarg);
   theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode(
@@ -248,6 +250,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_sygusFilterSolHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_sygusActiveGenHelp;
   static const std::string s_termDbModeHelp;
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 05388cdf6..41378d2cd 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -276,6 +276,16 @@ enum SygusActiveGenMode
   SYGUS_ACTIVE_GEN_AUTO,
 };
 
+enum SygusFilterSolMode
+{
+  /** do not filter solutions */
+  SYGUS_FILTER_SOL_NONE,
+  /** filter logically stronger solutions */
+  SYGUS_FILTER_SOL_STRONG,
+  /** filter logically weaker solutions */
+  SYGUS_FILTER_SOL_WEAK,
+};
+
 enum MacrosQuantMode {
   /** infer all definitions */
   MACROS_QUANT_MODE_ALL,
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index c555c37bf..d9d3e0d38 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1403,12 +1403,22 @@ header = "options/quantifiers_options.h"
   help       = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen"
 
 [[option]]
-  name       = "sygusSolFilterImplied"
+  name       = "sygusFilterSolMode"
   category   = "regular"
-  long       = "sygus-sol-filter-implied"
+  long       = "sygus-filter-sol=MODE"
+  type       = "CVC4::theory::quantifiers::SygusFilterSolMode"
+  default    = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE"
+  handler    = "stringToSygusFilterSolMode"
+  includes   = ["options/quantifiers_modes.h"]
+  help       = "mode for filtering sygus solutions"
+
+[[option]]
+  name       = "sygusFilterSolRevSubsume"
+  category   = "expert"
+  long       = "sygus-filter-sol-rev"
   type       = "bool"
   default    = "false"
-  help       = "use sygus to enumerate interesting satisfiability queries"
+  help       = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
 
 [[option]]
   name       = "sygusExprMinerCheckUseExport"
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 16e59c119..b65d1c522 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -113,6 +113,29 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   }
 }
 
+Result ExprMiner::doCheck(Node query)
+{
+  Node queryr = Rewriter::rewrite(query);
+  if (queryr.isConst())
+  {
+    if (!queryr.getConst<bool>())
+    {
+      return Result(Result::UNSAT);
+    }
+    else
+    {
+      return Result(Result::SAT);
+    }
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  bool needExport = false;
+  ExprManagerMapCollection varMap;
+  ExprManager em(nm->getOptions());
+  std::unique_ptr<SmtEngine> smte;
+  initializeChecker(smte, em, varMap, queryr, needExport);
+  return smte->checkSat();
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index c09f40d0e..59d9989c5 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -92,6 +92,14 @@ class ExprMiner
                          ExprManagerMapCollection& varMap,
                          Node query,
                          bool& needExport);
+  /**
+   * Run the satisfiability check on query and return the result
+   * (sat/unsat/unknown).
+   *
+   * In contrast to the above method, this call should be used for cases where
+   * the model for the query is not important.
+   */
+  Result doCheck(Node query);
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp
index cc97888e3..a808d386c 100644
--- a/src/theory/quantifiers/expr_miner_manager.cpp
+++ b/src/theory/quantifiers/expr_miner_manager.cpp
@@ -22,7 +22,7 @@ namespace quantifiers {
 ExpressionMinerManager::ExpressionMinerManager()
     : d_doRewSynth(false),
       d_doQueryGen(false),
-      d_doFilterImplied(false),
+      d_doFilterLogicalStrength(false),
       d_use_sygus_type(false),
       d_qe(nullptr),
       d_tds(nullptr)
@@ -36,7 +36,7 @@ void ExpressionMinerManager::initialize(const std::vector<Node>& vars,
 {
   d_doRewSynth = false;
   d_doQueryGen = false;
-  d_doFilterImplied = false;
+  d_doFilterLogicalStrength = false;
   d_sygus_fun = Node::null();
   d_use_sygus_type = false;
   d_qe = nullptr;
@@ -52,7 +52,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
 {
   d_doRewSynth = false;
   d_doQueryGen = false;
-  d_doFilterImplied = false;
+  d_doFilterLogicalStrength = false;
   d_sygus_fun = f;
   d_use_sygus_type = useSygusType;
   d_qe = qe;
@@ -107,12 +107,22 @@ void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh)
   d_qg.setThreshold(deqThresh);
 }
 
-void ExpressionMinerManager::enableFilterImpliedSolutions()
+void ExpressionMinerManager::enableFilterWeakSolutions()
 {
-  d_doFilterImplied = true;
+  d_doFilterLogicalStrength = true;
   std::vector<Node> vars;
   d_sampler.getVariables(vars);
-  d_solf.initialize(vars, &d_sampler);
+  d_sols.initialize(vars, &d_sampler);
+  d_sols.setLogicallyStrong(true);
+}
+
+void ExpressionMinerManager::enableFilterStrongSolutions()
+{
+  d_doFilterLogicalStrength = true;
+  std::vector<Node> vars;
+  d_sampler.getVariables(vars);
+  d_sols.initialize(vars, &d_sampler);
+  d_sols.setLogicallyStrong(false);
 }
 
 bool ExpressionMinerManager::addTerm(Node sol,
@@ -139,10 +149,10 @@ bool ExpressionMinerManager::addTerm(Node sol,
     d_qg.addTerm(solb, out);
   }
 
-  // filter if it's implied
-  if (ret && d_doFilterImplied)
+  // filter based on logical strength
+  if (ret && d_doFilterLogicalStrength)
   {
-    ret = d_solf.addTerm(solb, out);
+    ret = d_sols.addTerm(solb, out);
   }
   return ret;
 }
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index d8e6ae651..d817d3775 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -71,8 +71,10 @@ class ExpressionMinerManager
   void enableRewriteRuleSynth();
   /** enable query generation (--sygus-query-gen) */
   void enableQueryGeneration(unsigned deqThresh);
-  /** filter implied solutions (--sygus-sol-filter-implied) */
-  void enableFilterImpliedSolutions();
+  /** filter strong solutions (--sygus-filter-sol=strong) */
+  void enableFilterStrongSolutions();
+  /** filter weak solutions (--sygus-filter-sol=weak) */
+  void enableFilterWeakSolutions();
   /** add term
    *
    * Expression miners may print information on the output stream out, for
@@ -92,8 +94,8 @@ class ExpressionMinerManager
   bool d_doRewSynth;
   /** whether we are doing query generation */
   bool d_doQueryGen;
-  /** whether we are filtering implied candidates */
-  bool d_doFilterImplied;
+  /** whether we are filtering solutions based on logical strength */
+  bool d_doFilterLogicalStrength;
   /** the sygus function passed to initializeSygus, if any */
   Node d_sygus_fun;
   /** whether we are using sygus types */
@@ -106,8 +108,8 @@ class ExpressionMinerManager
   CandidateRewriteDatabase d_crd;
   /** query generator */
   QueryGenerator d_qg;
-  /** solution filter */
-  SolutionFilter d_solf;
+  /** solution filter based on logical strength */
+  SolutionFilterStrength d_sols;
   /** 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
index bea3356d1..19d39e997 100644
--- a/src/theory/quantifiers/solution_filter.cpp
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -26,13 +26,19 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SolutionFilter::SolutionFilter() {}
-void SolutionFilter::initialize(const std::vector<Node>& vars, SygusSampler* ss)
+SolutionFilterStrength::SolutionFilterStrength() : d_isStrong(true) {}
+void SolutionFilterStrength::initialize(const std::vector<Node>& vars,
+                                        SygusSampler* ss)
 {
   ExprMiner::initialize(vars, ss);
 }
 
-bool SolutionFilter::addTerm(Node n, std::ostream& out)
+void SolutionFilterStrength::setLogicallyStrong(bool isStrong)
+{
+  d_isStrong = isStrong;
+}
+
+bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
 {
   if (!n.getType().isBoolean())
   {
@@ -40,51 +46,58 @@ bool SolutionFilter::addTerm(Node n, std::ostream& out)
     Assert(false);
     return true;
   }
+  Node basen = d_isStrong ? n : n.negate();
   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())
+  // Do i subsume the disjunction of all previous solutions? If so, we discard
+  // this immediately
+  Node curr;
+  if (!d_curr_sols.empty())
   {
-    if (!imp.getConst<bool>())
+    curr = d_curr_sols.size() == 1
+               ? d_curr_sols[0]
+               : nm->mkNode(d_isStrong ? AND : OR, d_curr_sols);
+    Node imp = nm->mkNode(AND, basen.negate(), curr);
+    Trace("sygus-sol-implied")
+        << "  implies: check subsumed " << imp << "..." << std::endl;
+    // check the satisfiability query
+    Result r = doCheck(imp);
+    Trace("sygus-sol-implied") << "  implies: ...got : " << r << std::endl;
+    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
     {
-      // if the implication rewrites to false, we filter
-      Trace("sygus-sol-implied-filter") << "Filtered (by rewriting) : " << n
-                                        << std::endl;
+      // it is subsumed by the current, discard this
       return false;
     }
-    else
-    {
-      // if the implication rewrites to true, it is trivial
-      success = true;
-    }
   }
-  if (!success)
+  // check which solutions would have been filtered if the current had come
+  // first
+  if (options::sygusFilterSolRevSubsume())
   {
-    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)
+    std::vector<Node> nsubsume;
+    for (const Node& s : d_curr_sols)
     {
-      success = true;
+      Node imp = nm->mkNode(AND, s.negate(), basen);
+      Trace("sygus-sol-implied")
+          << "  implies: check subsuming " << imp << "..." << std::endl;
+      // check the satisfiability query
+      Result r = doCheck(imp);
+      Trace("sygus-sol-implied") << "  implies: ...got : " << r << std::endl;
+      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+      {
+        nsubsume.push_back(s);
+      }
+      else
+      {
+        Options& nodeManagerOptions = nm->getOptions();
+        std::ostream* out = nodeManagerOptions.getOut();
+        (*out) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
+               << std::endl;
+      }
     }
+    d_curr_sols.clear();
+    d_curr_sols.insert(d_curr_sols.end(), nsubsume.begin(), nsubsume.end());
   }
-  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;
+  d_curr_sols.push_back(basen);
+  return true;
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h
index 9f098cf69..d162f41f0 100644
--- a/src/theory/quantifiers/solution_filter.h
+++ b/src/theory/quantifiers/solution_filter.h
@@ -29,30 +29,43 @@ namespace theory {
 namespace quantifiers {
 
 /**
- * This class is used to filter solutions based on some criteria.
+ * This class is used to filter solutions based on logical strength.
  *
  * Currently, it is used to filter predicate solutions that are collectively
- * entailed by the previous predicate solutions.
+ * entailed by the previous predicate solutions (if we are looking for logically
+ * stronger solutions), or to filter predicate solutions that entail any
+ * previous predicate (if we are looking for logically weaker solutions).
  */
-class SolutionFilter : public ExprMiner
+class SolutionFilterStrength : public ExprMiner
 {
  public:
-  SolutionFilter();
-  ~SolutionFilter() {}
+  SolutionFilterStrength();
+  ~SolutionFilterStrength() {}
   /** 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.
+   * Add term to this miner. It is expected that n has Boolean type.
+   *
+   * If d_isStrong is true, then 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.
+   *
+   * Dually, if d_isStrong is false, then if this method returns false, then
+   * the entailment n |= n_1 V ... V n_m holds.
    */
   bool addTerm(Node n, std::ostream& out) override;
+  /** set logically strong */
+  void setLogicallyStrong(bool isStrong);
 
  private:
-  /** conjunction of all (non-implied) terms registered to this class */
-  Node d_conj;
+  /**
+   * Set of all (non-filtered) terms registered to this class. We store the
+   * negation of these terms if d_isStrong is false.
+   */
+  std::vector<Node> d_curr_sols;
+  /** whether we are trying to find the logically strongest solutions */
+  bool d_isStrong;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 3f0ac70f5..ff7bb6378 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1039,8 +1039,9 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
 
       bool is_unique_term = true;
 
-      if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen()
-                          || options::sygusSolFilterImplied()))
+      if (status != 0
+          && (options::sygusRewSynth() || options::sygusQueryGen()
+              || options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE))
       {
         Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
         std::map<Node, ExpressionMinerManager>::iterator its =
@@ -1057,9 +1058,16 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
           {
             d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
           }
-          if (options::sygusSolFilterImplied())
+          if (options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE)
           {
-            d_exprm[prog].enableFilterImpliedSolutions();
+            if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_STRONG)
+            {
+              d_exprm[prog].enableFilterStrongSolutions();
+            }
+            else if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_WEAK)
+            {
+              d_exprm[prog].enableFilterWeakSolutions();
+            }
           }
           its = d_exprm.find(prog);
         }