mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

Fixed test case

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-06-22 18:52:40 +01:00
parent 8c191781e7
commit 89b1d7d8da
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/test/qe_arith.cpp
View file

@ -382,8 +382,7 @@ static void add_random_ineq(
static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) { static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) {
qe::arith_project_plugin plugin(m); qe::arith_project_plugin plugin(m);
model mdl(m); model mdl(m);
expr_ref bound(m);
arith_util a(m); arith_util a(m);
for (unsigned i = 0; i < num_vars; ++i) { for (unsigned i = 0; i < num_vars; ++i) {
app_ref var(m); app_ref var(m);
@ -391,7 +390,8 @@ static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned nu
rational val = mbo.get_value(i); rational val = mbo.get_value(i);
mdl.register_decl(var->get_decl(), a.mk_numeral(val, false)); mdl.register_decl(var->get_decl(), a.mk_numeral(val, false));
} }
opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, bound); expr_ref ge(m), gt(m);
opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, ge, gt);
opt::inf_eps value2 = mbo.maximize(); opt::inf_eps value2 = mbo.maximize();
std::cout << "optimal: " << value1 << " " << value2 << "\n"; std::cout << "optimal: " << value1 << " " << value2 << "\n";
mbo.display(std::cout); mbo.display(std::cout);