mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
FPA theory bug fixes.
Also removed unnecessary intermediate variables. Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
2cd4edf1a2
commit
8b40d4a735
|
@ -2599,11 +2599,11 @@ void fpa_example() {
|
|||
Z3_config cfg;
|
||||
Z3_context ctx;
|
||||
Z3_sort double_sort, rm_sort;
|
||||
Z3_symbol symbol_rm, symbol_x, symbol_y;
|
||||
Z3_ast rm, x, y, n, c;
|
||||
|
||||
printf("\nFPA-example\n");
|
||||
LOG_MSG("FPA-example");
|
||||
Z3_symbol symbol_rm, symbol_x, symbol_y, symbol_q;
|
||||
Z3_ast rm, x, y, n, q, c1, c2, c3, c4, c5, c6;
|
||||
|
||||
printf("\nfpa_example\n");
|
||||
LOG_MSG("fpa_example");
|
||||
|
||||
cfg = Z3_mk_config();
|
||||
ctx = Z3_mk_context(cfg);
|
||||
|
@ -2620,16 +2620,32 @@ void fpa_example() {
|
|||
y = Z3_mk_const(ctx, symbol_y, double_sort);
|
||||
n = Z3_mk_fpa_double(ctx, 42.0, double_sort);
|
||||
|
||||
Z3_symbol q_s = Z3_mk_string_symbol(ctx, "q");
|
||||
Z3_ast q = Z3_mk_const(ctx, q_s, double_sort);
|
||||
c = Z3_mk_eq(ctx, q, Z3_mk_fpa_add(ctx, rm, x, y));
|
||||
symbol_q = Z3_mk_string_symbol(ctx, "q");
|
||||
q = Z3_mk_const(ctx, symbol_q, double_sort);
|
||||
c1 = Z3_mk_eq(ctx, q, Z3_mk_fpa_add(ctx, rm, x, y));
|
||||
|
||||
Z3_ast args[2] = { c, Z3_mk_eq(ctx, q, n) };
|
||||
c = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
|
||||
Z3_ast args[2] = { c1, Z3_mk_eq(ctx, q, n) };
|
||||
c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
|
||||
|
||||
printf("c = %s\n", Z3_ast_to_string(ctx, c));
|
||||
Z3_ast args2[2] = { c2, Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_round_nearest_ties_to_away(ctx))) };
|
||||
c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
|
||||
|
||||
Z3_assert_cnstr(ctx, c);
|
||||
Z3_ast and_args[3] = {
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y)),
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y)),
|
||||
Z3_mk_not(ctx, Z3_mk_fpa_is_inf(ctx, y)) };
|
||||
Z3_ast args3[2] = { c3, Z3_mk_and(ctx, 3, and_args) };
|
||||
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
|
||||
|
||||
|
||||
Z3_assert_cnstr(ctx, c4);
|
||||
Z3_push(ctx);
|
||||
|
||||
// c5 := (IEEEBV(x) == 7.0).
|
||||
c5 = Z3_mk_eq(ctx, Z3_mk_fpa_to_ieee_bv(ctx, x),
|
||||
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)));
|
||||
|
||||
Z3_assert_cnstr(ctx, c5);
|
||||
|
||||
Z3_model m = 0;
|
||||
Z3_lbool result = Z3_check_and_get_model(ctx, &m);
|
||||
|
@ -2639,19 +2655,44 @@ void fpa_example() {
|
|||
break;
|
||||
case Z3_L_UNDEF:
|
||||
printf("unknown\n");
|
||||
printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
break;
|
||||
case Z3_L_TRUE:
|
||||
printf("sat\n%s\n", Z3_model_to_string(ctx, m));
|
||||
Z3_del_model(ctx, m);
|
||||
break;
|
||||
}
|
||||
|
||||
Z3_pop(ctx, 1);
|
||||
|
||||
// c6 := (IEEEBV(x) == 28.0).
|
||||
c6 = Z3_mk_eq(ctx, Z3_mk_fpa_to_ieee_bv(ctx, x),
|
||||
Z3_mk_numeral(ctx, "4628574517030027264", Z3_mk_bv_sort(ctx, 64)));
|
||||
|
||||
Z3_assert_cnstr(ctx, c6);
|
||||
Z3_push(ctx);
|
||||
|
||||
m = 0;
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
switch (result) {
|
||||
case Z3_L_FALSE:
|
||||
printf("unsat\n");
|
||||
break;
|
||||
case Z3_L_UNDEF:
|
||||
printf("unknown\n");
|
||||
printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
break;
|
||||
case Z3_L_TRUE:
|
||||
printf("sat\n%s\n", Z3_model_to_string(ctx, m));
|
||||
printf("sat\n%s\n", Z3_model_to_string(ctx, m));
|
||||
Z3_del_model(ctx, m);
|
||||
break;
|
||||
}
|
||||
|
||||
if (m)
|
||||
Z3_del_model(ctx, m);
|
||||
Z3_pop(ctx, 1);
|
||||
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
|
||||
/*@}*/
|
||||
/*@}*/
|
||||
|
||||
|
|
|
@ -193,7 +193,7 @@ extern "C" {
|
|||
// floats are separated from all others to avoid huge rationals.
|
||||
float_util & fu = mk_c(c)->float_util();
|
||||
scoped_mpf tmp(fu.fm());
|
||||
if (mk_c(c)->float_util().is_numeral(to_expr(a), tmp)) {
|
||||
if (mk_c(c)->float_util().is_value(to_expr(a), tmp)) {
|
||||
return mk_c(c)->mk_external_string(fu.fm().to_string(tmp));
|
||||
}
|
||||
else {
|
||||
|
|
|
@ -60,15 +60,6 @@ namespace smt {
|
|||
ctx.mark_as_relevant(l);
|
||||
}
|
||||
|
||||
app_ref theory_fpa::mk_eq_bv_const(expr_ref const & e) {
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
app_ref bv_const(m);
|
||||
bv_const = m.mk_fresh_const(0, m.get_sort(e));
|
||||
mk_bv_eq(bv_const, e);
|
||||
return bv_const;
|
||||
}
|
||||
|
||||
bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
|
||||
TRACE("t_fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
|
||||
SASSERT(atom->get_family_id() == get_family_id());
|
||||
|
@ -128,7 +119,7 @@ namespace smt {
|
|||
proof_ref bv_pr(m);
|
||||
simp(t, bv_rm, bv_pr);
|
||||
|
||||
bv_term = mk_eq_bv_const(bv_rm);
|
||||
bv_term = bv_rm;
|
||||
}
|
||||
else if (m_converter.is_float(term_sort)) {
|
||||
SASSERT(is_app(t) && to_app(t)->get_num_args() == 3);
|
||||
|
@ -139,19 +130,13 @@ namespace smt {
|
|||
simp(a->get_arg(1), sig, pr_sig);
|
||||
simp(a->get_arg(2), exp, pr_exp);
|
||||
|
||||
app_ref bv_v_sgn = mk_eq_bv_const(sgn);
|
||||
app_ref bv_v_sig = mk_eq_bv_const(sig);
|
||||
app_ref bv_v_exp = mk_eq_bv_const(exp);
|
||||
|
||||
m_converter.mk_triple(bv_v_sgn, bv_v_sig, bv_v_exp, bv_term);
|
||||
m_converter.mk_triple(sgn, sig, exp, bv_term);
|
||||
}
|
||||
else if (term->get_decl_kind() == OP_TO_IEEE_BV) {
|
||||
SASSERT(is_app(t));
|
||||
expr_ref bv_e(m);
|
||||
proof_ref bv_pr(m);
|
||||
simp(t, bv_e, bv_pr);
|
||||
|
||||
bv_term = mk_eq_bv_const(bv_e);
|
||||
simp(t, bv_term, bv_pr);
|
||||
}
|
||||
else
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
@ -159,11 +144,12 @@ namespace smt {
|
|||
TRACE("t_fpa", tout << "converted: " << mk_ismt2_pp(bv_term, get_manager()) << "\n";);
|
||||
|
||||
SASSERT(!m_trans_map.contains(term));
|
||||
m_trans_map.insert(term, bv_term, 0);
|
||||
m_trans_map.insert(term, bv_term, 0);
|
||||
|
||||
enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : ctx.mk_enode(term, false, false, true);
|
||||
theory_var v = mk_var(e);
|
||||
ctx.attach_th_var(e, this, v);
|
||||
m_tvars.push_back(v);
|
||||
TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(term, get_manager()) << " := " << v << "\n";);
|
||||
SASSERT(e->get_th_var(get_id()) != null_theory_var);
|
||||
return v != null_theory_var;
|
||||
|
@ -180,23 +166,14 @@ namespace smt {
|
|||
|
||||
theory_var v = mk_var(n);
|
||||
ctx.attach_th_var(n, this, v);
|
||||
m_tvars.push_back(v);
|
||||
m_rw(owner, converted);
|
||||
m_trans_map.insert(owner, converted, 0);
|
||||
|
||||
if (m_converter.is_rm(m.get_sort(owner))) {
|
||||
mk_eq_bv_const(converted);
|
||||
}
|
||||
else {
|
||||
app * a = to_app(converted);
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
proof_ref pr_sgn(m), pr_sig(m), pr_exp(m);
|
||||
simp(a->get_arg(0), sgn, pr_sgn);
|
||||
simp(a->get_arg(1), sig, pr_sig);
|
||||
simp(a->get_arg(2), exp, pr_exp);
|
||||
|
||||
mk_eq_bv_const(sgn);
|
||||
mk_eq_bv_const(sig);
|
||||
mk_eq_bv_const(exp);
|
||||
sort * owner_sort = m.get_sort(owner);
|
||||
if (m_converter.is_rm(owner_sort)) {
|
||||
bv_util & bu = m_converter.bu();
|
||||
bu.mk_ule(converted, bu.mk_numeral(4, bu.get_bv_size(converted)));
|
||||
}
|
||||
|
||||
TRACE("t_fpa", tout << "new theory var (const): " << mk_ismt2_pp(owner, get_manager()) << " := " << v << "\n";);
|
||||
|
@ -215,7 +192,7 @@ namespace smt {
|
|||
m_trans_map.get(ax, ex, px);
|
||||
m_trans_map.get(ay, ey, py);
|
||||
|
||||
if (m_converter.fu().is_float(m.get_sort(get_enode(x)->get_owner()))) {
|
||||
if (m_converter.fu().is_float(get_enode(x)->get_owner())) {
|
||||
expr * sgn_x, *sig_x, *exp_x;
|
||||
expr * sgn_y, *sig_y, *exp_y;
|
||||
split_triple(ex, sgn_x, sig_x, exp_x);
|
||||
|
@ -225,7 +202,7 @@ namespace smt {
|
|||
mk_bv_eq(sig_x, sig_y);
|
||||
mk_bv_eq(exp_x, exp_y);
|
||||
}
|
||||
else if (m_converter.fu().is_rm(m.get_sort(get_enode(x)->get_owner()))) {
|
||||
else if (m_converter.fu().is_rm(get_enode(x)->get_owner())) {
|
||||
mk_bv_eq(ex, ey);
|
||||
}
|
||||
else
|
||||
|
@ -273,7 +250,13 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
|
||||
TRACE("bv", tout << num_scopes << "\n";);
|
||||
m_trail_stack.pop_scope(num_scopes);
|
||||
unsigned num_old_vars = get_old_num_vars(num_scopes);
|
||||
for (unsigned i = num_old_vars; i < get_num_vars(); i++) {
|
||||
m_trans_map.erase(get_enode(m_tvars[i])->get_owner());
|
||||
}
|
||||
m_tvars.shrink(num_old_vars);
|
||||
theory::pop_scope_eh(num_scopes);
|
||||
}
|
||||
|
||||
|
@ -405,6 +388,7 @@ namespace smt {
|
|||
void theory_fpa::assign_eh(bool_var v, bool is_true) {
|
||||
TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << ")\n";);
|
||||
/* CMW: okay to ignore? */
|
||||
theory::assign_eh(v, is_true);
|
||||
}
|
||||
|
||||
void theory_fpa::relevant_eh(app * n) {
|
||||
|
@ -441,14 +425,10 @@ namespace smt {
|
|||
ctx.mark_as_relevant(bv_exp);
|
||||
}
|
||||
else if (n->get_decl()->get_decl_kind() == OP_TO_IEEE_BV) {
|
||||
//literal l = mk_eq(n, ex, false);
|
||||
//ctx.mark_as_relevant(l);
|
||||
//ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
|
||||
expr_ref eq(m);
|
||||
app * ex_a = to_app(ex);
|
||||
if (n->get_id() > ex_a->get_id())
|
||||
std::swap(n, ex_a);
|
||||
expr_ref eq(m);
|
||||
std::swap(n, ex_a);
|
||||
eq = m.mk_eq(n, ex_a);
|
||||
ctx.internalize(eq, false);
|
||||
literal l = ctx.get_literal(eq);
|
||||
|
@ -464,7 +444,11 @@ namespace smt {
|
|||
|
||||
void theory_fpa::reset_eh() {
|
||||
pop_scope_eh(m_trail_stack.get_num_scopes());
|
||||
m_bool_var2atom.reset();
|
||||
m_rw.reset();
|
||||
m_trans_map.reset();
|
||||
m_bool_var2atom.reset();
|
||||
m_temporaries.reset();
|
||||
m_tvars.reset();
|
||||
theory::reset_eh();
|
||||
}
|
||||
|
||||
|
|
|
@ -55,6 +55,7 @@ namespace smt {
|
|||
th_trail_stack m_trail_stack;
|
||||
bool_var2atom m_bool_var2atom;
|
||||
enode_vector m_temporaries;
|
||||
int_vector m_tvars;
|
||||
|
||||
virtual final_check_status final_check_eh() { return FC_DONE; }
|
||||
virtual bool internalize_atom(app * atom, bool gate_ctx);
|
||||
|
@ -88,7 +89,6 @@ namespace smt {
|
|||
}
|
||||
|
||||
void mk_bv_eq(expr * x, expr * y);
|
||||
app_ref mk_eq_bv_const(expr_ref const & e);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue