mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
063b6e9ea5
9 changed files with 139 additions and 103 deletions
|
|
@ -2021,8 +2021,8 @@ public:
|
|||
app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); }
|
||||
app * mk_distinct(unsigned num_args, expr * const * args);
|
||||
app * mk_distinct_expanded(unsigned num_args, expr * const * args);
|
||||
app * mk_true() { return m_true; }
|
||||
app * mk_false() { return m_false; }
|
||||
app * mk_true() const { return m_true; }
|
||||
app * mk_false() const { return m_false; }
|
||||
app * mk_bool_val(bool b) { return b?m_true:m_false; }
|
||||
app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
|
||||
|
||||
|
|
|
|||
|
|
@ -1535,11 +1535,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
// Extend c
|
||||
expr_ref c_sig_ext(m);
|
||||
c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits - 1)));
|
||||
c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits+2)));
|
||||
c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext);
|
||||
mul_sig = m_bv_util.mk_concat(mul_sig, m_bv_util.mk_numeral(0, 3));
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2 * sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits+3);
|
||||
SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2*sbits+3);
|
||||
dbg_decouple("fpa2bv_fma_c_sig_ext", c_sig_ext);
|
||||
dbg_decouple("fpa2bv_fma_c_exp_ext", c_exp_ext);
|
||||
|
||||
|
|
@ -1550,10 +1551,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m);
|
||||
m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn);
|
||||
m_simp.mk_ite(swap_cond, c_sig_ext, mul_sig, e_sig); // has 2 * sbits
|
||||
m_simp.mk_ite(swap_cond, c_sig_ext, mul_sig, e_sig); // has 2 * sbits + 3
|
||||
m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2
|
||||
m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn);
|
||||
m_simp.mk_ite(swap_cond, mul_sig, c_sig_ext, f_sig); // has 2 * sbits
|
||||
m_simp.mk_ite(swap_cond, mul_sig, c_sig_ext, f_sig); // has 2 * sbits + 3
|
||||
m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2
|
||||
|
||||
SASSERT(is_well_sorted(m, e_sgn));
|
||||
|
|
@ -1563,8 +1564,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
SASSERT(is_well_sorted(m, f_sig));
|
||||
SASSERT(is_well_sorted(m, f_exp));
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+3);
|
||||
SASSERT(m_bv_util.get_bv_size(f_sig) == 2*sbits+3);
|
||||
SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2);
|
||||
|
||||
|
|
@ -1581,7 +1582,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
// cap the delta
|
||||
expr_ref cap(m), cap_le_delta(m);
|
||||
cap = m_bv_util.mk_numeral(2*sbits, ebits+2);
|
||||
cap = m_bv_util.mk_numeral(2*sbits+3, ebits+2);
|
||||
cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
|
||||
m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
|
||||
SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2);
|
||||
|
|
@ -1593,14 +1594,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
expr_ref alignment_sticky_raw(m), alignment_sticky(m);
|
||||
shifted_big = m_bv_util.mk_bv_lshr(
|
||||
m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)),
|
||||
m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta));
|
||||
shifted_f_sig = m_bv_util.mk_extract(3*sbits-1, sbits, shifted_big);
|
||||
m_bv_util.mk_zero_extend((3*sbits+3)-(ebits+2), exp_delta));
|
||||
shifted_f_sig = m_bv_util.mk_extract(3*sbits+2, sbits, shifted_big);
|
||||
alignment_sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big);
|
||||
alignment_sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, alignment_sticky_raw.get());
|
||||
dbg_decouple("fpa2bv_fma_shifted_f_sig", shifted_f_sig);
|
||||
dbg_decouple("fpa2bv_fma_f_sig_alignment_sticky", alignment_sticky);
|
||||
SASSERT(is_well_sorted(m, alignment_sticky));
|
||||
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+3);
|
||||
SASSERT(is_well_sorted(m, shifted_f_sig));
|
||||
|
||||
// Significant addition.
|
||||
|
|
@ -1612,14 +1613,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
m_simp.mk_eq(e_sgn, f_sgn, eq_sgn);
|
||||
dbg_decouple("fpa2bv_fma_eq_sgn", eq_sgn);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+5);
|
||||
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+5);
|
||||
|
||||
dbg_decouple("fpa2bv_fma_add_e_sig", e_sig);
|
||||
dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig);
|
||||
|
||||
expr_ref sum(m), e_plus_f(m), e_minus_f(m), sticky_wide(m);
|
||||
sticky_wide = m_bv_util.mk_zero_extend(2*sbits+1, alignment_sticky);
|
||||
sticky_wide = m_bv_util.mk_zero_extend(2*sbits+4, alignment_sticky);
|
||||
e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig);
|
||||
e_plus_f = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(0, 0, e_plus_f), zero_1),
|
||||
m_bv_util.mk_bv_add(e_plus_f, sticky_wide),
|
||||
|
|
@ -1632,12 +1633,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
dbg_decouple("fpa2bv_fma_f_sig_or_sticky", shifted_f_sig);
|
||||
|
||||
m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum);
|
||||
SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits+5);
|
||||
SASSERT(is_well_sorted(m, sum));
|
||||
dbg_decouple("fpa2bv_fma_add_sum", sum);
|
||||
|
||||
expr_ref sign_bv(m), n_sum(m);
|
||||
sign_bv = m_bv_util.mk_extract(2*sbits+1, 2*sbits+1, sum);
|
||||
sign_bv = m_bv_util.mk_extract(2*sbits+4, 2*sbits+4, sum);
|
||||
n_sum = m_bv_util.mk_bv_neg(sum);
|
||||
dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv);
|
||||
dbg_decouple("fpa2bv_fma_add_n_sum", n_sum);
|
||||
|
|
@ -1661,14 +1662,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
dbg_decouple("fpa2bv_fma_res_sgn", res_sgn);
|
||||
|
||||
expr_ref is_sig_neg(m);
|
||||
is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits + 1, sig_abs));
|
||||
is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2*sbits+4, 2*sbits+4, sig_abs));
|
||||
sig_abs = m.mk_ite(is_sig_neg, m_bv_util.mk_bv_neg(sig_abs), sig_abs);
|
||||
dbg_decouple("fpa2bv_fma_is_sig_neg", is_sig_neg);
|
||||
|
||||
// Result could have overflown into 4.xxx.
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs) == 2 * sbits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+4);
|
||||
expr_ref extra(m), extra_is_zero(m);
|
||||
extra = m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs);
|
||||
extra = m_bv_util.mk_extract(2*sbits+4, 2*sbits+3, sig_abs);
|
||||
extra_is_zero = m.mk_eq(extra, m_bv_util.mk_numeral(0, 2));
|
||||
dbg_decouple("fpa2bv_fma_extra", extra);
|
||||
|
||||
|
|
@ -1685,7 +1686,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
sig_lz_capped = m.mk_ite(m_bv_util.mk_sle(sig_lz, max_exp_delta), sig_lz, max_exp_delta);
|
||||
renorm_delta = m.mk_ite(m_bv_util.mk_sle(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
|
||||
res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta);
|
||||
sig_abs = m_bv_util.mk_bv_shl(sig_abs, m_bv_util.mk_zero_extend(2*sbits-ebits, renorm_delta));
|
||||
sig_abs = m_bv_util.mk_bv_shl(sig_abs, m_bv_util.mk_zero_extend(2*sbits+3-ebits, renorm_delta));
|
||||
dbg_decouple("fpa2bv_fma_min_exp", min_exp);
|
||||
dbg_decouple("fpa2bv_fma_max_exp_delta", max_exp_delta);
|
||||
dbg_decouple("fpa2bv_fma_sig_lz", sig_lz);
|
||||
|
|
@ -1699,30 +1700,30 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
}
|
||||
|
||||
expr_ref sig_abs_h1(m), sticky_h1(m), sticky_h1_red(m), sig_abs_h1_f(m), res_sig_1(m);
|
||||
sticky_h1 = m_bv_util.mk_extract(sbits - 5 + too_short, 0, sig_abs);
|
||||
sig_abs_h1 = m_bv_util.mk_extract(2 * sbits + 1 + too_short, sbits - 4 + too_short, sig_abs);
|
||||
sticky_h1_red = m_bv_util.mk_zero_extend(sbits + 5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get()));
|
||||
sticky_h1 = m_bv_util.mk_extract(sbits+too_short-2, 0, sig_abs);
|
||||
sig_abs_h1 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits-1+too_short, sig_abs);
|
||||
sticky_h1_red = m_bv_util.mk_zero_extend(sbits+5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get()));
|
||||
expr * sticky_h1_red_args[2] = { sig_abs_h1, sticky_h1_red };
|
||||
sig_abs_h1_f = m_bv_util.mk_bv_or(2, sticky_h1_red_args);
|
||||
res_sig_1 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h1_f);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits - 4 + too_short);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits + 6);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits + 6);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits + 6);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits + 4);
|
||||
res_sig_1 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h1_f);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits+too_short-1);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits+6);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits+6);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits+6);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits+4);
|
||||
|
||||
expr_ref sig_abs_h2(m), sticky_h2(m), sticky_h2_red(m), sig_abs_h2_f(m), res_sig_2(m);
|
||||
sticky_h2 = m_bv_util.mk_extract(sbits - 4 + too_short, 0, sig_abs);
|
||||
sig_abs_h2 = m_bv_util.mk_extract(2 * sbits + 1 + too_short, sbits - 3 + too_short, sig_abs);
|
||||
sticky_h2_red = m_bv_util.mk_zero_extend(sbits + 4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get()));
|
||||
sticky_h2 = m_bv_util.mk_extract(sbits+too_short-1, 0, sig_abs);
|
||||
sig_abs_h2 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits+too_short, sig_abs);
|
||||
sticky_h2_red = m_bv_util.mk_zero_extend(sbits+4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get()));
|
||||
expr * sticky_h2_red_args[2] = { sig_abs_h2, sticky_h2_red };
|
||||
sig_abs_h2_f = m_bv_util.mk_zero_extend(1, m_bv_util.mk_bv_or(2, sticky_h2_red_args));
|
||||
res_sig_2 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h2_f);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits - 3 + too_short);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits + 5);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits + 5);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits + 6);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig_2) == sbits + 4);
|
||||
res_sig_2 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h2_f);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits+too_short);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits+5);
|
||||
SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits+5);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits+6);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig_2) == sbits+4);
|
||||
|
||||
res_sig = m.mk_ite(extra_is_zero, res_sig_1, res_sig_2);
|
||||
|
||||
|
|
@ -2713,12 +2714,12 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
|
|||
SASSERT(m_util.is_bv2rm(args[0]));
|
||||
expr * bv_rm = to_app(args[0])->get_arg(0);
|
||||
|
||||
rational e;
|
||||
if (!m_arith_util.is_numeral(args[1], e))
|
||||
rational q;
|
||||
if (!m_arith_util.is_numeral(args[1], q))
|
||||
UNREACHABLE();
|
||||
|
||||
rational q;
|
||||
if (!m_arith_util.is_numeral(args[2], q))
|
||||
rational e;
|
||||
if (!m_arith_util.is_numeral(args[2], e))
|
||||
UNREACHABLE();
|
||||
|
||||
SASSERT(e.is_int64());
|
||||
|
|
|
|||
|
|
@ -1299,7 +1299,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
|
|||
is_pos = !is_pos;
|
||||
}
|
||||
if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) {
|
||||
IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << "Not arith literal: " << mk_pp(lit, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
SASSERT(lit->get_num_args() == 2);
|
||||
|
|
@ -1363,7 +1363,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
|
|||
rw(sum);
|
||||
}
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << "coeff,lit,sum " << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
|
||||
#endif
|
||||
|
||||
return true;
|
||||
|
|
|
|||
|
|
@ -41,9 +41,9 @@ public:
|
|||
m_rewriter(m)
|
||||
{}
|
||||
|
||||
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
|
||||
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
|
||||
quantifier_type qt = Q_none_pos;
|
||||
pull_quantifier(fml, qt, vars, result);
|
||||
pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(fml, m) << "\n";
|
||||
tout << mk_pp(result, m) << "\n";);
|
||||
|
|
@ -51,36 +51,38 @@ public:
|
|||
is_fa = (Q_forall_pos == qt);
|
||||
}
|
||||
|
||||
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
|
||||
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
|
||||
quantifier_type qt = Q_exists_pos;
|
||||
pull_quantifier(fml, qt, vars, result);
|
||||
pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(fml, m) << "\n";
|
||||
tout << mk_pp(result, m) << "\n";);
|
||||
}
|
||||
|
||||
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
|
||||
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
|
||||
quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos;
|
||||
expr_ref result(m);
|
||||
pull_quantifier(fml, qt, vars, result);
|
||||
pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(fml, m) << "\n";
|
||||
tout << mk_pp(result, m) << "\n";);
|
||||
fml = result;
|
||||
}
|
||||
|
||||
void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result) {
|
||||
void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) {
|
||||
unsigned nd = q->get_num_decls();
|
||||
for (unsigned i = 0; i < nd; ++i) {
|
||||
sort* s = q->get_decl_sort(i);
|
||||
app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s);
|
||||
symbol const& sym = q->get_decl_name (i);
|
||||
app* a = use_fresh ? m.mk_fresh_const(sym.str ().c_str (), s)
|
||||
: m.mk_const (sym, s);
|
||||
vars.push_back(a);
|
||||
}
|
||||
expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
|
||||
instantiate(m, q, exprs, result);
|
||||
}
|
||||
|
||||
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
|
||||
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
|
||||
unsigned index = var_counter().get_next_var(fml);
|
||||
while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
|
||||
quantifier* q = to_quantifier(fml);
|
||||
|
|
@ -97,7 +99,7 @@ public:
|
|||
return index;
|
||||
}
|
||||
app_ref_vector vars(m);
|
||||
pull_quantifier(is_forall, fml, vars);
|
||||
pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
|
||||
if (vars.empty()) {
|
||||
return index;
|
||||
}
|
||||
|
|
@ -192,7 +194,7 @@ private:
|
|||
}
|
||||
|
||||
|
||||
void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
|
||||
void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
|
||||
|
||||
if (!has_quantifiers(fml)) {
|
||||
result = fml;
|
||||
|
|
@ -209,38 +211,48 @@ private:
|
|||
if (m.is_and(fml)) {
|
||||
num_args = a->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
pull_quantifier(a->get_arg(i), qt, vars, tmp);
|
||||
pull_quantifier(a->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
|
||||
args.push_back(tmp);
|
||||
}
|
||||
if (rewrite_ok) {
|
||||
m_rewriter.mk_and(args.size(), args.c_ptr(), result);
|
||||
}
|
||||
else {
|
||||
result = m.mk_and (args.size (), args.c_ptr ());
|
||||
}
|
||||
}
|
||||
else if (m.is_or(fml)) {
|
||||
num_args = to_app(fml)->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp);
|
||||
pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
|
||||
args.push_back(tmp);
|
||||
}
|
||||
if (rewrite_ok) {
|
||||
m_rewriter.mk_or(args.size(), args.c_ptr(), result);
|
||||
}
|
||||
else {
|
||||
result = m.mk_or (args.size (), args.c_ptr ());
|
||||
}
|
||||
}
|
||||
else if (m.is_not(fml)) {
|
||||
pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
|
||||
pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp, use_fresh, rewrite_ok);
|
||||
negate(qt);
|
||||
result = m.mk_not(tmp);
|
||||
}
|
||||
else if (m.is_implies(fml, t1, t2)) {
|
||||
pull_quantifier(t1, negate(qt), vars, tmp);
|
||||
pull_quantifier(t1, negate(qt), vars, tmp, use_fresh, rewrite_ok);
|
||||
negate(qt);
|
||||
pull_quantifier(t2, qt, vars, result);
|
||||
pull_quantifier(t2, qt, vars, result, use_fresh, rewrite_ok);
|
||||
result = m.mk_implies(tmp, result);
|
||||
}
|
||||
else if (m.is_ite(fml, t1, t2, t3)) {
|
||||
expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m);
|
||||
pull_quantifier(t2, qt, vars, tt2);
|
||||
pull_quantifier(t3, qt, vars, tt3);
|
||||
pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
|
||||
pull_quantifier(t3, qt, vars, tt3, use_fresh, rewrite_ok);
|
||||
if (has_quantifiers(t1)) {
|
||||
pull_quantifier(t1, qt, vars, tt1);
|
||||
pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
|
||||
nt1 = m.mk_not(t1);
|
||||
pull_quantifier(nt1, qt, vars, ntt1);
|
||||
pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
|
||||
result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
|
||||
}
|
||||
else {
|
||||
|
|
@ -249,12 +261,12 @@ private:
|
|||
}
|
||||
else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) {
|
||||
expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m);
|
||||
pull_quantifier(t1, qt, vars, tt1);
|
||||
pull_quantifier(t2, qt, vars, tt2);
|
||||
pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
|
||||
pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
|
||||
nt1 = m.mk_not(t1);
|
||||
nt2 = m.mk_not(t2);
|
||||
pull_quantifier(nt1, qt, vars, ntt1);
|
||||
pull_quantifier(nt2, qt, vars, ntt2);
|
||||
pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
|
||||
pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok);
|
||||
result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
|
||||
}
|
||||
else {
|
||||
|
|
@ -271,8 +283,8 @@ private:
|
|||
break;
|
||||
}
|
||||
set_quantifier_type(qt, q->is_forall());
|
||||
extract_quantifier(q, vars, tmp);
|
||||
pull_quantifier(tmp, qt, vars, result);
|
||||
extract_quantifier(q, vars, tmp, use_fresh);
|
||||
pull_quantifier(tmp, qt, vars, result, use_fresh, rewrite_ok);
|
||||
break;
|
||||
}
|
||||
case AST_VAR:
|
||||
|
|
@ -295,18 +307,18 @@ quantifier_hoister::~quantifier_hoister() {
|
|||
dealloc(m_impl);
|
||||
}
|
||||
|
||||
void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
|
||||
(*m_impl)(fml, vars, is_fa, result);
|
||||
void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
|
||||
(*m_impl)(fml, vars, is_fa, result, use_fresh, rewrite_ok);
|
||||
}
|
||||
|
||||
void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
|
||||
m_impl->pull_exists(fml, vars, result);
|
||||
void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
|
||||
m_impl->pull_exists(fml, vars, result, use_fresh, rewrite_ok);
|
||||
}
|
||||
|
||||
void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
|
||||
m_impl->pull_quantifier(is_forall, fml, vars);
|
||||
void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
|
||||
m_impl->pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
|
||||
}
|
||||
|
||||
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
|
||||
return m_impl->pull_quantifier(is_forall, fml, sorts, names);
|
||||
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
|
||||
return m_impl->pull_quantifier(is_forall, fml, sorts, names, use_fresh, rewrite_ok);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -43,14 +43,14 @@ public:
|
|||
or, and, implies, ite (then and else branch only).
|
||||
*/
|
||||
|
||||
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result);
|
||||
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
|
||||
|
||||
/**
|
||||
\brief Pull top-most existential quantifier up.
|
||||
|
||||
The list of variables is empty if there are no top-level existential quantifier.
|
||||
*/
|
||||
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result);
|
||||
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
|
||||
|
||||
|
||||
/**
|
||||
|
|
@ -58,7 +58,7 @@ public:
|
|||
|
||||
The list of variables is empty if there are no top-level universal/existential quantifier.
|
||||
*/
|
||||
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars);
|
||||
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true);
|
||||
|
||||
/**
|
||||
\brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up.
|
||||
|
|
@ -66,7 +66,7 @@ public:
|
|||
Return index of maximal variable.
|
||||
*/
|
||||
|
||||
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names);
|
||||
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh = true, bool rewrite_ok = true);
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -2342,6 +2342,7 @@ private:
|
|||
elim_star m_elim_star;
|
||||
th_rewriter m_rewriter;
|
||||
|
||||
bool m_use_array_der;
|
||||
bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
|
||||
index = fmls.size();
|
||||
if (index <= 1) {
|
||||
|
|
@ -2359,13 +2360,14 @@ private:
|
|||
}
|
||||
|
||||
public:
|
||||
impl(ast_manager & m, params_ref const & p):
|
||||
impl(ast_manager & m, params_ref const & p, bool use_array_der):
|
||||
m(m),
|
||||
m_der(m, p),
|
||||
m_fm(m),
|
||||
m_array_der(m),
|
||||
m_elim_star(*this),
|
||||
m_rewriter(m) {}
|
||||
m_rewriter(m),
|
||||
m_use_array_der(use_array_der) {}
|
||||
|
||||
void operator()(app_ref_vector& vars, expr_ref& fml) {
|
||||
if (vars.empty()) {
|
||||
|
|
@ -2445,14 +2447,15 @@ public:
|
|||
m_array_der.set_is_variable_proc(is_var);
|
||||
m_der(fmls);
|
||||
m_fm(fmls);
|
||||
m_array_der(fmls);
|
||||
// AG: disalble m_array_der() since it interferes with other array handling
|
||||
if (m_use_array_der) m_array_der(fmls);
|
||||
TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
qe_lite::qe_lite(ast_manager & m, params_ref const & p) {
|
||||
m_impl = alloc(impl, m, p);
|
||||
qe_lite::qe_lite(ast_manager & m, params_ref const & p, bool use_array_der) {
|
||||
m_impl = alloc(impl, m, p, use_array_der);
|
||||
}
|
||||
|
||||
qe_lite::~qe_lite() {
|
||||
|
|
@ -2484,7 +2487,7 @@ class qe_lite_tactic : public tactic {
|
|||
|
||||
imp(ast_manager& m, params_ref const & p):
|
||||
m(m),
|
||||
m_qe(m, p)
|
||||
m_qe(m, p, true)
|
||||
{}
|
||||
|
||||
void checkpoint() {
|
||||
|
|
|
|||
|
|
@ -31,7 +31,10 @@ class qe_lite {
|
|||
class impl;
|
||||
impl * m_impl;
|
||||
public:
|
||||
qe_lite(ast_manager & m, params_ref const & p);
|
||||
/**
|
||||
use_array_der controls whether equalities over array reads are simplified
|
||||
*/
|
||||
qe_lite(ast_manager& m, params_ref const & p, bool use_array_der = true);
|
||||
|
||||
~qe_lite();
|
||||
|
||||
|
|
|
|||
|
|
@ -840,16 +840,19 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
SASSERT(m_mpz_manager.lt(mr.significand(), m_powers2(2*x.sbits)));
|
||||
SASSERT(m_mpz_manager.ge(mr.significand(), m_powers2(2*x.sbits - 2)));
|
||||
|
||||
// Introduce extra bits into c in _[0].[sbits-1] s.t. c in _[0].[2*sbits-2]
|
||||
c.set(x.ebits+2, 2*x.sbits-1, c.sign(), c.exponent(), c.significand());
|
||||
m_mpz_manager.mul2k(c.significand(), x.sbits - 1);
|
||||
// Introduce (sbits+3) extra bits into c in _[0].[sbits-1] s.t. c in _[0].[2*sbits-2]
|
||||
c.set(x.ebits+2, 2*x.sbits-1+3, c.sign(), c.exponent(), c.significand());
|
||||
m_mpz_manager.mul2k(c.significand(), x.sbits - 1 + 3);
|
||||
// And + 3 bits into mr as well.
|
||||
mr.set(x.ebits + 2, 2 * x.sbits - 1 + 3, mr.sign(), mr.exponent(), mr.significand());
|
||||
m_mpz_manager.mul2k(mr.significand(), 3);
|
||||
|
||||
TRACE("mpf_dbg", tout << "C_= " << to_string(c) << std::endl;
|
||||
tout << "C_= " << to_string_binary(c, 1, 0) << std::endl;);
|
||||
|
||||
SASSERT(m_mpz_manager.lt(c.significand(), m_powers2(2*x.sbits)));
|
||||
SASSERT(m_mpz_manager.lt(c.significand(), m_powers2(2*x.sbits + 3)));
|
||||
SASSERT(m_mpz_manager.is_zero(c.significand()) ||
|
||||
m_mpz_manager.ge(c.significand(), m_powers2(2*x.sbits - 2)));
|
||||
m_mpz_manager.ge(c.significand(), m_powers2(2*x.sbits - 2 + 3)));
|
||||
|
||||
if (exp(c) > exp(mr)) {
|
||||
TRACE("mpf_dbg", tout << "Swap!" << std::endl;);
|
||||
|
|
@ -860,8 +863,8 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
mpf_exp_t exp_delta_w = exp(mr) - exp(c);
|
||||
SASSERT(exp(mr) >= exp(c) && exp_delta_w >= 0);
|
||||
|
||||
if (exp_delta_w > 2 * x.sbits)
|
||||
exp_delta_w = 2 * x.sbits;
|
||||
if (exp_delta_w > 2 * x.sbits + 3)
|
||||
exp_delta_w = 2 * x.sbits + 3;
|
||||
|
||||
unsigned exp_delta = (unsigned)exp_delta_w;
|
||||
|
||||
|
|
@ -905,8 +908,8 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
// Renormalize
|
||||
bool renorm_sticky = false;
|
||||
|
||||
SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1)));
|
||||
if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits)))
|
||||
SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1 + 3)));
|
||||
if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits + 3)))
|
||||
{
|
||||
SASSERT(exp(res) < mk_max_exp(x.ebits)); // NYI.
|
||||
|
||||
|
|
@ -919,7 +922,7 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
|
||||
mpf_exp_t min_exp = mk_min_exp(x.ebits);
|
||||
unsigned sig_width = m_mpz_manager.prev_power_of_two(res.get().significand) + 1;
|
||||
mpf_exp_t sig_lz = 2 * x.sbits - sig_width;
|
||||
mpf_exp_t sig_lz = 2 * x.sbits + 3 - sig_width;
|
||||
mpf_exp_t max_exp_delta = res.exponent() - min_exp;
|
||||
unsigned renorm_delta = (unsigned) std::max((mpf_exp_t)0, std::min(sig_lz, max_exp_delta));
|
||||
res.get().exponent -= renorm_delta;
|
||||
|
|
@ -930,11 +933,11 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0));
|
||||
|
||||
if (x.sbits >= 4) {
|
||||
m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4), o.significand, sticky_rem);
|
||||
m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem);
|
||||
renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem);
|
||||
}
|
||||
else {
|
||||
m_mpz_manager.mul2k(res.significand(), 4 - x.sbits, o.significand);
|
||||
m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand);
|
||||
}
|
||||
|
||||
if (renorm_sticky && m_mpz_manager.is_even(o.significand))
|
||||
|
|
|
|||
|
|
@ -50,6 +50,7 @@ public:
|
|||
inc_ref();
|
||||
}
|
||||
|
||||
ref (ref && r): m_ptr (r.detach ()) {}
|
||||
~ref() {
|
||||
dec_ref();
|
||||
}
|
||||
|
|
@ -89,6 +90,14 @@ public:
|
|||
return *this;
|
||||
}
|
||||
|
||||
ref & operator=(ref &&r) {
|
||||
if (this != &r) {
|
||||
dec_ref ();
|
||||
m_ptr = r.detach ();
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
void reset() {
|
||||
dec_ref();
|
||||
m_ptr = 0;
|
||||
|
|
@ -107,6 +116,11 @@ public:
|
|||
friend bool operator!=(const ref & r1, const ref & r2) {
|
||||
return r1.m_ptr != r2.m_ptr;
|
||||
}
|
||||
friend void swap (ref &r1, ref &r2) {
|
||||
T* tmp = r1.m_ptr;
|
||||
r1.m_ptr = r2.m_ptr;
|
||||
r2.m_ptr = tmp;
|
||||
}
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue