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

fix mac build error

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-20 20:49:57 -07:00
parent bd7ba4b612
commit d27527d4df
2 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/c++/z3++.h
View file

@ -1939,8 +1939,10 @@ namespace z3 {
void add(expr const & e, char const * p) { void add(expr const & e, char const * p) {
add(e, ctx().bool_const(p)); add(e, ctx().bool_const(p));
} }
void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); } // fails for some compilers:
void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); check_error(); } // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); } check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
check_result check(unsigned n, expr * const assumptions) { check_result check(unsigned n, expr * const assumptions) {
array<Z3_ast> _assumptions(n); array<Z3_ast> _assumptions(n);

12
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -711,7 +711,7 @@ public:
m_imp = alloc(imp, m, p, r, owner); m_imp = alloc(imp, m, p, r, owner);
} }
virtual tactic * translate(ast_manager & m) { tactic * translate(ast_manager & m) override {
return alloc(solve_eqs_tactic, m, m_params, mk_expr_simp_replacer(m, m_params), true); return alloc(solve_eqs_tactic, m, m_params, mk_expr_simp_replacer(m, m_params), true);
} }
@ -719,12 +719,12 @@ public:
dealloc(m_imp); dealloc(m_imp);
} }
virtual void updt_params(params_ref const & p) { void updt_params(params_ref const & p) override {
m_params = p; m_params = p;
m_imp->updt_params(p); m_imp->updt_params(p);
} }
virtual void collect_param_descrs(param_descrs & r) { void collect_param_descrs(param_descrs & r) override {
r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations."); r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers."); r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver."); r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
@ -736,7 +736,7 @@ public:
report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars()); report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars());
} }
virtual void cleanup() { void cleanup() override {
unsigned num_elim_vars = m_imp->m_num_eliminated_vars; unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
ast_manager & m = m_imp->m(); ast_manager & m = m_imp->m();
expr_replacer * r = m_imp->m_r; expr_replacer * r = m_imp->m_r;
@ -751,11 +751,11 @@ public:
dealloc(d); dealloc(d);
} }
virtual void collect_statistics(statistics & st) const { void collect_statistics(statistics & st) const override {
st.update("eliminated vars", m_imp->get_num_eliminated_vars()); st.update("eliminated vars", m_imp->get_num_eliminated_vars());
} }
virtual void reset_statistics() { void reset_statistics() override {
m_imp->m_num_eliminated_vars = 0; m_imp->m_num_eliminated_vars = 0;
} }