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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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 : From 44d05e537548d01e31ab49dab81bf24701a610e0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Nov 2016 18:00:15 +0000 Subject: [PATCH 22/32] Fix cleanup/initialization of sat::simplifier. Relates to #570. --- src/sat/sat_clause.h | 6 +- src/sat/sat_probing.cpp | 18 ++--- src/sat/sat_simplifier.cpp | 36 ++++++---- src/sat/sat_simplifier.h | 21 ++++-- src/sat/sat_solver.cpp | 130 ++++++++++++++++++------------------- src/sat/sat_types.h | 4 +- 6 files changed, 119 insertions(+), 96 deletions(-) diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 1662b429f..1aededbb6 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -102,10 +102,14 @@ namespace sat { unsigned m_val1; unsigned m_val2; public: - bin_clause(literal l1, literal l2, bool learned):m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast(learned)) {} + bin_clause(literal l1, literal l2, bool learned) :m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast(learned)) {} literal get_literal1() const { return to_literal(m_val1); } literal get_literal2() const { return to_literal(m_val2 >> 1); } bool is_learned() const { return (m_val2 & 1) == 1; } + bool operator==(const bin_clause & other) const { + return m_val1 == other.m_val1 && m_val2 == other.m_val2 || + m_val1 == other.m_val2 && m_val2 == other.m_val1; + } }; class tmp_clause { diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index 165d39ad8..c00b68ac2 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -95,7 +95,7 @@ namespace sat { if (updt_cache) cache_bins(l, old_tr_sz); s.pop(1); - + literal_vector::iterator it = m_to_assert.begin(); literal_vector::iterator end = m_to_assert.end(); for (; it != end; ++it) { @@ -178,10 +178,10 @@ namespace sat { m_num_assigned(p.m_num_assigned) { m_watch.start(); } - + ~report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-probing :probing-assigned " << (m_probing.m_num_assigned - m_num_assigned) << " :cost " << m_probing.m_counter; @@ -189,7 +189,7 @@ namespace sat { verbose_stream() << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } }; - + bool probing::operator()(bool force) { if (!m_probing) return true; @@ -200,8 +200,8 @@ namespace sat { CASSERT("probing", s.check_invariant()); if (!force && m_counter > 0) return true; - - if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit) + + if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit) m_cached_bins.finalize(); report rpt(*this); @@ -256,14 +256,14 @@ namespace sat { } void probing::free_memory() { - m_assigned.cleanup(); + m_assigned.finalize(); m_to_assert.finalize(); } - + void probing::collect_statistics(statistics & st) const { st.update("probing assigned", m_num_assigned); } - + void probing::reset_statistics() { m_num_assigned = 0; } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b200524e7..151bdf45b 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -63,6 +63,7 @@ namespace sat { } simplifier::~simplifier() { + free_memory(); } inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } @@ -96,7 +97,7 @@ namespace sat { inline void simplifier::remove_clause_core(clause & c) { unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) - insert_todo(c[i].var()); + insert_elim_todo(c[i].var()); m_sub_todo.erase(c); c.set_removed(true); TRACE("resolution_bug", tout << "del_clause: " << c << "\n";); @@ -116,6 +117,7 @@ namespace sat { inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) { SASSERT(s.get_wlist(~l1).contains(watched(l2, learned))); s.get_wlist(~l1).erase(watched(l2, learned)); + m_sub_bin_todo.erase(bin_clause(l1, l2, learned)); } void simplifier::init_visited() { @@ -127,27 +129,36 @@ namespace sat { m_use_list.finalize(); m_sub_todo.finalize(); m_sub_bin_todo.finalize(); + m_elim_todo.finalize(); m_visited.finalize(); m_bs_cs.finalize(); m_bs_ls.finalize(); } + void simplifier::initialize() { + m_need_cleanup = false; + s.m_cleaner(true); + m_last_sub_trail_sz = s.m_trail.size(); + m_use_list.init(s.num_vars()); + m_sub_todo.reset(); + m_sub_bin_todo.reset(); + m_elim_todo.reset(); + init_visited(); + TRACE("after_cleanup", s.display(tout);); + CASSERT("sat_solver", s.check_invariant()); + } + void simplifier::operator()(bool learned) { if (s.inconsistent()) return; if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) return; + initialize(); + CASSERT("sat_solver", s.check_invariant()); TRACE("before_simplifier", s.display(tout);); - s.m_cleaner(true); - m_last_sub_trail_sz = s.m_trail.size(); - TRACE("after_cleanup", s.display(tout);); - CASSERT("sat_solver", s.check_invariant()); - m_need_cleanup = false; - m_use_list.init(s.num_vars()); - init_visited(); bool learned_in_use_lists = false; if (learned) { register_clauses(s.m_learned); @@ -158,7 +169,6 @@ namespace sat { if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) elim_blocked_clauses(); - if (!learned) m_num_calls++; @@ -617,7 +627,7 @@ namespace sat { TRACE("elim_lit", tout << "processing: " << c << "\n";); m_need_cleanup = true; m_num_elim_lits++; - insert_todo(l.var()); + insert_elim_todo(l.var()); c.elim(l); clause_use_list & occurs = m_use_list.get(l); occurs.erase_not_removed(c); @@ -920,7 +930,7 @@ namespace sat { void process(literal l) { TRACE("blocked_clause", tout << "processing: " << l << "\n";); model_converter::entry * new_entry = 0; - if (s.is_external(l.var()) || s.was_eliminated(l.var())) + if (s.is_external(l.var()) || s.was_eliminated(l.var())) return; { @@ -1235,12 +1245,14 @@ namespace sat { for (; it2 != end2; ++it2) { if (it2->is_binary_clause() && it2->get_literal() == l) { TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";); + m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned())); continue; } *itprev = *it2; itprev++; } wlist2.set_end(itprev); + m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned())); } } TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";); @@ -1343,7 +1355,7 @@ namespace sat { } TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); - + // eliminate variable model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 85922cf7c..f0f78b9c2 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -9,7 +9,7 @@ Abstract: SAT simplification procedures that use a "full" occurrence list: Subsumption, Blocked Clause Removal, Variable Elimination, ... - + Author: @@ -83,7 +83,7 @@ namespace sat { bool m_subsumption; unsigned m_subsumption_limit; bool m_elim_vars; - + // stats unsigned m_num_blocked_clauses; unsigned m_num_subsumed; @@ -97,6 +97,8 @@ namespace sat { void checkpoint(); + void initialize(); + void init_visited(); void mark_visited(literal l) { m_visited[l.index()] = true; } void unmark_visited(literal l) { m_visited[l.index()] = false; } @@ -135,7 +137,7 @@ namespace sat { void mark_as_not_learned_core(watch_list & wlist, literal l2); void mark_as_not_learned(literal l1, literal l2); void subsume(); - + void cleanup_watches(); void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists); @@ -145,7 +147,7 @@ namespace sat { lbool value(literal l) const; watch_list & get_wlist(literal l); watch_list const & get_wlist(literal l) const; - + struct blocked_clause_elim; void elim_blocked_clauses(); @@ -172,14 +174,19 @@ namespace sat { simplifier(solver & s, params_ref const & p); ~simplifier(); - void insert_todo(bool_var v) { m_elim_todo.insert(v); } - void reset_todo() { m_elim_todo.reset(); } + void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); } + + void reset_todos() { + m_elim_todo.reset(); + m_sub_todo.reset(); + m_sub_bin_todo.reset(); + } void operator()(bool learned); void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - + void free_memory(); void collect_statistics(statistics & st) const; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e0bb0f2a3..1aede522a 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -141,7 +141,7 @@ namespace sat { m_prev_phase.push_back(PHASE_NOT_AVAILABLE); m_assigned_since_gc.push_back(false); m_case_split_queue.mk_var_eh(v); - m_simplifier.insert_todo(v); + m_simplifier.insert_elim_todo(v); SASSERT(!was_eliminated(v)); return v; } @@ -151,7 +151,7 @@ namespace sat { for (unsigned i = 0; i < num_lits; i++) SASSERT(m_eliminated[lits[i].var()] == false); }); - + if (m_user_scope_literals.empty()) { mk_clause_core(num_lits, lits, false); } @@ -175,8 +175,8 @@ namespace sat { void solver::del_clause(clause& c) { if (!c.is_learned()) m_stats.m_non_learned_generation++; - m_cls_allocator.del_clause(&c); - m_stats.m_del_clause++; + m_cls_allocator.del_clause(&c); + m_stats.m_del_clause++; } clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) { @@ -188,7 +188,7 @@ namespace sat { return 0; // clause is equivalent to true. } ++m_stats.m_non_learned_generation; - } + } switch (num_lits) { case 0: @@ -739,10 +739,10 @@ namespace sat { m_restart_threshold = m_config.m_restart_initial; } - // iff3_finder(*this)(); + // iff3_finder(*this)(); simplify_problem(); if (check_inconsistent()) return l_false; - + if (m_config.m_max_conflicts == 0) { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";); @@ -763,7 +763,7 @@ namespace sat { restart(); simplify_problem(); - if (check_inconsistent()) return l_false; + if (check_inconsistent()) return l_false; gc(); } } @@ -891,7 +891,7 @@ namespace sat { else { mk_model(); return l_true; - } + } } @@ -920,8 +920,8 @@ namespace sat { return; } - TRACE("sat", - for (unsigned i = 0; i < num_lits; ++i) + TRACE("sat", + for (unsigned i = 0; i < num_lits; ++i) tout << lits[i] << " "; tout << "\n"; if (!m_user_scope_literals.empty()) { @@ -932,7 +932,7 @@ namespace sat { for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) { literal nlit = ~m_user_scope_literals[i]; - assign(nlit, justification()); + assign(nlit, justification()); } if (weights && !inconsistent()) { @@ -947,9 +947,9 @@ namespace sat { for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; - SASSERT(is_external(lit.var())); - add_assumption(lit); - assign(lit, justification()); + SASSERT(is_external(lit.var())); + add_assumption(lit); + assign(lit, justification()); } } @@ -962,10 +962,10 @@ namespace sat { unsigned num_cores = 0; for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; - SASSERT(is_external(lit.var())); + SASSERT(is_external(lit.var())); TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";); SASSERT(m_scope_lvl == 1); - add_assumption(lit); + add_assumption(lit); switch(value(lit)) { case l_undef: values.push_back(l_true); @@ -973,10 +973,10 @@ namespace sat { if (num_cores*2 >= num_lits) { break; } - propagate(false); + propagate(false); if (inconsistent()) { flet _init(m_initializing_preferred, true); - while (inconsistent()) { + while (inconsistent()) { if (!resolve_conflict()) { return true; } @@ -1001,15 +1001,15 @@ namespace sat { for (unsigned k = i; k >= j; --k) { if (is_assumption(lits[k])) { pop_assumption(); - } + } } values.resize(j); TRACE("sat", tout << "backjump " << (i - j + 1) << " steps " << num_cores << "\n";); i = j - 1; } - break; - - case l_false: + break; + + case l_false: ++num_cores; values.push_back(l_false); SASSERT(!inconsistent()); @@ -1028,14 +1028,14 @@ namespace sat { SASSERT(m_assumptions.size() <= i+1); if (m_core.size() <= 3) { m_inconsistent = true; - TRACE("opt", tout << "found small core: " << m_core << "\n";); + TRACE("opt", tout << "found small core: " << m_core << "\n";); IF_VERBOSE(11, verbose_stream() << "(sat.core: " << m_core << ")\n";); return true; } pop_assumption(); - m_inconsistent = false; + m_inconsistent = false; break; - case l_true: + case l_true: values.push_back(l_true); SASSERT(m_justification[lit.var()].get_kind() != justification::NONE || lvl(lit) == 0); break; @@ -1046,7 +1046,7 @@ namespace sat { if (m_weight >= max_weight) { // block the current correction set candidate. ++m_stats.m_blocked_corr_sets; - TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); + TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";); pop_to_base_level(); mk_clause_core(m_blocker); @@ -1062,17 +1062,17 @@ namespace sat { m_min_core.reset(); m_min_core.append(m_core); m_min_core_valid = true; - } + } } void solver::reset_assumptions() { m_assumptions.reset(); - m_assumption_set.reset(); + m_assumption_set.reset(); } void solver::add_assumption(literal lit) { - m_assumption_set.insert(lit); - m_assumptions.push_back(lit); + m_assumption_set.insert(lit); + m_assumptions.push_back(lit); } void solver::pop_assumption() { @@ -1089,8 +1089,8 @@ namespace sat { for (unsigned i = 0; i < m_min_core.size(); ++i) { literal lit = m_min_core[i]; SASSERT(is_external(lit.var())); - add_assumption(lit); - assign(lit, justification()); + add_assumption(lit); + assign(lit, justification()); } propagate(false); SASSERT(inconsistent()); @@ -1132,7 +1132,7 @@ namespace sat { m_min_core_valid = false; m_min_core.reset(); TRACE("sat", display(tout);); - + if (m_config.m_bcd) { bceq bc(*this); bc(); @@ -1149,11 +1149,11 @@ namespace sat { } IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";); - // Disable simplification during MUS computation. + // Disable simplification during MUS computation. // if (m_mus.is_active()) return; TRACE("sat", tout << "simplify\n";); - pop(scope_lvl()); + pop(scope_lvl()); SASSERT(scope_lvl() == 0); @@ -1166,7 +1166,7 @@ namespace sat { m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); - + if (!m_learned.empty()) { m_simplifier(true); CASSERT("sat_missed_prop", check_missed_propagation()); @@ -1260,7 +1260,7 @@ namespace sat { TRACE("sat", tout << "failed: " << c << "\n"; tout << "assumptions: " << m_assumptions << "\n"; tout << "trail: " << m_trail << "\n"; - tout << "model: " << m << "\n"; + tout << "model: " << m << "\n"; m_mc.display(tout); ); ok = false; @@ -1289,10 +1289,10 @@ namespace sat { } for (unsigned i = 0; i < m_assumptions.size(); ++i) { if (value_at(m_assumptions[i], m) != l_true) { - TRACE("sat", + TRACE("sat", tout << m_assumptions[i] << " does not model check\n"; tout << "trail: " << m_trail << "\n"; - tout << "model: " << m << "\n"; + tout << "model: " << m << "\n"; m_mc.display(tout); ); ok = false; @@ -1664,7 +1664,7 @@ namespace sat { resolve_conflict_for_unsat_core(); return false; } - + if (m_conflict_lvl == 0) { return false; } @@ -1849,11 +1849,11 @@ namespace sat { bool solver::resolve_conflict_for_init() { if (m_conflict_lvl == 0) { return false; - } + } m_lemma.reset(); m_lemma.push_back(null_literal); // asserted literal if (m_not_l != null_literal) { - TRACE("sat", tout << "not_l: " << m_not_l << "\n";); + TRACE("sat", tout << "not_l: " << m_not_l << "\n";); process_antecedent_for_init(m_not_l); } literal consequent = m_not_l; @@ -1988,7 +1988,7 @@ namespace sat { SASSERT(!is_marked(m_trail[i].var())); }}); - unsigned old_size = m_unmark.size(); + unsigned old_size = m_unmark.size(); int idx = skip_literals_above_conflict_level(); if (m_not_l != null_literal) { @@ -2005,7 +2005,7 @@ namespace sat { process_consequent_for_unsat_core(m_not_l, js); } } - + literal consequent = m_not_l; justification js = m_conflict; @@ -2031,7 +2031,7 @@ namespace sat { SASSERT(lvl(consequent) == m_conflict_lvl); js = m_justification[c_var]; idx--; - } + } reset_unmark(old_size); if (m_config.m_core_minimize) { if (m_min_core_valid && m_min_core.size() < m_core.size()) { @@ -2039,7 +2039,7 @@ namespace sat { m_core.reset(); m_core.append(m_min_core); } - // TBD: + // TBD: // apply optional clause minimization by detecting subsumed literals. // initial experiment suggests it has no effect. m_mus(); // ignore return value on cancelation. @@ -2511,7 +2511,7 @@ namespace sat { void solver::pop_reinit(unsigned num_scopes) { pop(num_scopes); - reinit_assumptions(); + reinit_assumptions(); } void solver::pop(unsigned num_scopes) { @@ -2578,13 +2578,13 @@ namespace sat { m_clauses_to_reinit.shrink(j); } - // + // // All new clauses that are added to the solver // are relative to the user-scope literals. - // + // void solver::user_push() { - literal lit; + literal lit; bool_var new_v = mk_var(true, false); lit = literal(new_v, false); m_user_scope_literals.push_back(lit); @@ -2674,7 +2674,7 @@ namespace sat { m_phase.shrink(v); m_prev_phase.shrink(v); m_assigned_since_gc.shrink(v); - m_simplifier.reset_todo(); + m_simplifier.reset_todos(); } } @@ -2698,7 +2698,7 @@ namespace sat { unassign_vars(i); break; } - } + } gc_var(lit.var()); } } @@ -3080,10 +3080,10 @@ namespace sat { } bool non_empty = true; m_seen[0].reset(); - while (non_empty) { + while (non_empty) { literal_vector mutex; bool turn = false; - m_reachable[turn] = ps; + m_reachable[turn] = ps; while (!m_reachable[turn].empty()) { literal p = m_reachable[turn].pop(); if (m_seen[0].contains(p)) { @@ -3100,7 +3100,7 @@ namespace sat { turn = !turn; } if (mutex.size() > 1) { - mutexes.push_back(mutex); + mutexes.push_back(mutex); } non_empty = !mutex.empty(); } @@ -3144,7 +3144,7 @@ namespace sat { switch (get_model()[v]) { case l_true: lits.push_back(literal(v, false)); break; case l_false: lits.push_back(literal(v, true)); break; - default: break; + default: break; } } is_sat = get_consequences(asms, lits, conseq); @@ -3171,7 +3171,7 @@ namespace sat { } propagate(false); if (check_inconsistent()) return l_false; - + unsigned num_units = 0, num_iterations = 0; extract_fixed_consequences(num_units, assumptions, vars, conseq); while (!vars.empty()) { @@ -3188,14 +3188,14 @@ namespace sat { push(); assign(~lit, justification()); propagate(false); - while (inconsistent()) { + while (inconsistent()) { if (!resolve_conflict()) { TRACE("sat", display(tout << "inconsistent\n");); m_inconsistent = false; is_sat = l_undef; break; } - propagate(false); + propagate(false); ++num_resolves; } if (scope_lvl() == 1) { @@ -3209,7 +3209,7 @@ namespace sat { else { is_sat = bounded_search(); if (is_sat == l_undef) { - restart(); + restart(); } } } @@ -3220,7 +3220,7 @@ namespace sat { if (is_sat == l_true) { delete_unfixed(vars); } - extract_fixed_consequences(num_units, assumptions, vars, conseq); + extract_fixed_consequences(num_units, assumptions, vars, conseq); IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences" << " iterations: " << num_iterations << " variables: " << vars.size() @@ -3240,10 +3240,10 @@ namespace sat { if (value(lit) == l_true) { to_keep.insert(lit); } - } + } unfixed = to_keep; } - + void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { if (scope_lvl() > 1) { pop(scope_lvl() - 1); @@ -3293,7 +3293,7 @@ namespace sat { } void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { - index_set s; + index_set s; if (assumptions.contains(lit)) { s.insert(lit.index()); } diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 00edaa593..509cc58ba 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -200,7 +200,7 @@ namespace sat { iterator begin() const { return m_set.begin(); } iterator end() const { return m_set.end(); } void reset() { m_set.reset(); m_in_set.reset(); } - void cleanup() { m_set.finalize(); m_in_set.finalize(); } + void finalize() { m_set.finalize(); m_in_set.finalize(); } uint_set& operator&=(uint_set const& other) { unsigned j = 0; for (unsigned i = 0; i < m_set.size(); ++i) { @@ -259,7 +259,7 @@ namespace sat { bool empty() const { return m_set.empty(); } unsigned size() const { return m_set.size(); } void reset() { m_set.reset(); } - void cleanup() { m_set.cleanup(); } + void finalize() { m_set.finalize(); } class iterator { uint_set::iterator m_it; public: From 22c9b9a79756b47196dca1f5c22e3a14881a04d7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Nov 2016 18:06:53 +0000 Subject: [PATCH 23/32] Fixed compiler warning --- src/sat/sat_clause.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 1aededbb6..27a0ed739 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -107,8 +107,8 @@ namespace sat { literal get_literal2() const { return to_literal(m_val2 >> 1); } bool is_learned() const { return (m_val2 & 1) == 1; } bool operator==(const bin_clause & other) const { - return m_val1 == other.m_val1 && m_val2 == other.m_val2 || - m_val1 == other.m_val2 && m_val2 == other.m_val1; + return (m_val1 == other.m_val1 && m_val2 == other.m_val2) || + (m_val1 == other.m_val2 && m_val2 == other.m_val1); } }; From 40d90a951c56c273764897ec7dad051ecb5326ba Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Nov 2016 16:52:56 +0000 Subject: [PATCH 24/32] Fixed interruption cleanup bug in sat_solver. Relates to #570. --- src/sat/sat_solver.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 85836b889..c0d736ebf 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -237,7 +237,10 @@ namespace sat { lbool status(clause const & c) const; clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); } void checkpoint() { - if (!m_rlimit.inc()) { throw solver_exception(Z3_CANCELED_MSG); } + if (!m_rlimit.inc()) { + m_mc.reset(); + throw solver_exception(Z3_CANCELED_MSG); + } ++m_num_checkpoints; if (m_num_checkpoints < 10) return; m_num_checkpoints = 0; From d66530a11291700b02fb465d2536dd2e2576eb70 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Nov 2016 17:06:55 +0000 Subject: [PATCH 25/32] Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570. --- src/sat/sat_probing.cpp | 5 +++-- src/sat/sat_probing.h | 2 +- src/sat/sat_simplifier.cpp | 10 ++++++---- src/sat/sat_simplifier.h | 2 +- src/sat/sat_solver.cpp | 2 +- src/sat/sat_solver.h | 1 + 6 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index c00b68ac2..0b5edb2c9 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -239,7 +239,7 @@ namespace sat { m_counter *= 2; } CASSERT("probing", s.check_invariant()); - free_memory(); + finalize(); return r; } @@ -255,9 +255,10 @@ namespace sat { // TODO } - void probing::free_memory() { + void probing::finalize() { m_assigned.finalize(); m_to_assert.finalize(); + m_cached_bins.finalize(); } void probing::collect_statistics(statistics & st) const { diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h index daf6817e3..cce165a34 100644 --- a/src/sat/sat_probing.h +++ b/src/sat/sat_probing.h @@ -69,7 +69,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void free_memory(); + void finalize(); void collect_statistics(statistics & st) const; void reset_statistics(); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 151bdf45b..f46540b89 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -63,7 +63,7 @@ namespace sat { } simplifier::~simplifier() { - free_memory(); + finalize(); } inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } @@ -125,7 +125,7 @@ namespace sat { m_visited.resize(2*s.num_vars(), false); } - void simplifier::free_memory() { + void simplifier::finalize() { m_use_list.finalize(); m_sub_todo.finalize(); m_sub_bin_todo.finalize(); @@ -154,6 +154,7 @@ namespace sat { if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) return; + initialize(); CASSERT("sat_solver", s.check_invariant()); @@ -166,6 +167,7 @@ namespace sat { } register_clauses(s.m_clauses); + if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) elim_blocked_clauses(); @@ -207,7 +209,7 @@ namespace sat { } CASSERT("sat_solver", s.check_invariant()); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); - free_memory(); + finalize(); } /** @@ -932,8 +934,8 @@ namespace sat { model_converter::entry * new_entry = 0; if (s.is_external(l.var()) || s.was_eliminated(l.var())) return; - { + { m_to_remove.reset(); { clause_use_list & occs = s.m_use_list.get(l); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index f0f78b9c2..9ee239083 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -187,7 +187,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void free_memory(); + void finalize(); void collect_statistics(statistics & st) const; void reset_statistics(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1aede522a..f1f6a6aa8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3042,7 +3042,7 @@ namespace sat { if (scope_lvl() > 0 || inconsistent()) return; m_simplifier(learned); - m_simplifier.free_memory(); + m_simplifier.finalize(); if (m_ext) m_ext->clauses_modifed(); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c0d736ebf..a44f07a23 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -239,6 +239,7 @@ namespace sat { void checkpoint() { if (!m_rlimit.inc()) { m_mc.reset(); + m_model_is_current = false; throw solver_exception(Z3_CANCELED_MSG); } ++m_num_checkpoints; From 890142ef9677e7eb3fcfa2efc7c2ca278e073e3c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Nov 2016 18:00:15 +0000 Subject: [PATCH 26/32] Fix cleanup/initialization of sat::simplifier. Relates to #570. --- src/sat/sat_clause.h | 6 +- src/sat/sat_probing.cpp | 18 ++--- src/sat/sat_simplifier.cpp | 29 +++++++-- src/sat/sat_simplifier.h | 21 ++++-- src/sat/sat_solver.cpp | 130 ++++++++++++++++++------------------- src/sat/sat_types.h | 4 +- 6 files changed, 119 insertions(+), 89 deletions(-) diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 1662b429f..1aededbb6 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -102,10 +102,14 @@ namespace sat { unsigned m_val1; unsigned m_val2; public: - bin_clause(literal l1, literal l2, bool learned):m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast(learned)) {} + bin_clause(literal l1, literal l2, bool learned) :m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast(learned)) {} literal get_literal1() const { return to_literal(m_val1); } literal get_literal2() const { return to_literal(m_val2 >> 1); } bool is_learned() const { return (m_val2 & 1) == 1; } + bool operator==(const bin_clause & other) const { + return m_val1 == other.m_val1 && m_val2 == other.m_val2 || + m_val1 == other.m_val2 && m_val2 == other.m_val1; + } }; class tmp_clause { diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index 165d39ad8..c00b68ac2 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -95,7 +95,7 @@ namespace sat { if (updt_cache) cache_bins(l, old_tr_sz); s.pop(1); - + literal_vector::iterator it = m_to_assert.begin(); literal_vector::iterator end = m_to_assert.end(); for (; it != end; ++it) { @@ -178,10 +178,10 @@ namespace sat { m_num_assigned(p.m_num_assigned) { m_watch.start(); } - + ~report() { m_watch.stop(); - IF_VERBOSE(SAT_VB_LVL, + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << " (sat-probing :probing-assigned " << (m_probing.m_num_assigned - m_num_assigned) << " :cost " << m_probing.m_counter; @@ -189,7 +189,7 @@ namespace sat { verbose_stream() << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } }; - + bool probing::operator()(bool force) { if (!m_probing) return true; @@ -200,8 +200,8 @@ namespace sat { CASSERT("probing", s.check_invariant()); if (!force && m_counter > 0) return true; - - if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit) + + if (m_probing_cache && memory::get_allocation_size() > m_probing_cache_limit) m_cached_bins.finalize(); report rpt(*this); @@ -256,14 +256,14 @@ namespace sat { } void probing::free_memory() { - m_assigned.cleanup(); + m_assigned.finalize(); m_to_assert.finalize(); } - + void probing::collect_statistics(statistics & st) const { st.update("probing assigned", m_num_assigned); } - + void probing::reset_statistics() { m_num_assigned = 0; } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 2a1930f4f..3e817b2a9 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -63,6 +63,7 @@ namespace sat { } simplifier::~simplifier() { + free_memory(); } inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } @@ -96,7 +97,7 @@ namespace sat { inline void simplifier::remove_clause_core(clause & c) { unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) - insert_todo(c[i].var()); + insert_elim_todo(c[i].var()); m_sub_todo.erase(c); c.set_removed(true); TRACE("resolution_bug", tout << "del_clause: " << c << "\n";); @@ -116,6 +117,7 @@ namespace sat { inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) { SASSERT(s.get_wlist(~l1).contains(watched(l2, learned))); s.get_wlist(~l1).erase(watched(l2, learned)); + m_sub_bin_todo.erase(bin_clause(l1, l2, learned)); } void simplifier::init_visited() { @@ -127,17 +129,33 @@ namespace sat { m_use_list.finalize(); m_sub_todo.finalize(); m_sub_bin_todo.finalize(); + m_elim_todo.finalize(); m_visited.finalize(); m_bs_cs.finalize(); m_bs_ls.finalize(); } + void simplifier::initialize() { + m_need_cleanup = false; + s.m_cleaner(true); + m_last_sub_trail_sz = s.m_trail.size(); + m_use_list.init(s.num_vars()); + m_sub_todo.reset(); + m_sub_bin_todo.reset(); + m_elim_todo.reset(); + init_visited(); + TRACE("after_cleanup", s.display(tout);); + CASSERT("sat_solver", s.check_invariant()); + } + void simplifier::operator()(bool learned) { if (s.inconsistent()) return; if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) return; + initialize(); + CASSERT("sat_solver", s.check_invariant()); TRACE("before_simplifier", s.display(tout);); @@ -160,7 +178,6 @@ namespace sat { if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) elim_blocked_clauses(); - if (!learned) m_num_calls++; @@ -619,7 +636,7 @@ namespace sat { TRACE("elim_lit", tout << "processing: " << c << "\n";); m_need_cleanup = true; m_num_elim_lits++; - insert_todo(l.var()); + insert_elim_todo(l.var()); c.elim(l); clause_use_list & occurs = m_use_list.get(l); occurs.erase_not_removed(c); @@ -922,7 +939,7 @@ namespace sat { void process(literal l) { TRACE("blocked_clause", tout << "processing: " << l << "\n";); model_converter::entry * new_entry = 0; - if (s.is_external(l.var()) || s.was_eliminated(l.var())) + if (s.is_external(l.var()) || s.was_eliminated(l.var())) return; { @@ -1237,12 +1254,14 @@ namespace sat { for (; it2 != end2; ++it2) { if (it2->is_binary_clause() && it2->get_literal() == l) { TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";); + m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned())); continue; } *itprev = *it2; itprev++; } wlist2.set_end(itprev); + m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned())); } } TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";); @@ -1345,7 +1364,7 @@ namespace sat { } TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); - + // eliminate variable model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); save_clauses(mc_entry, m_pos_cls); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 85922cf7c..f0f78b9c2 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -9,7 +9,7 @@ Abstract: SAT simplification procedures that use a "full" occurrence list: Subsumption, Blocked Clause Removal, Variable Elimination, ... - + Author: @@ -83,7 +83,7 @@ namespace sat { bool m_subsumption; unsigned m_subsumption_limit; bool m_elim_vars; - + // stats unsigned m_num_blocked_clauses; unsigned m_num_subsumed; @@ -97,6 +97,8 @@ namespace sat { void checkpoint(); + void initialize(); + void init_visited(); void mark_visited(literal l) { m_visited[l.index()] = true; } void unmark_visited(literal l) { m_visited[l.index()] = false; } @@ -135,7 +137,7 @@ namespace sat { void mark_as_not_learned_core(watch_list & wlist, literal l2); void mark_as_not_learned(literal l1, literal l2); void subsume(); - + void cleanup_watches(); void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists); @@ -145,7 +147,7 @@ namespace sat { lbool value(literal l) const; watch_list & get_wlist(literal l); watch_list const & get_wlist(literal l) const; - + struct blocked_clause_elim; void elim_blocked_clauses(); @@ -172,14 +174,19 @@ namespace sat { simplifier(solver & s, params_ref const & p); ~simplifier(); - void insert_todo(bool_var v) { m_elim_todo.insert(v); } - void reset_todo() { m_elim_todo.reset(); } + void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); } + + void reset_todos() { + m_elim_todo.reset(); + m_sub_todo.reset(); + m_sub_bin_todo.reset(); + } void operator()(bool learned); void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - + void free_memory(); void collect_statistics(statistics & st) const; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 68c42f712..5bc9e4ed9 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -141,7 +141,7 @@ namespace sat { m_prev_phase.push_back(PHASE_NOT_AVAILABLE); m_assigned_since_gc.push_back(false); m_case_split_queue.mk_var_eh(v); - m_simplifier.insert_todo(v); + m_simplifier.insert_elim_todo(v); SASSERT(!was_eliminated(v)); return v; } @@ -151,7 +151,7 @@ namespace sat { for (unsigned i = 0; i < num_lits; i++) SASSERT(m_eliminated[lits[i].var()] == false); }); - + if (m_user_scope_literals.empty()) { mk_clause_core(num_lits, lits, false); } @@ -175,8 +175,8 @@ namespace sat { void solver::del_clause(clause& c) { if (!c.is_learned()) m_stats.m_non_learned_generation++; - m_cls_allocator.del_clause(&c); - m_stats.m_del_clause++; + m_cls_allocator.del_clause(&c); + m_stats.m_del_clause++; } clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) { @@ -188,7 +188,7 @@ namespace sat { return 0; // clause is equivalent to true. } ++m_stats.m_non_learned_generation; - } + } switch (num_lits) { case 0: @@ -739,10 +739,10 @@ namespace sat { m_restart_threshold = m_config.m_restart_initial; } - // iff3_finder(*this)(); + // iff3_finder(*this)(); simplify_problem(); if (check_inconsistent()) return l_false; - + if (m_config.m_max_conflicts == 0) { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";); @@ -763,7 +763,7 @@ namespace sat { restart(); simplify_problem(); - if (check_inconsistent()) return l_false; + if (check_inconsistent()) return l_false; gc(); } } @@ -891,7 +891,7 @@ namespace sat { else { mk_model(); return l_true; - } + } } @@ -920,8 +920,8 @@ namespace sat { return; } - TRACE("sat", - for (unsigned i = 0; i < num_lits; ++i) + TRACE("sat", + for (unsigned i = 0; i < num_lits; ++i) tout << lits[i] << " "; tout << "\n"; if (!m_user_scope_literals.empty()) { @@ -932,7 +932,7 @@ namespace sat { for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) { literal nlit = ~m_user_scope_literals[i]; - assign(nlit, justification()); + assign(nlit, justification()); } if (weights && !inconsistent()) { @@ -947,9 +947,9 @@ namespace sat { for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; - SASSERT(is_external(lit.var())); - add_assumption(lit); - assign(lit, justification()); + SASSERT(is_external(lit.var())); + add_assumption(lit); + assign(lit, justification()); } } @@ -962,10 +962,10 @@ namespace sat { unsigned num_cores = 0; for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; - SASSERT(is_external(lit.var())); + SASSERT(is_external(lit.var())); TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";); SASSERT(m_scope_lvl == 1); - add_assumption(lit); + add_assumption(lit); switch(value(lit)) { case l_undef: values.push_back(l_true); @@ -973,10 +973,10 @@ namespace sat { if (num_cores*2 >= num_lits) { break; } - propagate(false); + propagate(false); if (inconsistent()) { flet _init(m_initializing_preferred, true); - while (inconsistent()) { + while (inconsistent()) { if (!resolve_conflict()) { return true; } @@ -1001,15 +1001,15 @@ namespace sat { for (unsigned k = i; k >= j; --k) { if (is_assumption(lits[k])) { pop_assumption(); - } + } } values.resize(j); TRACE("sat", tout << "backjump " << (i - j + 1) << " steps " << num_cores << "\n";); i = j - 1; } - break; - - case l_false: + break; + + case l_false: ++num_cores; values.push_back(l_false); SASSERT(!inconsistent()); @@ -1028,14 +1028,14 @@ namespace sat { SASSERT(m_assumptions.size() <= i+1); if (m_core.size() <= 3) { m_inconsistent = true; - TRACE("opt", tout << "found small core: " << m_core << "\n";); + TRACE("opt", tout << "found small core: " << m_core << "\n";); IF_VERBOSE(11, verbose_stream() << "(sat.core: " << m_core << ")\n";); return true; } pop_assumption(); - m_inconsistent = false; + m_inconsistent = false; break; - case l_true: + case l_true: values.push_back(l_true); SASSERT(m_justification[lit.var()].get_kind() != justification::NONE || lvl(lit) == 0); break; @@ -1046,7 +1046,7 @@ namespace sat { if (m_weight >= max_weight) { // block the current correction set candidate. ++m_stats.m_blocked_corr_sets; - TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); + TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";); pop_to_base_level(); mk_clause_core(m_blocker); @@ -1062,17 +1062,17 @@ namespace sat { m_min_core.reset(); m_min_core.append(m_core); m_min_core_valid = true; - } + } } void solver::reset_assumptions() { m_assumptions.reset(); - m_assumption_set.reset(); + m_assumption_set.reset(); } void solver::add_assumption(literal lit) { - m_assumption_set.insert(lit); - m_assumptions.push_back(lit); + m_assumption_set.insert(lit); + m_assumptions.push_back(lit); } void solver::pop_assumption() { @@ -1089,8 +1089,8 @@ namespace sat { for (unsigned i = 0; i < m_min_core.size(); ++i) { literal lit = m_min_core[i]; SASSERT(is_external(lit.var())); - add_assumption(lit); - assign(lit, justification()); + add_assumption(lit); + assign(lit, justification()); } propagate(false); SASSERT(inconsistent()); @@ -1132,7 +1132,7 @@ namespace sat { m_min_core_valid = false; m_min_core.reset(); TRACE("sat", display(tout);); - + if (m_config.m_bcd) { bceq bc(*this); bc(); @@ -1149,11 +1149,11 @@ namespace sat { } IF_VERBOSE(2, verbose_stream() << "(sat.simplify)\n";); - // Disable simplification during MUS computation. + // Disable simplification during MUS computation. // if (m_mus.is_active()) return; TRACE("sat", tout << "simplify\n";); - pop(scope_lvl()); + pop(scope_lvl()); SASSERT(scope_lvl() == 0); @@ -1166,7 +1166,7 @@ namespace sat { m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); - + if (!m_learned.empty()) { m_simplifier(true); CASSERT("sat_missed_prop", check_missed_propagation()); @@ -1260,7 +1260,7 @@ namespace sat { TRACE("sat", tout << "failed: " << c << "\n"; tout << "assumptions: " << m_assumptions << "\n"; tout << "trail: " << m_trail << "\n"; - tout << "model: " << m << "\n"; + tout << "model: " << m << "\n"; m_mc.display(tout); ); ok = false; @@ -1289,10 +1289,10 @@ namespace sat { } for (unsigned i = 0; i < m_assumptions.size(); ++i) { if (value_at(m_assumptions[i], m) != l_true) { - TRACE("sat", + TRACE("sat", tout << m_assumptions[i] << " does not model check\n"; tout << "trail: " << m_trail << "\n"; - tout << "model: " << m << "\n"; + tout << "model: " << m << "\n"; m_mc.display(tout); ); ok = false; @@ -1664,7 +1664,7 @@ namespace sat { resolve_conflict_for_unsat_core(); return false; } - + if (m_conflict_lvl == 0) { return false; } @@ -1849,11 +1849,11 @@ namespace sat { bool solver::resolve_conflict_for_init() { if (m_conflict_lvl == 0) { return false; - } + } m_lemma.reset(); m_lemma.push_back(null_literal); // asserted literal if (m_not_l != null_literal) { - TRACE("sat", tout << "not_l: " << m_not_l << "\n";); + TRACE("sat", tout << "not_l: " << m_not_l << "\n";); process_antecedent_for_init(m_not_l); } literal consequent = m_not_l; @@ -1988,7 +1988,7 @@ namespace sat { SASSERT(!is_marked(m_trail[i].var())); }}); - unsigned old_size = m_unmark.size(); + unsigned old_size = m_unmark.size(); int idx = skip_literals_above_conflict_level(); if (m_not_l != null_literal) { @@ -2005,7 +2005,7 @@ namespace sat { process_consequent_for_unsat_core(m_not_l, js); } } - + literal consequent = m_not_l; justification js = m_conflict; @@ -2031,7 +2031,7 @@ namespace sat { SASSERT(lvl(consequent) == m_conflict_lvl); js = m_justification[c_var]; idx--; - } + } reset_unmark(old_size); if (m_config.m_core_minimize) { if (m_min_core_valid && m_min_core.size() < m_core.size()) { @@ -2039,7 +2039,7 @@ namespace sat { m_core.reset(); m_core.append(m_min_core); } - // TBD: + // TBD: // apply optional clause minimization by detecting subsumed literals. // initial experiment suggests it has no effect. m_mus(); // ignore return value on cancelation. @@ -2511,7 +2511,7 @@ namespace sat { void solver::pop_reinit(unsigned num_scopes) { pop(num_scopes); - reinit_assumptions(); + reinit_assumptions(); } void solver::pop(unsigned num_scopes) { @@ -2578,13 +2578,13 @@ namespace sat { m_clauses_to_reinit.shrink(j); } - // + // // All new clauses that are added to the solver // are relative to the user-scope literals. - // + // void solver::user_push() { - literal lit; + literal lit; bool_var new_v = mk_var(true, false); lit = literal(new_v, false); m_user_scope_literals.push_back(lit); @@ -2674,7 +2674,7 @@ namespace sat { m_phase.shrink(v); m_prev_phase.shrink(v); m_assigned_since_gc.shrink(v); - m_simplifier.reset_todo(); + m_simplifier.reset_todos(); } } @@ -2698,7 +2698,7 @@ namespace sat { unassign_vars(i); break; } - } + } gc_var(lit.var()); } } @@ -3084,10 +3084,10 @@ namespace sat { } bool non_empty = true; m_seen[0].reset(); - while (non_empty) { + while (non_empty) { literal_vector mutex; bool turn = false; - m_reachable[turn] = ps; + m_reachable[turn] = ps; while (!m_reachable[turn].empty()) { literal p = m_reachable[turn].pop(); if (m_seen[0].contains(p)) { @@ -3104,7 +3104,7 @@ namespace sat { turn = !turn; } if (mutex.size() > 1) { - mutexes.push_back(mutex); + mutexes.push_back(mutex); } non_empty = !mutex.empty(); } @@ -3148,7 +3148,7 @@ namespace sat { switch (get_model()[v]) { case l_true: lits.push_back(literal(v, false)); break; case l_false: lits.push_back(literal(v, true)); break; - default: break; + default: break; } } is_sat = get_consequences(asms, lits, conseq); @@ -3175,7 +3175,7 @@ namespace sat { } propagate(false); if (check_inconsistent()) return l_false; - + unsigned num_units = 0, num_iterations = 0; extract_fixed_consequences(num_units, assumptions, vars, conseq); while (!vars.empty()) { @@ -3192,14 +3192,14 @@ namespace sat { push(); assign(~lit, justification()); propagate(false); - while (inconsistent()) { + while (inconsistent()) { if (!resolve_conflict()) { TRACE("sat", display(tout << "inconsistent\n");); m_inconsistent = false; is_sat = l_undef; break; } - propagate(false); + propagate(false); ++num_resolves; } if (scope_lvl() == 1) { @@ -3213,7 +3213,7 @@ namespace sat { else { is_sat = bounded_search(); if (is_sat == l_undef) { - restart(); + restart(); } } } @@ -3224,7 +3224,7 @@ namespace sat { if (is_sat == l_true) { delete_unfixed(vars); } - extract_fixed_consequences(num_units, assumptions, vars, conseq); + extract_fixed_consequences(num_units, assumptions, vars, conseq); IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences" << " iterations: " << num_iterations << " variables: " << vars.size() @@ -3244,10 +3244,10 @@ namespace sat { if (value(lit) == l_true) { to_keep.insert(lit); } - } + } unfixed = to_keep; } - + void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { if (scope_lvl() > 1) { pop(scope_lvl() - 1); @@ -3297,7 +3297,7 @@ namespace sat { } void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { - index_set s; + index_set s; if (assumptions.contains(lit)) { s.insert(lit.index()); } diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 00edaa593..509cc58ba 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -200,7 +200,7 @@ namespace sat { iterator begin() const { return m_set.begin(); } iterator end() const { return m_set.end(); } void reset() { m_set.reset(); m_in_set.reset(); } - void cleanup() { m_set.finalize(); m_in_set.finalize(); } + void finalize() { m_set.finalize(); m_in_set.finalize(); } uint_set& operator&=(uint_set const& other) { unsigned j = 0; for (unsigned i = 0; i < m_set.size(); ++i) { @@ -259,7 +259,7 @@ namespace sat { bool empty() const { return m_set.empty(); } unsigned size() const { return m_set.size(); } void reset() { m_set.reset(); } - void cleanup() { m_set.cleanup(); } + void finalize() { m_set.finalize(); } class iterator { uint_set::iterator m_it; public: From d099e2634247b128d50e357fb361b3808c19dbde Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Nov 2016 18:06:53 +0000 Subject: [PATCH 27/32] Fixed compiler warning --- src/sat/sat_clause.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 1aededbb6..27a0ed739 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -107,8 +107,8 @@ namespace sat { literal get_literal2() const { return to_literal(m_val2 >> 1); } bool is_learned() const { return (m_val2 & 1) == 1; } bool operator==(const bin_clause & other) const { - return m_val1 == other.m_val1 && m_val2 == other.m_val2 || - m_val1 == other.m_val2 && m_val2 == other.m_val1; + return (m_val1 == other.m_val1 && m_val2 == other.m_val2) || + (m_val1 == other.m_val2 && m_val2 == other.m_val1); } }; From 520e868adde0e5dae12cb575a15883c4c2a7b3e8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Nov 2016 16:52:56 +0000 Subject: [PATCH 28/32] Fixed interruption cleanup bug in sat_solver. Relates to #570. --- src/sat/sat_solver.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 85836b889..c0d736ebf 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -237,7 +237,10 @@ namespace sat { lbool status(clause const & c) const; clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); } void checkpoint() { - if (!m_rlimit.inc()) { throw solver_exception(Z3_CANCELED_MSG); } + if (!m_rlimit.inc()) { + m_mc.reset(); + throw solver_exception(Z3_CANCELED_MSG); + } ++m_num_checkpoints; if (m_num_checkpoints < 10) return; m_num_checkpoints = 0; From bfaa9ddf633b542a0aa01bd925a7c3d1a5b3097d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Nov 2016 17:06:55 +0000 Subject: [PATCH 29/32] Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570. --- src/sat/sat_probing.cpp | 5 +++-- src/sat/sat_probing.h | 2 +- src/sat/sat_simplifier.cpp | 10 ++++++---- src/sat/sat_simplifier.h | 2 +- src/sat/sat_solver.cpp | 2 +- src/sat/sat_solver.h | 1 + 6 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index c00b68ac2..0b5edb2c9 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -239,7 +239,7 @@ namespace sat { m_counter *= 2; } CASSERT("probing", s.check_invariant()); - free_memory(); + finalize(); return r; } @@ -255,9 +255,10 @@ namespace sat { // TODO } - void probing::free_memory() { + void probing::finalize() { m_assigned.finalize(); m_to_assert.finalize(); + m_cached_bins.finalize(); } void probing::collect_statistics(statistics & st) const { diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h index daf6817e3..cce165a34 100644 --- a/src/sat/sat_probing.h +++ b/src/sat/sat_probing.h @@ -69,7 +69,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void free_memory(); + void finalize(); void collect_statistics(statistics & st) const; void reset_statistics(); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 3e817b2a9..c42572f1e 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -63,7 +63,7 @@ namespace sat { } simplifier::~simplifier() { - free_memory(); + finalize(); } inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } @@ -125,7 +125,7 @@ namespace sat { m_visited.resize(2*s.num_vars(), false); } - void simplifier::free_memory() { + void simplifier::finalize() { m_use_list.finalize(); m_sub_todo.finalize(); m_sub_bin_todo.finalize(); @@ -154,6 +154,7 @@ namespace sat { if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) return; + initialize(); CASSERT("sat_solver", s.check_invariant()); @@ -175,6 +176,7 @@ namespace sat { } register_clauses(s.m_clauses); + if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) elim_blocked_clauses(); @@ -216,7 +218,7 @@ namespace sat { } CASSERT("sat_solver", s.check_invariant()); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); - free_memory(); + finalize(); } /** @@ -941,8 +943,8 @@ namespace sat { model_converter::entry * new_entry = 0; if (s.is_external(l.var()) || s.was_eliminated(l.var())) return; - { + { m_to_remove.reset(); { clause_use_list & occs = s.m_use_list.get(l); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index f0f78b9c2..9ee239083 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -187,7 +187,7 @@ namespace sat { void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void free_memory(); + void finalize(); void collect_statistics(statistics & st) const; void reset_statistics(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 5bc9e4ed9..7acfda822 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3042,7 +3042,7 @@ namespace sat { if (scope_lvl() > 0 || inconsistent()) return; m_simplifier(learned); - m_simplifier.free_memory(); + m_simplifier.finalize(); if (m_ext) m_ext->clauses_modifed(); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c0d736ebf..a44f07a23 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -239,6 +239,7 @@ namespace sat { void checkpoint() { if (!m_rlimit.inc()) { m_mc.reset(); + m_model_is_current = false; throw solver_exception(Z3_CANCELED_MSG); } ++m_num_checkpoints; From 014815a6408a1c54ee6c324353880fe46e46bf0a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Nov 2016 08:59:18 -0800 Subject: [PATCH 30/32] Fixed Windows distribution script. --- scripts/mk_win_dist.py | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 65d780f0d..92d89480f 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -236,23 +236,9 @@ def mk_zip(): VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'), re.compile('msvcp.*\.dll'), re.compile('msvcr.*\.dll')] - -VS_RUNTIME_FILES = [] -def cp_vs_runtime_visitor(pattern, dir, files): - global VS_RUNTIME_FILES - for filename in files: - for pat in VS_RUNTIME_PATS: - if pat.match(filename): - if fnmatch(filename, pattern): - fname = os.path.join(dir, filename) - if not os.path.isdir(fname): - VS_RUNTIME_FILES.append(fname) - break - # Copy Visual Studio Runtime libraries -def cp_vs_runtime_core(x64): - global VS_RUNTIME_FILES +def cp_vs_runtime_core(x64): if x64: platform = "x64" @@ -261,7 +247,15 @@ def cp_vs_runtime_core(x64): vcdir = os.environ['VCINSTALLDIR'] path = '%sredist\\%s' % (vcdir, platform) VS_RUNTIME_FILES = [] - os.walk(path, cp_vs_runtime_visitor, '*.dll') + for root, dirs, files in os.walk(path): + for filename in files: + if fnmatch(filename, '*.dll'): + for pat in VS_RUNTIME_PATS: + if pat.match(filename): + fname = os.path.join(root, filename) + if not os.path.isdir(fname): + VS_RUNTIME_FILES.append(fname) + bin_dist_path = os.path.join(DIST_DIR, get_dist_path(x64), 'bin') for f in VS_RUNTIME_FILES: shutil.copy(f, bin_dist_path) From ee60ba824f0a116ec0bb5e9e615dd4fe2e9802db Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Nov 2016 19:59:08 +0000 Subject: [PATCH 31/32] Bugfix for rewriter exceptions in theory_fpa. Relates to #570. --- src/smt/theory_fpa.cpp | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 89acc0ecf..4b53c1341 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -334,23 +334,30 @@ namespace smt { TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl; tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;); - if (m_fpa_util.is_rm(e)) { - SASSERT(m_fpa_util.is_bv2rm(e_conv)); - expr_ref bv_rm(m); - m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); - res = m_fpa_util.mk_bv2rm(bv_rm); + try { + if (m_fpa_util.is_rm(e)) { + SASSERT(m_fpa_util.is_bv2rm(e_conv)); + expr_ref bv_rm(m); + m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); + res = m_fpa_util.mk_bv2rm(bv_rm); + } + else if (m_fpa_util.is_float(e)) { + SASSERT(m_fpa_util.is_fp(e_conv)); + expr_ref sgn(m), sig(m), exp(m); + m_converter.split_fp(e_conv, sgn, exp, sig); + m_th_rw(sgn); + m_th_rw(exp); + m_th_rw(sig); + res = m_fpa_util.mk_fp(sgn, exp, sig); + } + else + UNREACHABLE(); } - else if (m_fpa_util.is_float(e)) { - SASSERT(m_fpa_util.is_fp(e_conv)); - expr_ref sgn(m), sig(m), exp(m); - m_converter.split_fp(e_conv, sgn, exp, sig); - m_th_rw(sgn); - m_th_rw(exp); - m_th_rw(sig); - res = m_fpa_util.mk_fp(sgn, exp, sig); + catch (rewriter_exception &) + { + m_th_rw.reset(); + throw; } - else - UNREACHABLE(); return res; } From c7787feebb5ed79b2274741b4f24299aa87a2057 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Nov 2016 19:59:22 +0000 Subject: [PATCH 32/32] Assertion fix for theory_fpa. Relates to #570. --- src/smt/theory_fpa.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 4b53c1341..57cd6a914 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -750,8 +750,15 @@ namespace smt { // These are the conversion functions fp.to_* */ SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); } - else - UNREACHABLE(); + else { + /* Theory variables can be merged when (= bv-term (bvwrap fp-term)), + in which case context::relevant_eh may call theory_fpa::relevant_eh + after theory_bv::relevant_eh, regardless of whether theory_fpa is + interested in this term. But, this can only happen because of + (bvwrap ...) terms, i.e., `n' must be a bit-vector expression, + which we can safely ignore. */ + SASSERT(m_bv_util.is_bv(n)); + } } void theory_fpa::reset_eh() {