diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt index 9009e6fa5..d5920b88e 100644 --- a/src/tactic/bv/CMakeLists.txt +++ b/src/tactic/bv/CMakeLists.txt @@ -4,7 +4,6 @@ z3_add_component(bv_tactics bit_blaster_tactic.cpp bv1_blaster_tactic.cpp bvarray2uf_rewriter.cpp - bvarray2uf_tactic.cpp bv_bound_chk_tactic.cpp bv_bounds_tactic.cpp bv_size_reduction_tactic.cpp diff --git a/src/tactic/bv/bvarray2uf_simplifier.h b/src/tactic/bv/bvarray2uf_simplifier.h new file mode 100644 index 000000000..df837bc5c --- /dev/null +++ b/src/tactic/bv/bvarray2uf_simplifier.h @@ -0,0 +1,66 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + bvarray2uf_simplifier.h + +Abstract: + + Simplifier that rewrites bit-vector arrays into bit-vector + (uninterpreted) functions. + +Author: + + Christoph (cwinter) 2015-11-04 + +--*/ +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/converters/generic_model_converter.h" +#include "tactic/bv/bvarray2uf_rewriter.h" + +class bvarray2uf_simplifier : public dependent_expr_simplifier { + bvarray2uf_rewriter m_rw; + generic_model_converter_ref m_fmc; + +public: + bvarray2uf_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls) + : dependent_expr_simplifier(m, fmls), + m_rw(m, p), + m_fmc(alloc(generic_model_converter, m, "bvarray2uf")) { + m_rw.set_mcs(m_fmc.get()); + } + + char const* name() const override { return "bvarray2uf"; } + + // bvarray2uf_rewriter does not support proofs + bool supports_proofs() const override { return false; } + + void reduce() override { + m_rw.reset(); + m_fmc = alloc(generic_model_converter, m, "bvarray2uf"); + m_rw.set_mcs(m_fmc.get()); + + expr_ref new_curr(m); + proof_ref new_pr(m); + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + m_rw(d.fml(), new_curr, new_pr); + m_fmls.update(idx, dependent_expr(m, new_curr, nullptr, d.dep())); + } + + // Add extra assertions generated by the rewriter (e.g., injectivity lemmas) + for (expr* a : m_rw.m_cfg.extra_assertions) + m_fmls.add(dependent_expr(m, a, nullptr, nullptr)); + + // Register model converter entries for array-to-UF model reconstruction + for (auto const& entry : m_fmc->entries()) { + if (entry.m_instruction == generic_model_converter::instruction::HIDE) + m_fmls.model_trail().hide(entry.m_f); + else if (entry.m_instruction == generic_model_converter::instruction::ADD) + m_fmls.model_trail().push(entry.m_f, entry.m_def, nullptr, {}); + } + } +}; diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp deleted file mode 100644 index 58a1e6238..000000000 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ /dev/null @@ -1,144 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - - bvarray2uf_tactic.cpp - -Abstract: - - Tactic that rewrites bit-vector arrays into bit-vector - (uninterpreted) functions. - -Author: - - Christoph (cwinter) 2015-11-04 - -Notes: - ---*/ -#include "tactic/tactical.h" -#include "ast/bv_decl_plugin.h" -#include "ast/rewriter/expr_replacer.h" -#include "ast/converters/generic_model_converter.h" -#include "ast/ast_smt2_pp.h" - -#include "tactic/bv/bvarray2uf_tactic.h" -#include "tactic/bv/bvarray2uf_rewriter.h" - -class bvarray2uf_tactic : public tactic { - - struct imp { - ast_manager & m_manager; - bool m_produce_cores; - bvarray2uf_rewriter m_rw; - - ast_manager & m() { return m_manager; } - - imp(ast_manager & m, params_ref const & p) : - m_manager(m), - m_produce_cores(false), - m_rw(m, p) { - updt_params(p); - } - - - void checkpoint() { - if (!m_manager.inc()) - throw tactic_exception(m_manager.limit().get_cancel_msg()); - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result) - { - tactic_report report("bvarray2uf", *g); - result.reset(); - fail_if_unsat_core_generation("bvarray2uf", g); - // bvarray2uf_rewriter does not support proofs (yet). - fail_if_proof_generation("bvarray2uf", g); - - bool produce_models = g->models_enabled(); - bool produce_proofs = g->proofs_enabled(); - model_converter_ref mc; - - if (produce_models) { - generic_model_converter * fmc = alloc(generic_model_converter, m_manager, "bvarray2uf"); - mc = fmc; - m_rw.set_mcs(fmc); - } - - - m_rw.reset(); - expr_ref new_curr(m_manager); - proof_ref new_pr(m_manager); - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; ++idx) { - if (g->inconsistent()) - break; - expr* curr = g->form(idx); - m_rw(curr, new_curr, new_pr); - if (produce_proofs) { - proof * pr = g->pr(idx); - new_pr = m_manager.mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); - } - - for (expr* a : m_rw.m_cfg.extra_assertions) - g->assert_expr(a); - - g->inc_depth(); - g->add(mc.get()); - result.push_back(g.get()); - } - - void updt_params(params_ref const & p) { - } - }; - - imp * m_imp; - params_ref m_params; - -public: - bvarray2uf_tactic(ast_manager & m, params_ref const & p) : - m_params(p) { - m_imp = alloc(imp, m, p); - } - - tactic * translate(ast_manager & m) override { - return alloc(bvarray2uf_tactic, m, m_params); - } - - ~bvarray2uf_tactic() override { - dealloc(m_imp); - } - - char const* name() const override { return "bvarray2uf"; } - - void updt_params(params_ref const & p) override { - m_params.append(p); - m_imp->updt_params(m_params); - } - - void collect_param_descrs(param_descrs & r) override { - insert_produce_models(r); - } - - void operator()(goal_ref const & in, - goal_ref_buffer & result) override { - (*m_imp)(in, result); - } - - void cleanup() override { - ast_manager & m = m_imp->m(); - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); - } - -}; - - -tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(bvarray2uf_tactic, m, p)); -} diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h index 393ab164c..d71752853 100644 --- a/src/tactic/bv/bvarray2uf_tactic.h +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -32,12 +32,23 @@ Tactic that rewrites bit-vector arrays into bit-vector #pragma once #include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "tactic/bv/bvarray2uf_simplifier.h" + class ast_manager; class tactic; -tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref()); +inline tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { + return alloc(bvarray2uf_simplifier, m, p, s); + }); +} + /* ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)") + ADD_SIMPLIFIER("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "alloc(bvarray2uf_simplifier, m, p, s)") */