mirror of
https://github.com/Z3Prover/z3
synced 2026-02-24 09:11:17 +00:00
Merge pull request #8729 from Z3Prover/copilot/convert-bvarray2uf-to-simplifier
Convert `bvarray2uf` tactic to a dependent_expr_simplifier
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
0b5480b6c3
4 changed files with 78 additions and 146 deletions
|
|
@ -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
|
||||
|
|
|
|||
66
src/tactic/bv/bvarray2uf_simplifier.h
Normal file
66
src/tactic/bv/bvarray2uf_simplifier.h
Normal file
|
|
@ -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, {});
|
||||
}
|
||||
}
|
||||
};
|
||||
|
|
@ -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));
|
||||
}
|
||||
|
|
@ -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)")
|
||||
*/
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue