diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 578c563b7..6eb7a2e11 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -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); } - /*@}*/ /*@}*/ diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 740fef2ac..d2829e990 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -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 { diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 9c03cb76c..a228ec4a5 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -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(); } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 998cc17e8..5c0d2acca 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -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); }; };