diff options
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 22 |
1 files changed, 5 insertions, 17 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 9bbb88699..a5a35f89d 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -32,25 +32,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// the number of d_drewrite objects we have allocated (to avoid name conflicts) -static unsigned drewrite_counter = 0; - CandidateRewriteDatabase::CandidateRewriteDatabase() : d_qe(nullptr), d_tds(nullptr), d_ext_rewrite(nullptr), d_using_sygus(false) { - if (options::sygusRewSynthFilterCong()) - { - // initialize the dynamic rewriter - std::stringstream ss; - ss << "_dyn_rewriter_" << drewrite_counter; - drewrite_counter++; - d_drewrite = std::unique_ptr<DynamicRewriter>( - new DynamicRewriter(ss.str(), &d_fake_context)); - d_sampler.setDynamicRewriter(d_drewrite.get()); - } } void CandidateRewriteDatabase::initialize(ExtendedRewriter* er, TypeNode tn, @@ -65,6 +52,7 @@ void CandidateRewriteDatabase::initialize(ExtendedRewriter* er, d_tds = nullptr; d_ext_rewrite = er; d_sampler.initialize(tn, vars, nsamples, unique_type_ids); + d_crewrite_filter.initialize(&d_sampler, nullptr, false); } void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe, @@ -81,6 +69,7 @@ void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe, d_tds = d_qe->getTermDatabaseSygus(); d_ext_rewrite = d_tds->getExtRewriter(); d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); + d_crewrite_filter.initialize(&d_sampler, d_tds, true); } bool CandidateRewriteDatabase::addTerm(Node sol, @@ -93,9 +82,8 @@ bool CandidateRewriteDatabase::addTerm(Node sol, if (eq_sol != sol) { is_unique_term = false; - // if eq_sol is null, then we have an uninteresting candidate rewrite, - // e.g. one that is alpha-equivalent to another. - if (!eq_sol.isNull()) + // should we filter the pair? + if (!d_crewrite_filter.filterPair(sol, eq_sol)) { // get the actual term Node solb = sol; @@ -215,7 +203,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, if (!is_unique_term) { // register this as a relevant pair (helps filtering) - d_sampler.registerRelevantPair(sol, eq_sol); + 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. |