mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
2770c8f884
commit
39d1ad3edb
|
@ -111,9 +111,10 @@ namespace api {
|
|||
m_last_obj = 0;
|
||||
u_map<api::object*>::iterator it = m_allocated_objects.begin();
|
||||
while (it != m_allocated_objects.end()) {
|
||||
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", it->m_key, typeid(*it->m_value).name()););
|
||||
api::object* val = it->m_value;
|
||||
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", it->m_key, typeid(*val).name()););
|
||||
m_allocated_objects.remove(it->m_key);
|
||||
dealloc(it->m_value);
|
||||
dealloc(val);
|
||||
it = m_allocated_objects.begin();
|
||||
}
|
||||
}
|
||||
|
|
|
@ -865,8 +865,6 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) {
|
|||
return r;
|
||||
}
|
||||
|
||||
static unsigned r_count = 0;
|
||||
|
||||
psort * pdecl_manager::register_psort(psort * n) {
|
||||
TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";);
|
||||
psort * r = m_table.insert_if_not_there(n);
|
||||
|
|
|
@ -867,7 +867,7 @@ namespace smt2 {
|
|||
throw parser_exception("invalid datatype declaration, too many data-type bodies defined");
|
||||
}
|
||||
symbol dt_name = m_dt_names[i];
|
||||
parse_datatype_dec(new_ct_decls);
|
||||
parse_datatype_dec(nullptr, new_ct_decls);
|
||||
d = pm().mk_pdatatype_decl(m_dt_name2arity.find(dt_name), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr());
|
||||
}
|
||||
else {
|
||||
|
@ -942,7 +942,7 @@ namespace smt2 {
|
|||
|
||||
pdatatype_decl_ref d(pm());
|
||||
pconstructor_decl_ref_buffer new_ct_decls(pm());
|
||||
parse_datatype_dec(new_ct_decls);
|
||||
parse_datatype_dec(&dt_name, new_ct_decls);
|
||||
d = pm().mk_pdatatype_decl(m_sort_id2param_idx.size(), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr());
|
||||
|
||||
check_missing(d, line, pos);
|
||||
|
@ -956,12 +956,16 @@ namespace smt2 {
|
|||
|
||||
// datatype_dec ::= ( constructor_dec+ ) | ( par ( symbol+ ) ( constructor_dec+ ) )
|
||||
|
||||
void parse_datatype_dec(pconstructor_decl_ref_buffer & ct_decls) {
|
||||
void parse_datatype_dec(symbol* dt_name, pconstructor_decl_ref_buffer & ct_decls) {
|
||||
check_lparen_next("invalid datatype declaration, '(' expected");
|
||||
if (curr_id() == m_par) {
|
||||
next();
|
||||
parse_sort_decl_params();
|
||||
check_lparen_next("invalid constructor declaration after par, '(' expected");
|
||||
unsigned sz = m_sort_id2param_idx.size();
|
||||
if (sz > 0 && dt_name) {
|
||||
m_ctx.insert(pm().mk_psort_dt_decl(sz, *dt_name));
|
||||
}
|
||||
parse_constructor_decls(ct_decls);
|
||||
check_rparen_next("invalid datatype declaration, ')' expected");
|
||||
}
|
||||
|
|
|
@ -3661,7 +3661,6 @@ void theory_seq::add_extract_axiom(expr* e) {
|
|||
literal ls_le_i = mk_simplified_literal(m_autil.mk_le(mk_sub(i, ls), zero));
|
||||
literal li_ge_ls = mk_simplified_literal(m_autil.mk_ge(ls_minus_i_l, zero));
|
||||
literal l_ge_zero = mk_simplified_literal(m_autil.mk_ge(l, zero));
|
||||
literal l_le_zero = mk_simplified_literal(m_autil.mk_le(l, zero));
|
||||
literal ls_le_0 = mk_simplified_literal(m_autil.mk_le(ls, zero));
|
||||
|
||||
add_axiom(~i_ge_0, ~ls_le_i, mk_seq_eq(xey, s));
|
||||
|
|
Loading…
Reference in a new issue