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

translate optimize from c++ API #2859

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-15 04:24:51 -08:00
parent 0d614b8c36
commit 773b27296f
3 changed files with 33 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
examples/c++/example.cpp
View file

@ -1044,6 +1044,27 @@ void opt_example() {
} }
} }
/**
* translate from one optimization context to another.
*/
void opt_translate_example() {
context c1, c2;
optimize o1(c1);
expr x = c1.int_const("x");
expr y = c1.int_const("y");
o1.add(10 >= x && x >= 0);
o1.add(10 >= y && y >= 0);
o1.add(x + y <= 11);
optimize::handle h1 = o1.maximize(x);
optimize::handle h2 = o1.maximize(y);
optimize o2(c2, o1);
expr z = c2.int_const("z");
expr x2 = c2.int_const("x");
o2.add(x2 + z == 2);
o2.minimize(z);
std::cout << o2 << "\n";
}
void extract_example() { void extract_example() {
std::cout << "extract example\n"; std::cout << "extract example\n";
context c; context c;
@ -1305,6 +1326,7 @@ int main() {
exists_expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n";
substitute_example(); std::cout << "\n"; substitute_example(); std::cout << "\n";
opt_example(); std::cout << "\n"; opt_example(); std::cout << "\n";
opt_translate_example(); std::cout << "\n";
extract_example(); std::cout << "\n"; extract_example(); std::cout << "\n";
param_descrs_example(); std::cout << "\n"; param_descrs_example(); std::cout << "\n";
sudoku_example(); std::cout << "\n"; sudoku_example(); std::cout << "\n";

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

@ -1872,6 +1872,8 @@ namespace z3 {
ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); } ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); } ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); } ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); } ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
operator Z3_ast_vector() const { return m_vector; } operator Z3_ast_vector() const { return m_vector; }
unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); } unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
@ -2778,6 +2780,11 @@ namespace z3 {
Z3_optimize_inc_ref(o.ctx(), o.m_opt); Z3_optimize_inc_ref(o.ctx(), o.m_opt);
m_opt = o.m_opt; m_opt = o.m_opt;
} }
optimize(context& c, optimize& src):object(c) {
m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt);
add(expr_vector(c, src.assertions()));
for (expr& o : expr_vector(c, src.objectives())) minimize(o);
}
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);
Z3_optimize_dec_ref(ctx(), m_opt); Z3_optimize_dec_ref(ctx(), m_opt);
@ -2791,6 +2798,9 @@ namespace z3 {
assert(e.is_bool()); assert(e.is_bool());
Z3_optimize_assert(ctx(), m_opt, e); Z3_optimize_assert(ctx(), m_opt, e);
} }
void add(expr_vector const& es) {
for (expr& e : es) add(e);
}
handle add(expr const& e, unsigned weight) { handle add(expr const& e, unsigned weight) {
assert(e.is_bool()); assert(e.is_bool());
std::stringstream strm; std::stringstream strm;

2
src/opt/opt_context.cpp
View file

@ -217,7 +217,7 @@ namespace opt {
break; break;
case O_MAXIMIZE: case O_MAXIMIZE:
result = o.m_term; result = o.m_term;
if (m_arith.is_arith_expr(result)) { if (m_arith.is_int_real(result)) {
result = m_arith.mk_uminus(result); result = m_arith.mk_uminus(result);
} }
else if (m_bv.is_bv(result)) { else if (m_bv.is_bv(result)) {