mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix push/pop bugs in optimize context, add example to c++, fix bug in arithemtic bounds axiom addition

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-02 09:32:38 -07:00
parent 31f16d7aa4
commit 3f8083dfa6
3 changed files with 34 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -972,7 +972,29 @@ void substitute_example() {
std::cout << new_f << std::endl;
}
void opt_example() {
context c;
optimize opt(c);
params p(c);
p.set("priority",c.str_symbol("pareto"));
opt.set(p);
expr x = c.int_const("x");
expr y = c.int_const("y");
opt.add(10 >= x && x >= 0);
opt.add(10 >= y && y >= 0);
opt.add(x + y <= 11);
optimize::handle h1 = opt.maximize(x);
optimize::handle h2 = opt.maximize(y);
check_result r = sat;
while (true) {
if (sat == opt.check()) {
std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n";
}
else {
break;
}
}
}
int main() {
try {
@ -1012,6 +1034,7 @@ int main() {
expr_vector_example(); std::cout << "\n";
exists_expr_vector_example(); std::cout << "\n";
substitute_example(); std::cout << "\n";
opt_example(); std::cout << "\n";
std::cout << "done\n";
}
catch (exception & ex) {