mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +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:16:47 -07:00
parent 81260c7ffb
commit bd7ba4b612
4 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_solver.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/ --*/
#include <cmath>
#include "sat/sat_solver.h" #include "sat/sat_solver.h"
#include "sat/sat_integrity_checker.h" #include "sat/sat_integrity_checker.h"
#include "sat/sat_lookahead.h" #include "sat/sat_lookahead.h"

2
src/tactic/model_converter.cpp
View file

@ -120,7 +120,7 @@ public:
m = m_model; m = m_model;
} }
void operator()(labels_vec & r) { void operator()(labels_vec & r) override {
r.append(m_labels.size(), m_labels.c_ptr()); r.append(m_labels.size(), m_labels.c_ptr());
} }

8
src/tactic/sine_filter.cpp
View file

@ -36,14 +36,14 @@ public:
sine_tactic(ast_manager& m, params_ref const& p): sine_tactic(ast_manager& m, params_ref const& p):
m(m), m_params(p) {} m(m), m_params(p) {}
virtual tactic * translate(ast_manager & m) { tactic * translate(ast_manager & m) override {
return alloc(sine_tactic, m, m_params); return alloc(sine_tactic, m, m_params);
} }
virtual void updt_params(params_ref const & p) { void updt_params(params_ref const & p) override {
} }
virtual void collect_param_descrs(param_descrs & r) { void collect_param_descrs(param_descrs & r) override {
} }
void operator()(goal_ref const & g, goal_ref_buffer& result) override { void operator()(goal_ref const & g, goal_ref_buffer& result) override {
@ -63,7 +63,7 @@ public:
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
} }
virtual void cleanup() { void cleanup() override {
} }
private: private:

8
src/tactic/tactical.cpp
View file

@ -1040,7 +1040,7 @@ public:
virtual ~fail_if_tactic() {} virtual ~fail_if_tactic() {}
void cleanup() {} void cleanup() override {}
void operator()(goal_ref const & in, goal_ref_buffer& result) override { void operator()(goal_ref const & in, goal_ref_buffer& result) override {
if (m_p->operator()(*(in.get())).is_true()) { if (m_p->operator()(*(in.get())).is_true()) {
@ -1093,7 +1093,7 @@ public:
} }
} }
virtual tactic * translate(ast_manager & m) { return translate_core<if_no_unsat_cores_tactical>(m); } tactic * translate(ast_manager & m) override { return translate_core<if_no_unsat_cores_tactical>(m); }
}; };
class if_no_models_tactical : public unary_tactical { class if_no_models_tactical : public unary_tactical {
@ -1109,7 +1109,9 @@ public:
} }
} }
virtual tactic * translate(ast_manager & m) { return translate_core<if_no_models_tactical>(m); } tactic * translate(ast_manager & m) override {
return translate_core<if_no_models_tactical>(m);
}
}; };
tactic * if_no_proofs(tactic * t) { tactic * if_no_proofs(tactic * t) {