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

Down compatibility for C++03

Browse source
This commit is contained in:
Alexey Vishnyakov 2020-02-12 20:30:04 +03:00 • committed by Nikolaj Bjorner
parent bbce6bfa07
commit fdc27d61e4
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -84,8 +84,9 @@ namespace z3 {
std::string m_msg; std::string m_msg;
public: public:
exception(char const * msg):m_msg(msg) {} exception(char const * msg):m_msg(msg) {}
virtual ~exception() throw() {}
char const * msg() const { return m_msg.c_str(); } char const * msg() const { return m_msg.c_str(); }
char const * what() const noexcept { return m_msg.c_str(); } char const * what() const throw() { return m_msg.c_str(); }
friend std::ostream & operator<<(std::ostream & out, exception const & e); friend std::ostream & operator<<(std::ostream & out, exception const & e);
}; };
inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; } inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
@ -2784,7 +2785,8 @@ namespace z3 {
m_opt = Z3_mk_optimize(c); m_opt = Z3_mk_optimize(c);
Z3_optimize_inc_ref(c, m_opt); Z3_optimize_inc_ref(c, m_opt);
add(expr_vector(c, src.assertions())); add(expr_vector(c, src.assertions()));
for (expr const& o : expr_vector(c, src.objectives())) minimize(o); expr_vector v(c, src.objectives());
for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
} }
optimize& operator=(optimize const& o) { optimize& operator=(optimize const& o) {
Z3_optimize_inc_ref(o.ctx(), o.m_opt); Z3_optimize_inc_ref(o.ctx(), o.m_opt);
@ -2800,7 +2802,7 @@ namespace z3 {
Z3_optimize_assert(ctx(), m_opt, e); Z3_optimize_assert(ctx(), m_opt, e);
} }
void add(expr_vector const& es) { void add(expr_vector const& es) {
for (expr const& e : es) add(e); for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
} }
handle add(expr const& e, unsigned weight) { handle add(expr const& e, unsigned weight) {
assert(e.is_bool()); assert(e.is_bool());