diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 999d495a3..0c28058ed 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -58,7 +58,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 454bba7ca..cee8c0460 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -63,7 +63,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index f9c48c2bd..70230e346 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -74,6 +74,10 @@ public: m_lemma_limit = p.div0_ackermann_limit(); } + virtual void collect_param_descrs(param_descrs & r) { + ackermannize_bv_tactic_params::collect_param_descrs(r); + } + virtual void collect_statistics(statistics & st) const { st.update("ackr-constraints", m_st.m_ackrs_sz); } diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 34dab3ed6..9aea9d6f4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1066,15 +1066,14 @@ extern "C" { case OP_BV2INT: return Z3_OP_BV2INT; case OP_CARRY: return Z3_OP_CARRY; case OP_XOR3: return Z3_OP_XOR3; - case OP_BSMUL_NO_OVFL: - case OP_BUMUL_NO_OVFL: - case OP_BSMUL_NO_UDFL: - case OP_BSDIV_I: - case OP_BUDIV_I: - case OP_BSREM_I: - case OP_BUREM_I: - case OP_BSMOD_I: - return Z3_OP_UNINTERPRETED; + case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL; + case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL; + case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; + case OP_BSDIV_I: return Z3_OP_BSDIV_I; + case OP_BUDIV_I: return Z3_OP_BUDIV_I; + case OP_BSREM_I: return Z3_OP_BSREM_I; + case OP_BUREM_I: return Z3_OP_BUREM_I; + case OP_BSMOD_I: return Z3_OP_BSMOD_I; default: UNREACHABLE(); return Z3_OP_UNINTERPRETED; diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 63092b2cf..10ede0922 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -50,14 +50,13 @@ extern "C" { Z3_CATCH; } - Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) { + Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) { Z3_TRY; LOG_Z3_model_get_const_interp(c, m, a); RESET_ERROR_CODE(); CHECK_NON_NULL(m, 0); expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a)); if (!r) { - SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } mk_c(c)->save_ast_trail(r); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6e8544770..9fb664819 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1582,6 +1582,9 @@ namespace z3 { return static_cast(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); } + // returns interpretation of constant declaration c. + // If c is not assigned any value in the model it returns + // an expression with a null ast reference. expr get_const_interp(func_decl c) const { check_context(*this, c); Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c); diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 848883ba3..942201b0e 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3468,7 +3468,7 @@ def is_bv_value(a): """ return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) -def BV2Int(a): +def BV2Int(a, is_signed=False): """Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) @@ -3477,6 +3477,10 @@ def BV2Int(a): >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) + >>> x > BV2Int(b, is_signed=False) + x > BV2Int(b) + >>> x > BV2Int(b, is_signed=True) + x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) >>> solve(x > BV2Int(b), b == 1, x < 3) [b = 1, x = 2] """ @@ -3484,7 +3488,7 @@ def BV2Int(a): _z3_assert(is_bv(a), "Z3 bit-vector expression expected") ctx = a.ctx ## investigate problem with bv2int - return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx) + return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) def BitVecSort(sz, ctx=None): """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. @@ -5516,7 +5520,10 @@ class ModelRef(Z3PPObject): decl = decl.decl() try: if decl.arity() == 0: - r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) + _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) + if _r.value is None: + return None + r = _to_expr_ref(_r, self.ctx) if is_as_array(r): return self.get_interp(get_as_array_func(r)) else: diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7c846cc99..9d89bc957 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1060,6 +1060,15 @@ typedef enum { Z3_OP_CARRY, Z3_OP_XOR3, + Z3_OP_BSMUL_NO_OVFL, + Z3_OP_BUMUL_NO_OVFL, + Z3_OP_BSMUL_NO_UDFL, + Z3_OP_BSDIV_I, + Z3_OP_BUDIV_I, + Z3_OP_BSREM_I, + Z3_OP_BUREM_I, + Z3_OP_BSMOD_I, + // Proofs Z3_OP_PR_UNDEF = 0x500, Z3_OP_PR_TRUE, diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index aefa6294a..e6b9dda07 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1928,8 +1928,7 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & tie_pttrn = m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits-1)); m_simp.mk_eq(rem, tie_pttrn, tie2); div_last = m_bv_util.mk_extract(0, 0, div); - tie2_c = m.mk_ite(tie2, m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)), - m.mk_and(rm_is_rta, m.mk_eq(div_last, zero_1))), + tie2_c = m.mk_ite(tie2, m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)), rm_is_rta), m_bv_util.mk_ule(tie_pttrn, rem)); m_simp.mk_ite(tie2_c, div_p1, div, v51); @@ -2235,14 +2234,17 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args SASSERT(is_well_sorted(m, result)); } + void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) { + SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + mk_to_fp_float(s, to_app(rm)->get_arg(0), x, result); +} + +void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_ref & result) { unsigned from_sbits = m_util.get_sbits(m.get_sort(x)); unsigned from_ebits = m_util.get_ebits(m.get_sort(x)); - unsigned to_sbits = m_util.get_sbits(s); - unsigned to_ebits = m_util.get_ebits(s); - - SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM)); - expr * bv_rm = to_app(rm)->get_arg(0); + unsigned to_sbits = m_util.get_sbits(to_srt); + unsigned to_ebits = m_util.get_ebits(to_srt); if (from_sbits == to_sbits && from_ebits == to_ebits) result = x; @@ -2253,20 +2255,20 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * one1 = m_bv_util.mk_numeral(1, 1); expr_ref ninf(m), pinf(m); - mk_pinf(f, pinf); - mk_ninf(f, ninf); + mk_pinf(to_srt, pinf); + mk_ninf(to_srt, ninf); // NaN -> NaN mk_is_nan(x, c1); - mk_nan(f, v1); + mk_nan(to_srt, v1); // +0 -> +0 mk_is_pzero(x, c2); - mk_pzero(f, v2); + mk_pzero(to_srt, v2); // -0 -> -0 mk_is_nzero(x, c3); - mk_nzero(f, v3); + mk_nzero(to_srt, v3); // +oo -> +oo mk_is_pinf(x, c4); @@ -2380,8 +2382,8 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * dbg_decouple("fpa2bv_to_float_res_exp", res_exp); expr_ref rounded(m); - expr_ref rm_e(bv_rm, m); - round(s, rm_e, res_sgn, res_sig, res_exp, rounded); + expr_ref rm_e(rm, m); + round(to_srt, rm_e, res_sgn, res_sig, res_exp, rounded); expr_ref is_neg(m), sig_inf(m); m_simp.mk_eq(sgn, one1, is_neg); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index b6a6bdbb3..32c3124db 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -144,6 +144,9 @@ public: void dbg_decouple(const char * prefix, expr_ref & e); expr_ref_vector m_extra_assertions; + bool is_special(func_decl * f) { return m_specials.contains(f); } + bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); } + protected: void mk_one(func_decl *f, expr_ref & sign, expr_ref & result); @@ -201,6 +204,8 @@ private: void mk_div(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result); void mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & result); void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result); + + void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result); }; #endif diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index ab711dde7..6f6daf8df 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -212,14 +212,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // auxiliary function for pull_ite_core expr * mk_eq_value(expr * lhs, expr * value) { - SASSERT(m().is_value(value)); - if (m().is_value(lhs)) { - if (m().are_equal(lhs, value)) { - return m().mk_true(); - } - else if (m().are_distinct(lhs, value)) { - return m().mk_false(); - } + if (m().are_equal(lhs, value)) { + return m().mk_true(); + } + else if (m().are_distinct(lhs, value)) { + return m().mk_false(); } return m().mk_eq(lhs, value); } diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index 309e0c777..2bf4d5ba3 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -670,7 +670,7 @@ grobner::equation * grobner::simplify(equation const * source, equation * target simplify(target); } } - while (simplified); + while (simplified && !m_manager.canceled()); TRACE("grobner", tout << "result: "; display_equation(tout, *target);); return result ? target : 0; } @@ -697,7 +697,10 @@ grobner::equation * grobner::simplify_using_processed(equation * eq) { simplified = true; eq = new_eq; } - } + if (m_manager.canceled()) { + return 0; + } + } } while (simplified); TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq);); @@ -749,13 +752,13 @@ grobner::equation * grobner::pick_next() { /** \brief Use the given equation to simplify processed terms. */ -void grobner::simplify_processed(equation * eq) { +bool grobner::simplify_processed(equation * eq) { ptr_buffer to_insert; ptr_buffer to_remove; ptr_buffer to_delete; equation_set::iterator it = m_processed.begin(); equation_set::iterator end = m_processed.end(); - for (; it != end; ++it) { + for (; it != end && !m_manager.canceled(); ++it) { equation * curr = *it; m_changed_leading_term = false; // if the leading term is simplified, then the equation has to be moved to m_to_process @@ -795,6 +798,7 @@ void grobner::simplify_processed(equation * eq) { end1 = to_delete.end(); for (; it1 != end1; ++it1) del_equation(*it1); + return !m_manager.canceled(); } /** @@ -944,7 +948,8 @@ bool grobner::compute_basis_step() { m_equations_to_unfreeze.push_back(eq); eq = new_eq; } - simplify_processed(eq); + if (m_manager.canceled()) return false; + if (!simplify_processed(eq)) return false; superpose(eq); m_processed.insert(eq); simplify_to_process(eq); @@ -954,7 +959,7 @@ bool grobner::compute_basis_step() { bool grobner::compute_basis(unsigned threshold) { compute_basis_init(); - while (m_num_new_equations < threshold) { + while (m_num_new_equations < threshold && !m_manager.canceled()) { if (compute_basis_step()) return true; } return false; diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h index 6084bf77d..770f0a538 100644 --- a/src/math/grobner/grobner.h +++ b/src/math/grobner/grobner.h @@ -175,7 +175,7 @@ protected: equation * pick_next(); - void simplify_processed(equation * eq); + bool simplify_processed(equation * eq); void simplify_to_process(equation * eq); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index e67e3cb5e..a5b900ab7 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -114,7 +114,8 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; family_id fid = f->get_family_id(); - if (num == 0 && (fid == null_family_id || m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) { + bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f); + if (num == 0 && (fid == null_family_id || is_uninterp)) { expr * val = m_model.get_const_interp(f); if (val != 0) { result = val; @@ -150,7 +151,7 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); - else if (fid == m_ar_rw.get_fid()) + else if (s_fid == m_ar_rw.get_fid()) st = mk_array_eq(args[0], args[1], result); if (st != BR_FAILED) return st; diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 2a6ff04d4..e8e93dafc 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -219,9 +219,17 @@ public: virtual void set_next_arg(cmd_context & ctx, func_decl* t) { m_target = t; + if (t->get_family_id() != null_family_id) { + throw cmd_exception("Invalid query argument, expected uinterpreted function name, but argument is interpreted"); + } + datalog::context& dlctx = m_dl_ctx->dlctx(); + if (!dlctx.get_predicates().contains(t)) { + throw cmd_exception("Invalid query argument, expected a predicate registered as a relation"); + } } virtual void prepare(cmd_context & ctx) { + ctx.m(); // ensure manager is initialized. parametric_cmd::prepare(ctx); m_target = 0; } @@ -383,6 +391,7 @@ public: virtual unsigned get_arity() const { return VAR_ARITY; } virtual void prepare(cmd_context & ctx) { + ctx.m(); // ensure manager is initialized. m_arg_idx = 0; m_query_arg_idx = 0; m_domain = 0; @@ -443,6 +452,7 @@ public: virtual unsigned get_arity() const { return 2; } virtual void prepare(cmd_context & ctx) { + ctx.m(); // ensure manager is initialized. m_arg_idx = 0; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index f5d98e498..f8f78835c 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -141,6 +141,13 @@ class alternate_min_max_cmd : public cmd { app_ref_vector* m_vars; svector m_is_max; unsigned m_position; + + app_ref_vector& vars(cmd_context& ctx) { + if (!m_vars) { + m_vars = alloc(app_ref_vector, ctx.m()); + } + return *m_vars; + } public: alternate_min_max_cmd(): cmd("min-max"), @@ -150,6 +157,7 @@ public: virtual void reset(cmd_context & ctx) { dealloc(m_vars); + m_vars = 0; m_is_max.reset(); m_position = 0; } @@ -176,8 +184,7 @@ public: } else { m_is_max.push_back(is_max); - if (!m_vars) m_vars = alloc(app_ref_vector, ctx.m()); - m_vars->push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i]))); + vars(ctx).push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i]))); } } ++m_position; @@ -188,8 +195,8 @@ public: throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable"); } ++m_position; - if (!m_vars) m_vars = alloc(app_ref_vector, ctx.m()); - get_opt(ctx).min_max(to_app(t), *m_vars, m_is_max); + get_opt(ctx).min_max(to_app(t), vars(ctx), m_is_max); + reset(ctx); } virtual void failure_cleanup(cmd_context & ctx) { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 4d65b9a25..0c19e7987 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -218,11 +218,9 @@ namespace opt { import_scoped_state(); normalize(); internalize(); - update_solver(); - solver& s = get_solver(); - s.assert_expr(m_hard_constraints); - std::cout << "min-max is TBD\n"; - return l_undef; + qe::max_min_opt max_min(m, m_params); + max_min.add(m_hard_constraints); + return max_min.check(is_max, vars, t); } diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 60111a473..58a290c0b 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -51,13 +51,6 @@ namespace qe { } return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t); } - - -#if 0 - obj_map m_expr2var; - ptr_vector m_var2expr; - -#endif struct arith_project_plugin::imp { @@ -88,18 +81,23 @@ namespace qe { } } - void insert_mul(expr* x, rational const& v, obj_map& ts) - { + void insert_mul(expr* x, rational const& v, obj_map& ts) { rational w; if (ts.find(x, w)) { ts.insert(x, w + v); } else { + TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << "\n";); ts.insert(x, v); } } - void linearize(model& model, opt::model_based_opt& mbo, expr* lit, obj_map& tids) { + // + // extract linear inequalities from literal 'lit' into the model-based optimization manager 'mbo'. + // It uses the current model to choose values for conditionals and it primes mbo with the current + // interpretation of sub-expressions that are treated as variables for mbo. + // + void linearize(opt::model_based_opt& mbo, model& model, expr* lit, obj_map& tids) { obj_map ts; rational c(0), mul(1); expr_ref t(m); @@ -112,19 +110,19 @@ namespace qe { SASSERT(!m.is_not(lit)); if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) { if (is_not) mul.neg(); - linearize(model, mul, e1, c, ts); - linearize(model, -mul, e2, c, ts); + linearize(mbo, model, mul, e1, c, ts, tids); + linearize(mbo, model, -mul, e2, c, ts, tids); ty = is_not ? opt::t_lt : opt::t_le; } else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) { if (is_not) mul.neg(); - linearize(model, mul, e1, c, ts); - linearize(model, -mul, e2, c, ts); + linearize(mbo, model, mul, e1, c, ts, tids); + linearize(mbo, model, -mul, e2, c, ts, tids); ty = is_not ? opt::t_le: opt::t_lt; } else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) { - linearize(model, mul, e1, c, ts); - linearize(model, -mul, e2, c, ts); + linearize(mbo, model, mul, e1, c, ts, tids); + linearize(mbo, model, -mul, e2, c, ts, tids); ty = opt::t_eq; } else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) { @@ -137,55 +135,63 @@ namespace qe { UNREACHABLE(); } else { + TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";); return; } - if (ty == opt::t_lt && is_int()) { +#if 0 + TBD for integers + if (ty == opt::t_lt && false) { c += rational(1); ty = opt::t_le; } +#endif vars coeffs; - extract_coefficients(ts, tids, coeffs); + extract_coefficients(mbo, model, ts, tids, coeffs); mbo.add_constraint(coeffs, c, ty); } - void linearize(model& model, rational const& mul, expr* t, rational& c, obj_map& ts) { + // + // convert linear arithmetic term into an inequality for mbo. + // + void linearize(opt::model_based_opt& mbo, model& model, rational const& mul, expr* t, rational& c, + obj_map& ts, obj_map& tids) { expr* t1, *t2, *t3; rational mul1; expr_ref val(m); if (a.is_mul(t, t1, t2) && is_numeral(model, t1, mul1)) { - linearize(model, mul* mul1, t2, c, ts); + linearize(mbo, model, mul* mul1, t2, c, ts, tids); } else if (a.is_mul(t, t1, t2) && is_numeral(model, t2, mul1)) { - linearize(model, mul* mul1, t1, c, ts); + linearize(mbo, model, mul* mul1, t1, c, ts, tids); } else if (a.is_add(t)) { app* ap = to_app(t); for (unsigned i = 0; i < ap->get_num_args(); ++i) { - linearize(model, mul, ap->get_arg(i), c, ts); + linearize(mbo, model, mul, ap->get_arg(i), c, ts, tids); } } else if (a.is_sub(t, t1, t2)) { - linearize(model, mul, t1, c, ts); - linearize(model, -mul, t2, c, ts); + linearize(mbo, model, mul, t1, c, ts, tids); + linearize(mbo, model, -mul, t2, c, ts, tids); } else if (a.is_uminus(t, t1)) { - linearize(model, -mul, t1, c, ts); + linearize(mbo, model, -mul, t1, c, ts, tids); } else if (a.is_numeral(t, mul1)) { c += mul*mul1; } - else if (extract_mod(model, t, val)) { - insert_mul(val, mul, ts); - } else if (m.is_ite(t, t1, t2, t3)) { VERIFY(model.eval(t1, val)); SASSERT(m.is_true(val) || m.is_false(val)); TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";); if (m.is_true(val)) { - linearize(model, mul, t2, c, ts); + linearize(mbo, model, mul, t2, c, ts, tids); + linearize(mbo, model, t1, tids); } else { - linearize(model, mul, t3, c, ts); + expr_ref not_t1(mk_not(m, t1), m); + linearize(mbo, model, mul, t3, c, ts, tids); + linearize(mbo, model, not_t1, tids); } } else { @@ -193,6 +199,9 @@ namespace qe { } } + // + // extract linear terms from t into c and ts. + // void is_linear(model& model, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) { expr* t1, *t2, *t3; rational mul1; @@ -245,7 +254,9 @@ namespace qe { } } - + // + // extract linear inequalities from literal lit. + // bool is_linear(model& model, expr* lit, bool& found_eq) { rational c(0), mul(1); expr_ref t(m); @@ -977,13 +988,13 @@ namespace qe { // extract objective function. vars coeffs; rational c(0), mul(1); - linearize(mdl, mul, t, c, ts); - extract_coefficients(ts, tids, coeffs); + linearize(mbo, mdl, mul, t, c, ts, tids); + extract_coefficients(mbo, mdl, ts, tids, coeffs); mbo.set_objective(coeffs, c); // extract linear constraints for (unsigned i = 0; i < fmls.size(); ++i) { - linearize(mdl, mbo, fmls[i], tids); + linearize(mbo, mdl, fmls[i], tids); } // find optimal value @@ -1021,13 +1032,21 @@ namespace qe { return value; } - void extract_coefficients(obj_map const& ts, obj_map& tids, vars& coeffs) { + void extract_coefficients(opt::model_based_opt& mbo, model& model, obj_map const& ts, obj_map& tids, vars& coeffs) { coeffs.reset(); obj_map::iterator it = ts.begin(), end = ts.end(); for (; it != end; ++it) { unsigned id; if (!tids.find(it->m_key, id)) { - id = tids.size(); + rational r; + expr_ref val(m); + if (model.eval(it->m_key, val) && a.is_numeral(val, r)) { + id = mbo.add_var(r); + } + else { + TRACE("qe", tout << "extraction of coefficients cancelled\n";); + return; + } tids.insert(it->m_key, id); } coeffs.push_back(var(id, it->m_value)); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index e09f87e5f..73f6a9d4c 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -548,8 +548,7 @@ namespace qe { unsigned m_num_rounds; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } - }; - + }; ast_manager& m; params_ref m_params; @@ -619,7 +618,7 @@ namespace qe { } kernel& get_kernel(unsigned j) { - if (is_exists(j)) { + if (m_kernel_ex || is_exists(j)) { return m_ex; } else { @@ -704,96 +703,7 @@ namespace qe { for (unsigned i = 0; i < vars.size(); ++i) { m_pred_abs.fmc()->insert(vars[i]->get_decl()); } - } - -#if 0 - void hoist_ite(expr_ref& fml) { - app* ite; - scoped_ptr replace = mk_default_expr_replacer(m); - th_rewriter rewriter(m); - while (find_ite(fml, ite)) { - expr* cond, *th, *el; - VERIFY(m.is_ite(ite, cond, th, el)); - expr_ref tmp1(fml, m), tmp2(fml, m); - replace->apply_substitution(cond, m.mk_true(), tmp1); - replace->apply_substitution(cond, m.mk_false(), tmp2); - fml = m.mk_ite(cond, tmp1, tmp2); - rewriter(fml); - } - } - - bool find_ite(expr* e, app*& ite) { - ptr_vector todo; - todo.push_back(e); - ast_mark visited; - while(!todo.empty()) { - e = todo.back(); - todo.pop_back(); - if (visited.is_marked(e)) { - continue; - } - visited.mark(e, true); - if (m.is_ite(e) && !m.is_bool(e)) { - ite = to_app(e); - return true; - } - if (is_app(e)) { - app* a = to_app(e); - todo.append(a->get_num_args(), a->get_args()); - } - } - return false; - } - - // slower - void hoist_ite2(expr_ref& fml) { - obj_map result; - expr_ref_vector trail(m); - ptr_vector todo, args; - todo.push_back(fml); - - while (!todo.empty()) { - expr* e = todo.back(); - if (result.contains(e)) { - todo.pop_back(); - continue; - } - if (!is_app(e)) { - todo.pop_back(); - result.insert(e, e); - continue; - } - app* a = to_app(e); - expr* r; - unsigned sz = a->get_num_args(); - args.reset(); - for (unsigned i = 0; i < sz; ++i) { - if (result.find(a->get_arg(i), r)) { - args.push_back(r); - } - else { - todo.push_back(a->get_arg(i)); - } - } - if (sz == args.size()) { - r = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); - trail.push_back(r); - if (m.is_bool(e) && m.get_basic_family_id() != a->get_family_id()) { - expr_ref fml(r, m); - hoist_ite(fml); - trail.push_back(fml); - r = fml; - } - result.insert(e, r); - todo.pop_back(); - } - } - fml = result.find(fml); - } -#endif - - - + } void initialize_levels() { // initialize levels. @@ -1160,7 +1070,8 @@ namespace qe { m_level(0), m_mode(mode), m_avars(m), - m_free_vars(m) + m_free_vars(m), + m_kernel_ex(false) { reset(); } @@ -1326,6 +1237,92 @@ namespace qe { m_ex.assert_expr(bound); } + + bool m_kernel_ex; + + lbool max_min(expr_ref_vector const& fmls, svector const& is_max, app_ref_vector const& vars, app* t) { + m_kernel_ex = true; + // Assume this is the only call to check. + expr_ref_vector defs(m); + app_ref_vector free_vars(m), vars1(m); + expr_ref fml = mk_and(fmls); + m_pred_abs.get_free_vars(fml, free_vars); + m_pred_abs.abstract_atoms(fml, defs); + fml = m_pred_abs.mk_abstract(fml); + get_kernel(0).k().assert_expr(mk_and(defs)); + get_kernel(0).k().assert_expr(fml); + obj_hashtable var_set; + for (unsigned i = 0; i < vars.size(); ++i) { + var_set.insert(vars[i]); + } + for (unsigned i = 0; i < free_vars.size(); ++i) { + app* v = free_vars[i].get(); + if (!var_set.contains(v)) { + vars1.push_back(v); + } + } + // + // Insert all variables in alternating list of max/min objectives. + // By convention, the outer-most level is max. + // + bool is_m = true; + for (unsigned i = 0; i < vars.size(); ++i) { + if (is_m != is_max[i]) { + m_vars.push_back(vars1); + vars1.reset(); + is_m = is_max[i]; + } + vars1.push_back(vars[i]); + } + m_vars.push_back(vars1); + + return max_min(); + } + + lbool max_min() { + while (true) { + ++m_stats.m_num_rounds; + check_cancel(); + expr_ref_vector asms(m_asms); + m_pred_abs.get_assumptions(m_model.get(), asms); + // + // TBD: add bound to asms. + // + smt::kernel& k = get_kernel(m_level).k(); + lbool res = k.check(asms); + switch (res) { + case l_true: + k.get_model(m_model); + SASSERT(validate_model(asms)); + TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); ); + // + // TBD: compute new bound on objective. + // + push(); + break; + case l_false: + switch (m_level) { + case 0: return l_false; + case 1: + // TBD + break; + default: + if (m_model.get()) { + project(asms); + } + else { + pop(1); + } + break; + } + break; + case l_undef: + return res; + } + } + return l_undef; + } + }; lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p) { @@ -1333,6 +1330,50 @@ namespace qe { qsat qs(m, p, qsat_maximize); return qs.maximize(fmls, t, mdl, value); } + + + struct max_min_opt::imp { + + expr_ref_vector m_fmls; + qsat m_qsat; + + imp(ast_manager& m, params_ref const& p): + m_fmls(m), + m_qsat(m, p, qsat_maximize) + {} + + void add(expr* e) { + m_fmls.push_back(e); + } + + lbool check(svector const& is_max, app_ref_vector const& vars, app* t) { + return m_qsat.max_min(m_fmls, is_max, vars, t); + } + + }; + + max_min_opt::max_min_opt(ast_manager& m, params_ref const& p) { + m_imp = alloc(imp, m, p); + } + + max_min_opt::~max_min_opt() { + dealloc(m_imp); + } + + void max_min_opt::add(expr* e) { + m_imp->add(e); + } + + void max_min_opt::add(expr_ref_vector const& fmls) { + for (unsigned i = 0; i < fmls.size(); ++i) { + add(fmls[i]); + } + } + + lbool max_min_opt::check(svector const& is_max, app_ref_vector const& vars, app* t) { + return m_imp->check(is_max, vars, t); + } + }; tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) { @@ -1350,94 +1391,3 @@ tactic * mk_qe_rec_tactic(ast_manager& m, params_ref const& p) { -#if 0 - - class min_max_opt { - struct imp; - imp* m_imp; - public: - min_max_opt(ast_manager& m); - ~min_max_opt(); - void add(expr* e); - void add(expr_ref_vector const& fmls); - lbool check(svector const& is_max, app_ref_vector const& vars, app* t); - }; - - struct min_max_opt::imp { - ast_manager& m; - expr_ref_vector m_fmls; - pred_abs m_pred_abs; - qe::mbp m_mbp; - kernel m_kernel; - vector m_vars; - - imp(ast_manager& m): - m(m), - m_fmls(m), - m_pred_abs(m), - m_mbp(m), - m_kernel(m) {} - - void add(expr* e) { - m_fmls.push_back(e); - } - - lbool check(svector const& is_max, app_ref_vector const& vars, app* t) { - // Assume this is the only call to check. - expr_ref_vector defs(m); - app_ref_vector free_vars(m), vars1(m); - expr_ref fml = mk_and(m_fmls); - m_pred_abs.get_free_vars(fml, free_vars); - m_pred_abs.abstract_atoms(fml, defs); - fml = m_pred_abs.mk_abstract(fml); - m_kernel.assert_expr(mk_and(defs)); - m_kernel.assert_expr(fml); - obj_hashtable var_set; - for (unsigned i = 0; i < vars.size(); ++i) { - var_set.insert(vars[i]); - } - for (unsigned i = 0; i < free_vars.size(); ++i) { - app* v = free_vars[i].get(); - if (!var_set.contains(v)) { - vars1.push_back(v); - } - } - bool is_m = is_max[0]; - for (unsigned i = 0; i < vars.size(); ++i) { - if (is_m != is_max[i]) { - m_vars.push_back(vars1); - vars1.reset(); - is_m = is_max[i]; - } - vars1.push_back(vars[i]); - } - - // TBD - - return l_undef; - } - }; - - min_max_opt::min_max_opt(ast_manager& m) { - m_imp = alloc(imp, m); - } - - min_max_opt::~min_max_opt() { - dealloc(m_imp); - } - - void min_max_opt::add(expr* e) { - m_imp->add(e); - } - - void min_max_opt::add(expr_ref_vector const& fmls) { - for (unsigned i = 0; i < fmls.size(); ++i) { - add(fmls[i]); - } - } - - lbool min_max_opt::check(svector const& is_max, app_ref_vector const& vars, app* t) { - return m_imp->check(is_max, vars, t); - } - -#endif diff --git a/src/qe/qsat.h b/src/qe/qsat.h index 456711c4f..59cf6d8a0 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -114,6 +114,17 @@ namespace qe { void collect_statistics(statistics& st) const; }; + class max_min_opt { + struct imp; + imp* m_imp; + public: + max_min_opt(ast_manager& m, params_ref const& p = params_ref()); + ~max_min_opt(); + void add(expr* e); + void add(expr_ref_vector const& fmls); + lbool check(svector const& is_max, app_ref_vector const& vars, app* t); + }; + lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p); } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 23e1f746d..543b1348e 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -85,8 +85,63 @@ namespace smt { } void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - // TODO: This introduces temporary variables/func_decls that should be filtered in the end. - fpa2bv_converter::mk_uninterpreted_function(f, num, args, result); + // TODO: This introduces temporary func_decls that should be filtered in the end. + + TRACE("t_fpa", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; ); + SASSERT(f->get_arity() == num); + + expr_ref_buffer new_args(m); + + for (unsigned i = 0; i < num; i++) { + if (is_float(args[i]) || is_rm(args[i])) { + expr_ref ai(m), wrapped(m); + ai = args[i]; + wrapped = m_th.wrap(ai); + new_args.push_back(wrapped); + m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, m.get_sort(ai)), ai)); + } + else + new_args.push_back(args[i]); + } + + func_decl * fd; + if (m_uf2bvuf.find(f, fd)) + mk_uninterpreted_output(f->get_range(), fd, new_args, result); + else { + sort_ref_buffer new_domain(m); + + for (unsigned i = 0; i < f->get_arity(); i++) { + sort * di = f->get_domain()[i]; + if (is_float(di)) + new_domain.push_back(m_bv_util.mk_sort(m_util.get_sbits(di) + m_util.get_ebits(di))); + else if (is_rm(di)) + new_domain.push_back(m_bv_util.mk_sort(3)); + else + new_domain.push_back(di); + } + + sort * frng = f->get_range(); + sort_ref rng(frng, m); + if (m_util.is_float(frng)) + rng = m_bv_util.mk_sort(m_util.get_ebits(frng) + m_util.get_sbits(frng)); + else if (m_util.is_rm(frng)) + rng = m_bv_util.mk_sort(3); + + func_decl_ref fbv(m); + fbv = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), rng); + TRACE("t_fpa", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl;); + + m_uf2bvuf.insert(f, fbv); + m.inc_ref(f); + m.inc_ref(fbv); + + mk_uninterpreted_output(frng, fbv, new_args, result); + } + + expr_ref fapp(m); + fapp = m.mk_app(f, num, args); + m_extra_assertions.push_back(m.mk_eq(fapp, result)); + TRACE("t_fpa", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; ); } expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) { @@ -284,30 +339,40 @@ namespace smt { app_ref theory_fpa::wrap(expr * e) { SASSERT(!m_fpa_util.is_wrap(e)); ast_manager & m = get_manager(); - sort * e_srt = m.get_sort(e); + app_ref res(m); - func_decl *w; + if (is_app(e) && + to_app(e)->get_family_id() == get_family_id() && + to_app(e)->get_decl_kind() == OP_FPA_FP) { + expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) }; + res = m_bv_util.mk_concat(3, cargs); + m_th_rw((expr_ref&)res); + } + else { + sort * e_srt = m.get_sort(e); + func_decl * w; - if (!m_wraps.find(e_srt, w)) { - SASSERT(!m_wraps.contains(e_srt)); + if (!m_wraps.find(e_srt, w)) { + SASSERT(!m_wraps.contains(e_srt)); - sort * bv_srt; - if (m_converter.is_rm(e_srt)) - bv_srt = m_bv_util.mk_sort(3); - else { - SASSERT(m_converter.is_float(e_srt)); - unsigned ebits = m_fpa_util.get_ebits(e_srt); - unsigned sbits = m_fpa_util.get_sbits(e_srt); - bv_srt = m_bv_util.mk_sort(ebits + sbits); + sort * bv_srt; + if (m_converter.is_rm(e_srt)) + bv_srt = m_bv_util.mk_sort(3); + else { + SASSERT(m_converter.is_float(e_srt)); + unsigned ebits = m_fpa_util.get_ebits(e_srt); + unsigned sbits = m_fpa_util.get_sbits(e_srt); + bv_srt = m_bv_util.mk_sort(ebits + sbits); + } + + w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); + m_wraps.insert(e_srt, w); + m.inc_ref(w); } - w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); - m_wraps.insert(e_srt, w); - m.inc_ref(w); + res = m.mk_app(w, e); } - - app_ref res(m); - res = m.mk_app(w, e); + return res; } @@ -389,59 +454,6 @@ namespace smt { return res; } -#if 0 - expr_ref theory_fpa::convert_uf(expr * e) { - SASSERT(is_app(e)); - ast_manager & m = get_manager(); - expr_ref res(m); - - app * a = to_app(e); - func_decl * f = a->get_decl(); - sort * const * domain = f->get_domain(); - unsigned arity = f->get_arity(); - - expr_ref_buffer new_args(m); - expr_ref unwrapped(m); - - for (unsigned i = 0; i < arity; i++) { - expr * ai = a->get_arg(i); - if (m_fpa_util.is_float(ai) || m_fpa_util.is_rm(ai)) { - if (m_fpa_util.is_unwrap(ai)) - unwrapped = ai; - else { - // unwrapped = unwrap(wrap(ai), domain[i]); - // assert_cnstr(m.mk_eq(unwrapped, ai)); - // assert_cnstr(); - unwrapped = convert_term(ai); - } - - new_args.push_back(unwrapped); - TRACE("t_fpa_detail", tout << "UF arg(" << i << ") = " << mk_ismt2_pp(unwrapped, get_manager()) << "\n";); - } - else - new_args.push_back(ai); - } - - sort * rng = f->get_range(); - if (m_fpa_util.is_float(rng)) { - unsigned sbits = m_fpa_util.get_sbits(rng); - unsigned bv_sz = m_fpa_util.get_ebits(rng) + sbits; - expr_ref wrapped(m); - wrapped = wrap(m.mk_app(f, new_args.size(), new_args.c_ptr())); - - m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped), - m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped), - m_bv_util.mk_extract(sbits - 2, 0, wrapped), - res); - } - else - res = m.mk_app(f, new_args.size(), new_args.c_ptr()); - - TRACE("t_fpa_detail", tout << "UF call = " << mk_ismt2_pp(res, get_manager()) << "\n";); - return res; - } -#endif - expr_ref theory_fpa::convert_conversion_term(expr * e) { /* This is for the conversion functions fp.to_* */ ast_manager & m = get_manager(); @@ -606,6 +618,7 @@ namespace smt { // Therefore, we translate and assert them here. fpa_op_kind k = (fpa_op_kind)term->get_decl_kind(); switch (k) { + case OP_FPA_TO_FP: case OP_FPA_TO_UBV: case OP_FPA_TO_SBV: case OP_FPA_TO_REAL: @@ -966,4 +979,16 @@ namespace smt { out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl; } } + + bool theory_fpa::include_func_interp(func_decl * f) { + TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;); + func_decl * wt; + + if (m_wraps.find(f->get_range(), wt) || m_unwraps.find(f->get_range(), wt)) + return wt == f; + else if (m_converter.is_uf2bvuf(f) || m_converter.is_special(f)) + return false; + else + return true; + } }; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 1b0fc6c54..d693e3ede 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -83,7 +83,7 @@ namespace smt { virtual ~fpa2bv_converter_wrapped() {} virtual void mk_const(func_decl * f, expr_ref & result); virtual void mk_rm_const(func_decl * f, expr_ref & result); - virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); @@ -112,7 +112,7 @@ namespace smt { result.append(m_deps); } - virtual app * mk_value(model_generator & mg, ptr_vector & values); + virtual app * mk_value(model_generator & mg, ptr_vector & values); }; class fpa_rm_value_proc : public model_value_proc { @@ -163,6 +163,7 @@ namespace smt { virtual char const * get_name() const { return "fpa"; } virtual model_value_proc * mk_value(enode * n, model_generator & mg); + virtual bool include_func_interp(func_decl * f); void assign_eh(bool_var v, bool is_true); virtual void relevant_eh(app * n); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 86761412f..239ba7420 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2823,6 +2823,7 @@ void theory_seq::add_elim_string_axiom(expr* n) { - len(unit(u)) = 1 if x = unit(u) - len(str) = str.length() if x = str - len(empty) = 0 if x = empty + - len(int.to.str(i)) >= 1 if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|)) - len(x) >= 0 otherwise */ void theory_seq::add_length_axiom(expr* n) { @@ -2837,16 +2838,17 @@ void theory_seq::add_length_axiom(expr* n) { m_rewrite(len); SASSERT(n != len); add_axiom(mk_eq(len, n, false)); - if (!ctx.at_base_level()) { - m_trail_stack.push(push_replay(alloc(replay_axiom, m, n))); - } + } + else if (m_util.str.is_itos(x)) { + add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(1)))); } else { add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0)))); - if (!ctx.at_base_level()) { - m_trail_stack.push(push_replay(alloc(replay_axiom, m, n))); - } } + if (!ctx.at_base_level()) { + m_trail_stack.push(push_replay(alloc(replay_axiom, m, n))); + } + } diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index d4e738ed7..db60f3fcd 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -163,6 +163,59 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr result = m_manager.mk_distinct_expanded(num, args); res = BR_REWRITE1; } + else if (m_manager.is_term_ite(f) && is_bv_array(f->get_range())) { + expr_ref c(args[0], m_manager); + func_decl_ref f_t(mk_uf_for_array(args[1]), m_manager); + func_decl_ref f_f(mk_uf_for_array(args[2]), m_manager); + + TRACE("bvarray2uf_rw", tout << "(ite " << c << ", " << f_t->get_name() + << ", " << f_f->get_name() << ")" << std::endl;); + + sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[1])) }; + symbol names[1] = { symbol("x") }; + var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); + + app_ref f_a(m_manager), f_ta(m_manager), f_fa(m_manager); + f_a = m_manager.mk_app(f, num, args); + f_ta = m_manager.mk_app(f_t, x.get()); + f_fa = m_manager.mk_app(f_f, x.get()); + + app_ref e(m_manager); + func_decl_ref itefd(m_manager); + e = m_manager.mk_ite(c, f_ta, f_fa); + + func_decl * bv_f = 0; + if (!m_arrays_fs.find(f_a, bv_f)) { + sort * domain = get_index_sort(args[1]); + sort * range = get_value_sort(args[1]); + bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range); + TRACE("bvarray2uf_rw", tout << mk_ismt2_pp(e, m_manager) << " -> " << bv_f->get_name() << std::endl; ); + if (is_uninterp_const(e)) { + if (m_emc) + m_emc->insert(e->get_decl(), + m_array_util.mk_as_array(m_manager.get_sort(e), bv_f)); + } + else if (m_fmc) + m_fmc->insert(bv_f); + m_arrays_fs.insert(e, bv_f); + m_manager.inc_ref(e); + m_manager.inc_ref(bv_f); + } + + expr_ref q(m_manager), body(m_manager); + body = m_manager.mk_eq(m_manager.mk_app(bv_f, x), e); + q = m_manager.mk_forall(1, sorts, names, body); + extra_assertions.push_back(q); + + result = m_array_util.mk_as_array(f->get_range(), bv_f); + + TRACE("bvarray2uf_rw", tout << "result: " << mk_ismt2_pp(result, m_manager) << ")" << std::endl;); + res = BR_DONE; + + } + else if (f->get_family_id() == m_manager.get_basic_family_id() && is_bv_array(f->get_range())) { + NOT_IMPLEMENTED_YET(); + } else if (f->get_family_id() == null_family_id) { TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; ); diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index a1b5c2859..f14ccf3e2 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -280,12 +280,170 @@ static void test2(char const *ex) { ctx.assert_expr(pr1); ctx.assert_expr(npr2); VERIFY(l_false == ctx.check()); - ctx.pop(1); - - + ctx.pop(1); } +typedef opt::model_based_opt::var var_t; + +static void mk_var(unsigned x, app_ref& v) { + ast_manager& m = v.get_manager(); + arith_util a(m); + std::ostringstream strm; + strm << "v" << x; + v = m.mk_const(symbol(strm.str().c_str()), a.mk_real()); +} + +static void mk_term(vector const& vars, rational const& coeff, app_ref& term) { + ast_manager& m = term.get_manager(); + expr_ref_vector ts(m); + arith_util a(m); + + for (unsigned i = 0; i < vars.size(); ++i) { + app_ref var(m); + mk_var(vars[i].m_id, var); + rational coeff = vars[i].m_coeff; + ts.push_back(a.mk_mul(a.mk_numeral(coeff, false), var)); + } + ts.push_back(a.mk_numeral(coeff, a.mk_real())); + term = a.mk_add(ts.size(), ts.c_ptr()); +} + +static void add_random_ineq( + expr_ref_vector& fmls, + opt::model_based_opt& mbo, + random_gen& r, + svector const& values, + unsigned max_vars, + unsigned max_coeff) +{ + ast_manager& m = fmls.get_manager(); + arith_util a(m); + + unsigned num_vars = values.size(); + uint_set used_vars; + vector vars; + int value = 0; + for (unsigned i = 0; i < max_vars; ++i) { + unsigned x = r(num_vars); + if (used_vars.contains(x)) { + continue; + } + used_vars.insert(x); + int coeff = r(max_coeff + 1); + if (coeff == 0) { + continue; + } + unsigned sign = r(2); + coeff = sign == 0 ? coeff : -coeff; + vars.push_back(var_t(x, rational(coeff))); + value += coeff*values[x]; + } + unsigned abs_value = value < 0 ? - value : value; + // value + k <= 0 + // k <= - value + // range for k is 2*|value| + // k <= - value - range + opt::ineq_type rel = opt::t_le; + + int coeff = 0; + if (r(4) == 0) { + rel = opt::t_eq; + coeff = -value; + } + else { + if (abs_value > 0) { + coeff = -value - r(2*abs_value); + } + else { + coeff = 0; + } + if (coeff != -value && r(3) == 0) { + rel = opt::t_lt; + } + } + expr_ref fml(m); + app_ref t1(m); + app_ref t2(a.mk_numeral(rational(0), a.mk_real()), m); + mk_term(vars, rational(coeff), t1); + switch (rel) { + case opt::t_eq: + fml = m.mk_eq(t1, t2); + break; + case opt::t_lt: + fml = a.mk_lt(t1, t2); + break; + case opt::t_le: + fml = a.mk_le(t1, t2); + break; + } + fmls.push_back(fml); + mbo.add_constraint(vars, rational(coeff), rel); +} + +static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) { + qe::arith_project_plugin plugin(m); + model mdl(m); + expr_ref bound(m); + arith_util a(m); + for (unsigned i = 0; i < num_vars; ++i) { + app_ref var(m); + mk_var(i, var); + rational val = mbo.get_value(i); + mdl.register_decl(var->get_decl(), a.mk_numeral(val, false)); + } + opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, bound); + opt::inf_eps value2 = mbo.maximize(); + std::cout << "optimal: " << value1 << " " << value2 << "\n"; + mbo.display(std::cout); +} + +static void check_random_ineqs(random_gen& r, ast_manager& m, unsigned num_vars, unsigned max_value, unsigned num_ineqs, unsigned max_vars, unsigned max_coeff) { + opt::model_based_opt mbo; + expr_ref_vector fmls(m); + + svector values; + for (unsigned i = 0; i < num_vars; ++i) { + values.push_back(r(max_value + 1)); + mbo.add_var(rational(values.back())); + } + for (unsigned i = 0; i < num_ineqs; ++i) { + add_random_ineq(fmls, mbo, r, values, max_vars, max_coeff); + } + + vector vars; + vars.reset(); + vars.push_back(var_t(0, rational(2))); + vars.push_back(var_t(1, rational(-2))); + mbo.set_objective(vars, rational(0)); + + + mbo.display(std::cout); + app_ref t(m); + mk_term(vars, rational(0), t); + + test_maximize(mbo, m, num_vars, fmls, t); + + for (unsigned i = 0; i < values.size(); ++i) { + std::cout << i << ": " << values[i] << " -> " << mbo.get_value(i) << "\n"; + } +} + +static void check_random_ineqs() { + random_gen r(1); + ast_manager m; + reg_decl_plugins(m); + + for (unsigned i = 0; i < 100; ++i) { + check_random_ineqs(r, m, 4, 5, 5, 3, 6); + } +} + + + + void tst_qe_arith() { + check_random_ineqs(); + return; // enable_trace("qe"); testI(example8); testR(example7); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index de215c958..e84298231 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1095,7 +1095,7 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o TRACE("mpf_dbg", tout << "tie= " << tie << "; tie = " << more_than_tie << std::endl;); if (tie) { if ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) || - (rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div))) { + (rm == MPF_ROUND_NEAREST_TAWAY)) { TRACE("mpf_dbg", tout << "div++ (1)" << std::endl;); m_mpz_manager.inc(div); } @@ -1214,11 +1214,194 @@ void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) { } } +void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig) { + if (m_mpz_manager.is_zero(sig)) + return; + + const mpz & pg = m_powers2(sbits); + while (m_mpz_manager.ge(sig, pg)) { + m_mpz_manager.machine_div2k(sig, 1); + exp++; + } + + const mpz & pl = m_powers2(sbits-1); + while (m_mpz_manager.lt(sig, pl)) { + m_mpz_manager.mul2k(sig, 1); + exp--; + } +} + +void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial) { + unsigned ebits = x.ebits; + unsigned sbits = x.sbits; + + SASSERT(-1 <= exp_diff && exp_diff < INT64_MAX); + SASSERT(exp_diff < ebits+sbits || partial); + + signed int D = (signed int)(exp_diff); + mpf_exp_t N = sbits-1; + + TRACE("mpf_dbg_rem", tout << "x=" << to_string(x) << std::endl; + tout << "y=" << to_string(y) << std::endl; + tout << "d=" << D << std::endl; + tout << "partial=" << partial << std::endl;); + + SASSERT(m_mpz_manager.lt(x.significand, m_powers2(sbits))); + SASSERT(m_mpz_manager.ge(x.significand, m_powers2(sbits - 1))); + SASSERT(m_mpz_manager.lt(y.significand, m_powers2(sbits))); + SASSERT(m_mpz_manager.ge(y.significand, m_powers2(sbits - 1))); + + // 1. Compute a/b + bool x_div_y_sgn = x.sign != y.sign; + mpf_exp_t x_div_y_exp = D; + scoped_mpz x_sig_shifted(m_mpz_manager), x_div_y_sig_lrg(m_mpz_manager), x_div_y_rem(m_mpz_manager); + scoped_mpz x_rem_y_sig(m_mpz_manager); + m_mpz_manager.mul2k(x.significand, 2*sbits + 2, x_sig_shifted); + m_mpz_manager.machine_div_rem(x_sig_shifted, y.significand, x_div_y_sig_lrg, x_div_y_rem); // rem useful? + // x/y is in x_diuv_y_sig_lrg and has sbits+3 extra bits. + + TRACE("mpf_dbg_rem", tout << "X/Y_exp=" << x_div_y_exp << std::endl; + tout << "X/Y_sig_lrg=" << m_mpz_manager.to_string(x_div_y_sig_lrg) << std::endl; + tout << "X/Y_rem=" << m_mpz_manager.to_string(x_div_y_rem) << std::endl; + tout << "X/Y~=" << to_string_hexfloat(x_div_y_sgn, x_div_y_exp, x_div_y_sig_lrg, ebits, sbits, sbits+3) << std::endl;); + + // 2. Round a/b to integer Q/QQ + bool Q_sgn = x_div_y_sgn; + mpf_exp_t Q_exp = x_div_y_exp; + scoped_mpz Q_sig(m_mpz_manager), Q_rem(m_mpz_manager); + unsigned Q_shft = (sbits-1) + (sbits+3) - (unsigned) (partial ? N :Q_exp); + if (partial) { + // Round according to MPF_ROUND_TOWARD_ZERO + SASSERT(0 < N && N < Q_exp && Q_exp < INT_MAX); + m_mpz_manager.machine_div2k(x_div_y_sig_lrg, Q_shft, Q_sig); + } + else { + // Round according to MPF_ROUND_NEAREST_TEVEN + m_mpz_manager.machine_div_rem(x_div_y_sig_lrg, m_powers2(Q_shft), Q_sig, Q_rem); + const mpz & shiftm1_p = m_powers2(Q_shft-1); + bool tie = m_mpz_manager.eq(Q_rem, shiftm1_p); + bool more_than_tie = m_mpz_manager.gt(Q_rem, shiftm1_p); + TRACE("mpf_dbg_rem", tout << "tie= " << tie << "; >tie= " << more_than_tie << std::endl;); + if ((tie && m_mpz_manager.is_odd(Q_sig)) || more_than_tie) + m_mpz_manager.inc(Q_sig); + } + m_mpz_manager.mul2k(Q_sig, Q_shft); + m_mpz_manager.machine_div2k(Q_sig, sbits+3); + renormalize(ebits, sbits, Q_exp, Q_sig); + + TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl; + tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl; + tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;); + + if ((D == -1 || partial) && m_mpz_manager.is_zero(Q_sig)) + return; // This means x % y = x. + + // no extra bits in Q_sig. + SASSERT(!m_mpz_manager.is_zero(Q_sig)); + SASSERT(m_mpz_manager.lt(Q_sig, m_powers2(sbits))); + SASSERT(m_mpz_manager.ge(Q_sig, m_powers2(sbits - 1))); + + + // 3. Compute Y*Q / Y*QQ*2^{D-N} + bool YQ_sgn = y.sign ^ Q_sgn; + scoped_mpz YQ_sig(m_mpz_manager); + mpf_exp_t YQ_exp = Q_exp + y.exponent; + m_mpz_manager.mul(y.significand, Q_sig, YQ_sig); + renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits. + + TRACE("mpf_dbg_rem", tout << "YQ_sgn=" << YQ_sgn << std::endl; + tout << "YQ_exp=" << YQ_exp << std::endl; + tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl; + tout << "YQ=" << to_string_hexfloat(YQ_sgn, YQ_exp, YQ_sig, ebits, sbits, sbits-1) << std::endl;); + + // `sbits-1' extra bits in YQ_sig. + SASSERT(m_mpz_manager.lt(YQ_sig, m_powers2(2*sbits-1))); + SASSERT(m_mpz_manager.ge(YQ_sig, m_powers2(2*sbits-2)) || YQ_exp <= mk_bot_exp(ebits)); + + // 4. Compute X-Y*Q + mpf_exp_t X_YQ_exp = x.exponent; + scoped_mpz X_YQ_sig(m_mpz_manager); + mpf_exp_t exp_delta = exp(x) - YQ_exp; + TRACE("mpf_dbg_rem", tout << "exp_delta=" << exp_delta << std::endl;); + SASSERT(INT_MIN < exp_delta && exp_delta <= INT_MAX); + scoped_mpz minuend(m_mpz_manager), subtrahend(m_mpz_manager); + + scoped_mpz x_sig_lrg(m_mpz_manager); + m_mpz_manager.mul2k(x.significand, sbits-1, x_sig_lrg); // sbits-1 extra bits into x + + m_mpz_manager.set(minuend, x_sig_lrg); + m_mpz_manager.set(subtrahend, YQ_sig); + + SASSERT(m_mpz_manager.lt(minuend, m_powers2(2*sbits-1))); + SASSERT(m_mpz_manager.ge(minuend, m_powers2(2*sbits-2))); + SASSERT(m_mpz_manager.lt(subtrahend, m_powers2(2*sbits-1))); + SASSERT(m_mpz_manager.ge(subtrahend, m_powers2(2*sbits-2))); + + if (exp_delta != 0) { + scoped_mpz sticky_rem(m_mpz_manager); + m_mpz_manager.set(sticky_rem, 0); + if (exp_delta > sbits+5) + sticky_rem.swap(subtrahend); + else if (exp_delta > 0) + m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem); + else { + SASSERT(exp_delta < 0); + exp_delta = -exp_delta; + m_mpz_manager.mul2k(subtrahend, (int)exp_delta); + } + if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(subtrahend)) + m_mpz_manager.inc(subtrahend); + TRACE("mpf_dbg_rem", tout << "aligned subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;); + } + + m_mpz_manager.sub(minuend, subtrahend, X_YQ_sig); + TRACE("mpf_dbg_rem", tout << "X_YQ_sig'=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;); + + bool neg = m_mpz_manager.is_neg(X_YQ_sig); + if (neg) m_mpz_manager.neg(X_YQ_sig); + bool X_YQ_sgn = ((!x.sign && !YQ_sgn && neg) || + (x.sign && YQ_sgn && !neg) || + (x.sign && !YQ_sgn)); + + // 5. Rounding + if (m_mpz_manager.is_zero(X_YQ_sig)) + mk_zero(ebits, sbits, x.sign, x); + else { + renormalize(ebits, 2*sbits-1, X_YQ_exp, X_YQ_sig); + + TRACE("mpf_dbg_rem", tout << "minuend=" << m_mpz_manager.to_string(minuend) << std::endl; + tout << "subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl; + tout << "X_YQ_sgn=" << X_YQ_sgn << std::endl; + tout << "X_YQ_exp=" << X_YQ_exp << std::endl; + tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl; + tout << "X-YQ=" << to_string_hexfloat(X_YQ_sgn, X_YQ_exp, X_YQ_sig, ebits, sbits, sbits-1) << std::endl;); + + // `sbits-1' extra bits in X_YQ_sig + SASSERT(m_mpz_manager.lt(X_YQ_sig, m_powers2(2*sbits-1))); + scoped_mpz rnd_bits(m_mpz_manager); + m_mpz_manager.machine_div_rem(X_YQ_sig, m_powers2(sbits-1), X_YQ_sig, rnd_bits); + TRACE("mpf_dbg_rem", tout << "final sticky=" << m_mpz_manager.to_string(rnd_bits) << std::endl; ); + + // Round to nearest, ties to even. + if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie. + if (m_mpz_manager.is_odd(X_YQ_sig)) { + m_mpz_manager.inc(X_YQ_sig); + } + } + else if (m_mpz_manager.gt(rnd_bits, mpz(32))) + m_mpz_manager.inc(X_YQ_sig); + + set(x, ebits, sbits, X_YQ_sgn, X_YQ_exp, X_YQ_sig); + } + + TRACE("mpf_dbg_rem", tout << "partial remainder = " << to_string_hexfloat(x) << std::endl;); +} + void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { SASSERT(x.sbits == y.sbits && x.ebits == y.ebits); - TRACE("mpf_dbg", tout << "X = " << to_string(x) << std::endl;); - TRACE("mpf_dbg", tout << "Y = " << to_string(y) << std::endl;); + TRACE("mpf_dbg_rem", tout << "X = " << to_string(x) << "=" << to_string_hexfloat(x) << std::endl; + tout << "Y = " << to_string(y) << "=" << to_string_hexfloat(y) << std::endl;); if (is_nan(x) || is_nan(y)) mk_nan(x.ebits, x.sbits, o); @@ -1231,58 +1414,35 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { else if (is_zero(x)) set(o, x); else { - // This is a generalized version of the algorithm for FPREM1 in the Intel + SASSERT(is_regular(x) && is_regular(y)); + + // This is a generalized version of the algorithm for FPREM1 in the `Intel // 64 and IA-32 Architectures Software Developer's Manual', - // Section 3-402 Vol. 2A FPREM1-Partial Remainder'. + // Section 3-402 Vol. 2A `FPREM1-Partial Remainder'. scoped_mpf ST0(*this), ST1(*this); set(ST0, x); set(ST1, y); + unpack(ST0, true); + unpack(ST1, true); - const mpf_exp_t B = x.sbits-1; // max bits per iteration. + const mpf_exp_t B = x.sbits; mpf_exp_t D; do { - D = ST0.exponent() - ST1.exponent(); - TRACE("mpf_dbg_rem", tout << "st0=" << to_string_hexfloat(ST0) << std::endl; - tout << "st1=" << to_string_hexfloat(ST1) << std::endl; - tout << "D=" << D << std::endl;); - - if (D < B) { - scoped_mpf ST0_DIV_ST1(*this), Q(*this), ST1_MUL_Q(*this), ST0p(*this); - div(MPF_ROUND_NEAREST_TEVEN, ST0, ST1, ST0_DIV_ST1); - round_to_integral(MPF_ROUND_NEAREST_TEVEN, ST0_DIV_ST1, Q); - mul(MPF_ROUND_NEAREST_TEVEN, ST1, Q, ST1_MUL_Q); - sub(MPF_ROUND_NEAREST_TEVEN, ST0, ST1_MUL_Q, ST0p); - TRACE("mpf_dbg_rem", tout << "ST0/ST1=" << to_string_hexfloat(ST0_DIV_ST1) << std::endl; - tout << "Q=" << to_string_hexfloat(Q) << std::endl; - tout << "ST1*Q=" << to_string_hexfloat(ST1_MUL_Q) << std::endl; - tout << "ST0'=" << to_string_hexfloat(ST0p) << std::endl;); - set(ST0, ST0p); + if (ST0.exponent() < ST1.exponent() - 1) { + D = 0; } else { - const mpf_exp_t N = B; - scoped_mpf ST0_DIV_ST1(*this), QQ(*this), ST1_MUL_QQ(*this), ST0p(*this); - div(MPF_ROUND_TOWARD_ZERO, ST0, ST1, ST0_DIV_ST1); - ST0_DIV_ST1.get().exponent -= D - N; - round_to_integral(MPF_ROUND_TOWARD_ZERO, ST0_DIV_ST1, QQ); - mul(MPF_ROUND_NEAREST_TEVEN, ST1, QQ, ST1_MUL_QQ); - ST1_MUL_QQ.get().exponent += D - N; - sub(MPF_ROUND_NEAREST_TEVEN, ST0, ST1_MUL_QQ, ST0p); - TRACE("mpf_dbg_rem", tout << "ST0/ST1/2^{D-N}=" << to_string_hexfloat(ST0_DIV_ST1) << std::endl; - tout << "QQ=" << to_string_hexfloat(QQ) << std::endl; - tout << "ST1*QQ*2^{D-N}=" << to_string_hexfloat(ST1_MUL_QQ) << std::endl; - tout << "ST0'=" << to_string_hexfloat(ST0p) << std::endl;); - SASSERT(!eq(ST0, ST0p)); - set(ST0, ST0p); + D = ST0.exponent() - ST1.exponent(); + partial_remainder(ST0.get(), ST1.get(), D, (D >= B)); } + } while (D >= B && !ST0.is_zero()); - SASSERT(ST0.exponent() - ST1.exponent() <= D); - } while (D >= B); - - set(o, ST0); - if (is_zero(o)) - o.sign = x.sign; + m_mpz_manager.mul2k(ST0.significand(), 3); + set(o, x.ebits, x.sbits, MPF_ROUND_TOWARD_ZERO, ST0); + round(MPF_ROUND_NEAREST_TEVEN, o); } + TRACE("mpf_dbg_rem", tout << "R = " << to_string(o) << "=" << to_string_hexfloat(o) << std::endl; ); TRACE("mpf_dbg", tout << "REMAINDER = " << to_string(o) << std::endl;); } @@ -1365,7 +1525,7 @@ std::string mpf_manager::to_string(mpf const & x) { } //DEBUG_CODE( - // res += " " + to_string_hexfloat(x); + // res += " " + to_string_raw(x); //); return res; @@ -1407,6 +1567,19 @@ std::string mpf_manager::to_string_raw(mpf const & x) { return res; } +std::string mpf_manager::to_string_hexfloat(bool sgn, mpf_exp_t exp, scoped_mpz const & sig, unsigned ebits, unsigned sbits, unsigned rbits) { + scoped_mpf q(*this); + scoped_mpz q_sig(m_mpz_manager); + m_mpz_manager.set(q_sig, sig); + if (rbits != 0) m_mpz_manager.div(q_sig, m_powers2(rbits), q_sig); // restore scale + if (m_mpz_manager.ge(q_sig, m_powers2(sbits-1))) + m_mpz_manager.sub(q_sig, m_powers2(sbits-1), q_sig); // strip hidden bit + else if (exp == mk_min_exp(ebits)) + exp = mk_bot_exp(ebits); + set(q, ebits, sbits, sgn, exp, q_sig); + return to_string(q.get()); +} + std::string mpf_manager::to_string_hexfloat(mpf const & x) { std::stringstream ss(""); std::ios::fmtflags ff = ss.setf(std::ios_base::hex | std::ios_base::uppercase | diff --git a/src/util/mpf.h b/src/util/mpf.h index 1bd0ac952..31523c3ed 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -185,9 +185,6 @@ public: void mk_pinf(unsigned ebits, unsigned sbits, mpf & o); void mk_ninf(unsigned ebits, unsigned sbits, mpf & o); - std::string to_string_raw(mpf const & a); - std::string to_string_hexfloat(mpf const & a); - unsynch_mpz_manager & mpz_manager(void) { return m_mpz_manager; } unsynch_mpq_manager & mpq_manager(void) { return m_mpq_manager; } @@ -226,6 +223,9 @@ protected: void round(mpf_rounding_mode rm, mpf & o); void round_sqrt(mpf_rounding_mode rm, mpf & o); + void renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig); + void partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial); + void mk_round_inf(mpf_rounding_mode rm, mpf & o); // Convert x into a mpz numeral. zm is the manager that owns o. @@ -284,6 +284,9 @@ protected: } }; + std::string to_string_raw(mpf const & a); + std::string to_string_hexfloat(mpf const & a); + std::string to_string_hexfloat(bool sgn, mpf_exp_t exp, scoped_mpz const & sig, unsigned ebits, unsigned sbits, unsigned rbits); public: powers2 m_powers2; }; @@ -291,6 +294,7 @@ public: class scoped_mpf : public _scoped_numeral { friend class mpf_manager; mpz & significand() { return get().significand; } + const mpz & significand() const { return get().significand; } bool sign() const { return get().sign; } mpf_exp_t exponent() const { return get().exponent; } unsigned sbits() const { return get().sbits; }