From 527c5191a60b2bca8155a078175a34daf64a6529 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Sep 2016 12:24:24 -0700 Subject: [PATCH] Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 65 ++++++++++++++++++++++++++++++++++++++--- src/opt/opt_cmds.cpp | 5 +--- src/opt/opt_context.cpp | 27 ++++++----------- src/opt/opt_solver.cpp | 3 ++ 4 files changed, 74 insertions(+), 26 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4d832afd6..0efb3dcce 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2331,11 +2331,68 @@ namespace z3 { inline expr store(expr const & a, int i, int v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range())); } + +#define MK_EXPR1(_fn, _arg) \ + Z3_ast r = _fn(_arg.ctx(), _arg); \ + _arg.check_error(); \ + return expr(_arg.ctx(), r); + +#define MK_EXPR2(_fn, _arg1, _arg2) \ + check_context(_arg1, _arg2); \ + Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \ + _arg1.check_error(); \ + return expr(_arg1.ctx(), r); + inline expr const_array(sort const & d, expr const & v) { - check_context(d, v); - Z3_ast r = Z3_mk_const_array(d.ctx(), d, v); - d.check_error(); - return expr(d.ctx(), r); + MK_EXPR2(Z3_mk_const_array, d, v); + } + + inline expr empty_set(sort const& s) { + MK_EXPR1(Z3_mk_empty_set, s); + } + + inline expr full_set(sort const& s) { + MK_EXPR1(Z3_mk_full_set, s); + } + + inline expr set_add(expr const& s, expr const& e) { + MK_EXPR2(Z3_mk_set_add, s, e); + } + + inline expr set_del(expr const& s, expr const& e) { + MK_EXPR2(Z3_mk_set_del, s, e); + } + + inline expr set_union(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast es[2] = { a, b }; + Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr set_intersect(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast es[2] = { a, b }; + Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr set_difference(expr const& a, expr const& b) { + MK_EXPR2(Z3_mk_set_difference, a, b); + } + + inline expr set_complement(expr const& a) { + MK_EXPR1(Z3_mk_set_complement, a); + } + + inline expr set_member(expr const& s, expr const& e) { + MK_EXPR2(Z3_mk_set_member, s, e); + } + + inline expr set_subset(expr const& a, expr const& b) { + MK_EXPR2(Z3_mk_set_subset, a, b); } // sequence and regular expression operations. diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 5406eaca3..571c26e2d 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -97,10 +97,7 @@ public: virtual void execute(cmd_context & ctx) { symbol w("weight"); - rational weight = ps().get_rat(symbol("weight"), rational(0)); - if (weight.is_zero()) { - weight = rational::one(); - } + rational weight = ps().get_rat(symbol("weight"), rational::one()); symbol id = ps().get_sym(symbol("id"), symbol::null); get_opt(ctx, m_opt).add_soft_constraint(m_formula, weight, id); reset(ctx); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index aad034130..68a5dc302 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -91,10 +91,7 @@ namespace opt { unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) { if (w.is_neg()) { - throw default_exception("Negative weight supplied. Weight should be positive"); - } - if (w.is_zero()) { - throw default_exception("Zero weight supplied. Weight should be positive"); + throw default_exception("Negative weight supplied. Weight should be non-negative"); } if (!m.is_bool(f)) { throw default_exception("Soft constraint should be Boolean"); @@ -105,9 +102,11 @@ namespace opt { } SASSERT(m_indices.contains(id)); unsigned idx = m_indices[id]; - m_objectives[idx].m_terms.push_back(f); - m_objectives[idx].m_weights.push_back(w); - m_objectives_term_trail.push_back(idx); + if (w.is_pos()) { + m_objectives[idx].m_terms.push_back(f); + m_objectives[idx].m_weights.push_back(w); + m_objectives_term_trail.push_back(idx); + } return idx; } @@ -852,9 +851,7 @@ namespace opt { func_decl* f = m.mk_fresh_func_decl(name,"", domain.size(), domain.c_ptr(), m.mk_bool_sort()); m_objective_fns.insert(f, index); m_objective_refs.push_back(f); - if (sz > 0) { - m_objective_orig.insert(f, args[0]); - } + m_objective_orig.insert(f, sz > 0 ? args[0] : 0); return m.mk_app(f, sz, args); } @@ -873,10 +870,7 @@ namespace opt { } void context::from_fmls(expr_ref_vector const& fmls) { - TRACE("opt", - for (unsigned i = 0; i < fmls.size(); ++i) { - tout << mk_pp(fmls[i], m) << "\n"; - }); + TRACE("opt", tout << fmls << "\n";); m_hard_constraints.reset(); expr_ref orig_term(m); for (unsigned i = 0; i < fmls.size(); ++i) { @@ -1054,10 +1048,7 @@ namespace opt { break; } } - TRACE("opt", - for (unsigned i = 0; i < fmls.size(); ++i) { - tout << mk_pp(fmls[i].get(), m) << "\n"; - }); + TRACE("opt", tout << fmls << "\n";); } void context::internalize() { diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 7637da1e8..64ab2823f 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -78,6 +78,9 @@ namespace opt { } void opt_solver::assert_expr(expr * t) { + if (has_quantifiers(t)) { + m_params.m_relevancy_lvl = 2; + } m_context.assert_expr(t); }