mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
This commit is contained in:
parent
1e463955c2
commit
5c2624950b
|
@ -21,6 +21,7 @@ Notes:
|
|||
#include "tactic/model_converter.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
|
||||
/**
|
||||
|
@ -40,9 +41,7 @@ struct bit_blaster_model_converter : public model_converter {
|
|||
obj_map<func_decl, expr*> const & const2bits,
|
||||
ptr_vector<func_decl> const& newbits):
|
||||
m_vars(m), m_bits(m), m_newbits(m) {
|
||||
for (auto const& kv : const2bits) {
|
||||
func_decl * v = kv.m_key;
|
||||
expr * bits = kv.m_value;
|
||||
for (auto const& [v, bits] : const2bits) {
|
||||
SASSERT(!TO_BOOL || is_app_of(bits, m.get_family_id("bv"), OP_MKBV));
|
||||
SASSERT(TO_BOOL || is_app_of(bits, m.get_family_id("bv"), OP_CONCAT));
|
||||
m_vars.push_back(v);
|
||||
|
|
|
@ -37,7 +37,7 @@ class bv1_blaster_tactic : public tactic {
|
|||
bv_util m_util;
|
||||
obj_map<func_decl, expr*> m_const2bits;
|
||||
ptr_vector<func_decl> m_newbits;
|
||||
expr_ref_vector m_saved;
|
||||
ast_ref_vector m_saved;
|
||||
expr_ref m_bit1;
|
||||
expr_ref m_bit0;
|
||||
|
||||
|
@ -108,9 +108,11 @@ class bv1_blaster_tactic : public tactic {
|
|||
for (unsigned i = 0; i < bv_size; i++) {
|
||||
bits.push_back(m().mk_fresh_const(nullptr, b));
|
||||
m_newbits.push_back(to_app(bits.back())->get_decl());
|
||||
m_saved.push_back(m_newbits.back());
|
||||
}
|
||||
r = butil().mk_concat(bits.size(), bits.data());
|
||||
m_saved.push_back(r);
|
||||
m_saved.push_back(f);
|
||||
m_const2bits.insert(f, r);
|
||||
result = r;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue