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

remove assignments to lambdas, exposed by #4169

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-30 12:35:07 -07:00
parent 9c52d4e615
commit 7ae20476c2
3 changed files with 22 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context.cpp
View file

@ -62,6 +62,7 @@ namespace smt {
m_fingerprints(m, m_region), m_fingerprints(m, m_region),
m_b_internalized_stack(m), m_b_internalized_stack(m),
m_e_internalized_stack(m), m_e_internalized_stack(m),
m_l_internalized_stack(m),
m_final_check_idx(0), m_final_check_idx(0),
m_is_auxiliary(false), m_is_auxiliary(false),
m_par(nullptr), m_par(nullptr),

13
src/smt/smt_context.h
View file

@ -107,6 +107,7 @@ namespace smt {
// enodes. Examples: boolean expression nested in an // enodes. Examples: boolean expression nested in an
// uninterpreted function. // uninterpreted function.
expr_ref_vector m_e_internalized_stack; // stack of the expressions already internalized as enodes. expr_ref_vector m_e_internalized_stack; // stack of the expressions already internalized as enodes.
quantifier_ref_vector m_l_internalized_stack;
ptr_vector<justification> m_justifications; ptr_vector<justification> m_justifications;
@ -776,7 +777,6 @@ namespace smt {
void undo(context & ctx) override { ctx.undo_mk_bool_var(); } void undo(context & ctx) override { ctx.undo_mk_bool_var(); }
}; };
mk_bool_var_trail m_mk_bool_var_trail; mk_bool_var_trail m_mk_bool_var_trail;
void undo_mk_bool_var(); void undo_mk_bool_var();
friend class mk_enode_trail; friend class mk_enode_trail;
@ -784,11 +784,18 @@ namespace smt {
public: public:
void undo(context & ctx) override { ctx.undo_mk_enode(); } void undo(context & ctx) override { ctx.undo_mk_enode(); }
}; };
mk_enode_trail m_mk_enode_trail; mk_enode_trail m_mk_enode_trail;
void undo_mk_enode(); void undo_mk_enode();
friend class mk_lambda_trail;
class mk_lambda_trail : public trail<context> {
public:
void undo(context & ctx) override { ctx.undo_mk_lambda(); }
};
mk_lambda_trail m_mk_lambda_trail;
void undo_mk_lambda();
void apply_sort_cnstr(app * term, enode * e); void apply_sort_cnstr(app * term, enode * e);
bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits); bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits);

12
src/smt/smt_internalizer.cpp
View file

@ -575,6 +575,8 @@ namespace smt {
internalize_quantifier(fa, true); internalize_quantifier(fa, true);
if (!e_internalized(lam_name)) internalize_uninterpreted(lam_name); if (!e_internalized(lam_name)) internalize_uninterpreted(lam_name);
m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr); m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr);
m_l_internalized_stack.push_back(q);
m_trail_stack.push_back(&m_mk_lambda_trail);
} }
/** /**
@ -992,6 +994,14 @@ namespace smt {
return e; return e;
} }
void context::undo_mk_lambda() {
SASSERT(!m_l_internalized_stack.empty());
m_stats.m_num_del_enode++;
quantifier * n = m_l_internalized_stack.back();
m_app2enode[n->get_id()] = nullptr;
m_l_internalized_stack.pop_back();
}
void context::undo_mk_enode() { void context::undo_mk_enode() {
SASSERT(!m_e_internalized_stack.empty()); SASSERT(!m_e_internalized_stack.empty());
m_stats.m_num_del_enode++; m_stats.m_num_del_enode++;
@ -1001,7 +1011,7 @@ namespace smt {
unsigned n_id = n->get_id(); unsigned n_id = n->get_id();
SASSERT(is_app(n)); SASSERT(is_app(n));
enode * e = m_app2enode[n_id]; enode * e = m_app2enode[n_id];
m_app2enode[n_id] = 0; m_app2enode[n_id] = nullptr;
if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) { if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) {
SASSERT(m_cg_table.contains_ptr(e)); SASSERT(m_cg_table.contains_ptr(e));
m_cg_table.erase(e); m_cg_table.erase(e);