mirror of
https://github.com/Z3Prover/z3
synced 2026-05-16 15:15:35 +00:00
Refactor FPA/BV soundness bug fix to be self-contained in theory_fpa
This commit is contained in:
tryh4rd-26
parent
759ab463b9
commit
8b98967451
3 changed files with 30 additions and 137 deletions
|
|
@ -26,7 +26,6 @@ Revision History:
|
|||
#include "smt/smt_model_generator.h"
|
||||
#include "smt/proto_model/proto_model.h"
|
||||
#include "model/model_v2_pp.h"
|
||||
#include "smt/theory_fpa.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -133,11 +132,6 @@ namespace smt {
|
|||
root2proc.insert(r, proc);
|
||||
}
|
||||
}
|
||||
|
||||
theory * fpa_th = m_context->get_theory(m.mk_family_id("fpa"));
|
||||
if (fpa_th) {
|
||||
static_cast<theory_fpa*>(fpa_th)->register_fpa2bv_processors(*this, root2proc, roots, procs);
|
||||
}
|
||||
}
|
||||
|
||||
model_value_proc* model_generator::mk_model_value(enode* r) {
|
||||
|
|
@ -376,22 +370,18 @@ namespace smt {
|
|||
enode * child = d.get_enode();
|
||||
TRACE(mg_top_sort, tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): "
|
||||
<< mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
|
||||
child = child->get_root();
|
||||
app * child_val = nullptr;
|
||||
m_root2value.find(child, child_val);
|
||||
CTRACE("mg", !child_val,
|
||||
tout << "null dependency value for: " << mk_pp(child->get_expr(), m) << "\n";);
|
||||
dependency_values.push_back(child_val);
|
||||
}
|
||||
}
|
||||
val = proc->mk_value(*this, dependency_values);
|
||||
}
|
||||
register_value(val);
|
||||
m_asts.push_back(val);
|
||||
m_root2value.insert(n, val);
|
||||
}
|
||||
}
|
||||
// send model
|
||||
child = child->get_root();
|
||||
dependency_values.push_back(m_root2value[child]);
|
||||
}
|
||||
}
|
||||
val = proc->mk_value(*this, dependency_values);
|
||||
}
|
||||
register_value(val);
|
||||
m_asts.push_back(val);
|
||||
m_root2value.insert(n, val);
|
||||
}
|
||||
}
|
||||
// send model
|
||||
for (enode * n : m_context->enodes()) {
|
||||
if (is_uninterp_const(n->get_expr()) && m_context->is_relevant(n)) {
|
||||
func_decl * d = n->get_expr()->get_decl();
|
||||
|
|
@ -413,9 +403,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
app * model_generator::get_value(enode * n) const {
|
||||
app * val = nullptr;
|
||||
m_root2value.find(n->get_root(), val);
|
||||
return val;
|
||||
return m_root2value[n->get_root()];
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -472,6 +472,22 @@ namespace smt {
|
|||
wu = m.mk_eq(m_converter.unwrap(wrapped, n->get_sort()), n);
|
||||
TRACE(t_fpa, tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, m) << std::endl;);
|
||||
assert_cnstr(wu);
|
||||
|
||||
// For non-FPA-family terms (e.g. datatype accessors like
|
||||
// get-fp), mk_uf creates a separate BV UF that is not
|
||||
// linked to bvwrap. Assert wrap(n) == concat(conv_components)
|
||||
// to close the constraint gap (same pattern as numerals above).
|
||||
if (n->get_family_id() != get_family_id()) {
|
||||
expr_ref conv_e = convert(n);
|
||||
if (m_fpa_util.is_fp(conv_e) && to_app(conv_e)->get_num_args() == 3) {
|
||||
app_ref conv_a(m);
|
||||
conv_a = to_app(conv_e.get());
|
||||
expr_ref cc(m);
|
||||
cc = m_bv_util.mk_concat({conv_a->get_arg(0), conv_a->get_arg(1), conv_a->get_arg(2)});
|
||||
assert_cnstr(m.mk_eq(wrapped, cc));
|
||||
assert_cnstr(mk_side_conditions());
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -647,101 +663,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
app * theory_fpa::fpa2bv_value_proc::mk_value(model_generator & mg, expr_ref_vector const & values) {
|
||||
ast_manager & m = m_th.get_manager();
|
||||
fpa_util & fu = m_th.m_fpa_util;
|
||||
bv_util & bu = m_th.m_bv_util;
|
||||
context & ctx = m_th.get_context();
|
||||
|
||||
app * fpa_val = (values.empty() || !values[0]) ? nullptr : to_app(values[0]);
|
||||
if (!fpa_val) {
|
||||
if (!mg.get_root2value().find(m_fpa_n, fpa_val)) {
|
||||
datatype_util dt(m);
|
||||
expr * expr_n = m_fpa_n->get_expr();
|
||||
if (is_app(expr_n) && to_app(expr_n)->get_num_args() == 1) {
|
||||
func_decl * f = to_app(expr_n)->get_decl();
|
||||
if (dt.is_accessor(f)) {
|
||||
enode * arg_n = m_fpa_n->get_arg(0)->get_root();
|
||||
app * arg_val = nullptr;
|
||||
if (mg.get_root2value().find(arg_n, arg_val)) {
|
||||
if (dt.is_constructor(arg_val)) {
|
||||
ptr_vector<func_decl> const * accessors = dt.get_constructor_accessors(arg_val->get_decl());
|
||||
if (accessors) {
|
||||
for (unsigned i = 0; i < accessors->size(); ++i) {
|
||||
if ((*accessors)[i] == f) {
|
||||
expr * acc_val = arg_val->get_arg(i);
|
||||
if (m.is_value(acc_val)) {
|
||||
fpa_val = to_app(acc_val);
|
||||
}
|
||||
else if (is_app(acc_val) && ctx.e_internalized(acc_val)) {
|
||||
enode * acc_n = ctx.get_enode(acc_val)->get_root();
|
||||
mg.get_root2value().find(acc_n, fpa_val);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!fpa_val) {
|
||||
TRACE("fpa", tout << "fpa2bv_value_proc: defaulting to +0.0 for " << mk_pp(m_fpa_n->get_expr(), m) << "\n";);
|
||||
fpa_val = fu.mk_pzero(m_ebits, m_sbits);
|
||||
}
|
||||
|
||||
scoped_mpf v(fu.fm());
|
||||
if (fu.is_numeral(fpa_val, v)) {
|
||||
expr_ref result_fp(m);
|
||||
m_th.m_converter.mk_numeral(fpa_val->get_sort(), v, result_fp);
|
||||
if (fu.is_fp(result_fp)) {
|
||||
expr * sgn = to_app(result_fp)->get_arg(0);
|
||||
expr * exp = to_app(result_fp)->get_arg(1);
|
||||
expr * sig = to_app(result_fp)->get_arg(2);
|
||||
return bu.mk_concat(bu.mk_concat(sgn, exp), sig);
|
||||
}
|
||||
}
|
||||
return bu.mk_numeral(0, m_ebits + m_sbits);
|
||||
}
|
||||
|
||||
void theory_fpa::register_fpa2bv_processors(model_generator & mg, obj_map<enode, model_value_proc *> & root2proc, ptr_vector<enode> & roots, ptr_vector<model_value_proc> & procs) {
|
||||
for (auto const& kv : m_conversions) {
|
||||
expr * fpa_expr = kv.m_key;
|
||||
expr * bv_expr = kv.m_value;
|
||||
if (ctx.e_internalized(fpa_expr) && ctx.e_internalized(bv_expr) && m_fpa_util.is_float(fpa_expr)) {
|
||||
app_ref owner(m);
|
||||
owner = get_ite_value(fpa_expr);
|
||||
if (!owner || owner->get_family_id() == get_family_id())
|
||||
continue;
|
||||
|
||||
enode * fpa_n = ctx.get_enode(fpa_expr)->get_root();
|
||||
enode * bv_n = ctx.get_enode(bv_expr)->get_root();
|
||||
|
||||
// if (!root2proc.contains(fpa_n))
|
||||
// continue;
|
||||
|
||||
if (root2proc.contains(bv_n)) {
|
||||
if (dynamic_cast<fpa2bv_value_proc*>(root2proc[bv_n]))
|
||||
continue;
|
||||
}
|
||||
|
||||
unsigned ebits = m_fpa_util.get_ebits(fpa_expr->get_sort());
|
||||
unsigned sbits = m_fpa_util.get_sbits(fpa_expr->get_sort());
|
||||
model_value_proc * proc = alloc(fpa2bv_value_proc, this, ebits, sbits, fpa_n);
|
||||
procs.push_back(proc);
|
||||
|
||||
bool is_new = !root2proc.contains(bv_n);
|
||||
root2proc.insert(bv_n, proc);
|
||||
if (is_new) {
|
||||
roots.push_back(bv_n);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_fpa::display(std::ostream & out) const
|
||||
{
|
||||
|
||||
|
|
|
|||
|
|
@ -56,22 +56,6 @@ namespace smt {
|
|||
app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
|
||||
};
|
||||
|
||||
class fpa2bv_value_proc : public model_value_proc {
|
||||
theory_fpa & m_th;
|
||||
unsigned m_ebits;
|
||||
unsigned m_sbits;
|
||||
enode * m_fpa_n;
|
||||
public:
|
||||
fpa2bv_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits, enode * fpa_n) :
|
||||
m_th(*th), m_ebits(ebits), m_sbits(sbits), m_fpa_n(fpa_n) {}
|
||||
|
||||
void get_dependencies(buffer<model_value_dependency> & result) override {
|
||||
result.push_back(model_value_dependency(m_fpa_n));
|
||||
}
|
||||
|
||||
app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
|
||||
};
|
||||
|
||||
class fpa_rm_value_proc : public model_value_proc {
|
||||
theory_fpa & m_th;
|
||||
ast_manager & m;
|
||||
|
|
@ -126,7 +110,6 @@ namespace smt {
|
|||
|
||||
public:
|
||||
theory_fpa(context& ctx);
|
||||
void register_fpa2bv_processors(model_generator & mg, obj_map<enode, model_value_proc *> & root2proc, ptr_vector<enode> & roots, ptr_vector<model_value_proc> & procs);
|
||||
~theory_fpa() override;
|
||||
|
||||
void display(std::ostream & out) const override;
|
||||
|
|
@ -144,3 +127,4 @@ namespace smt {
|
|||
};
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue