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

fix clang compilation errors

Browse source
This commit is contained in:
Arie Gurfinkel 2019-09-07 18:20:05 +03:00 committed by Nikolaj Bjorner
parent 3b1a73b9e8
commit d44081db7d
1 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -239,7 +239,7 @@ namespace smtfd {
m_nv_trail.shrink(m_nv_trail.size() - n); m_nv_trail.shrink(m_nv_trail.size() - n);
} }
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) const {
return out << "abs:\n" << m_atoms << "\n"; return out << "abs:\n" << m_atoms << "\n";
} }
@ -639,15 +639,18 @@ namespace smtfd {
ref<::solver> m_fd_solver; ref<::solver> m_fd_solver;
ref<::solver> m_smt_solver; ref<::solver> m_smt_solver;
expr_ref_vector m_assertions; expr_ref_vector m_assertions;
unsigned_vector m_assertions_lim; unsigned_vector m_assertions_lim;
unsigned m_assertions_qhead; unsigned m_assertions_qhead;
expr_ref_vector m_toggles; expr_ref_vector m_toggles;
expr_ref m_toggle, m_not_toggle; expr_ref m_toggle;
expr_ref m_not_toggle;
model_ref m_model; model_ref m_model;
std::string m_reason_unknown; std::string m_reason_unknown;
unsigned m_max_lemmas; unsigned m_max_lemmas;
stats m_stats; stats m_stats;
unsigned m_useful_smt, m_non_useful_smt, m_max_conflicts; unsigned m_useful_smt;
unsigned m_non_useful_smt;
unsigned m_max_conflicts;
bool m_smt_known; bool m_smt_known;
void flush_assertions() { void flush_assertions() {
@ -688,7 +691,7 @@ namespace smtfd {
if (r == l_false) { if (r == l_false) {
m_fd_solver->get_unsat_core(core); m_fd_solver->get_unsat_core(core);
TRACE("smtfd", display(tout << core);); TRACE("smtfd", display(tout << core););
core.erase(m_not_toggle); core.erase(m_not_toggle.get());
SASSERT(!asms.contains(m_not_toggle)); SASSERT(!asms.contains(m_not_toggle));
SASSERT(!asms.contains(m_toggle)); SASSERT(!asms.contains(m_toggle));
} }
@ -772,7 +775,7 @@ namespace smtfd {
asms.push_back(m.mk_not(a)); asms.push_back(m.mk_not(a));
} }
} }
asms.erase(m_toggle); asms.erase(m_toggle.get());
} }
void checkpoint() { void checkpoint() {
@ -794,8 +797,8 @@ namespace smtfd {
} }
} }
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out, unsigned n = 0, expr * const * assumptions = nullptr) const override {
init(); if (!m_fd_solver) return out;
m_fd_solver->display(out); m_fd_solver->display(out);
m_smt_solver->display(out); m_smt_solver->display(out);
out << m_assumptions << "\n"; out << m_assumptions << "\n";
@ -811,9 +814,9 @@ namespace smtfd {
solver(ast_manager& m, params_ref const& p): solver(ast_manager& m, params_ref const& p):
solver_na2as(m), solver_na2as(m),
m(m), m(m),
m_abs(m),
m_assertions(m), m_assertions(m),
m_assertions_qhead(0), m_assertions_qhead(0),
m_abs(m),
m_toggles(m), m_toggles(m),
m_toggle(m.mk_true(), m), m_toggle(m.mk_true(), m),
m_not_toggle(m.mk_false(), m), m_not_toggle(m.mk_false(), m),
@ -933,7 +936,7 @@ namespace smtfd {
} }
void get_unsat_core(expr_ref_vector & r) override { void get_unsat_core(expr_ref_vector & r) override {
m_fd_solver->get_unsat_core(r); m_fd_solver->get_unsat_core(r);
r.erase(m_toggle); r.erase(m_toggle.get());
rep(r); rep(r);
} }
void get_model_core(model_ref & mdl) override { void get_model_core(model_ref & mdl) override {