mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-24 17:21:21 +00:00
Code Activity

Add bvarray2uf_simplifier: convert tactic to simplifier

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-21 23:50:32 +00:00
parent 6bd009ed6a
commit 0cc4afa097
2 changed files with 79 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

66
src/tactic/bv/bvarray2uf_simplifier.h Normal file
View 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, {});
}
}
};

13
src/tactic/bv/bvarray2uf_tactic.h
View file

@ -32,12 +32,25 @@ Tactic that rewrites bit-vector arrays into bit-vector
#pragma once
#include "util/params.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_bvarray2uf2_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_TACTIC("bvarray2uf2", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf2_tactic(m, p)")
ADD_SIMPLIFIER("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "alloc(bvarray2uf_simplifier, m, p, s)")
*/