From 5716eaafed5136adb7e5bfcc1c4ab147b13b3e81 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 14 Sep 2016 13:49:49 +0100 Subject: [PATCH 01/21] whitespace --- src/smt/smt_conflict_resolution.cpp | 164 ++++++++++++++-------------- 1 file changed, 82 insertions(+), 82 deletions(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index b28c4e773..4568abb55 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -22,13 +22,13 @@ Revision History: #include"ast_ll_pp.h" namespace smt { - + // --------------------------- // // Base class // // --------------------------- - + conflict_resolution::conflict_resolution(ast_manager & m, context & ctx, dyn_ack_manager & dyn_ack_manager, @@ -42,7 +42,7 @@ namespace smt { m_dyn_ack_manager(dyn_ack_manager), m_assigned_literals(assigned_literals), m_lemma_atoms(m), - m_todo_js_qhead(0), + m_todo_js_qhead(0), m_antecedents(0), m_watches(watches), m_new_proofs(m), @@ -67,7 +67,7 @@ namespace smt { } /** - \brief Find a common ancestor (anc) of n1 and n2 in the 'proof' tree. + \brief Find a common ancestor (anc) of n1 and n2 in the 'proof' tree. The common ancestor is used to produce irredundant transitivity proofs. n1 = a1 = ... = ai = ANC = ... = root @@ -100,7 +100,7 @@ namespace smt { */ void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) { SASSERT(m_antecedents); - TRACE("conflict_detail", + TRACE("conflict_detail", ast_manager& m = get_manager(); tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m); switch (js.get_kind()) { @@ -133,7 +133,7 @@ namespace smt { mark_eq(lhs->get_arg(1), rhs->get_arg(0)); } else { - for (unsigned i = 0; i < num_args; i++) + for (unsigned i = 0; i < num_args; i++) mark_eq(lhs->get_arg(i), rhs->get_arg(i)); } break; @@ -146,9 +146,9 @@ namespace smt { /** \brief Process the transitivity 'proof' from n1 and n2, where n1 and n2 are in the same branch - + n1 -> ... -> n2 - + This method may update m_antecedents, m_todo_js and m_todo_eqs. The resultant set of literals is stored in m_antecedents. @@ -163,7 +163,7 @@ namespace smt { /** \brief Process the justification of n1 = n2. - + This method may update m_antecedents, m_todo_js and m_todo_eqs. The resultant set of literals is stored in m_antecedents. @@ -180,8 +180,8 @@ namespace smt { The result is stored in result. - \remark This method does not reset the vectors m_antecedents, m_todo_js, m_todo_eqs, nor reset the - marks in the justification objects. + \remark This method does not reset the vectors m_antecedents, m_todo_js, m_todo_eqs, nor reset the + marks in the justification objects. */ void conflict_resolution::justification2literals_core(justification * js, literal_vector & result) { SASSERT(m_todo_js_qhead <= m_todo_js.size()); @@ -294,13 +294,13 @@ namespace smt { if (js) r = std::max(r, get_justification_max_lvl(js)); break; - } + } case b_justification::BIN_CLAUSE: r = std::max(r, m_ctx.get_assign_level(js.get_literal())); break; case b_justification::AXIOM: break; - case b_justification::JUSTIFICATION: + case b_justification::JUSTIFICATION: r = std::max(r, get_justification_max_lvl(js.get_justification())); break; default: @@ -313,8 +313,8 @@ namespace smt { bool_var var = antecedent.var(); unsigned lvl = m_ctx.get_assign_level(var); SASSERT(var < static_cast(m_ctx.get_num_bool_vars())); - TRACE("conflict", tout << "processing antecedent (level " << lvl << "):"; - m_ctx.display_literal(tout, antecedent); + TRACE("conflict", tout << "processing antecedent (level " << lvl << "):"; + m_ctx.display_literal(tout, antecedent); m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";); if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) { @@ -386,17 +386,17 @@ namespace smt { consequent = false_literal; if (not_l != null_literal) consequent = ~not_l; - + m_conflict_lvl = get_max_lvl(consequent, js); - TRACE("conflict_bug", - tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level() + TRACE("conflict_bug", + tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level() << " search_lvl: " << m_ctx.get_search_level() << "\n"; tout << "js.kind: " << js.get_kind() << "\n"; tout << "consequent: " << consequent << ": "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n"; m_ctx.display(tout, js); tout << "\n"; - ); + ); // m_conflict_lvl can be smaller than m_ctx.get_search_level() when: // there are user level scopes created using the Z3 API, and @@ -413,7 +413,7 @@ namespace smt { } TRACE("conflict", tout << "conflict_lvl: " << m_conflict_lvl << "\n";); - + SASSERT(!m_assigned_literals.empty()); SASSERT(m_todo_js.empty()); @@ -425,32 +425,32 @@ namespace smt { /** \brief Cleanup datastructures used during resolve(), minimize lemma (when minimization is enabled), compute m_new_scope_lvl and m_lemma_iscope_lvl, generate proof if needed. - + This method assumes that the lemma is stored in m_lemma (and the associated atoms in m_lemma_atoms). - + \warning This method assumes the literals in m_lemma[1] ... m_lemma[m_lemma.size() - 1] are marked. */ void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) { unmark_justifications(0); - + TRACE("conflict", tout << "before minimization:\n"; m_ctx.display_literals(tout, m_lemma); tout << "\n";); - + TRACE("conflict_verbose", tout << "before minimization:\n"; m_ctx.display_literals_verbose(tout, m_lemma); tout << "\n";); - + if (m_params.m_minimize_lemmas) minimize_lemma(); - + TRACE("conflict", tout << "after minimization:\n"; m_ctx.display_literals(tout, m_lemma); tout << "\n";); - + TRACE("conflict_verbose", tout << "after minimization:\n"; m_ctx.display_literals_verbose(tout, m_lemma); @@ -459,7 +459,7 @@ namespace smt { TRACE("conflict_bug", m_ctx.display_literals_verbose(tout, m_lemma); tout << "\n";); - + literal_vector::iterator it = m_lemma.begin(); literal_vector::iterator end = m_lemma.end(); m_new_scope_lvl = m_ctx.get_search_level(); @@ -478,11 +478,11 @@ namespace smt { m_lemma_iscope_lvl = lvl; } } - + TRACE("conflict", tout << "new scope level: " << m_new_scope_lvl << "\n"; tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";); - + if (m_manager.proofs_enabled()) mk_conflict_proof(conflict, not_l); } @@ -505,7 +505,7 @@ namespace smt { TRACE("conflict", tout << "not_l: "; m_ctx.display_literal(tout, not_l); tout << "\n";); process_antecedent(not_l, num_marks); } - + do { if (get_manager().has_trace_stream()) { @@ -542,7 +542,7 @@ namespace smt { process_antecedent(~l, num_marks); } justification * js = cls->get_justification(); - if (js) + if (js) process_justification(js, num_marks); break; } @@ -558,13 +558,13 @@ namespace smt { default: UNREACHABLE(); } - + while (true) { literal l = m_assigned_literals[idx]; - if (m_ctx.is_marked(l.var())) + if (m_ctx.is_marked(l.var())) break; CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(), - tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l); + tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l); tout << "\n";); SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl || // it may also be an (out-of-order) asserted literal @@ -580,7 +580,7 @@ namespace smt { idx--; num_marks--; m_ctx.unset_mark(c_var); - } + } while (num_marks > 0); TRACE("conflict", tout << "FUIP: "; m_ctx.display_literal(tout, consequent); tout << "\n";); @@ -589,8 +589,8 @@ namespace smt { m_lemma_atoms.set(0, m_ctx.bool_var2expr(consequent.var())); // TODO: - // - // equality optimization should go here. + // + // equality optimization should go here. // finalize_resolve(conflict, not_l); @@ -600,7 +600,7 @@ namespace smt { /** \brief Return an approximation for the set of scope levels where the literals in m_lemma - were assigned. + were assigned. */ level_approx_set conflict_resolution::get_lemma_approx_level_set() { level_approx_set result; @@ -640,7 +640,7 @@ namespace smt { unsigned lvl = m_ctx.get_assign_level(var); if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) { if (m_lvl_set.may_contain(lvl)) { - m_ctx.set_mark(var); + m_ctx.set_mark(var); m_unmark.push_back(var); m_lemma_min_stack.push_back(var); } @@ -667,18 +667,18 @@ namespace smt { } /** - \brief Return true if lit is implied by other marked literals - and/or literals assigned at the base level. - The set lvl_set is used as an optimization. + \brief Return true if lit is implied by other marked literals + and/or literals assigned at the base level. + The set lvl_set is used as an optimization. The idea is to stop the recursive search with a failure - as soon as we find a literal assigned in a level that is not in lvl_set. + as soon as we find a literal assigned in a level that is not in lvl_set. */ bool conflict_resolution::implied_by_marked(literal lit) { m_lemma_min_stack.reset(); // avoid recursive function m_lemma_min_stack.push_back(lit.var()); unsigned old_size = m_unmark.size(); unsigned old_js_qhead = m_todo_js_qhead; - + while (!m_lemma_min_stack.empty()) { bool_var var = m_lemma_min_stack.back(); m_lemma_min_stack.pop_back(); @@ -739,7 +739,7 @@ namespace smt { m_unmark.reset(); m_lvl_set = get_lemma_approx_level_set(); - + unsigned sz = m_lemma.size(); unsigned i = 1; // the first literal is the FUIP unsigned j = 1; @@ -756,7 +756,7 @@ namespace smt { j++; } } - + reset_unmark_and_justifications(0, 0); m_lemma .shrink(j); m_lemma_atoms.shrink(j); @@ -810,7 +810,7 @@ namespace smt { } if (m_manager.coarse_grain_proofs()) return pr; - TRACE("norm_eq_proof", + TRACE("norm_eq_proof", tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n"; tout << mk_ll_pp(pr, m_manager, true, false);); SASSERT(m_manager.is_eq(fact) || m_manager.is_iff(fact)); @@ -906,7 +906,7 @@ namespace smt { return 0; } } - + /** \brief Return the proof object associated with the given literal if it already exists. Otherwise, return 0 and add l to the todo-list. @@ -939,13 +939,13 @@ namespace smt { // p1: is a proof of "A" // p2: is a proof of "not A" // [unit-resolution p1 p2]: false - // + // // Let us assume that "A" was assigned first during propagation. // Then, the "resolve" method will never select "not A" as a hypothesis. - // "not_A" will be the not_l argument in this method. + // "not_A" will be the not_l argument in this method. // Since we are assuming that "A" was assigned first", m_ctx.get_justification("A") will be // p1. - // + // // So, the test "m_ctx.get_justification(l.var()) == js" is used to check // if l was assigned before ~l. if ((m_ctx.is_marked(l.var()) && m_ctx.get_justification(l.var()) == js) || (js.get_kind() == b_justification::AXIOM)) { @@ -1022,11 +1022,11 @@ namespace smt { tout << mk_pp(m_manager.get_fact(prs[i]), m_manager) << "\n"; } tout << "consequent:\n" << mk_pp(l_exr, m_manager) << "\n";); - TRACE("get_proof", + TRACE("get_proof", tout << l.index() << " " << true_literal.index() << " " << false_literal.index() << " "; m_ctx.display_literal(tout, l); tout << " --->\n"; tout << mk_ll_pp(l_exr, m_manager);); - CTRACE("get_proof_bug_after", + CTRACE("get_proof_bug_after", invocation_counter >= DUMP_AFTER_NUM_INVOCATIONS, tout << l.index() << " " << true_literal.index() << " " << false_literal.index() << " "; m_ctx.display_literal(tout, l); tout << " --->\n"; @@ -1040,7 +1040,7 @@ namespace smt { } } } - + /** \brief Return the proof object associated with the given justification if it already exists. Otherwise, return 0 and add js to the todo-list. @@ -1094,7 +1094,7 @@ namespace smt { i = 2; } } - for (; i < num_lits; i++) + for (; i < num_lits; i++) if (get_proof(~cls->get_literal(i)) == 0) visited = false; return visited; @@ -1109,7 +1109,7 @@ namespace smt { SASSERT(pr); TRACE("proof_gen_bug", tout << "lit2pr_saved: #" << l << "\n";); m_lit2proof.insert(l, pr); - TRACE("mk_proof", + TRACE("mk_proof", tout << mk_bounded_pp(m_ctx.bool_var2expr(l.var()), m_manager, 10) << "\n"; tout << "storing proof for: "; m_ctx.display_literal(tout, l); tout << "\n"; tout << mk_ll_pp(pr, m_manager);); @@ -1118,7 +1118,7 @@ namespace smt { /** \brief Given that lhs = ... = rhs, and lhs reaches rhs in the 'proof' tree branch. Then, return true if all proof objects needed to create the proof steps are already - available. Otherwise return false and update m_todo_pr with info about the proof + available. Otherwise return false and update m_todo_pr with info about the proof objects that need to be created. */ bool conflict_resolution::visit_trans_proof(enode * lhs, enode * rhs) { @@ -1174,7 +1174,7 @@ namespace smt { /** \brief Return true if all proof objects that are used to build the proof that lhs = rhs were - already built. If the result is false, then m_todo_pr is updated with info about the proof + already built. If the result is false, then m_todo_pr is updated with info about the proof objects that need to be created. */ bool conflict_resolution::visit_eq_justications(enode * lhs, enode * rhs) { @@ -1226,7 +1226,7 @@ namespace smt { if (prs1.size() == 1) pr = prs1[0]; else { - TRACE("mk_transitivity", + TRACE("mk_transitivity", unsigned sz = prs1.size(); for (unsigned i = 0; i < sz; i++) { tout << mk_ll_pp(prs1[i], m_manager) << "\n"; @@ -1288,7 +1288,7 @@ namespace smt { } case tp_elem::LITERAL: { literal l = to_literal(elem.m_lidx); - if (m_lit2proof.contains(l)) + if (m_lit2proof.contains(l)) m_todo_pr.pop_back(); else { b_justification js = m_ctx.get_justification(l.var()); @@ -1342,11 +1342,11 @@ namespace smt { void conflict_resolution::process_antecedent_for_unsat_core(literal antecedent) { bool_var var = antecedent.var(); - TRACE("conflict", tout << "processing antecedent: "; - m_ctx.display_literal_info(tout << antecedent << " ", antecedent); - tout << (m_ctx.is_marked(var)?"marked":"not marked"); - tout << "\n";); - + TRACE("conflict", tout << "processing antecedent: "; + m_ctx.display_literal_info(tout << antecedent << " ", antecedent); + tout << (m_ctx.is_marked(var)?"marked":"not marked"); + tout << "\n";); + if (!m_ctx.is_marked(var)) { m_ctx.set_mark(var); m_unmark.push_back(var); @@ -1355,7 +1355,7 @@ namespace smt { m_assumptions.push_back(antecedent); } } - + void conflict_resolution::process_justification_for_unsat_core(justification * js) { literal_vector & antecedents = m_tmp_literal_vector; antecedents.reset(); @@ -1370,7 +1370,7 @@ namespace smt { SASSERT(m_ctx.tracking_assumptions()); m_assumptions.reset(); m_unmark.reset(); - + SASSERT(m_conflict_lvl <= m_ctx.get_search_level()); unsigned search_lvl = m_ctx.get_search_level(); @@ -1378,17 +1378,17 @@ namespace smt { literal consequent = false_literal; if (not_l != null_literal) { consequent = ~not_l; - } - + } + int idx = skip_literals_above_conflict_level(); - + if (not_l != null_literal) process_antecedent_for_unsat_core(consequent); - + if (m_assigned_literals.empty()) { goto end_unsat_core; } - + while (true) { TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";); switch (js.get_kind()) { @@ -1411,7 +1411,7 @@ namespace smt { process_antecedent_for_unsat_core(~l); } justification * js = cls->get_justification(); - if (js) + if (js) process_justification_for_unsat_core(js); break; } @@ -1430,17 +1430,17 @@ namespace smt { if (m_ctx.is_assumption(consequent.var())) { m_assumptions.push_back(consequent); - } + } while (idx >= 0) { literal l = m_assigned_literals[idx]; TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";); - if (m_ctx.get_assign_level(l) < search_lvl) - goto end_unsat_core; - if (m_ctx.is_marked(l.var())) + if (m_ctx.get_assign_level(l) < search_lvl) + goto end_unsat_core; + if (m_ctx.is_marked(l.var())) break; idx--; } - if (idx < 0) { + if (idx < 0) { goto end_unsat_core; } @@ -1456,12 +1456,12 @@ namespace smt { TRACE("unsat_core", tout << "assumptions:\n"; m_ctx.display_literals(tout, m_assumptions); tout << "\n";); reset_unmark_and_justifications(0, 0); } - - conflict_resolution * mk_conflict_resolution(ast_manager & m, + + conflict_resolution * mk_conflict_resolution(ast_manager & m, context & ctx, dyn_ack_manager & dack_manager, smt_params const & params, - literal_vector const & assigned_literals, + literal_vector const & assigned_literals, vector & watches) { return alloc(conflict_resolution, m, ctx, dack_manager, params, assigned_literals, watches); } From 6b474adc8adb3e8a01a04b76055fa2a59674c48f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 16 Sep 2016 16:48:22 +0100 Subject: [PATCH 02/21] Added accessors to extract sign/exponent/significand BV numerals from FP numerals. --- src/api/api_fpa.cpp | 97 +++++++++++++++++++++++++++++++++++++++++ src/api/dotnet/FPNum.cs | 52 +++++++++++++++++++--- src/api/java/FPNum.java | 27 ++++++++++++ src/api/ml/z3.ml | 3 ++ src/api/ml/z3.mli | 12 +++++ src/api/python/z3/z3.py | 24 ++++++++++ src/api/z3_fpa.h | 36 +++++++++++++++ 7 files changed, 246 insertions(+), 5 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 5d423c725..048113eca 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -909,6 +909,8 @@ extern "C" { Z3_TRY; LOG_Z3_fpa_get_numeral_sign(c, t, sgn); RESET_ERROR_CODE(); + CHECK_NON_NULL(t, 0); + CHECK_VALID_AST(t, 0); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); @@ -929,6 +931,101 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t) { + Z3_TRY; + LOG_Z3_fpa_get_numeral_sign_bv(c, t); + RESET_ERROR_CODE(); + CHECK_NON_NULL(t, 0); + CHECK_VALID_AST(t, 0); + ast_manager & m = mk_c(c)->m(); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); + family_id fid = mk_c(c)->get_fpa_fid(); + fpa_util & fu = mk_c(c)->fpautil(); + api::context * ctx = mk_c(c); + expr * e = to_expr(t); + if (!is_app(e) || + is_app_of(e, fid, OP_FPA_NAN)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + if (is_app_of(e, fid, OP_FPA_PLUS_INF)) { + expr * r = ctx->bvutil().mk_numeral(0, 1); + ctx->save_ast_trail(r); + RETURN_Z3(of_expr(r)); + } + if (is_app_of(e, fid, OP_FPA_MINUS_INF)) { + expr * r = ctx->bvutil().mk_numeral(1, 1); + ctx->save_ast_trail(r); + RETURN_Z3(of_expr(r)); + } + if (!fu.is_fp(e)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + app * a = to_app(e); + RETURN_Z3(of_expr(a->get_arg(0))); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t) { + Z3_TRY; + LOG_Z3_fpa_get_numeral_exponent_bv(c, t); + RESET_ERROR_CODE(); + CHECK_NON_NULL(t, 0); + CHECK_VALID_AST(t, 0); + ast_manager & m = mk_c(c)->m(); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); + family_id fid = mk_c(c)->get_fpa_fid(); + fpa_util & fu = mk_c(c)->fpautil(); + expr * e = to_expr(t); + if (!is_app(e) || + is_app_of(e, fid, OP_FPA_NAN) || + is_app_of(e, fid, OP_FPA_PLUS_INF) || + is_app_of(e, fid, OP_FPA_MINUS_INF)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + if (!fu.is_fp(e)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + api::context * ctx = mk_c(c); + app * a = to_app(e); + RETURN_Z3(of_expr(a->get_arg(1))); + Z3_CATCH_RETURN(0); + } + + Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t) { + Z3_TRY; + LOG_Z3_fpa_get_numeral_significand_bv(c, t); + RESET_ERROR_CODE(); + CHECK_NON_NULL(t, 0); + CHECK_VALID_AST(t, 0); + ast_manager & m = mk_c(c)->m(); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); + family_id fid = mk_c(c)->get_fpa_fid(); + fpa_util & fu = mk_c(c)->fpautil(); + expr * e = to_expr(t); + if (!is_app(e) || + is_app_of(e, fid, OP_FPA_NAN) || + is_app_of(e, fid, OP_FPA_PLUS_INF) || + is_app_of(e, fid, OP_FPA_MINUS_INF)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + if (!fu.is_fp(e)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + api::context * ctx = mk_c(c); + app * a = to_app(e); + RETURN_Z3(of_expr(a->get_arg(2))); + Z3_CATCH_RETURN(0); + } + Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_fpa_get_numeral_significand_string(c, t); diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index ac1fae5f5..ed0367481 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2013-06-10 Notes: - + --*/ using System; using System.Diagnostics.Contracts; @@ -27,6 +27,48 @@ namespace Microsoft.Z3 [ContractVerification(true)] public class FPNum : FPExpr { + /// + /// The sign of a floating-point numeral as a bit-vector expression + /// + /// + /// NaN's do not have a bit-vector sign, so they are invalid arguments. + /// + public BitVecExpr BVSign + { + get + { + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject)); + } + } + + /// + /// The exponent of a floating-point numeral as a bit-vector expression + /// + /// + /// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. + /// + public BitVecExpr BVExponent + { + get + { + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject)); + } + } + + /// + /// The significand of a floating-point numeral as a bit-vector expression + /// + /// + /// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. + /// + public BitVecExpr BVSignificand + { + get + { + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject)); + } + } + /// /// Retrieves the sign of a floating-point literal /// @@ -38,7 +80,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) throw new Z3Exception("Sign is not a Boolean value"); return res != 0; } @@ -63,7 +105,7 @@ namespace Microsoft.Z3 /// The significand value of a floating-point numeral as a UInt64 /// /// - /// This function extracts the significand bits, without the + /// This function extracts the significand bits, without the /// hidden bit or normalization. Throws an exception if the /// significand does not fit into a UInt64. /// @@ -73,7 +115,7 @@ namespace Microsoft.Z3 { UInt64 result = 0; if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) - throw new Z3Exception("Significand is not a 64 bit unsigned integer"); + throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return result; } } @@ -113,7 +155,7 @@ namespace Microsoft.Z3 /// /// Returns a string representation of the numeral. - /// + /// public override string ToString() { return Native.Z3_get_numeral_string(Context.nCtx, NativeObject); diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 402d25ebe..7bfca0f86 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -21,6 +21,33 @@ package com.microsoft.z3; */ public class FPNum extends FPExpr { + /** + * The sign of a floating-point numeral as a bit-vector expression + * Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments. + * @throws Z3Exception + */ + public BitVecExpr getBVSign() { + return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject())); + } + + /** + * The exponent of a floating-point numeral as a bit-vector expression + * Remarks: +oo, -oo, and NaN's do not have a bit-vector exponent, so they are invalid arguments. + * @throws Z3Exception + */ + public BitVecExpr getBVExponent() { + return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject())); + } + + /** + * The significand of a floating-point numeral as a bit-vector expression + * Remarks: +oo, -oo, and NaN's do not have a bit-vector significand, so they are invalid arguments. + * @throws Z3Exception + */ + public BitVecExpr getBVSignificand() { + return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject())); + } + /** * Retrieves the sign of a floating-point literal * Remarks: returns true if the numeral is negative diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index b7016c4c8..613db591e 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1324,6 +1324,9 @@ struct let mk_to_real = Z3native.mk_fpa_to_real let get_ebits = Z3native.fpa_get_ebits let get_sbits = Z3native.fpa_get_sbits + let get_numeral_sign_bv = Z3native.fpa_get_numeral_sign_bv + let get_numeral_exponent_bv = Z3native.fpa_get_numeral_exponent_bv + let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv let get_numeral_sign = Z3native.fpa_get_numeral_sign let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 1c91b28aa..e08028c61 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2138,6 +2138,18 @@ sig (** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *) val get_sbits : context -> Sort.sort -> int + (** Return the sign of a floating-point numeral as a bit-vector expression. + Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. *) + val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr + + (** Return the exponent of a floating-point numeral as a bit-vector expression. + Remark: +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. *) + val get_numeral_exponent_bv : context -> Expr.expr -> Expr.expr + + (** Return the significand value of a floating-point numeral as a bit-vector expression. + Remark: +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. *) + val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr + (** Retrieves the sign of a floating-point literal. *) val get_numeral_sign : context -> Expr.expr -> bool * int diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a037bbc5d..fc9ef6d62 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8446,6 +8446,30 @@ class FPNumRef(FPRef): k = self.decl().kind() return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True) + """ + The sign of a floating-point numeral as a bit-vector expression + + Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. + """ + def BVSign(self): + return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), ctx) + + """ + The exponent of a floating-point numeral as a bit-vector expression + + Remark: +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. + """ + def BVExponent(self): + return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast()), ctx) + + """ + The sign of a floating-point numeral as a bit-vector expression + + Remark: +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. + """ + def BVSignificand(self): + return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), ctx) + """ The sign of the numeral. diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 510fa0473..9abbb7b60 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -822,6 +822,42 @@ extern "C" { */ unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s); + /** + \brief Retrieves the sign of a floating-point literal as a bit-vector expression. + + \param c logical context + \param t a floating-point numeral + + Remarks: NaN is an invalid argument. + + def_API('Z3_fpa_get_numeral_sign_bv', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t); + + /** + \brief Retrieves the significand of a floating-point literal as a bit-vector expression. + + \param c logical context + \param t a floating-point numeral + + Remarks: +oo, -oo and NaN are invalid arguments. + + def_API('Z3_fpa_get_numeral_significand_bv', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t); + + /** + \brief Retrieves the exponent of a floating-point literal as a bit-vector expression. + + \param c logical context + \param t a floating-point numeral + + Remarks: +oo, -oo and NaN are invalid arguments. + + def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t); + /** \brief Retrieves the sign of a floating-point literal. From 89d38385db100947e25229d40e5f2b88909e2891 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 17 Oct 2016 13:31:07 +0100 Subject: [PATCH 03/21] Added functions to test FP numerals for special values. --- src/api/api_fpa.cpp | 96 +++++++++++++++++++++++++++++++++++++++ src/api/z3_fpa.h | 60 ++++++++++++++++++++++++ src/ast/fpa_decl_plugin.h | 4 ++ 3 files changed, 160 insertions(+) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 048113eca..cc8648c2a 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1183,4 +1183,100 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) { + Z3_TRY; + Z3_fpa_is_numeral_nan(c, t); + RESET_ERROR_CODE(); + ast_manager & m = mk_c(c)->m(); + api::context * ctx = mk_c(c); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + fpa_util & fu = ctx->fpautil(); + if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + return fu.is_nan(to_expr(t)); + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) { + Z3_TRY; + Z3_fpa_is_numeral_inf(c, t); + RESET_ERROR_CODE(); + ast_manager & m = mk_c(c)->m(); + api::context * ctx = mk_c(c); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + fpa_util & fu = ctx->fpautil(); + if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + return fu.is_inf(to_expr(t)); + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) { + Z3_TRY; + Z3_fpa_is_numeral_zero(c, t); + RESET_ERROR_CODE(); + ast_manager & m = mk_c(c)->m(); + api::context * ctx = mk_c(c); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + fpa_util & fu = ctx->fpautil(); + if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + return fu.is_zero(to_expr(t)); + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) { + Z3_TRY; + Z3_fpa_is_numeral_normal(c, t); + RESET_ERROR_CODE(); + ast_manager & m = mk_c(c)->m(); + api::context * ctx = mk_c(c); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + fpa_util & fu = ctx->fpautil(); + if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + return fu.is_normal(to_expr(t)); + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) { + Z3_TRY; + Z3_fpa_is_numeral_subnormal(c, t); + RESET_ERROR_CODE(); + ast_manager & m = mk_c(c)->m(); + api::context * ctx = mk_c(c); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + fpa_util & fu = ctx->fpautil(); + if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + return fu.is_subnormal(to_expr(t)); + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) { + Z3_TRY; + Z3_fpa_is_numeral_positive(c, t); + RESET_ERROR_CODE(); + ast_manager & m = mk_c(c)->m(); + api::context * ctx = mk_c(c); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + fpa_util & fu = ctx->fpautil(); + if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + return fu.is_positive(to_expr(t)); + Z3_CATCH_RETURN(Z3_FALSE); + } + }; diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 9abbb7b60..d5da90808 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -822,6 +822,66 @@ extern "C" { */ unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s); + /** + \brief Checks whether a given floating-point numeral is a NaN. + + \param c logical context + \param t a floating-point numeral + + def_API('Z3_fpa_is_numeral_nan', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t); + + /** + \brief Checks whether a given floating-point numeral is a +oo or -oo. + + \param c logical context + \param t a floating-point numeral + + def_API('Z3_fpa_is_numeral_inf', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t); + + /** + \brief Checks whether a given floating-point numeral is +zero or -zero. + + \param c logical context + \param t a floating-point numeral + + def_API('Z3_fpa_is_numeral_zero', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t); + + /** + \brief Checks whether a given floating-point numeral is normal. + + \param c logical context + \param t a floating-point numeral + + def_API('Z3_fpa_is_numeral_normal', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t); + + /** + \brief Checks whether a given floating-point numeral is subnormal. + + \param c logical context + \param t a floating-point numeral + + def_API('Z3_fpa_is_numeral_subnormal', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t); + + /** + \brief Checks whether a given floating-point numeral is positive. + + \param c logical context + \param t a floating-point numeral + + def_API('Z3_fpa_is_numeral_positive', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t); + /** \brief Retrieves the sign of a floating-point literal as a bit-vector expression. diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index c00bed7ae..7c9c311a8 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -288,11 +288,15 @@ public: app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); } bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); } + bool is_inf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_inf(v); } bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); } bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); } bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); } bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); } bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); } + bool is_normal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_normal(v); } + bool is_subnormal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_denormal(v); } + bool is_positive(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pos(v); } app * mk_fp(expr * sgn, expr * exp, expr * sig) { SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); From 8926b3311da59c2298035b1ca4e33727b5bceeb7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 17 Oct 2016 14:05:38 +0100 Subject: [PATCH 04/21] Fixed FP numeral special value sig/exp extraction functions. --- src/api/z3_fpa.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index d5da90808..5544099d6 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -828,7 +828,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - def_API('Z3_fpa_is_numeral_nan', AST, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_is_numeral_nan', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t); @@ -838,7 +838,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - def_API('Z3_fpa_is_numeral_inf', AST, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_is_numeral_inf', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t); @@ -848,7 +848,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - def_API('Z3_fpa_is_numeral_zero', AST, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_is_numeral_zero', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t); @@ -858,7 +858,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - def_API('Z3_fpa_is_numeral_normal', AST, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_is_numeral_normal', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t); @@ -868,7 +868,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - def_API('Z3_fpa_is_numeral_subnormal', AST, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_is_numeral_subnormal', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t); @@ -878,7 +878,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - def_API('Z3_fpa_is_numeral_positive', AST, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_is_numeral_positive', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t); From 0a11e8f3c00d35e1acdbe729c13b019a3875073b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 21 Oct 2016 16:00:56 +0100 Subject: [PATCH 05/21] Resolved rebase conflicts --- src/api/api_fpa.cpp | 94 +++++++++++++++++++++++++++------------------ 1 file changed, 56 insertions(+), 38 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index cc8648c2a..ce0cf1ae6 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -913,8 +913,9 @@ extern "C" { CHECK_VALID_AST(t, 0); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); - fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); family_id fid = mk_c(c)->get_fpa_fid(); + fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); + fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -941,30 +942,27 @@ extern "C" { mpf_manager & mpfm = mk_c(c)->fpautil().fm(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); family_id fid = mk_c(c)->get_fpa_fid(); + fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); fpa_util & fu = mk_c(c)->fpautil(); api::context * ctx = mk_c(c); expr * e = to_expr(t); - if (!is_app(e) || - is_app_of(e, fid, OP_FPA_NAN)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - if (is_app_of(e, fid, OP_FPA_PLUS_INF)) { - expr * r = ctx->bvutil().mk_numeral(0, 1); - ctx->save_ast_trail(r); - RETURN_Z3(of_expr(r)); - } - if (is_app_of(e, fid, OP_FPA_MINUS_INF)) { - expr * r = ctx->bvutil().mk_numeral(1, 1); - ctx->save_ast_trail(r); - RETURN_Z3(of_expr(r)); - } - if (!fu.is_fp(e)) { + scoped_mpf val(mpfm); + bool r = plugin->is_numeral(to_expr(t), val); + if (!r || mpfm.is_nan(val)) { SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); + return 0; } - app * a = to_app(e); - RETURN_Z3(of_expr(a->get_arg(0))); + app * a; + if (mpfm.is_pos(val)) + a = ctx->bvutil().mk_numeral(0, 1); + else + a = ctx->bvutil().mk_numeral(1, 1); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -978,22 +976,31 @@ extern "C" { mpf_manager & mpfm = mk_c(c)->fpautil().fm(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); family_id fid = mk_c(c)->get_fpa_fid(); + fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); - if (!is_app(e) || - is_app_of(e, fid, OP_FPA_NAN) || - is_app_of(e, fid, OP_FPA_PLUS_INF) || - is_app_of(e, fid, OP_FPA_MINUS_INF)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - if (!fu.is_fp(e)) { + scoped_mpf val(mpfm); + bool r = plugin->is_numeral(e, val); + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - api::context * ctx = mk_c(c); - app * a = to_app(e); - RETURN_Z3(of_expr(a->get_arg(1))); + unsigned ebits = val.get().get_ebits(); + mpf_exp_t q = mpfm.exp(val); + mpf_exp_t q_biassed = mpfm.bias_exp(ebits, q); + app * a; + if (mpfm.is_inf(val)) + a = mk_c(c)->bvutil().mk_numeral(-1, ebits); + else if (mpfm.is_zero(val) || mpfm.is_denormal(val)) + a = mk_c(c)->bvutil().mk_numeral(0, ebits); + else + a = mk_c(c)->bvutil().mk_numeral(q_biassed, ebits); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -1007,22 +1014,27 @@ extern "C" { mpf_manager & mpfm = mk_c(c)->fpautil().fm(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); family_id fid = mk_c(c)->get_fpa_fid(); + fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); + SASSERT(plugin != 0); fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); - if (!is_app(e) || - is_app_of(e, fid, OP_FPA_NAN) || - is_app_of(e, fid, OP_FPA_PLUS_INF) || - is_app_of(e, fid, OP_FPA_MINUS_INF)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - if (!fu.is_fp(e)) { + scoped_mpf val(mpfm); + bool r = plugin->is_numeral(e, val); + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - api::context * ctx = mk_c(c); - app * a = to_app(e); - RETURN_Z3(of_expr(a->get_arg(2))); + unsigned sbits = val.get().get_sbits(); + scoped_mpq q(mpqm); + mpqm.set(q, mpfm.sig(val)); + if (mpfm.is_inf(val)) mpqm.set(q, 0); + app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -1038,6 +1050,7 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); SASSERT(plugin != 0); + fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1045,8 +1058,8 @@ extern "C" { } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); - if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG) + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { + SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } unsigned sbits = val.get().get_sbits(); @@ -1071,6 +1084,7 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); SASSERT(plugin != 0); + fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1081,7 +1095,7 @@ extern "C" { bool r = plugin->is_numeral(e, val); const mpz & z = mpfm.sig(val); if (!r || - !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val)) || + !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val)) || !mpzm.is_uint64(z)) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; @@ -1101,6 +1115,7 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); + fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1108,12 +1123,13 @@ extern "C" { } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); - if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } mpf_exp_t exp = mpfm.is_zero(val) ? 0 : mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) : mpfm.exp(val); std::stringstream ss; ss << exp; @@ -1130,6 +1146,7 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); + fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1138,13 +1155,14 @@ extern "C" { } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); - if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; return 0; } *n = mpfm.is_zero(val) ? 0 : mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) : mpfm.exp(val); return 1; Z3_CATCH_RETURN(0); From abcb6040d4593545a7019a4f4431444bc4d03dad Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 21 Oct 2016 17:39:31 +0100 Subject: [PATCH 06/21] Refactored FPA numeral accessors. --- src/api/api_fpa.cpp | 102 +++++++++++++++++---------------- src/api/dotnet/FPNum.cs | 71 ++++++++++------------- src/api/java/FPNum.java | 66 ++++++++++----------- src/api/python/z3/z3.py | 60 +++++++++---------- src/api/python/z3/z3printer.py | 4 +- src/api/z3_fpa.h | 44 ++++++++------ 6 files changed, 175 insertions(+), 172 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index ce0cf1ae6..669df8666 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -946,7 +946,7 @@ extern "C" { fpa_util & fu = mk_c(c)->fpautil(); api::context * ctx = mk_c(c); expr * e = to_expr(t); - if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } @@ -956,6 +956,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } + std::cout << "val=" << mpfm.to_string(val) << std::endl; app * a; if (mpfm.is_pos(val)) a = ctx->bvutil().mk_numeral(0, 1); @@ -966,44 +967,6 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t) { - Z3_TRY; - LOG_Z3_fpa_get_numeral_exponent_bv(c, t); - RESET_ERROR_CODE(); - CHECK_NON_NULL(t, 0); - CHECK_VALID_AST(t, 0); - ast_manager & m = mk_c(c)->m(); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); - unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); - family_id fid = mk_c(c)->get_fpa_fid(); - fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); - fpa_util & fu = mk_c(c)->fpautil(); - expr * e = to_expr(t); - if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { - SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); - } - scoped_mpf val(mpfm); - bool r = plugin->is_numeral(e, val); - if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); - } - unsigned ebits = val.get().get_ebits(); - mpf_exp_t q = mpfm.exp(val); - mpf_exp_t q_biassed = mpfm.bias_exp(ebits, q); - app * a; - if (mpfm.is_inf(val)) - a = mk_c(c)->bvutil().mk_numeral(-1, ebits); - else if (mpfm.is_zero(val) || mpfm.is_denormal(val)) - a = mk_c(c)->bvutil().mk_numeral(0, ebits); - else - a = mk_c(c)->bvutil().mk_numeral(q_biassed, ebits); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_expr(a)); - Z3_CATCH_RETURN(0); - } - Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_fpa_get_numeral_significand_bv(c, t); @@ -1018,7 +981,7 @@ extern "C" { SASSERT(plugin != 0); fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); - if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } @@ -1106,9 +1069,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t) { + Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased) { Z3_TRY; - LOG_Z3_fpa_get_numeral_exponent_string(c, t); + LOG_Z3_fpa_get_numeral_exponent_string(c, t, biased); RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); @@ -1127,19 +1090,21 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } + unsigned ebits = val.get().get_ebits(); mpf_exp_t exp = mpfm.is_zero(val) ? 0 : - mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : - mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) : - mpfm.exp(val); + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + if (!biased) mpfm.unbias_exp(ebits, exp); std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); Z3_CATCH_RETURN(""); } - Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n) { + Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased) { Z3_TRY; - LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n); + LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n, biased); RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); @@ -1160,14 +1125,51 @@ extern "C" { *n = 0; return 0; } + unsigned ebits = val.get().get_ebits(); *n = mpfm.is_zero(val) ? 0 : - mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : - mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) : - mpfm.exp(val); + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + if (!biased) *n = mpfm.unbias_exp(ebits, *n); return 1; Z3_CATCH_RETURN(0); } + Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased) { + Z3_TRY; + LOG_Z3_fpa_get_numeral_exponent_bv(c, t, biased); + RESET_ERROR_CODE(); + CHECK_NON_NULL(t, 0); + CHECK_VALID_AST(t, 0); + ast_manager & m = mk_c(c)->m(); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); + family_id fid = mk_c(c)->get_fpa_fid(); + fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); + fpa_util & fu = mk_c(c)->fpautil(); + expr * e = to_expr(t); + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + scoped_mpf val(mpfm); + bool r = plugin->is_numeral(e, val); + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + RETURN_Z3(0); + } + unsigned ebits = val.get().get_ebits(); + mpf_exp_t exp = mpfm.is_zero(val) ? 0 : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + if (!biased) exp = mpfm.unbias_exp(ebits, exp); + app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_expr(a)); + Z3_CATCH_RETURN(0); + } + Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_to_ieee_bv(c, t); diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index ed0367481..705e7304e 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// /// NaN's do not have a bit-vector sign, so they are invalid arguments. /// - public BitVecExpr BVSign + public BitVecExpr SignBV { get { @@ -41,34 +41,6 @@ namespace Microsoft.Z3 } } - /// - /// The exponent of a floating-point numeral as a bit-vector expression - /// - /// - /// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. - /// - public BitVecExpr BVExponent - { - get - { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject)); - } - } - - /// - /// The significand of a floating-point numeral as a bit-vector expression - /// - /// - /// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. - /// - public BitVecExpr BVSignificand - { - get - { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject)); - } - } - /// /// Retrieves the sign of a floating-point literal /// @@ -121,28 +93,47 @@ namespace Microsoft.Z3 } /// - /// Return the exponent value of a floating-point numeral as a string + /// The significand of a floating-point numeral as a bit-vector expression /// - public string Exponent + /// + /// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. + /// + public BitVecExpr SignificandBV { get { - return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject); + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject)); } } + /// + /// Return the (biased) exponent value of a floating-point numeral as a string + /// + public string Exponent(bool biased = true) + { + return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0); + } + /// /// Return the exponent value of a floating-point numeral as a signed 64-bit integer /// - public Int64 ExponentInt64 + public Int64 ExponentInt64(bool biased = true) { - get - { - Int64 result = 0; - if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0) - throw new Z3Exception("Exponent is not a 64 bit integer"); - return result; - } + Int64 result = 0; + if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0) + throw new Z3Exception("Exponent is not a 64 bit integer"); + return result; + } + + /// + /// The exponent of a floating-point numeral as a bit-vector expression + /// + /// + /// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. + /// + public BitVecExpr ExponentBV(bool biased = true) + { + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0)); } #region Internal diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 7bfca0f86..252d9e012 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -20,34 +20,7 @@ package com.microsoft.z3; * FloatingPoint Numerals */ public class FPNum extends FPExpr -{ - /** - * The sign of a floating-point numeral as a bit-vector expression - * Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments. - * @throws Z3Exception - */ - public BitVecExpr getBVSign() { - return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject())); - } - - /** - * The exponent of a floating-point numeral as a bit-vector expression - * Remarks: +oo, -oo, and NaN's do not have a bit-vector exponent, so they are invalid arguments. - * @throws Z3Exception - */ - public BitVecExpr getBVExponent() { - return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject())); - } - - /** - * The significand of a floating-point numeral as a bit-vector expression - * Remarks: +oo, -oo, and NaN's do not have a bit-vector significand, so they are invalid arguments. - * @throws Z3Exception - */ - public BitVecExpr getBVSignificand() { - return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject())); - } - +{ /** * Retrieves the sign of a floating-point literal * Remarks: returns true if the numeral is negative @@ -60,6 +33,15 @@ public class FPNum extends FPExpr return res.value != 0; } + /** + * The sign of a floating-point numeral as a bit-vector expression + * Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments. + * @throws Z3Exception + */ + public BitVecExpr getSignBV() { + return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject())); + } + /** * The significand value of a floating-point numeral as a string * Remarks: The significand s is always 0 < s < 2.0; the resulting string is long @@ -84,25 +66,45 @@ public class FPNum extends FPExpr throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return res.value; } + + /** + * The significand of a floating-point numeral as a bit-vector expression + * Remarks: NaN is an invalid argument. + * @throws Z3Exception + */ + public BitVecExpr getSignificandBV() { + return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject())); + } /** * Return the exponent value of a floating-point numeral as a string + * Remarks: NaN is an invalid argument. * @throws Z3Exception */ - public String getExponent() { - return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject()); + public String getExponent(boolean biased) { + return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased); } /** * Return the exponent value of a floating-point numeral as a signed 64-bit integer + * Remarks: NaN is an invalid argument. * @throws Z3Exception */ - public long getExponentInt64() { + public long getExponentInt64(boolean biased) { Native.LongPtr res = new Native.LongPtr(); - if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res)) + if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased)) throw new Z3Exception("Exponent is not a 64 bit integer"); return res.value; } + + /** + * The exponent of a floating-point numeral as a bit-vector expression + * Remarks: NaN is an invalid argument. + * @throws Z3Exception + */ + public BitVecExpr getExponentBV(boolean biased) { + return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased)); + } public FPNum(Context ctx, long obj) { diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index fc9ef6d62..e651fc04f 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8445,31 +8445,7 @@ class FPNumRef(FPRef): def isNegative(self): k = self.decl().kind() return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True) - - """ - The sign of a floating-point numeral as a bit-vector expression - - Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. - """ - def BVSign(self): - return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), ctx) - """ - The exponent of a floating-point numeral as a bit-vector expression - - Remark: +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments. - """ - def BVExponent(self): - return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast()), ctx) - - """ - The sign of a floating-point numeral as a bit-vector expression - - Remark: +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments. - """ - def BVSignificand(self): - return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), ctx) - """ The sign of the numeral. @@ -8486,6 +8462,15 @@ class FPNumRef(FPRef): raise Z3Exception("error retrieving the sign of a numeral.") return l.value != 0 + """ + The sign of a floating-point numeral as a bit-vector expression + + Remark: NaN's are invalid arguments. + """ + def sign_as_bv(self): + return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) + + """ The significand of the numeral. @@ -8495,6 +8480,14 @@ class FPNumRef(FPRef): """ def significand(self): return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) + + """ + The significand of a floating-point numeral as a bit-vector expression + + Remark: NaN are invalid arguments. + """ + def significand_as_bv(self): + return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) """ The exponent of the numeral. @@ -8503,8 +8496,8 @@ class FPNumRef(FPRef): >>> x.exponent() 1 """ - def exponent(self): - return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast()) + def exponent(self, biased=True): + return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) """ The exponent of the numeral as a long. @@ -8513,12 +8506,21 @@ class FPNumRef(FPRef): >>> x.exponent_as_long() 1 """ - def exponent_as_long(self): + def exponent_as_long(self, biased=True): ptr = (ctypes.c_longlong * 1)() - if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr): + if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased): raise Z3Exception("error retrieving the exponent of a numeral.") return ptr[0] + """ + The exponent of a floating-point numeral as a bit-vector expression + + Remark: NaNs are invalid arguments. + """ + def exponent_as_bv(self, biased=True): + return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) + + """ The string representation of the numeral. @@ -8527,7 +8529,7 @@ class FPNumRef(FPRef): 1.25*(2**4) """ def as_string(self): - s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast()) + s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast()) return ("FPVal(%s, %s)" % (s, self.sort())) def is_fp(a): diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 2e3a528bf..8a67fa911 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -620,8 +620,8 @@ class Formatter: r = [] sgn = c_int(0) sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) + exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False) sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast) - exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast) r.append(to_format('FPVal(')) if sgnb and sgn.value != 0: r.append(to_format('-')) @@ -650,8 +650,8 @@ class Formatter: r = [] sgn = (ctypes.c_int)(0) sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn)) + exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False) sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast) - exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast) if sgnb and sgn.value != 0: r.append(to_format('-')) r.append(to_format(sig)) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 5544099d6..420106838 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -900,24 +900,12 @@ extern "C" { \param c logical context \param t a floating-point numeral - Remarks: +oo, -oo and NaN are invalid arguments. + Remarks: NaN is an invalid argument. def_API('Z3_fpa_get_numeral_significand_bv', AST, (_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t); - /** - \brief Retrieves the exponent of a floating-point literal as a bit-vector expression. - - \param c logical context - \param t a floating-point numeral - - Remarks: +oo, -oo and NaN are invalid arguments. - - def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST))) - */ - Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t); - /** \brief Retrieves the sign of a floating-point literal. @@ -954,23 +942,25 @@ extern "C" { Remarks: This function extracts the significand bits in `t`, without the hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the - significand does not fit into a uint64. + significand does not fit into a uint64. NaN is an invalid argument. def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64))) */ Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n); /** - \brief Return the exponent value of a floating-point numeral as a string + \brief Return the exponent value of a floating-point numeral as a string. \param c logical context \param t a floating-point numeral + \param biased flag to indicate whether the result is in biased representation Remarks: This function extracts the exponent in `t`, without normalization. + NaN is an invalid argument. - def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST))) + def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST), _in(BOOL))) */ - Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t); + Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased); /** \brief Return the exponent value of a floating-point numeral as a signed 64-bit integer @@ -978,12 +968,28 @@ extern "C" { \param c logical context \param t a floating-point numeral \param n exponent + \param biased flag to indicate whether the result is in biased representation Remarks: This function extracts the exponent in `t`, without normalization. + NaN is an invalid argument. - def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) + def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _in(BOOL))) */ - Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n); + Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased); + + /** + \brief Retrieves the exponent of a floating-point literal as a bit-vector expression. + + \param c logical context + \param t a floating-point numeral + \param biased flag to indicate whether the result is in biased representation + + Remarks: This function extracts the exponent in `t`, without normalization. + NaN is an invalid arguments. + + def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST), _in(BOOL))) + */ + Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased); /** \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. From 5fee1ea3c0719b953ea5f3cae0784c5fe12cb78d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 24 Oct 2016 14:08:33 +0100 Subject: [PATCH 07/21] removed unused variables --- src/api/api_fpa.cpp | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 669df8666..9b8934d30 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -915,7 +915,6 @@ extern "C" { mpf_manager & mpfm = mk_c(c)->fpautil().fm(); family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); - fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -940,10 +939,8 @@ extern "C" { CHECK_VALID_AST(t, 0); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); - unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); - fpa_util & fu = mk_c(c)->fpautil(); api::context * ctx = mk_c(c); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { @@ -979,7 +976,6 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); SASSERT(plugin != 0); - fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1013,7 +1009,6 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); SASSERT(plugin != 0); - fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1047,7 +1042,6 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); SASSERT(plugin != 0); - fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1078,7 +1072,6 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); - fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1111,7 +1104,6 @@ extern "C" { family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); - fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1143,10 +1135,8 @@ extern "C" { CHECK_VALID_AST(t, 0); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); - unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); - fpa_util & fu = mk_c(c)->fpautil(); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1207,9 +1197,7 @@ extern "C" { Z3_TRY; Z3_fpa_is_numeral_nan(c, t); RESET_ERROR_CODE(); - ast_manager & m = mk_c(c)->m(); api::context * ctx = mk_c(c); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1223,9 +1211,7 @@ extern "C" { Z3_TRY; Z3_fpa_is_numeral_inf(c, t); RESET_ERROR_CODE(); - ast_manager & m = mk_c(c)->m(); api::context * ctx = mk_c(c); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1239,9 +1225,7 @@ extern "C" { Z3_TRY; Z3_fpa_is_numeral_zero(c, t); RESET_ERROR_CODE(); - ast_manager & m = mk_c(c)->m(); api::context * ctx = mk_c(c); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1255,9 +1239,7 @@ extern "C" { Z3_TRY; Z3_fpa_is_numeral_normal(c, t); RESET_ERROR_CODE(); - ast_manager & m = mk_c(c)->m(); api::context * ctx = mk_c(c); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1271,9 +1253,7 @@ extern "C" { Z3_TRY; Z3_fpa_is_numeral_subnormal(c, t); RESET_ERROR_CODE(); - ast_manager & m = mk_c(c)->m(); api::context * ctx = mk_c(c); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1287,9 +1267,7 @@ extern "C" { Z3_TRY; Z3_fpa_is_numeral_positive(c, t); RESET_ERROR_CODE(); - ast_manager & m = mk_c(c)->m(); api::context * ctx = mk_c(c); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { SET_ERROR_CODE(Z3_INVALID_ARG); From dc78a0413528087ba8fc1148840655de808848d2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Oct 2016 12:20:45 +0100 Subject: [PATCH 08/21] removed debug output --- src/api/api_fpa.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 9b8934d30..8196fb826 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -953,7 +953,6 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - std::cout << "val=" << mpfm.to_string(val) << std::endl; app * a; if (mpfm.is_pos(val)) a = ctx->bvutil().mk_numeral(0, 1); From 963dfad10e304a6677c9e16dfb97f4c6ca478d6f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Oct 2016 14:15:43 +0100 Subject: [PATCH 09/21] fix for biased flag on get_numeral_exponent_string --- src/api/api_fpa.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 8196fb826..b24b7df0a 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1087,7 +1087,7 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); - if (!biased) mpfm.unbias_exp(ebits, exp); + if (!biased) exp = mpfm.unbias_exp(ebits, exp); std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); From cf93e39666d286faea77475725657f0caf1bb6f8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Oct 2016 15:54:33 +0100 Subject: [PATCH 10/21] Fixed FPA unbiased exponent accessors --- src/api/api_fpa.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index b24b7df0a..dc06bae5b 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1087,7 +1087,8 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); - if (!biased) exp = mpfm.unbias_exp(ebits, exp); + if (mpfm.is_normal(val) && !biased) + exp = mpfm.exp(val); std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); @@ -1121,7 +1122,8 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); - if (!biased) *n = mpfm.unbias_exp(ebits, *n); + if (mpfm.is_normal(val) && !biased) + *n = mpfm.exp(val); return 1; Z3_CATCH_RETURN(0); } @@ -1152,7 +1154,11 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); - if (!biased) exp = mpfm.unbias_exp(ebits, exp); + if (mpfm.is_normal(val) && !biased) { + std::cout << "unbiassing" << std::endl; + exp = mpfm.exp(val); + } + app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_expr(a)); From c573a7446bfe8038d0692a0cfd738fbdb557c339 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Oct 2016 18:44:25 +0100 Subject: [PATCH 11/21] Added FPA numeral predicates to .NET API --- src/api/dotnet/FPNum.cs | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index 705e7304e..05eda00b3 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -136,6 +136,36 @@ namespace Microsoft.Z3 return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0)); } + /// + /// Indicates whether the numeral is a NaN. + /// + public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } + + /// + /// Indicates whether the numeral is a +oo or -oo. + /// + public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } + + /// + /// Indicates whether the numeral is +zero or -zero. + /// + public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } } + + /// + /// Indicates whether the numeral is normal. + /// + public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } + + /// + /// Indicates whether the numeral is subnormal. + /// + public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } } + + /// + /// Indicates whether the numeral is positive. + /// + public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } + #region Internal internal FPNum(Context ctx, IntPtr obj) : base(ctx, obj) From 935c523ef8ed8672b2e99a45f4d1caca29bfd81b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Oct 2016 18:44:35 +0100 Subject: [PATCH 12/21] Added FPA numeral predicates to Java API --- src/api/java/FPNum.java | 64 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 62 insertions(+), 2 deletions(-) diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 252d9e012..a8f8af4ff 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -105,6 +105,67 @@ public class FPNum extends FPExpr public BitVecExpr getExponentBV(boolean biased) { return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased)); } + + + /** + * Indicates whether the numeral is a NaN. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isNaN() + { + return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject()); + } + + /** + * Indicates whether the numeral is a +oo or -oo. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isInf() + { + return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject()); + } + + /** + * Indicates whether the numeral is +zero or -zero. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isZero() + { + return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject()); + } + + /** + * Indicates whether the numeral is normal. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isNormal() + { + return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject()); + } + + /** + * Indicates whether the numeral is subnormal. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isSubnormal() + { + return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject()); + } + + /** + * Indicates whether the numeral is positive. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isPositive() + { + return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject()); + } public FPNum(Context ctx, long obj) { @@ -117,6 +178,5 @@ public class FPNum extends FPExpr public String toString() { return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } - + } } From 23c58a1ef6aa8ccc33d750921854ab9fb4b3cc42 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Oct 2016 18:53:20 +0100 Subject: [PATCH 13/21] Added FPA numeral predicates to ML API --- src/api/ml/z3.ml | 6 ++++++ src/api/ml/z3.mli | 18 ++++++++++++++++++ 2 files changed, 24 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index dbf36c6a4..565adf976 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1332,6 +1332,12 @@ struct let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64 let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv + let is_numeral_nan = Z3native.fpa_is_numeral_nan + let is_numeral_inf = Z3native.fpa_is_numeral_inf + let is_numeral_zero = Z3native.fpa_is_numeral_zero + let is_numeral_normal = Z3native.fpa_is_numeral_normal + let is_numeral_subnormal = Z3native.fpa_is_numeral_subnormal + let is_numeral_positive = Z3native.fpa_is_numeral_positive let mk_to_ieee_bv = Z3native.mk_fpa_to_ieee_bv let mk_to_fp_int_real = Z3native.mk_fpa_to_fp_int_real let numeral_to_string x = Z3native.get_numeral_string (Expr.gc x) x diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 2a73c08fb..a2ecf54c2 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2168,6 +2168,24 @@ sig significand does not fit into an int. *) val get_numeral_significand_uint : context -> Expr.expr -> bool * int + (** Indicates whether a floating-point numeral is a NaN. *) + val is_numeral_nan : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is +oo or -oo. *) + val is_numeral_inf : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is +zero or -zero. *) + val is_numeral_zero : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is normal. *) + val is_numeral_normal : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is subnormal. *) + val is_numeral_subnormal : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is positive. *) + val is_numeral_positive : context -> Expr.expr -> bool + (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr From e4f7ff98813902ba5a23cfc7ef41629820befb56 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 27 Oct 2016 15:06:24 +0100 Subject: [PATCH 14/21] Added Z3_fpa_is_numeral_negative to FPA API --- src/api/api_fpa.cpp | 34 ++++++++++++++++++++++++---------- src/api/z3_fpa.h | 10 ++++++++++ src/ast/fpa_decl_plugin.h | 1 + 3 files changed, 35 insertions(+), 10 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index dc06bae5b..39294005c 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1087,7 +1087,7 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); - if (mpfm.is_normal(val) && !biased) + if (mpfm.is_normal(val) && !biased) exp = mpfm.exp(val); std::stringstream ss; ss << exp; @@ -1122,7 +1122,7 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); - if (mpfm.is_normal(val) && !biased) + if (mpfm.is_normal(val) && !biased) *n = mpfm.exp(val); return 1; Z3_CATCH_RETURN(0); @@ -1155,10 +1155,10 @@ extern "C" { mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); if (mpfm.is_normal(val) && !biased) { - std::cout << "unbiassing" << std::endl; + std::cout << "unbiassing" << std::endl; exp = mpfm.exp(val); } - + app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_expr(a)); @@ -1200,7 +1200,7 @@ extern "C" { Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) { Z3_TRY; - Z3_fpa_is_numeral_nan(c, t); + LOG_Z3_fpa_is_numeral_nan(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -1214,7 +1214,7 @@ extern "C" { Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) { Z3_TRY; - Z3_fpa_is_numeral_inf(c, t); + LOG_Z3_fpa_is_numeral_inf(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -1228,7 +1228,7 @@ extern "C" { Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) { Z3_TRY; - Z3_fpa_is_numeral_zero(c, t); + LOG_Z3_fpa_is_numeral_zero(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -1242,7 +1242,7 @@ extern "C" { Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) { Z3_TRY; - Z3_fpa_is_numeral_normal(c, t); + LOG_Z3_fpa_is_numeral_normal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -1256,7 +1256,7 @@ extern "C" { Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) { Z3_TRY; - Z3_fpa_is_numeral_subnormal(c, t); + LOG_Z3_fpa_is_numeral_subnormal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -1270,7 +1270,7 @@ extern "C" { Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) { Z3_TRY; - Z3_fpa_is_numeral_positive(c, t); + LOG_Z3_fpa_is_numeral_positive(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -1282,4 +1282,18 @@ extern "C" { Z3_CATCH_RETURN(Z3_FALSE); } + Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t) { + Z3_TRY; + LOG_Z3_fpa_is_numeral_negative(c, t); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + fpa_util & fu = ctx->fpautil(); + if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + return fu.is_negative(to_expr(t)); + Z3_CATCH_RETURN(Z3_FALSE); + } + }; diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 420106838..70fafe6ea 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -882,6 +882,16 @@ extern "C" { */ Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t); + /** + \brief Checks whether a given floating-point numeral is negative. + + \param c logical context + \param t a floating-point numeral + + def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST))) + */ + Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t); + /** \brief Retrieves the sign of a floating-point literal as a bit-vector expression. diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 7c9c311a8..cf341a07b 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -297,6 +297,7 @@ public: bool is_normal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_normal(v); } bool is_subnormal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_denormal(v); } bool is_positive(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pos(v); } + bool is_negative(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_neg(v); } app * mk_fp(expr * sgn, expr * exp, expr * sig) { SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); From 95d7b33ebb2e27e85cc49d8490b3593c1b2e7ec7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 27 Oct 2016 15:07:10 +0100 Subject: [PATCH 15/21] Added is_numeral_negative to .NET and Java APIs --- src/api/dotnet/FPNum.cs | 5 +++++ src/api/java/FPNum.java | 11 +++++++++++ 2 files changed, 16 insertions(+) diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index 05eda00b3..808752eaa 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -166,6 +166,11 @@ namespace Microsoft.Z3 /// public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } + /// + /// Indicates whether the numeral is negative. + /// + public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } } + #region Internal internal FPNum(Context ctx, IntPtr obj) : base(ctx, obj) diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index a8f8af4ff..813e82889 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -166,6 +166,17 @@ public class FPNum extends FPExpr { return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject()); } + + /** + * Indicates whether the numeral is negative. + * @throws Z3Exception on error + * @return a boolean + **/ + public boolean isNegative() + { + return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject()); + } + public FPNum(Context ctx, long obj) { From 253cfeb0af93dc06f246db2f71d8877f3555aa68 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 27 Oct 2016 15:07:34 +0100 Subject: [PATCH 16/21] Added FPA numeral accessors/predicates to Python API --- src/api/python/z3/z3.py | 87 ++++++++++++++++++++++++----------------- 1 file changed, 51 insertions(+), 36 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e651fc04f..a2274e97b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8432,27 +8432,13 @@ def is_fprm_value(a): ### FP Numerals -class FPNumRef(FPRef): - def isNaN(self): - return self.decl().kind() == Z3_OP_FPA_NAN +class FPNumRef(FPRef): + """The sign of the numeral. - def isInf(self): - return self.decl().kind() == Z3_OP_FPA_PLUS_INF or self.decl().kind() == Z3_OP_FPA_MINUS_INF - - def isZero(self): - return self.decl().kind() == Z3_OP_FPA_PLUS_ZERO or self.decl().kind() == Z3_OP_FPA_MINUS_ZERO - - def isNegative(self): - k = self.decl().kind() - return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True) - - """ - The sign of the numeral. - - >>> x = FPNumRef(+1.0, FPSort(8, 24)) + >>> x = FPVal(+1.0, FPSort(8, 24)) >>> x.sign() False - >>> x = FPNumRef(-1.0, FPSort(8, 24)) + >>> x = FPVal(-1.0, FPSort(8, 24)) >>> x.sign() True """ @@ -8462,47 +8448,50 @@ class FPNumRef(FPRef): raise Z3Exception("error retrieving the sign of a numeral.") return l.value != 0 - """ - The sign of a floating-point numeral as a bit-vector expression + """The sign of a floating-point numeral as a bit-vector expression. Remark: NaN's are invalid arguments. """ def sign_as_bv(self): return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx) + """The significand of the numeral. - """ - The significand of the numeral. - - >>> x = FPNumRef(2.5, FPSort(8, 24)) + >>> x = FPVal(2.5, FPSort(8, 24)) >>> x.significand() 1.25 """ def significand(self): return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) - + + """The significand of the numeral as a long. + + >>> x = FPVal(2.5, FPSort(8, 24)) + >>> x.significand_as_long() + 1.25 """ - The significand of a floating-point numeral as a bit-vector expression + def significand_as_long(self): + return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast()) + + """The significand of the numeral as a bit-vector expression. Remark: NaN are invalid arguments. """ def significand_as_bv(self): return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx) - """ - The exponent of the numeral. + """The exponent of the numeral. - >>> x = FPNumRef(2.5, FPSort(8, 24)) + >>> x = FPVal(2.5, FPSort(8, 24)) >>> x.exponent() 1 """ def exponent(self, biased=True): return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased) - """ - The exponent of the numeral as a long. + """The exponent of the numeral as a long. - >>> x = FPNumRef(2.5, FPSort(8, 24)) + >>> x = FPVal(2.5, FPSort(8, 24)) >>> x.exponent_as_long() 1 """ @@ -8512,19 +8501,45 @@ class FPNumRef(FPRef): raise Z3Exception("error retrieving the exponent of a numeral.") return ptr[0] - """ - The exponent of a floating-point numeral as a bit-vector expression + """The exponent of the numeral as a bit-vector expression. Remark: NaNs are invalid arguments. """ def exponent_as_bv(self, biased=True): return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx) + """Indicates whether the numeral is a NaN.""" + def isNaN(self): + return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast()) + + """Indicates whether the numeral is +oo or -oo.""" + def isInf(self): + return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast()) + + """Indicates whether the numeral is +zero or -zero.""" + def isZero(self): + return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast()) + + """Indicates whether the numeral is normal.""" + def isNormal(self): + return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast()) + + """Indicates whether the numeral is subnormal.""" + def isSubnormal(self): + return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast()) + + """Indicates whether the numeral is postitive.""" + def isPositive(self): + return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast()) + + """Indicates whether the numeral is negative.""" + def isNegative(self): + return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast()) """ The string representation of the numeral. - >>> x = FPNumRef(20, FPSort(8, 24)) + >>> x = FPVal(20, FPSort(8, 24)) >>> x.as_string() 1.25*(2**4) """ @@ -8682,7 +8697,7 @@ def FPVal(sig, exp=None, fps=None, ctx=None): >>> v = FPVal(20.0, FPSort(8, 24)) >>> v 1.25*(2**4) - >>> print("0x%.8x" % v.exponent_as_long()) + >>> print("0x%.8x" % v.exponent_as_long(False)) 0x00000004 >>> v = FPVal(2.25, FPSort(8, 24)) >>> v From 9c16d16bc881bdcacbc4374054fce16c3b5bd839 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Oct 2016 12:22:28 +0100 Subject: [PATCH 17/21] removed debug output --- src/api/api_fpa.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 39294005c..46234c0d2 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1154,10 +1154,8 @@ extern "C" { mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.bias_exp(ebits, mpfm.exp(val)); - if (mpfm.is_normal(val) && !biased) { - std::cout << "unbiassing" << std::endl; + if (mpfm.is_normal(val) && !biased) exp = mpfm.exp(val); - } app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits); mk_c(c)->save_ast_trail(a); From 9ebea09d05fab108f8adff2ec8ca9d7c3095859b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 10:28:39 +0000 Subject: [PATCH 18/21] added is_numeral_negative to ML API. --- src/api/ml/z3.ml | 1 + src/api/ml/z3.mli | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 565adf976..2051a2c48 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1338,6 +1338,7 @@ struct let is_numeral_normal = Z3native.fpa_is_numeral_normal let is_numeral_subnormal = Z3native.fpa_is_numeral_subnormal let is_numeral_positive = Z3native.fpa_is_numeral_positive + let is_numeral_negative = Z3native.fpa_is_numeral_negative let mk_to_ieee_bv = Z3native.mk_fpa_to_ieee_bv let mk_to_fp_int_real = Z3native.mk_fpa_to_fp_int_real let numeral_to_string x = Z3native.get_numeral_string (Expr.gc x) x diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index a2ecf54c2..979e0cfab 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2185,6 +2185,9 @@ sig (** Indicates whether a floating-point numeral is positive. *) val is_numeral_positive : context -> Expr.expr -> bool + + (** Indicates whether a floating-point numeral is negative. *) + val is_numeral_negative : context -> Expr.expr -> bool (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr From 758a6d98fb82cd9559a000a9c94b64d94800e296 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 12:35:48 +0000 Subject: [PATCH 19/21] FPA API clarification --- src/api/z3_fpa.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 70fafe6ea..e92b728d7 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -253,9 +253,9 @@ extern "C" { This is the operator named `fp' in the SMT FP theory definition. Note that \c sign is required to be a bit-vector of size 1. Significand and exponent - are required to be greater than 1 and 2 respectively. The FloatingPoint sort + are required to be longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes - of the arguments. + of the arguments. The exponent is assumed to be in IEEE-754 biased representation. \param c logical context \param sgn sign From 4e7077db7039114a3b5ecb20cd04d2d65ceb9c44 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 12:38:12 +0000 Subject: [PATCH 20/21] Bugfix for denormal numeral exponents --- src/api/api_fpa.cpp | 56 +++++++++++++++++++++++++++++---------------- 1 file changed, 36 insertions(+), 20 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 46234c0d2..35c8d8fc1 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -990,7 +990,7 @@ extern "C" { scoped_mpq q(mpqm); mpqm.set(q, mpfm.sig(val)); if (mpfm.is_inf(val)) mpqm.set(q, 0); - app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits); + app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits-1); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); @@ -1083,12 +1083,18 @@ extern "C" { return ""; } unsigned ebits = val.get().get_ebits(); - mpf_exp_t exp = mpfm.is_zero(val) ? 0 : - mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : - mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : - mpfm.bias_exp(ebits, mpfm.exp(val)); - if (mpfm.is_normal(val) && !biased) - exp = mpfm.exp(val); + mpf_exp_t exp; + if (biased) { + exp = mpfm.is_zero(val) ? 0 : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)) + } + else { + exp = mpfm.is_zero(val) ? 0 : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.exp(val); + } std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); @@ -1118,12 +1124,17 @@ extern "C" { return 0; } unsigned ebits = val.get().get_ebits(); - *n = mpfm.is_zero(val) ? 0 : - mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : - mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : - mpfm.bias_exp(ebits, mpfm.exp(val)); - if (mpfm.is_normal(val) && !biased) - *n = mpfm.exp(val); + if (biased) { + *n = mpfm.is_zero(val) ? 0 : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + } + else { + *n = mpfm.is_zero(val) ? 0 : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.exp(val); + } return 1; Z3_CATCH_RETURN(0); } @@ -1150,13 +1161,18 @@ extern "C" { RETURN_Z3(0); } unsigned ebits = val.get().get_ebits(); - mpf_exp_t exp = mpfm.is_zero(val) ? 0 : - mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : - mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : - mpfm.bias_exp(ebits, mpfm.exp(val)); - if (mpfm.is_normal(val) && !biased) - exp = mpfm.exp(val); - + mpf_exp_t exp; + if (biased) { + exp = mpfm.is_zero(val) ? 0 : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.bias_exp(ebits, mpfm.exp(val)); + } + else { + exp = mpfm.is_zero(val) ? 0 : + mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : + mpfm.exp(val); + } app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_expr(a)); From 80e136f09097b9fa1b274255a163f78507c7a178 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Nov 2016 13:51:09 +0000 Subject: [PATCH 21/21] build fix --- src/api/api_fpa.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 35c8d8fc1..4454cc577 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1087,7 +1087,7 @@ extern "C" { if (biased) { exp = mpfm.is_zero(val) ? 0 : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : - mpfm.bias_exp(ebits, mpfm.exp(val)) + mpfm.bias_exp(ebits, mpfm.exp(val)); } else { exp = mpfm.is_zero(val) ? 0 :