diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-27 14:37:41 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-27 14:37:41 -0600 |
| commit | e986a322232ac3edcd139ec7b424291ea3d5033a (patch) | |
| tree | e42cff1cd563e393ee973b469f97e46e4b509add /src/theory/quantifiers/candidate_rewrite_database.h | |
| parent | 2c4025e44771707ba548b6d8aa5a8a13ec3cd8f1 (diff) | |
Add option for whether to filter candidate rewrite pairs (#5825)
This option should be disabled for the new sygus reconstruction algorithm on #5779.
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.h')
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 41ec0677b..9f8ab8c86 100644 --- 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 */ |