mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable
This commit is contained in:
commit
203a62bbdb
|
@ -341,22 +341,22 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
|
|||
}
|
||||
else {
|
||||
SASSERT(u.is_irrational_algebraic_numeral(t));
|
||||
anum const & val = u.to_irrational_algebraic_numeral(t);
|
||||
anum const & val2 = u.to_irrational_algebraic_numeral(t);
|
||||
algebraic_numbers::manager & am = u.am();
|
||||
format * vf;
|
||||
std::ostringstream buffer;
|
||||
bool is_neg = false;
|
||||
if (decimal) {
|
||||
scoped_anum abs_val(am);
|
||||
am.set(abs_val, val);
|
||||
if (am.is_neg(val)) {
|
||||
am.set(abs_val, val2);
|
||||
if (am.is_neg(val2)) {
|
||||
is_neg = true;
|
||||
am.neg(abs_val);
|
||||
}
|
||||
am.display_decimal(buffer, abs_val, decimal_prec);
|
||||
}
|
||||
else {
|
||||
am.display_root_smt2(buffer, val);
|
||||
am.display_root_smt2(buffer, val2);
|
||||
}
|
||||
vf = mk_string(get_manager(), buffer.str().c_str());
|
||||
return is_neg ? mk_neg(vf) : vf;
|
||||
|
|
|
@ -44,12 +44,12 @@ app * mk_list_assoc_app(ast_manager & m, family_id fid, decl_kind k, unsigned nu
|
|||
return mk_list_assoc_app(m, decl, num_args, args);
|
||||
}
|
||||
|
||||
bool is_well_formed_vars(ptr_vector<sort>& bound, expr* e) {
|
||||
bool is_well_formed_vars(ptr_vector<sort>& bound, expr * top) {
|
||||
ptr_vector<expr> todo;
|
||||
ast_mark mark;
|
||||
todo.push_back(e);
|
||||
todo.push_back(top);
|
||||
while (!todo.empty()) {
|
||||
expr* e = todo.back();
|
||||
expr * e = todo.back();
|
||||
todo.pop_back();
|
||||
if (mark.is_marked(e)) {
|
||||
continue;
|
||||
|
|
|
@ -149,10 +149,10 @@ enum status {
|
|||
*/
|
||||
static bool is_recursive_datatype(parameter const * parameters) {
|
||||
unsigned num_types = parameters[0].get_int();
|
||||
unsigned tid = parameters[1].get_int();
|
||||
unsigned top_tid = parameters[1].get_int();
|
||||
buffer<status> already_found(num_types, WHITE);
|
||||
buffer<unsigned> todo;
|
||||
todo.push_back(tid);
|
||||
todo.push_back(top_tid);
|
||||
while (!todo.empty()) {
|
||||
unsigned tid = todo.back();
|
||||
if (already_found[tid] == BLACK) {
|
||||
|
@ -198,11 +198,11 @@ static bool is_recursive_datatype(parameter const * parameters) {
|
|||
*/
|
||||
static sort_size get_datatype_size(parameter const * parameters) {
|
||||
unsigned num_types = parameters[0].get_int();
|
||||
unsigned tid = parameters[1].get_int();
|
||||
unsigned top_tid = parameters[1].get_int();
|
||||
buffer<sort_size> szs(num_types, sort_size());
|
||||
buffer<status> already_found(num_types, WHITE);
|
||||
buffer<unsigned> todo;
|
||||
todo.push_back(tid);
|
||||
todo.push_back(top_tid);
|
||||
while (!todo.empty()) {
|
||||
unsigned tid = todo.back();
|
||||
if (already_found[tid] == BLACK) {
|
||||
|
@ -280,7 +280,7 @@ static sort_size get_datatype_size(parameter const * parameters) {
|
|||
}
|
||||
}
|
||||
}
|
||||
return szs[tid];
|
||||
return szs[top_tid];
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -657,8 +657,8 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const {
|
|||
for (unsigned tid = 0; tid < num_types; tid++) {
|
||||
unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset
|
||||
unsigned num_constructors = parameters[o].get_int();
|
||||
for (unsigned s = 1; s <= num_constructors; s++) {
|
||||
unsigned k_i = parameters[o + s].get_int();
|
||||
for (unsigned si = 1; si <= num_constructors; si++) {
|
||||
unsigned k_i = parameters[o + si].get_int();
|
||||
unsigned num_accessors = parameters[k_i + 2].get_int();
|
||||
unsigned r = 0;
|
||||
for (; r < num_accessors; r++) {
|
||||
|
|
|
@ -367,16 +367,16 @@ struct expr2polynomial::imp {
|
|||
begin_loop:
|
||||
checkpoint();
|
||||
frame & fr = m_frame_stack.back();
|
||||
app * t = fr.m_curr;
|
||||
TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(t, m()) << "\n";);
|
||||
unsigned num_args = t->get_num_args();
|
||||
app * a = fr.m_curr;
|
||||
TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(a, m()) << "\n";);
|
||||
unsigned num_args = a->get_num_args();
|
||||
while (fr.m_idx < num_args) {
|
||||
expr * arg = t->get_arg(fr.m_idx);
|
||||
expr * arg = a->get_arg(fr.m_idx);
|
||||
fr.m_idx++;
|
||||
if (!visit(arg))
|
||||
goto begin_loop;
|
||||
}
|
||||
process_app(t);
|
||||
process_app(a);
|
||||
m_frame_stack.pop_back();
|
||||
}
|
||||
}
|
||||
|
|
|
@ -2219,13 +2219,13 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
|
|||
SASSERT(sz == 3);
|
||||
BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
|
||||
|
||||
mpf_rounding_mode rm;
|
||||
mpf_rounding_mode mrm;
|
||||
switch (bv_rm) {
|
||||
case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
|
||||
case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break;
|
||||
case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break;
|
||||
case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break;
|
||||
case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break;
|
||||
case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break;
|
||||
case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break;
|
||||
case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break;
|
||||
case BV_RM_TO_POSITIVE: mrm = MPF_ROUND_TOWARD_POSITIVE; break;
|
||||
case BV_RM_TO_ZERO: mrm = MPF_ROUND_TOWARD_ZERO; break;
|
||||
default: UNREACHABLE();
|
||||
}
|
||||
|
||||
|
@ -2237,17 +2237,15 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
|
|||
return mk_pzero(f, result);
|
||||
else {
|
||||
scoped_mpf v(m_mpf_manager);
|
||||
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
|
||||
m_util.fm().set(v, ebits, sbits, mrm, q.to_mpq());
|
||||
|
||||
|
||||
|
||||
expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
|
||||
expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
|
||||
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
|
||||
s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
|
||||
sig = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
|
||||
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
|
||||
mk_bias(unbiased_exp, e);
|
||||
mk_bias(unbiased_exp, exp);
|
||||
|
||||
mk_fp(sgn, e, s, result);
|
||||
mk_fp(sgn, exp, sig, result);
|
||||
}
|
||||
}
|
||||
else if (m_util.au().is_numeral(x)) {
|
||||
|
@ -2275,37 +2273,37 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
|
|||
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m);
|
||||
|
||||
expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
|
||||
expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
|
||||
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1);
|
||||
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
|
||||
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
|
||||
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
|
||||
mk_bias(unbiased_exp, e);
|
||||
mk_fp(sgn, e, s, v1);
|
||||
mk_bias(unbiased_exp, exp);
|
||||
mk_fp(sgn, exp, sig, v1);
|
||||
|
||||
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
|
||||
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
|
||||
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
|
||||
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
|
||||
mk_bias(unbiased_exp, e);
|
||||
mk_fp(sgn, e, s, v2);
|
||||
mk_bias(unbiased_exp, exp);
|
||||
mk_fp(sgn, exp, sig, v2);
|
||||
|
||||
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
|
||||
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
|
||||
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
|
||||
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
|
||||
mk_bias(unbiased_exp, e);
|
||||
mk_fp(sgn, e, s, v3);
|
||||
mk_bias(unbiased_exp, exp);
|
||||
mk_fp(sgn, exp, sig, v3);
|
||||
|
||||
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
|
||||
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
|
||||
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
|
||||
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
|
||||
mk_bias(unbiased_exp, e);
|
||||
mk_fp(sgn, e, s, v4);
|
||||
mk_bias(unbiased_exp, exp);
|
||||
mk_fp(sgn, exp, sig, v4);
|
||||
|
||||
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
|
||||
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
|
||||
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
|
||||
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
|
||||
mk_bias(unbiased_exp, e);
|
||||
mk_bias(unbiased_exp, exp);
|
||||
|
||||
mk_fp(sgn, e, s, result);
|
||||
mk_fp(sgn, exp, sig, result);
|
||||
mk_ite(rm_tn, v4, result, result);
|
||||
mk_ite(rm_tp, v3, result, result);
|
||||
mk_ite(rm_nte, v2, result, result);
|
||||
|
@ -3350,7 +3348,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
|
|||
// the maximum shift is `sbits', because after that the mantissa
|
||||
// would be zero anyways. So we can safely cut the shift variable down,
|
||||
// as long as we check the higher bits.
|
||||
expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m);
|
||||
expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m);
|
||||
zero_s = m_bv_util.mk_numeral(0, sbits-1);
|
||||
sbits_s = m_bv_util.mk_numeral(sbits, sbits);
|
||||
sh = m_bv_util.mk_extract(ebits-1, sbits, shift);
|
||||
|
|
|
@ -145,24 +145,24 @@ class func_decl_dependencies::top_sort {
|
|||
return false;
|
||||
m_todo.push_back(f);
|
||||
while (!m_todo.empty()) {
|
||||
func_decl * f = m_todo.back();
|
||||
func_decl * cf = m_todo.back();
|
||||
|
||||
switch (get_color(f)) {
|
||||
switch (get_color(cf)) {
|
||||
case CLOSED:
|
||||
m_todo.pop_back();
|
||||
break;
|
||||
case OPEN:
|
||||
set_color(f, IN_PROGRESS);
|
||||
if (visit_children(f)) {
|
||||
set_color(cf, IN_PROGRESS);
|
||||
if (visit_children(cf)) {
|
||||
SASSERT(m_todo.back() == f);
|
||||
m_todo.pop_back();
|
||||
set_color(f, CLOSED);
|
||||
set_color(cf, CLOSED);
|
||||
}
|
||||
break;
|
||||
case IN_PROGRESS:
|
||||
if (all_children_closed(f)) {
|
||||
SASSERT(m_todo.back() == f);
|
||||
set_color(f, CLOSED);
|
||||
if (all_children_closed(cf)) {
|
||||
SASSERT(m_todo.back() == cf);
|
||||
set_color(cf, CLOSED);
|
||||
} else {
|
||||
m_todo.reset();
|
||||
return true;
|
||||
|
|
|
@ -464,18 +464,18 @@ void bit_blaster_tpl<Cfg>::mk_udiv_urem(unsigned sz, expr * const * a_bits, expr
|
|||
// update p
|
||||
if (i < sz - 1) {
|
||||
for (unsigned j = sz - 1; j > 0; j--) {
|
||||
expr_ref i(m());
|
||||
mk_ite(q, t.get(j-1), p.get(j-1), i);
|
||||
p.set(j, i);
|
||||
expr_ref ie(m());
|
||||
mk_ite(q, t.get(j-1), p.get(j-1), ie);
|
||||
p.set(j, ie);
|
||||
}
|
||||
p.set(0, a_bits[sz - i - 2]);
|
||||
}
|
||||
else {
|
||||
// last step: p contains the remainder
|
||||
for (unsigned j = 0; j < sz; j++) {
|
||||
expr_ref i(m());
|
||||
mk_ite(q, t.get(j), p.get(j), i);
|
||||
p.set(j, i);
|
||||
expr_ref ie(m());
|
||||
mk_ite(q, t.get(j), p.get(j), ie);
|
||||
p.set(j, ie);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -324,7 +324,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
|
|||
}
|
||||
result_stack().push_back(def);
|
||||
TRACE("get_macro", tout << "bindings:\n";
|
||||
for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
|
||||
for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";);
|
||||
begin_scope();
|
||||
m_num_qvars = 0;
|
||||
m_root = def;
|
||||
|
|
|
@ -75,7 +75,7 @@ public:
|
|||
iterator end_shared() const { return m_shared.end(); }
|
||||
void reset();
|
||||
void cleanup();
|
||||
void display(std::ostream & out, ast_manager & m) const;
|
||||
void display(std::ostream & out, ast_manager & mgr) const;
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -34,8 +34,8 @@ struct arith_bounds_tactic : public tactic {
|
|||
bounds_arith_subsumption(in, result);
|
||||
}
|
||||
|
||||
virtual tactic* translate(ast_manager& m) {
|
||||
return alloc(arith_bounds_tactic, m);
|
||||
virtual tactic* translate(ast_manager & mgr) {
|
||||
return alloc(arith_bounds_tactic, mgr);
|
||||
}
|
||||
|
||||
void checkpoint() {
|
||||
|
|
|
@ -709,8 +709,6 @@ public:
|
|||
tactic_ref_vector ts2;
|
||||
goal_ref_vector g_copies;
|
||||
|
||||
ast_manager & m = in->m();
|
||||
|
||||
for (unsigned i = 0; i < r1_size; i++) {
|
||||
ast_manager * new_m = alloc(ast_manager, m, !m.proof_mode());
|
||||
managers.push_back(new_m);
|
||||
|
|
Loading…
Reference in a new issue