From ac7fffa9cbf440fa01178c5b00a132dd49f168b6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Mar 2014 08:34:31 -0700 Subject: [PATCH 1/5] fix bug exposed by example by Robert White Signed-off-by: Nikolaj Bjorner --- src/duality/duality.h | 2 +- src/interp/iz3hash.h | 4 ++-- src/opt/weighted_maxsat.cpp | 44 +++++++++++++++++++++---------------- 3 files changed, 28 insertions(+), 22 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index fe86ed2ec..aa147d93e 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -29,7 +29,7 @@ using namespace stl_ext; namespace Duality { - class implicant_solver; + struct implicant_solver; /* Generic operations on Z3 formulas */ diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 355c03817..e4faa9ec3 100644 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -52,7 +52,7 @@ namespace hash_space { class hash { public: size_t operator()(const std::string &s) const { - return string_hash(s.c_str(), s.size(), 0); + return string_hash(s.c_str(), static_cast(s.size()), 0); } }; @@ -374,7 +374,7 @@ namespace hash_space { void resize(size_t new_size) { const size_t old_n = buckets.size(); if (new_size <= old_n) return; - const size_t n = next_prime(new_size); + const size_t n = next_prime(static_cast(new_size)); if (n <= old_n) return; Table tmp(n, (Entry*)(0)); for (size_t i = 0; i < old_n; ++i) { diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 2aeabfbb8..8a8bb2aba 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -59,6 +59,7 @@ namespace smt { rational m_rmin_cost; // current maximal cost assignment. scoped_mpz m_zcost; // current sum of asserted costs scoped_mpz m_zmin_cost; // current maximal cost assignment. + bool m_found_optimal; u_map m_bool2var; // bool_var -> theory_var svector m_var2bool; // theory_var -> bool_var bool m_propagate; @@ -79,6 +80,7 @@ namespace smt { m_old_values(m_mpz), m_zcost(m_mpz), m_zmin_cost(m_mpz), + m_found_optimal(false), m_propagate(false), m_normalize(false) {} @@ -93,14 +95,21 @@ namespace smt { void get_assignment(svector& result) { result.reset(); - std::sort(m_cost_save.begin(), m_cost_save.end()); - for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) { - if (j < m_cost_save.size() && m_cost_save[j] == i) { + if (!m_found_optimal) { + for (unsigned i = 0; i < m_vars.size(); ++i) { result.push_back(false); - ++j; } - else { - result.push_back(true); + } + else { + std::sort(m_cost_save.begin(), m_cost_save.end()); + for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) { + if (j < m_cost_save.size() && m_cost_save[j] == i) { + result.push_back(false); + ++j; + } + else { + result.push_back(true); + } } } TRACE("opt", @@ -189,10 +198,6 @@ namespace smt { return m_min_cost_atom; } - bool found_solution() const { - return !m_cost_save.empty(); - } - // scoped_mpz leaks. class numeral_trail : public trail { @@ -273,6 +278,7 @@ namespace smt { m_min_cost_atom = 0; m_min_cost_atoms.reset(); m_propagate = false; + m_found_optimal = false; m_assigned.reset(); } @@ -303,7 +309,7 @@ namespace smt { } bool is_optimal() const { - return m_mpz.lt(m_zcost, m_zmin_cost); + return !m_found_optimal || m_zcost < m_zmin_cost; } expr_ref mk_block() { @@ -329,22 +335,22 @@ namespace smt { rational rw = rational(q); IF_VERBOSE(1, verbose_stream() << "(wmaxsat with upper bound: " << rw << ")\n";); m_zmin_cost = weight; + m_found_optimal = true; m_cost_save.reset(); m_cost_save.append(m_costs); - } - - expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); - - TRACE("opt", - tout << result << "\n"; - if (is_optimal()) { + TRACE("opt", tout << "costs: "; for (unsigned i = 0; i < m_costs.size(); ++i) { tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; } tout << "\n"; get_context().display(tout); - }); + ); + } + expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); + TRACE("opt", + tout << result << " weight: " << weight << "\n"; + tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";); return result; } From a6d7d23bb5c4145f77b5e1a5f33b5c1064b7d563 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Mar 2014 08:34:54 -0700 Subject: [PATCH 2/5] fix compilation warnings Signed-off-by: Nikolaj Bjorner --- src/duality/duality.h | 2 +- src/duality/duality_solver.cpp | 2 +- src/interp/iz3hash.h | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index fe86ed2ec..aa147d93e 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -29,7 +29,7 @@ using namespace stl_ext; namespace Duality { - class implicant_solver; + struct implicant_solver; /* Generic operations on Z3 formulas */ diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index a47e90f95..dc261a351 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2201,7 +2201,7 @@ namespace Duality { #endif int expand_max = 1; if(0&&duality->BatchExpand){ - int thing = stack.size() * 0.1; + int thing = stack.size() /10; expand_max = std::max(1,thing); if(expand_max > 1) std::cout << "foo!\n"; diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 355c03817..02c533c85 100644 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -52,7 +52,7 @@ namespace hash_space { class hash { public: size_t operator()(const std::string &s) const { - return string_hash(s.c_str(), s.size(), 0); + return string_hash(s.c_str(), static_cast(s.size()), 0); } }; @@ -107,7 +107,7 @@ namespace hash_space { 4294967291ul }; - inline unsigned long next_prime(unsigned long n) { + inline size_t next_prime(size_t n) { const unsigned long* to = primes + (int)num_primes; for(const unsigned long* p = primes; p < to; p++) if(*p >= n) return *p; From 4c95bb4dd901f0ba33d025538233c6598b165554 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Mar 2014 08:51:50 -0700 Subject: [PATCH 3/5] add 'distinct' to C++ API Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 12 ++++++++++++ src/api/dotnet/Context.cs | 2 ++ src/api/dotnet/Expr.cs | 1 + 3 files changed, 15 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index c75acc5e2..8f228cdba 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -652,6 +652,8 @@ namespace z3 { return expr(c.ctx(), r); } + friend expr distinct(expr_vector const& args); + friend expr operator==(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_eq(a.ctx(), a, b); @@ -1065,6 +1067,16 @@ namespace z3 { array vars(xs); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); } + + + inline expr distinct(expr_vector const& args) { + assert(args.size() > 0); + context& ctx = args[0].ctx(); + array _args(args); + Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr()); + ctx.check_error(); + return expr(ctx, r); + } class func_entry : public object { Z3_func_entry m_entry; diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ae8b233d1..47294244a 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -916,6 +916,8 @@ namespace Microsoft.Z3 CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } + + #endregion #region Arithmetic diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index b2927e2c3..49b46edeb 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -320,6 +320,7 @@ namespace Microsoft.Z3 /// Indicates whether the term is an implication /// public bool IsImplies { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } } + #endregion #region Arithmetic Terms From 13e454ad63e01ce380ca9b72aef1d4efa79dee3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Mar 2014 09:29:21 -0700 Subject: [PATCH 4/5] adding C++ API for optimization Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 60 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 8f228cdba..e83dae7cc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1479,6 +1479,66 @@ namespace z3 { } }; + class optimize : public object { + Z3_optimize m_opt; + public: + class handle { + unsigned m_h; + public: + handle(unsigned h): m_h(h) {} + unsigned h() const { return m_h; } + }; + optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); } + ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); } + operator Z3_optimize() const { return m_opt; } + + void add(expr const& e) { + assert(e.is_bool()); + Z3_optimize_assert(ctx(), m_opt, e); + } + handle add(expr const& e, unsigned weight) { + assert(e.is_bool()); + std::stringstream strm; + strm << weight; + return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0)); + } + handle add(expr const& e, char const* weight) { + assert(e.is_bool()); + return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0)); + } + handle maximzie(expr const& e) { + return handle(Z3_optimize_maximize(ctx(), m_opt, e)); + } + handle minimize(expr const& e) { + return handle(Z3_optimize_minimize(ctx(), m_opt, e)); + } + + check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); } + + model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); } + + void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); } + + expr lower(handle const& h) { + Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h()); + check_error(); + return expr(ctx(), r); + } + + expr upper(handle const& h) { + Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h()); + check_error(); + return expr(ctx(), r); + } + + stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); } + + friend std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; } + + std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; } + + }; + inline tactic fail_if(probe const & p) { Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p); p.check_error(); From cc577a431a40ad3edaca2a2e23edaacd01e2a2be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Mar 2014 09:39:14 -0700 Subject: [PATCH 5/5] C++ API Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e83dae7cc..9941e5082 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1491,7 +1491,6 @@ namespace z3 { optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); } ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); } operator Z3_optimize() const { return m_opt; } - void add(expr const& e) { assert(e.is_bool()); Z3_optimize_assert(ctx(), m_opt, e); @@ -1512,31 +1511,22 @@ namespace z3 { handle minimize(expr const& e) { return handle(Z3_optimize_minimize(ctx(), m_opt, e)); } - check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); } - model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); } - void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); } - expr lower(handle const& h) { Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h()); check_error(); return expr(ctx(), r); } - expr upper(handle const& h) { Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h()); check_error(); return expr(ctx(), r); } - - stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); } - + stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; } - - std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; } - + std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; } }; inline tactic fail_if(probe const & p) {