Add option for whether to filter candidate rewrite pairs (#5825)

This option should be disabled for the new sygus reconstruction algorithm on #5779.

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index fef9bec22edfdef8cc7174492a54f2769184c133..ad13bd6e0904add12326a7482f3ac56c6a169279 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -34,13 +34,15 @@ namespace quantifiers {
 
 CandidateRewriteDatabase::CandidateRewriteDatabase(bool doCheck,
                                                    bool rewAccel,
-                                                   bool silent)
+                                                   bool silent,
+                                                   bool filterPairs)
     : d_qe(nullptr),
       d_tds(nullptr),
       d_ext_rewrite(nullptr),
       d_doCheck(doCheck),
       d_rewAccel(rewAccel),
       d_silent(silent),
+      d_filterPairs(filterPairs),
       d_using_sygus(false)
 {
 }
@@ -53,7 +55,10 @@ void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars,
   d_qe = nullptr;
   d_tds = nullptr;
   d_ext_rewrite = nullptr;
-  d_crewrite_filter.initialize(ss, nullptr, false);
+  if (d_filterPairs)
+  {
+    d_crewrite_filter.initialize(ss, nullptr, false);
+  }
   ExprMiner::initialize(vars, ss);
 }
 
@@ -68,7 +73,10 @@ void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars,
   d_qe = qe;
   d_tds = d_qe->getTermDatabaseSygus();
   d_ext_rewrite = nullptr;
-  d_crewrite_filter.initialize(ss, d_tds, d_using_sygus);
+  if (d_filterPairs)
+  {
+    d_crewrite_filter.initialize(ss, d_tds, d_using_sygus);
+  }
   ExprMiner::initialize(vars, ss);
 }
 
@@ -103,7 +111,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol,
   {
     is_unique_term = false;
     // should we filter the pair?
-    if (!d_crewrite_filter.filterPair(sol, eq_sol))
+    if (!d_filterPairs || !d_crewrite_filter.filterPair(sol, eq_sol))
     {
       // get the actual term
       Node solb = sol;
@@ -200,7 +208,10 @@ Node CandidateRewriteDatabase::addTerm(Node sol,
       if (!is_unique_term)
       {
         // register this as a relevant pair (helps filtering)
-        d_crewrite_filter.registerRelevantPair(sol, eq_sol);
+        if (d_filterPairs)
+        {
+          d_crewrite_filter.registerRelevantPair(sol, eq_sol);
+        }
         // The analog of terms sol and eq_sol are equivalent under
         // sample points but do not rewrite to the same term. Hence,
         // this indicates a candidate rewrite.

diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index 41ec0677bfb5cb3123304612c3551b4cb7d5b54e..9f8ab8c86221e0ced4fc87af3ee5a73a0693118e 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -32,8 +32,8 @@ namespace quantifiers {
 /** CandidateRewriteDatabase
  *
  * This maintains the necessary data structures for generating a database
- * of candidate rewrite rules (see Reynolds et al "Rewrites for SMT Solvers
- * Using Syntax-Guided Enumeration" SMT 2018). The primary responsibilities
+ * of candidate rewrite rules (see Noetzli et al "Syntax-Guided Rewrite Rule
+ * Enumeration for SMT Solvers" SAT 2019). The primary responsibilities
  * of this class are to perform the "equivalence checking" and "congruence
  * and matching filtering" in Figure 1. The equivalence checking is done
  * through a combination of the sygus sampler object owned by this class
@@ -51,10 +51,13 @@ class CandidateRewriteDatabase : public ExprMiner
    * discovered rewrites (see option sygusRewSynthAccel()).
    * @param silent Whether to silence the output of rewrites discovered by this
    * class.
+   * @param filterPairs Whether to filter rewrite pairs using filtering
+   * techniques from the SAT 2019 paper above.
    */
   CandidateRewriteDatabase(bool doCheck,
                            bool rewAccel = false,
-                           bool silent = false);
+                           bool silent = false,
+                           bool filterPairs = true);
   ~CandidateRewriteDatabase() {}
   /**  Initialize this class */
   void initialize(const std::vector<Node>& var,
@@ -119,6 +122,8 @@ class CandidateRewriteDatabase : public ExprMiner
   bool d_rewAccel;
   /** if true, we silence the output of candidate rewrites */
   bool d_silent;
+  /** if true, we filter pairs of terms to check equivalence */
+  bool d_filterPairs;
   /** whether we are using sygus */
   bool d_using_sygus;
   /** candidate rewrite filter */