mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Eliminated unused variables

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-23 13:12:05 +00:00
parent 436a51d8f0
commit 6aa5ec9f77
2 changed files with 2 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/tactic/bv/bvarray2uf_rewriter.cpp
View file

@ -335,43 +335,13 @@ bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
unsigned curr_sz = m_bindings.size();
SASSERT(old_q->get_num_decls() <= curr_sz);
unsigned num_decls = old_q->get_num_decls();
unsigned old_sz = curr_sz - num_decls;
string_buffer<> name_buffer;
ptr_buffer<sort> new_decl_sorts;
sbuffer<symbol> new_decl_names;
for (unsigned i = 0; i < num_decls; i++) {
symbol const & n = old_q->get_decl_name(i);
sort * s = old_q->get_decl_sort(i);
NOT_IMPLEMENTED_YET();
}
result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
m_bindings.shrink(old_sz);
TRACE("bvarray2uf_rw_q", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
" new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
NOT_IMPLEMENTED_YET();
return true;
}
bool bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
if (t->get_idx() >= m_bindings.size())
return false;
expr_ref new_exp(m());
sort * s = t->get_sort();
NOT_IMPLEMENTED_YET();
result = new_exp;
result_pr = 0;
TRACE("bvarray2uf_rw_q", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}

4
src/tactic/bv/elim_small_bv_tactic.cpp
View file

@ -90,10 +90,8 @@ class elim_small_bv_tactic : public tactic {
// (VAR 0) is in the first position of substitution; (VAR num_decls-1) is in the last position.
for (unsigned i = 0; i < max_var_idx_p1; i++) {
sort * s = uv.get(i);
for (unsigned i = 0; i < max_var_idx_p1; i++)
substitution.push_back(0);
}
// (VAR num_decls) ... (VAR num_decls+sz-1); are in positions num_decls .. num_decls+sz-1