From 7fe67877489f2acda6f6fddbdcf0806877fba7e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Dec 2022 04:44:02 -0800 Subject: [PATCH] ufbv-rewriter is really a demodulator rewriter and does not reference ufbv so moving first the rewriter into place of other rewriters --- src/ast/rewriter/CMakeLists.txt | 1 + .../rewriter/demodulator_rewriter.cpp} | 50 +++++++++---------- .../rewriter/demodulator_rewriter.h} | 9 ++-- src/tactic/ufbv/CMakeLists.txt | 1 - src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 12 ++--- 5 files changed, 37 insertions(+), 36 deletions(-) rename src/{tactic/ufbv/ufbv_rewriter.cpp => ast/rewriter/demodulator_rewriter.cpp} (93%) rename src/{tactic/ufbv/ufbv_rewriter.h => ast/rewriter/demodulator_rewriter.h} (97%) diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index c785804c1..9eef651c8 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -11,6 +11,7 @@ z3_add_component(rewriter cached_var_subst.cpp char_rewriter.cpp datatype_rewriter.cpp + demodulator_rewriter.cpp der.cpp distribute_forall.cpp dl_rewriter.cpp diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/ast/rewriter/demodulator_rewriter.cpp similarity index 93% rename from src/tactic/ufbv/ufbv_rewriter.cpp rename to src/ast/rewriter/demodulator_rewriter.cpp index a6a4e1957..8a6911925 100644 --- a/src/tactic/ufbv/ufbv_rewriter.cpp +++ b/src/ast/rewriter/demodulator_rewriter.cpp @@ -24,9 +24,9 @@ Revision History: #include "ast/ast_pp.h" #include "ast/for_each_expr.h" #include "ast/rewriter/var_subst.h" -#include "tactic/ufbv/ufbv_rewriter.h" +#include "ast/rewriter/demodulator_rewriter.h" -ufbv_rewriter::ufbv_rewriter(ast_manager & m): +demodulator_rewriter::demodulator_rewriter(ast_manager & m): m(m), m_match_subst(m), m_bsimp(m), @@ -41,7 +41,7 @@ ufbv_rewriter::ufbv_rewriter(ast_manager & m): m_bsimp.updt_params(p); } -ufbv_rewriter::~ufbv_rewriter() { +demodulator_rewriter::~demodulator_rewriter() { reset_dealloc_values(m_fwd_idx); reset_dealloc_values(m_back_idx); for (auto & kv : m_demodulator2lhs_rhs) { @@ -51,7 +51,7 @@ ufbv_rewriter::~ufbv_rewriter() { } } -bool ufbv_rewriter::is_demodulator(expr * e, app_ref & large, expr_ref & small) const { +bool demodulator_rewriter::is_demodulator(expr * e, app_ref & large, expr_ref & small) const { if (!is_forall(e)) { return false; } @@ -117,7 +117,7 @@ public: void operator()(app * n) {} }; -int ufbv_rewriter::is_subset(expr * e1, expr * e2) const { +int demodulator_rewriter::is_subset(expr * e1, expr * e2) const { uint_set ev1, ev2; if (m.is_value(e1)) @@ -134,7 +134,7 @@ int ufbv_rewriter::is_subset(expr * e1, expr * e2) const { 0 ; } -int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const { +int demodulator_rewriter::is_smaller(expr * e1, expr * e2) const { unsigned sz1 = 0, sz2 = 0; // values are always smaller! @@ -186,14 +186,14 @@ public: unsigned get_max() { return m_max_var_id; } }; -unsigned ufbv_rewriter::max_var_id(expr * e) +unsigned demodulator_rewriter::max_var_id(expr * e) { max_var_id_proc proc; for_each_expr(proc, e); return proc.get_max(); } -void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demodulator) { +void demodulator_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demodulator) { SASSERT(large->get_kind() == AST_APP); SASSERT(demodulator); SASSERT(large && small); @@ -217,7 +217,7 @@ void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demo m_demodulator2lhs_rhs.insert(demodulator, expr_pair(large, small)); } -void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) { +void demodulator_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) { TRACE("demodulator_fwd", tout << "REMOVE: " << std::hex << (size_t)demodulator << std::endl; ); fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); @@ -234,7 +234,7 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) { } } -bool ufbv_rewriter::check_fwd_idx_consistency() { +bool demodulator_rewriter::check_fwd_idx_consistency() { for (auto & kv : m_fwd_idx) { quantifier_set * set = kv.m_value; SASSERT(set); @@ -247,7 +247,7 @@ bool ufbv_rewriter::check_fwd_idx_consistency() { return true; } -void ufbv_rewriter::show_fwd_idx(std::ostream & out) { +void demodulator_rewriter::show_fwd_idx(std::ostream & out) { for (auto & kv : m_fwd_idx) { quantifier_set * set = kv.m_value; SASSERT(!set); @@ -265,7 +265,7 @@ void ufbv_rewriter::show_fwd_idx(std::ostream & out) { } } -bool ufbv_rewriter::rewrite1(func_decl * f, expr_ref_vector & m_new_args, expr_ref & np) { +bool demodulator_rewriter::rewrite1(func_decl * f, expr_ref_vector & m_new_args, expr_ref & np) { fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); if (it != m_fwd_idx.end()) { TRACE("demodulator_bug", tout << "trying to rewrite: " << f->get_name() << " args:\n"; @@ -294,7 +294,7 @@ bool ufbv_rewriter::rewrite1(func_decl * f, expr_ref_vector & m_new_args, expr_r return false; } -bool ufbv_rewriter::rewrite_visit_children(app * a) { +bool demodulator_rewriter::rewrite_visit_children(app * a) { bool res=true; unsigned j = a->get_num_args(); while (j > 0) { @@ -327,11 +327,11 @@ bool ufbv_rewriter::rewrite_visit_children(app * a) { return res; } -void ufbv_rewriter::rewrite_cache(expr * e, expr * new_e, bool done) { +void demodulator_rewriter::rewrite_cache(expr * e, expr * new_e, bool done) { m_rewrite_cache.insert(e, expr_bool_pair(new_e, done)); } -expr * ufbv_rewriter::rewrite(expr * n) { +expr * demodulator_rewriter::rewrite(expr * n) { if (m_fwd_idx.empty()) return n; @@ -441,7 +441,7 @@ expr * ufbv_rewriter::rewrite(expr * n) { return r; } -class ufbv_rewriter::add_back_idx_proc { +class demodulator_rewriter::add_back_idx_proc { back_idx_map & m_back_idx; expr * m_expr; public: @@ -467,7 +467,7 @@ public: } }; -class ufbv_rewriter::remove_back_idx_proc { +class demodulator_rewriter::remove_back_idx_proc { back_idx_map & m_back_idx; expr * m_expr; public: @@ -488,7 +488,7 @@ public: } }; -void ufbv_rewriter::reschedule_processed(func_decl * f) { +void demodulator_rewriter::reschedule_processed(func_decl * f) { //use m_back_idx to find all formulas p in m_processed that contains f { back_idx_map::iterator it = m_back_idx.find_iterator(f); if (it != m_back_idx.end()) { @@ -511,7 +511,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) { } } -bool ufbv_rewriter::can_rewrite(expr * n, expr * lhs) { +bool demodulator_rewriter::can_rewrite(expr * n, expr * lhs) { // this is a quick check, we just traverse d and check if there is an expression in d that is an instance of lhs of n'. // we cannot use the trick used for m_processed, since the main loop would not terminate. @@ -568,7 +568,7 @@ bool ufbv_rewriter::can_rewrite(expr * n, expr * lhs) { return false; } -void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { +void demodulator_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { // use m_back_idx to find all demodulators d in m_fwd_idx that contains f { //ptr_vector to_remove; @@ -616,7 +616,7 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { } } -void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, +void demodulator_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { if (m.proofs_enabled()) { TRACE("tactic", tout << "PRE_DEMODULATOR=true is not supported when proofs are enabled.";); @@ -710,7 +710,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * } -ufbv_rewriter::match_subst::match_subst(ast_manager & m): +demodulator_rewriter::match_subst::match_subst(ast_manager & m): m(m), m_subst(m) { } @@ -742,7 +742,7 @@ struct match_args_aux_proc { void operator()(app * n) {} }; -bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { +bool demodulator_rewriter::match_subst::match_args(app * lhs, expr * const * args) { m_cache.reset(); m_todo.reset(); @@ -858,7 +858,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { } -bool ufbv_rewriter::match_subst::operator()(app * lhs, expr * rhs, expr * const * args, expr_ref & new_rhs) { +bool demodulator_rewriter::match_subst::operator()(app * lhs, expr * rhs, expr * const * args, expr_ref & new_rhs) { if (match_args(lhs, args)) { if (m_all_args_eq) { @@ -873,7 +873,7 @@ bool ufbv_rewriter::match_subst::operator()(app * lhs, expr * rhs, expr * const return false; } -bool ufbv_rewriter::match_subst::operator()(expr * t, expr * i) { +bool demodulator_rewriter::match_subst::operator()(expr * t, expr * i) { m_cache.reset(); m_todo.reset(); if (is_var(t)) diff --git a/src/tactic/ufbv/ufbv_rewriter.h b/src/ast/rewriter/demodulator_rewriter.h similarity index 97% rename from src/tactic/ufbv/ufbv_rewriter.h rename to src/ast/rewriter/demodulator_rewriter.h index d855047a0..a60debabf 100644 --- a/src/tactic/ufbv/ufbv_rewriter.h +++ b/src/ast/rewriter/demodulator_rewriter.h @@ -3,7 +3,7 @@ Copyright (c) 2006 Microsoft Corporation Module Name: - demodulator.h + demodulator_rewriter.h Abstract: @@ -16,6 +16,7 @@ Author: Revision History: Christoph M. Wintersteiger (cwinter) 2012-10-24: Moved from demodulator.h to ufbv_rewriter.h + Nikolaj Bjorner (nbjorner) 2022-12-4: Moved to rewriter and renamed to demodulator_rewriter.h --*/ #pragma once @@ -91,7 +92,7 @@ The code in spc_rewriter.* does something like that. We cannot reuse this code d for the superposion engine in Z3, but we can adapt it for our needs in the preprocessor. */ -class ufbv_rewriter final { +class demodulator_rewriter final { class rewrite_proc; class add_back_idx_proc; class remove_back_idx_proc; @@ -193,8 +194,8 @@ class ufbv_rewriter final { int is_subset(expr * e1, expr * e2) const; public: - ufbv_rewriter(ast_manager & m); - ~ufbv_rewriter(); + demodulator_rewriter(ast_manager & m); + ~demodulator_rewriter(); void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); diff --git a/src/tactic/ufbv/CMakeLists.txt b/src/tactic/ufbv/CMakeLists.txt index 511dc2b2d..2c2567b91 100644 --- a/src/tactic/ufbv/CMakeLists.txt +++ b/src/tactic/ufbv/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(ufbv_tactic SOURCES macro_finder_tactic.cpp quasi_macros_tactic.cpp - ufbv_rewriter.cpp ufbv_rewriter_tactic.cpp ufbv_tactic.cpp COMPONENT_DEPENDENCIES diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index e254523c0..46958982a 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -17,21 +17,21 @@ Notes: --*/ #include "tactic/tactical.h" -#include "tactic/ufbv/ufbv_rewriter.h" +#include "ast/rewriter/demodulator_rewriter.h" #include "tactic/ufbv/ufbv_rewriter_tactic.h" -class ufbv_rewriter_tactic : public tactic { +class demodulator_rewriter_tactic : public tactic { ast_manager & m_manager; params_ref m_params; public: - ufbv_rewriter_tactic(ast_manager & m, params_ref const & p): + demodulator_rewriter_tactic(ast_manager & m, params_ref const & p): m_manager(m), m_params(p) {} char const* name() const override { return "ufbv"; } tactic * translate(ast_manager & m) override { - return alloc(ufbv_rewriter_tactic, m, m_params); + return alloc(demodulator_rewriter_tactic, m, m_params); } void updt_params(params_ref const & p) override { @@ -50,7 +50,7 @@ public: bool produce_proofs = g->proofs_enabled(); - ufbv_rewriter dem(m_manager); + demodulator_rewriter dem(m_manager); expr_ref_vector forms(m_manager), new_forms(m_manager); proof_ref_vector proofs(m_manager), new_proofs(m_manager); @@ -79,5 +79,5 @@ public: }; tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p) { - return alloc(ufbv_rewriter_tactic, m, p); + return alloc(demodulator_rewriter_tactic, m, p); }