mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

format

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-02 12:30:26 -07:00
parent fc36fb115f
commit 4aaf026b49
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -96,27 +96,27 @@ namespace euf {
stats m_stats; stats m_stats;
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;
sat::sat_internalizer* m_to_si; sat::sat_internalizer* m_to_si;
scoped_ptr<euf::ackerman> m_ackerman; scoped_ptr<euf::ackerman> m_ackerman;
scoped_ptr<sat::dual_solver> m_dual_solver; scoped_ptr<sat::dual_solver> m_dual_solver;
user::solver* m_user_propagator{ nullptr }; user::solver* m_user_propagator = nullptr;
th_solver* m_qsolver { nullptr }; th_solver* m_qsolver = nullptr;
unsigned m_generation { 0 }; unsigned m_generation = 0;
mutable ptr_vector<expr> m_todo; mutable ptr_vector<expr> m_todo;
ptr_vector<expr> m_bool_var2expr; ptr_vector<expr> m_bool_var2expr;
ptr_vector<size_t> m_explain; ptr_vector<size_t> m_explain;
unsigned m_num_scopes{ 0 }; unsigned m_num_scopes = 0;
unsigned_vector m_var_trail; unsigned_vector m_var_trail;
svector<scope> m_scopes; svector<scope> m_scopes;
scoped_ptr_vector<th_solver> m_solvers; scoped_ptr_vector<th_solver> m_solvers;
ptr_vector<th_solver> m_id2solver; ptr_vector<th_solver> m_id2solver;
constraint* m_conflict{ nullptr }; constraint* m_conflict = nullptr;
constraint* m_eq{ nullptr }; constraint* m_eq = nullptr;
constraint* m_lit{ nullptr }; constraint* m_lit = nullptr;
// internalization // internalization
bool visit(expr* e) override; bool visit(expr* e) override;