diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-04 14:31:14 +0100 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-04 06:31:14 -0700 |
| commit | 9a8d9420f03ba27fc5cbb9674b0c809ecc53e85e (patch) | |
| tree | 73b0b5ca75435c2816f5bf0c93144e269450bc18 /src/theory/quantifiers/candidate_rewrite_database.h | |
| parent | 714ede2487fb58ea46858380eecfff72c2e2d4ac (diff) | |
Reorganize candidate rewrite rule filtering (#2116)
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.h')
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index a2a6c5745..7f51043e2 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -21,6 +21,7 @@ #include <memory> #include <unordered_set> #include <vector> +#include "theory/quantifiers/candidate_rewrite_filter.h" #include "theory/quantifiers/sygus_sampler.h" namespace CVC4 { @@ -116,11 +117,9 @@ class CandidateRewriteDatabase * This is used for the sygusRewSynth() option to synthesize new candidate * rewrite rules. */ - SygusSamplerExt d_sampler; - /** a (dummy) user context, used for d_drewrite */ - context::UserContext d_fake_context; - /** dynamic rewriter class */ - std::unique_ptr<DynamicRewriter> d_drewrite; + SygusSampler d_sampler; + /** candidate rewrite filter */ + CandidateRewriteFilter d_crewrite_filter; /** * Cache of skolems for each free variable that appears in a synthesis check * (for --sygus-rr-synth-check). |