mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#4637

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-13 13:32:38 -07:00
parent a892e4793b
commit 7d391d44a2
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2848,20 +2848,23 @@ namespace z3 {
void add(expr_vector const& es) { void add(expr_vector const& es) {
for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it); for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
} }
handle add(expr const& e, unsigned weight) {
assert(e.is_bool());
auto str = std::to_string(weight);
return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
}
void add(expr const& e, expr const& t) { void add(expr const& e, expr const& t) {
assert(e.is_bool()); assert(e.is_bool());
Z3_optimize_assert_and_track(ctx(), m_opt, e, t); Z3_optimize_assert_and_track(ctx(), m_opt, e, t);
} }
handle add(expr const& e, char const* weight) { handle add_soft(expr const& e, unsigned weight) {
assert(e.is_bool());
auto str = std::to_string(weight);
return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, str.c_str(), 0));
}
handle add_soft(expr const& e, char const* weight) {
assert(e.is_bool()); assert(e.is_bool());
return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0)); return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
} }
handle add(expr const& e, unsigned weight) {
return add_soft(e, weight);
}
handle maximize(expr const& e) { handle maximize(expr const& e) {
return handle(Z3_optimize_maximize(ctx(), m_opt, e)); return handle(Z3_optimize_maximize(ctx(), m_opt, e));
} }