mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

ensure that initialization order for euf_solver is aligned

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-20 08:48:15 -07:00
parent 2f1514a259
commit 6292b06c67
2 changed files with 47 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/euf_solver.cpp
View file

@ -46,14 +46,13 @@ namespace euf {
m_trail(), m_trail(),
m_rewriter(m), m_rewriter(m),
m_unhandled_functions(m), m_unhandled_functions(m),
m_lookahead(nullptr),
m_to_m(&m), m_to_m(&m),
m_to_si(&si), m_to_si(&si),
m_values(m), m_values(m),
m_clause(m),
m_expr_args(m),
m_clause_visitor(m), m_clause_visitor(m),
m_smt_proof_checker(m, p) m_smt_proof_checker(m, p),
m_clause(m),
m_expr_args(m)
{ {
updt_params(p); updt_params(p);
m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2); m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2);

32
src/sat/smt/euf_solver.h
View file

@ -121,7 +121,7 @@ namespace euf {
th_rewriter m_rewriter; th_rewriter m_rewriter;
func_decl_ref_vector m_unhandled_functions; func_decl_ref_vector m_unhandled_functions;
sat::lookahead* m_lookahead = nullptr; sat::lookahead* m_lookahead = nullptr;
ast_manager* m_to_m; ast_manager* m_to_m = nullptr;
sat::sat_internalizer* m_to_si; sat::sat_internalizer* m_to_si;
scoped_ptr<euf::ackerman> m_ackerman; scoped_ptr<euf::ackerman> m_ackerman;
user_propagator::on_clause_eh_t m_on_clause; user_propagator::on_clause_eh_t m_on_clause;
@ -145,6 +145,22 @@ namespace euf {
constraint* m_eq = nullptr; constraint* m_eq = nullptr;
constraint* m_lit = nullptr; constraint* m_lit = nullptr;
// proofs
bool m_proof_initialized = false;
ast_pp_util m_clause_visitor;
bool m_display_all_decls = false;
smt_proof_checker m_smt_proof_checker;
typedef std::pair<expr*, expr*> expr_pair;
literal_vector m_proof_literals;
svector<expr_pair> m_proof_eqs, m_proof_deqs, m_expr_pairs;
unsigned m_lit_head = 0, m_lit_tail = 0, m_cc_head = 0, m_cc_tail = 0;
unsigned m_eq_head = 0, m_eq_tail = 0, m_deq_head = 0, m_deq_tail = 0;
symbol m_euf = symbol("euf");
symbol m_smt = symbol("smt");
expr_ref_vector m_clause;
expr_ref_vector m_expr_args;
// internalization // internalization
bool visit(expr* e) override; bool visit(expr* e) override;
@ -201,24 +217,12 @@ namespace euf {
void log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint); void log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint);
void log_justification(literal l, th_explain const& jst); void log_justification(literal l, th_explain const& jst);
typedef std::pair<expr*, expr*> expr_pair;
literal_vector m_proof_literals;
svector<expr_pair> m_proof_eqs, m_proof_deqs, m_expr_pairs;
unsigned m_lit_head = 0, m_lit_tail = 0, m_cc_head = 0, m_cc_tail = 0;
unsigned m_eq_head = 0, m_eq_tail = 0, m_deq_head = 0, m_deq_tail = 0;
symbol m_euf = symbol("euf");
symbol m_smt = symbol("smt");
expr_ref_vector m_clause;
expr_ref_vector m_expr_args;
eq_proof_hint* mk_hint(symbol const& th, literal lit, literal_vector const& r); eq_proof_hint* mk_hint(symbol const& th, literal lit, literal_vector const& r);
bool m_proof_initialized = false;
void init_proof(); void init_proof();
ast_pp_util m_clause_visitor;
bool m_display_all_decls = false;
smt_proof_checker m_smt_proof_checker;
void on_clause(unsigned n, literal const* lits, sat::status st) override; void on_clause(unsigned n, literal const* lits, sat::status st) override;
void on_lemma(unsigned n, literal const* lits, sat::status st); void on_lemma(unsigned n, literal const* lits, sat::status st);
void on_proof(unsigned n, literal const* lits, sat::status st); void on_proof(unsigned n, literal const* lits, sat::status st);