diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index c75acc5e2..9941e5082 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; @@ -1467,6 +1479,56 @@ 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(); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 5d3e1ad7a..847115951 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 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..2b364bc1b 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; @@ -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; }