mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-06-22 20:25:55 -07:00
parent 5b497b6249 fad1dffbf0
commit 41edf5f91e
3 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -23,7 +23,7 @@ void demorgan() {
expr x = c.bool_const("x");
expr y = c.bool_const("y");
expr conjecture = !(x && y) == (!x || !y);
expr conjecture = (!(x && y)) == (!x || !y);
solver s(c);
// adding the negation of the conjecture as a constraint.

3
scripts/mk_util.py
View file

@ -2472,7 +2472,8 @@ def mk_makefile():
out.write(' %s' % c.name)
out.write('\n\t@echo Z3 was successfully built.\n')
out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR)
out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR)
pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH"
out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH and %s environment variables.\"\n" % (BUILD_DIR, pathvar))
if not IS_WINDOWS:
out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
out.write('\t@echo " sudo make install"\n\n')

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) {
qe::arith_project_plugin plugin(m);
model mdl(m);
expr_ref bound(m);
model mdl(m);
arith_util a(m);
for (unsigned i = 0; i < num_vars; ++i) {
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);
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();
std::cout << "optimal: " << value1 << " " << value2 << "\n";
mbo.display(std::cout);