mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add comments to elim_unconstrained and remove unused function

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-12 18:01:38 -08:00
parent efbe0a6554
commit 9d09064ad0
2 changed files with 8 additions and 12 deletions

16
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -103,12 +103,6 @@ void elim_unconstrained::eliminate() {
}
}
void elim_unconstrained::add_term(expr* t) {
expr_ref_vector terms(m);
terms.push_back(t);
init_terms(terms);
}
expr* elim_unconstrained::get_parent(unsigned n) const {
for (expr* p : get_node(n).m_parents)
if (get_node(p).m_refcount > 0 && get_node(p).m_term == get_node(p).m_orig)
@ -128,20 +122,23 @@ void elim_unconstrained::init_nodes() {
terms.push_back(m_fmls[i].fml());
m_trail.append(terms);
m_heap.reset();
m_frozen.reset();
// initialize nodes for terms in the original goal
init_terms(terms);
// top-level terms have reference count > 0
for (expr* e : terms)
inc_ref(e);
// freeze subterms before the head.
// freeze subterms before the already processed head
terms.reset();
for (unsigned i = 0; i < m_qhead; ++i)
terms.push_back(m_fmls[i].fml());
for (expr* e : subterms::all(terms))
m_frozen.mark(e, true);
// freeze subterms that occur with recursive function definitions
recfun::util rec(m);
if (rec.has_rec_defs()) {
for (func_decl* f : rec.get_rec_funs()) {
@ -152,6 +149,9 @@ void elim_unconstrained::init_nodes() {
}
}
/**
* Create nodes for all terms in the goal
*/
void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
unsigned max_id = 0;
for (expr* e : subterms::all(terms))

4
src/ast/simplifiers/elim_unconstrained.h
View file

@ -58,14 +58,10 @@ class elim_unconstrained : public dependent_expr_simplifier {
void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(t->get_id()); }
void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(t->get_id()); }
void gc(expr* t);
expr* get_parent(unsigned n) const;
void init_refcounts();
void dec_refcounts(expr* t);
void add_term(expr* t);
void init_terms(expr_ref_vector const& terms);
void init_nodes();
void eliminate();
void reconstruct_terms();