mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-02 08:33:45 +00:00
Code Activity

Remove old bvarray2uf_tactic implementation; use simplifier as basis

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

1
src/tactic/bv/CMakeLists.txt
View file

@ -4,7 +4,6 @@ z3_add_component(bv_tactics
bit_blaster_tactic.cpp bit_blaster_tactic.cpp
bv1_blaster_tactic.cpp bv1_blaster_tactic.cpp
bvarray2uf_rewriter.cpp bvarray2uf_rewriter.cpp
bvarray2uf_tactic.cpp
bv_bound_chk_tactic.cpp bv_bound_chk_tactic.cpp
bv_bounds_tactic.cpp bv_bounds_tactic.cpp
bv_size_reduction_tactic.cpp bv_size_reduction_tactic.cpp

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

@ -32,15 +32,14 @@ Tactic that rewrites bit-vector arrays into bit-vector
#pragma once #pragma once
#include "util/params.h" #include "util/params.h"
#include "tactic/tactic.h"
#include "tactic/dependent_expr_state_tactic.h" #include "tactic/dependent_expr_state_tactic.h"
#include "tactic/bv/bvarray2uf_simplifier.h" #include "tactic/bv/bvarray2uf_simplifier.h"
class ast_manager; class ast_manager;
class tactic; 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()) {
inline tactic * mk_bvarray2uf2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p, return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
return alloc(bvarray2uf_simplifier, m, p, s); return alloc(bvarray2uf_simplifier, m, p, s);
@ -49,7 +48,6 @@ inline tactic * mk_bvarray2uf2_tactic(ast_manager & m, params_ref const & p = pa
/* /*
ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)") 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)") ADD_SIMPLIFIER("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "alloc(bvarray2uf_simplifier, m, p, s)")
*/ */