From 3bbc09c1d2c800ea4ac646c66a886d25a87c4938 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Fri, 16 Feb 2018 14:44:22 +0000 Subject: [PATCH 01/30] MSS based MaxSMT solver --- src/opt/maxsmt.cpp | 4 ++ src/opt/mss_solver.cpp | 156 +++++++++++++++++++++++++++++++++++++++++ src/opt/mss_solver.h | 12 ++++ src/opt/opt_params.pyg | 8 +-- 4 files changed, 176 insertions(+), 4 deletions(-) create mode 100755 src/opt/mss_solver.cpp create mode 100755 src/opt/mss_solver.h diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 91e843ca0..9bc4f4f14 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -21,6 +21,7 @@ Notes: #include "opt/maxsmt.h" #include "opt/maxres.h" #include "opt/wmax.h" +#include "opt/mss_solver.h" #include "ast/ast_pp.h" #include "util/uint_set.h" #include "opt/opt_context.h" @@ -240,6 +241,9 @@ namespace opt { else if (maxsat_engine == symbol("pd-maxres")) { m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints); } + else if (maxsat_engine == symbol("mss")) { + m_msolver = mk_mss_solver(m_c, m_index, m_weights, m_soft_constraints); + } else if (maxsat_engine == symbol("wmax")) { m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints); } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp new file mode 100755 index 000000000..501b43ee4 --- /dev/null +++ b/src/opt/mss_solver.cpp @@ -0,0 +1,156 @@ +#include "solver/solver.h" +#include "opt/maxsmt.h" +#include "opt/mss_solver.h" +#include "opt/mss.h" +#include "opt/opt_context.h" +#include "opt/opt_params.hpp" + +using namespace opt; + +class mss_solver: public maxsmt_solver_base { + +private: + typedef ptr_vector exprs; + mss m_mss; + unsigned m_index; + expr_ref_vector m_asms; + unsigned m_max_mss; + +public: + mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft): + maxsmt_solver_base(c, ws, soft), + m_mss(c.get_solver(), m), + m_index(id), + m_asms(m), + m_max_mss(UINT_MAX) { + } + + virtual ~mss_solver() {} + + virtual lbool operator()() { + if (!init()) return l_undef; + init_asms(); + lbool is_sat = check_sat(m_asms); + if (is_sat == l_undef) return l_undef; + if (is_sat == l_true) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";); + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl.get()); + return l_true; + } + return enumerate_mss(); + } + + virtual void updt_params(params_ref& p) { + maxsmt_solver_base::updt_params(p); + opt_params _p(p); + m_max_mss = _p.mss_max(); + } + +private: + void init_asms() { + m_asms.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + expr* e = m_soft[i]; + m_asms.push_back(relax_and_assert(e)); + } + } + + expr_ref relax_and_assert(expr* e) { + expr_ref asum(m); + if (is_literal(e)) { + asum = e; + } + else { + asum = mk_fresh_bool("r"); + e = m.mk_iff(asum, e); + s().assert_expr(e); + } + return asum; + } + + bool is_literal(expr* l) { + return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); + } + + lbool enumerate_mss() { + expr_ref_vector asms(m); + for (unsigned i = 0; i < m_max_mss; ++i) { + exprs mss, mcs; + lbool is_sat = next_mss(asms, mss, mcs); + if (is_sat == l_false && i == 0) return l_false; + if (is_sat == l_undef && i == 0) return l_undef; + if (is_sat == l_false || is_sat == l_undef) return l_true; + asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr()))); + } + return l_true; + } + + lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) { + mss.reset(); + mcs.reset(); + lbool is_sat = check_sat(asms); + if (is_sat != l_true) return is_sat; + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl.get()); + vector dummy; + push_exprs(mss, m_asms); + push_exprs(mss, asms); + is_sat = m_mss(mdl.get(), dummy, mss, mcs); + SASSERT(is_sat == l_true); + mdl.reset(); + m_mss.get_model(mdl); + update_assignment(mdl.get()); + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + return is_sat; + } + + void push_exprs(exprs& dst, expr_ref_vector const& src) { + for (unsigned i = 0; i < src.size(); ++i) { + dst.push_back(src[i]); + } + } + + lbool check_sat() { + expr_ref_vector dummy(m); + return check_sat(dummy); + } + + lbool check_sat(expr_ref_vector const& asms) { + return s().check_sat(asms); + } + + void update_assignment(model* mdl) { + rational upper(0); + for (unsigned i = 0; i < m_soft.size(); ++i) { + if (!is_true(mdl, m_soft[i])) { + upper += m_weights[i]; + } + } + if (upper > m_upper) return; + if (!m_c.verify_model(m_index, mdl, upper)) return; + m_model = mdl; + m_c.model_updated(mdl); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_assignment[i] = is_true(m_soft[i]); + } + // TODO: DEBUG verify assignment + m_upper = upper; + trace_bounds("mss-solver"); + } + + bool is_true(model* mdl, expr* e) { + expr_ref tmp(m); + return mdl->eval(e, tmp, true) && m.is_true(tmp); + } + + bool is_true(expr* e) { + return is_true(m_model.get(), e); + } +}; + +maxsmt_solver_base* opt::mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { + return alloc(mss_solver, c, id, ws, soft); +} diff --git a/src/opt/mss_solver.h b/src/opt/mss_solver.h new file mode 100755 index 000000000..5c274cd4c --- /dev/null +++ b/src/opt/mss_solver.h @@ -0,0 +1,12 @@ +#ifndef MSS_SOLVER_H_ +#define MSS_SOLVER_H_ + +#include "opt/maxsmt.h" + +namespace opt { + + maxsmt_solver_base* mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft); + +} + +#endif diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 1d6d7ee6a..4cb22389d 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -2,13 +2,13 @@ def_module_params('opt', description='optimization parameters', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), - ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), - ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), + ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), @@ -20,8 +20,8 @@ def_module_params('opt', ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'), ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'), - ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core') - + ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'), + ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate') )) From 3a7efb91ae073c346716b4213c06d32fc39510a6 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Fri, 16 Feb 2018 19:48:29 +0000 Subject: [PATCH 02/30] implemented CLD --- src/opt/mss.cpp | 12 ++++---- src/opt/mss_solver.cpp | 62 ++++++++++++++++++++++++++++++++++++++---- 2 files changed, 62 insertions(+), 12 deletions(-) diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp index cc0fa8d7d..47f4b6e02 100644 --- a/src/opt/mss.cpp +++ b/src/opt/mss.cpp @@ -155,10 +155,10 @@ namespace opt { lbool is_sat = l_true; for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) { bool has_mcs = false; - bool is_last = i + 1 < m_cores.size(); + bool not_last = i + 1 < m_cores.size(); SASSERT(check_invariant()); update_core(m_cores[i]); // remove members of mss - is_sat = process_core(1, m_cores[i], has_mcs, is_last); + is_sat = process_core(1, m_cores[i], has_mcs, not_last); } if (is_sat == l_true) { SASSERT(check_invariant()); @@ -183,7 +183,7 @@ namespace opt { // at least one literal in core is false in current model. // pick literals in core that are not yet in mss. // - lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) { + lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) { SASSERT(sz > 0); if (core.empty()) { return l_true; @@ -191,7 +191,7 @@ namespace opt { if (m.canceled()) { return l_undef; } - if (sz == 1 && core.size() == 1 && is_last && !has_mcs) { + if (sz == 1 && core.size() == 1 && not_last && !has_mcs) { // there has to be at least one false // literal in the core. TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";); @@ -214,7 +214,7 @@ namespace opt { SASSERT(m_mss_set.contains(core[i])); }); update_core(core); - return process_core(2*sz, core, has_mcs, is_last); + return process_core(2*sz, core, has_mcs, not_last); case l_false: if (sz == 1) { has_mcs = true; @@ -232,7 +232,7 @@ namespace opt { } update_core(core); } - return process_core(1, core, has_mcs, is_last); + return process_core(1, core, has_mcs, not_last); case l_undef: return l_undef; } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index 501b43ee4..d27b6300c 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -98,15 +98,61 @@ private: vector dummy; push_exprs(mss, m_asms); push_exprs(mss, asms); - is_sat = m_mss(mdl.get(), dummy, mss, mcs); - SASSERT(is_sat == l_true); - mdl.reset(); - m_mss.get_model(mdl); - update_assignment(mdl.get()); - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + is_sat = cld(mdl.get(), mss, mcs); + if (is_sat == l_true) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + } + /*is_sat = m_mss(mdl.get(), dummy, mss, mcs); + SASSERT(is_sat != l_false); + if (is_sat == l_true) { + mdl.reset(); + m_mss.get_model(mdl); + update_assignment(mdl.get()); + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + }*/ return is_sat; } + lbool cld(model_ref initial_model, exprs& mss, exprs& mcs) { + exprs sat, undef; + undef.append(mss); + update_sat(initial_model, sat, undef); + lbool is_sat = l_true; + while (is_sat == l_true) { + expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); + sat.push_back(asum); + is_sat = check_sat(sat); + sat.pop_back(); + if (is_sat == l_true) { + model_ref mdl; + s().get_model(mdl); + update_sat(mdl, sat, undef); + update_assignment(mdl.get()); + } + } + if (is_sat == l_false) { + mss.reset(); + mcs.reset(); + mss.append(sat); + mcs.append(undef); + is_sat = l_true; + } + return is_sat; + } + + void update_sat(model_ref mdl, exprs& sat, exprs& undef) { + for (unsigned i = 0; i < undef.size();) { + if (is_true(mdl.get(), undef[i])) { + sat.push_back(undef[i]); + undef[i] = undef.back(); + undef.pop_back(); + } + else { + ++i; + } + } + } + void push_exprs(exprs& dst, expr_ref_vector const& src) { for (unsigned i = 0; i < src.size(); ++i) { dst.push_back(src[i]); @@ -122,6 +168,10 @@ private: return s().check_sat(asms); } + lbool check_sat(exprs const& asms) { + return s().check_sat(asms.size(), asms.c_ptr()); + } + void update_assignment(model* mdl) { rational upper(0); for (unsigned i = 0; i < m_soft.size(); ++i) { From e5aa79ba6a1f1e5e5ba38716c71247ccb70c0391 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Mon, 19 Feb 2018 13:29:15 +0000 Subject: [PATCH 03/30] disjoint cores --- src/opt/mss_solver.cpp | 221 +++++++++++++++++++++++++++++------------ src/opt/opt_params.pyg | 3 +- 2 files changed, 161 insertions(+), 63 deletions(-) diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index d27b6300c..1ac351855 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -11,45 +11,85 @@ class mss_solver: public maxsmt_solver_base { private: typedef ptr_vector exprs; + typedef obj_hashtable expr_set; mss m_mss; unsigned m_index; - expr_ref_vector m_asms; + exprs m_asms; + unsigned m_mss_found; + vector m_cores; + unsigned m_core_idx; + model_ref m_last_model; + exprs m_mss_trail; + exprs m_mcs_trail; + unsigned_vector m_mss_trail_lim; + unsigned_vector m_mcs_trail_lim; unsigned m_max_mss; + bool m_disjoint_cores; public: mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft): maxsmt_solver_base(c, ws, soft), m_mss(c.get_solver(), m), m_index(id), - m_asms(m), - m_max_mss(UINT_MAX) { + m_mss_found(0), + m_core_idx(0), + m_max_mss(UINT_MAX), + m_disjoint_cores(false) { } virtual ~mss_solver() {} virtual lbool operator()() { if (!init()) return l_undef; - init_asms(); - lbool is_sat = check_sat(m_asms); - if (is_sat == l_undef) return l_undef; - if (is_sat == l_true) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";); - model_ref mdl; - s().get_model(mdl); - update_assignment(mdl.get()); - return l_true; + init_local(); + lbool is_sat = disjoint_cores(); + if (is_sat != l_true) return is_sat; + if (m_cores.size() == 0) return l_true; + update_model(); + exprs asms; + while (true) { + exprs mss, mcs; + mss.append(m_cores[m_core_idx]); + is_sat = cld(m_last_model, mss, mcs); + if (is_sat == l_undef || m.canceled()) return l_undef; + SASSERT(is_sat == l_true); + update_trails(mss, mcs); + if (m_core_idx < m_cores.size()-1) { + m_core_idx++; + } + else { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_mss_trail.size() + m_asms.size() << " :mcs " << m_mcs_trail.size() << ")\n";); + if (++m_mss_found >= m_max_mss) return l_true; + asms.push_back(relax_and_assert(m.mk_or(m_mcs_trail.size(), m_mcs_trail.c_ptr()))); + is_sat = backtrack(asms); + if (is_sat == l_false) { + SASSERT(m_core_idx == 0); + is_sat = disjoint_cores(asms); + } + if (is_sat == l_undef) return l_undef; + if (is_sat == l_false) return l_true; + } } - return enumerate_mss(); + return l_true; } virtual void updt_params(params_ref& p) { maxsmt_solver_base::updt_params(p); opt_params _p(p); m_max_mss = _p.mss_max(); + m_disjoint_cores = _p.mss_disjoint_cores(); } private: - void init_asms() { + void init_local() { + m_cores.reset(); + m_core_idx = 0; + m_mss_found = 0; + m_last_model.reset(); + m_mss_trail.reset(); + m_mcs_trail.reset(); + m_mss_trail_lim.reset(); + m_mcs_trail_lim.reset(); m_asms.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { expr* e = m_soft[i]; @@ -74,42 +114,84 @@ private: return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); } - lbool enumerate_mss() { - expr_ref_vector asms(m); - for (unsigned i = 0; i < m_max_mss; ++i) { - exprs mss, mcs; - lbool is_sat = next_mss(asms, mss, mcs); - if (is_sat == l_false && i == 0) return l_false; - if (is_sat == l_undef && i == 0) return l_undef; - if (is_sat == l_false || is_sat == l_undef) return l_true; - asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr()))); + lbool disjoint_cores(exprs const& asms) { + expr_set asm_lits, core_lits; + for (unsigned i = 0; i < asms.size(); ++i) { + asm_lits.insert(asms[i]); } - return l_true; + lbool is_sat = l_false; + exprs core; + while (is_sat == l_false) { + exprs tmp_asms; + tmp_asms.append(asms); + tmp_asms.append(m_asms); + is_sat = check_sat(tmp_asms); + if (is_sat == l_true) { + update_model(); + } + else if (is_sat == l_false) { + core.reset(); + s().get_unsat_core(core); + for (unsigned i = 0; i < core.size();) { + if (asm_lits.contains(core[i])) { + core[i] = core.back(); + core.pop_back(); + } + else { + core_lits.insert(core[i]); + ++i; + } + } + if (core.empty()) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver empty core)\n";); + return l_false; + } + if (m_disjoint_cores) { + m_cores.push_back(core); + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :core-size " << core.size() << " :num-cores " << m_cores.size() << ")\n";); + for (unsigned i = 0; i < m_asms.size();) { + if (core_lits.contains(m_asms[i]) || !m_disjoint_cores) { + m_asms[i] = m_asms.back(); + m_asms.pop_back(); + } + else { + ++i; + } + } + } + else { + m_cores.push_back(m_asms); + m_asms.reset(); + } + } + } + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :num-cores " << m_cores.size() << ")\n";); + // TODO: update m_lower? + return is_sat; } - lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) { - mss.reset(); - mcs.reset(); - lbool is_sat = check_sat(asms); - if (is_sat != l_true) return is_sat; - model_ref mdl; - s().get_model(mdl); - update_assignment(mdl.get()); - vector dummy; - push_exprs(mss, m_asms); - push_exprs(mss, asms); - is_sat = cld(mdl.get(), mss, mcs); - if (is_sat == l_true) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + lbool disjoint_cores() { + return disjoint_cores(exprs()); + } + + lbool backtrack(exprs& asms) { + SASSERT(m_mss_trail_lim.size() == m_mcs_trail_lim.size()); + lbool is_sat = l_false; + while (is_sat == l_false && m_core_idx > 0) { + m_core_idx--; + m_mss_trail.resize(m_mss_trail_lim.back()); + m_mss_trail_lim.pop_back(); + m_mcs_trail.resize(m_mcs_trail_lim.back()); + m_mcs_trail_lim.pop_back(); + exprs tmp_asms; + tmp_asms.append(asms); + get_trail_asms(tmp_asms); + is_sat = check_sat(tmp_asms); + if (is_sat == l_true) { + update_model(); + } } - /*is_sat = m_mss(mdl.get(), dummy, mss, mcs); - SASSERT(is_sat != l_false); - if (is_sat == l_true) { - mdl.reset(); - m_mss.get_model(mdl); - update_assignment(mdl.get()); - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); - }*/ + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";); return is_sat; } @@ -118,19 +200,19 @@ private: undef.append(mss); update_sat(initial_model, sat, undef); lbool is_sat = l_true; - while (is_sat == l_true) { + while (is_sat == l_true && !undef.empty()) { expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); - sat.push_back(asum); - is_sat = check_sat(sat); - sat.pop_back(); + exprs asms; + asms.append(sat); + get_trail_asms(asms); + asms.push_back(asum); + is_sat = check_sat(asms); if (is_sat == l_true) { - model_ref mdl; - s().get_model(mdl); - update_sat(mdl, sat, undef); - update_assignment(mdl.get()); + update_model(); + update_sat(m_last_model, sat, undef); } } - if (is_sat == l_false) { + if (is_sat == l_false || undef.empty()) { mss.reset(); mcs.reset(); mss.append(sat); @@ -140,6 +222,26 @@ private: return is_sat; } + void get_trail_asms(exprs& asms) { + asms.append(m_mss_trail); + for (unsigned i = 0; i < m_mcs_trail.size(); ++i) { + asms.push_back(m.mk_not(m_mcs_trail[i])); + } + } + + void update_trails(exprs const& mss, exprs const& mcs) { + m_mss_trail_lim.push_back(m_mss_trail.size()); + m_mcs_trail_lim.push_back(m_mcs_trail.size()); + m_mss_trail.append(mss); + m_mcs_trail.append(mcs); + } + + void update_model() { + m_last_model.reset(); + s().get_model(m_last_model); + update_assignment(m_last_model.get()); + } + void update_sat(model_ref mdl, exprs& sat, exprs& undef) { for (unsigned i = 0; i < undef.size();) { if (is_true(mdl.get(), undef[i])) { @@ -160,12 +262,7 @@ private: } lbool check_sat() { - expr_ref_vector dummy(m); - return check_sat(dummy); - } - - lbool check_sat(expr_ref_vector const& asms) { - return s().check_sat(asms); + return check_sat(exprs()); } lbool check_sat(exprs const& asms) { @@ -186,7 +283,7 @@ private: for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); } - // TODO: DEBUG verify assignment + // TODO: DEBUG verify assignment? m_upper = upper; trace_bounds("mss-solver"); } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 4cb22389d..41548452a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -21,7 +21,8 @@ def_module_params('opt', ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'), ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'), ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'), - ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate') + ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate'), + ('mss.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores') )) From dab8e49e2240bc5144940b9df2689967b78136ca Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 16 Apr 2018 18:28:13 +0100 Subject: [PATCH 04/30] Fixed corner-case in fp.to_ubv. --- src/ast/fpa/fpa2bv_converter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d23794e54..b079fc2ca 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3252,7 +3252,9 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args expr_ref ul(m), in_range(m); if (!is_signed) { ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz))); - in_range = m.mk_and(m.mk_not(x_is_neg), m.mk_not(ovfl), + in_range = m.mk_and(m.mk_or(m.mk_not(x_is_neg), + m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz+3))), + m.mk_not(ovfl), m_bv_util.mk_ule(pre_rounded, ul)); } else { From 6224db71f32db0ff2308fb0c993f556e7b595f41 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Apr 2018 07:18:33 -0700 Subject: [PATCH 05/30] fix #1579 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index aabe43110..6ae63a1a6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1350,9 +1350,10 @@ void cmd_context::restore_func_decls(unsigned old_sz) { } void cmd_context::restore_psort_inst(unsigned old_sz) { - for (unsigned i = old_sz; i < m_psort_inst_stack.size(); ++i) { + for (unsigned i = m_psort_inst_stack.size(); i-- > old_sz; ) { pdecl * s = m_psort_inst_stack[i]; - s->reset_cache(*m_pmanager); + s->reset_cache(pm()); + pm().dec_ref(s); } m_psort_inst_stack.resize(old_sz); } @@ -2024,8 +2025,8 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) { } } if (m_owner.m_scopes.size() > 0) { + m_owner.pm().inc_ref(pd); m_owner.m_psort_inst_stack.push_back(pd); - } } From 97cee7d0a46b2b26d2d15d62ebee791096ecbe58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Apr 2018 07:30:26 -0700 Subject: [PATCH 06/30] fix #1576, hopefully Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_util.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index e8a1c5139..88b4c398d 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -31,6 +31,7 @@ Revision History: #include "muz/base/dl_rule.h" #include "muz/base/dl_util.h" #include "util/stopwatch.h" +#include namespace datalog { @@ -623,9 +624,9 @@ namespace datalog { bool string_to_uint64(const char * s, uint64_t & res) { #if _WINDOWS - int converted = sscanf_s(s, "%I64u", &res); + int converted = sscanf_s(s, "%" SCNu64, &res); #else - int converted = sscanf(s, "%I64u", &res); + int converted = sscanf(s, "%" SCNu64, &res); #endif if(converted==0) { return false; From 393d25f661024677fd5d80b8fd3a3e476de8afd6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Apr 2018 21:12:43 -0700 Subject: [PATCH 07/30] add web assembly link Signed-off-by: Nikolaj Bjorner --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 8ebf6a078..54804175d 100644 --- a/README.md +++ b/README.md @@ -189,3 +189,7 @@ python -c 'import z3; print(z3.get_version_string())' See [``examples/python``](examples/python) for examples. +### ``Web Assembly`` + +[WebAssembly](https://github.com/cpitclaudel/z3.wasm) +Web Assembly bindings are provided by Clément Pit-Claudel. From b79440a21d404bcf0c2e34e83f1c04555342cfb9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Apr 2018 21:13:24 -0700 Subject: [PATCH 08/30] add web assembly link Signed-off-by: Nikolaj Bjorner --- README.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/README.md b/README.md index 54804175d..447034a84 100644 --- a/README.md +++ b/README.md @@ -191,5 +191,4 @@ See [``examples/python``](examples/python) for examples. ### ``Web Assembly`` -[WebAssembly](https://github.com/cpitclaudel/z3.wasm) -Web Assembly bindings are provided by Clément Pit-Claudel. +[WebAssembly](https://github.com/cpitclaudel/z3.wasm) bindings are provided by Clément Pit-Claudel. From f22abaa7135f46953211fc304aa51e938e0d0948 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Apr 2018 11:44:30 +0300 Subject: [PATCH 09/30] enable patterns on equality, add trace for variables for axiom profiling. Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 7 ++++++- src/parsers/util/pattern_validation.cpp | 2 +- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7e143e1a3..12ca136c5 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2254,7 +2254,12 @@ var * ast_manager::mk_var(unsigned idx, sort * s) { unsigned sz = var::get_obj_size(); void * mem = allocate_node(sz); var * new_node = new (mem) var(idx, s); - return register_node(new_node); + var * r = register_node(new_node); + + if (m_trace_stream && r == new_node) { + *m_trace_stream << "[mk-var] #" << r->get_id() << "\n"; + } + return r; } app * ast_manager::mk_label(bool pos, unsigned num_names, symbol const * names, expr * n) { diff --git a/src/parsers/util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp index 0d076aadd..df1f6cd00 100644 --- a/src/parsers/util/pattern_validation.cpp +++ b/src/parsers/util/pattern_validation.cpp @@ -48,7 +48,7 @@ struct pattern_validation_functor { bool is_forbidden(func_decl const * decl) { family_id fid = decl->get_family_id(); - if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE) + if (fid == m_bfid && decl->get_decl_kind() != OP_EQ && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE) return true; if (fid == m_lfid) return true; From 279f1986a6e2d337c7ed5eb2d5033696906e846c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Apr 2018 07:11:15 +0200 Subject: [PATCH 10/30] fix #1575, fix #1585 Signed-off-by: Nikolaj Bjorner --- src/ast/pattern/expr_pattern_match.cpp | 2 +- src/cmd_context/cmd_context.cpp | 7 ++++--- src/smt/theory_seq.cpp | 11 +++++++++-- src/smt/theory_seq.h | 13 +++++++------ 4 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index d688c840c..c441fb4ce 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -387,7 +387,7 @@ expr_pattern_match::initialize(char const * spec_string) { m_instrs.push_back(instr(BACKTRACK)); std::istringstream is(spec_string); - cmd_context ctx(true, &m_manager); + cmd_context ctx(true, &m_manager); bool ps = ctx.print_success_enabled(); ctx.set_print_success(false); VERIFY(parse_smt2_commands(ctx, is)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6ae63a1a6..11f800b25 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -718,8 +718,8 @@ void cmd_context::init_manager_core(bool new_manager) { } m_dt_eh = alloc(dt_eh, *this); m_pmanager->set_new_datatype_eh(m_dt_eh.get()); - if (!has_logic()) { - TRACE("cmd_context", tout << "init manager\n";); + if (!has_logic() && new_manager) { + TRACE("cmd_context", tout << "init manager " << m_logic << "\n";); // add list type only if the logic is not specified. // it prevents clashes with builtin types. insert(pm().mk_plist_decl()); @@ -757,6 +757,7 @@ void cmd_context::init_external_manager() { } bool cmd_context::set_logic(symbol const & s) { + TRACE("cmd_context", tout << s << "\n";); if (has_logic()) throw cmd_exception("the logic has already been set"); if (has_manager() && m_main_ctx) @@ -1240,7 +1241,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) { m_aux_pdecls.push_back(p); } -void cmd_context::reset(bool finalize) { +void cmd_context::reset(bool finalize) { m_processing_pareto = false; m_logic = symbol::null; m_check_sat_result = nullptr; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 94841603d..ff5bb4486 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1473,7 +1473,7 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) { if (l == r) { return false; } - TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";); + TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n"; display_deps(tout, deps);); m_new_solution = true; m_rep.update(l, r, deps); enode* n1 = ensure_enode(l); @@ -1513,7 +1513,9 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de change = canonize(r, rs, dep2) || change; deps = m_dm.mk_join(dep2, deps); TRACE("seq", tout << l << " = " << r << " ==> "; - tout << ls << " = " << rs << "\n";); + tout << ls << " = " << rs << "\n"; + display_deps(tout, deps); + ); if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) { return true; } @@ -2674,7 +2676,12 @@ void theory_seq::init_model(expr_ref_vector const& es) { } } +void theory_seq::finalize_model(model_generator& mg) { + m_rep.pop_scope(1); +} + void theory_seq::init_model(model_generator & mg) { + m_rep.push_scope(); m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); for (ne const& n : m_nqs) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 21aedd7e3..a17b29eba 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -64,14 +64,14 @@ namespace smt { // + a cache for normalization. class solution_map { enum map_update { INS, DEL }; - ast_manager& m; + ast_manager& m; dependency_manager& m_dm; - eqdep_map_t m_map; - eval_cache m_cache; - expr_ref_vector m_lhs, m_rhs; + eqdep_map_t m_map; + eval_cache m_cache; + expr_ref_vector m_lhs, m_rhs; ptr_vector m_deps; - svector m_updates; - unsigned_vector m_limit; + svector m_updates; + unsigned_vector m_limit; void add_trail(map_update op, expr* l, expr* r, dependency* d); public: @@ -362,6 +362,7 @@ namespace smt { void collect_statistics(::statistics & st) const override; model_value_proc * mk_value(enode * n, model_generator & mg) override; void init_model(model_generator & mg) override; + void finalize_model(model_generator & mg) override; void init_search_eh() override; void init_model(expr_ref_vector const& es); From 0b4e54be38c73c65bf51184828fae54f07f162cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Apr 2018 07:15:04 +0200 Subject: [PATCH 11/30] fix #1583 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 186abda48..e5cac969f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -367,6 +367,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); return mk_re_concat(args[0], args[1], result); case OP_RE_UNION: + if (num_args == 1) { + result = args[0]; return BR_DONE; + } SASSERT(num_args == 2); return mk_re_union(args[0], args[1], result); case OP_RE_RANGE: From 480e1c4daba6a9f5cae5a7c12010613e88584cae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Apr 2018 07:20:24 +0200 Subject: [PATCH 12/30] add warning message for optimization with quantifiers. Fix #1580 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1950a199d..69177e290 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -265,6 +265,9 @@ namespace opt { normalize(); internalize(); update_solver(); + if (contains_quantifiers()) { + warning_msg("optimization with quantified constraints is not supported"); + } #if 0 if (is_qsat_opt()) { return run_qsat_opt(); @@ -368,7 +371,6 @@ namespace opt { if (result == l_true && committed) m_optsmt.commit_assignment(index); if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) { throw default_exception("unbounded objectives on quantified constraints is not supported"); - result = l_undef; } return result; } From 19bb883263d6c38fe6e8af85fcbc0a9c32f27149 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Apr 2018 12:12:39 +0200 Subject: [PATCH 13/30] fix #1581 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ff5bb4486..db8dbd340 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2360,9 +2360,21 @@ bool theory_seq::check_int_string() { void theory_seq::add_stoi_axiom(expr* e) { TRACE("seq", tout << mk_pp(e, m) << "\n";); - SASSERT(m_util.str.is_stoi(e)); - literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1))); + expr* s = nullptr; + VERIFY (m_util.str.is_stoi(e, s)); + + // stoi(s) >= -1 + literal l = mk_simplified_literal(m_autil.mk_ge(e, m_autil.mk_int(-1))); add_axiom(l); + + // stoi(s) >= 0 <=> s in (0-9)+ + expr_ref num_re(m); + num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9"))); + num_re = m_util.re.mk_plus(num_re); + app_ref in_re(m_util.re.mk_in_re(s, num_re), m); + literal ge0 = mk_simplified_literal(m_autil.mk_ge(e, m_autil.mk_int(0))); + add_axiom(~ge0, mk_literal(in_re)); + add_axiom(ge0, ~mk_literal(in_re)); } bool theory_seq::add_stoi_val_axiom(expr* e) { @@ -2406,8 +2418,9 @@ bool theory_seq::add_stoi_val_axiom(expr* e) { lits.push_back(~is_digit(ith_char)); nums.push_back(digit2int(ith_char)); } - for (unsigned i = sz, c = 1; i-- > 0; c *= 10) { - coeff = m_autil.mk_int(c); + rational c(1); + for (unsigned i = sz; i-- > 0; c *= rational(10)) { + coeff = m_autil.mk_numeral(c, true); nums[i] = m_autil.mk_mul(coeff, nums[i].get()); } num = m_autil.mk_add(nums.size(), nums.c_ptr()); @@ -3482,8 +3495,8 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { literal_vector lits; lits.push_back(~lit); - for (unsigned i = 0; i < states.size(); ++i) { - lits.push_back(mk_accept(e1, zero, e3, states[i])); + for (unsigned s : states) { + lits.push_back(mk_accept(e1, zero, e3, s)); } if (lits.size() == 2) { propagate_lit(nullptr, 1, &lit, lits[1]); From 5166b96d206dcb03e358d3aaeaae06123f8281cd Mon Sep 17 00:00:00 2001 From: bannsec Date: Mon, 23 Apr 2018 17:17:51 -0400 Subject: [PATCH 14/30] Fancy dots are not allowed here!! --- src/smt/theory_datatype.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 9ff81fa08..049555297 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -461,7 +461,7 @@ namespace smt { TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";); enode* app_parent = nullptr; - // first: explain that root=v, given that app=cstor(…,v,…) + // first: explain that root=v, given that app=cstor(...,v,...) for (enode * arg : enode::args(oc_get_cstor(app))) { // found an argument which is equal to root if (arg->get_root() == root->get_root()) { From a1d870f19f6638432eb5f15f0f1a59319a9927ab Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 24 Apr 2018 12:43:11 +0100 Subject: [PATCH 15/30] Added tactic for QF_FPLRA --- src/solver/smt_logics.cpp | 11 ++-- src/tactic/fpa/qffplra_tactic.cpp | 72 +++++++++++++++++++++++++ src/tactic/fpa/qffplra_tactic.h | 38 +++++++++++++ src/tactic/portfolio/default_tactic.cpp | 12 +++-- 4 files changed, 123 insertions(+), 10 deletions(-) create mode 100644 src/tactic/fpa/qffplra_tactic.cpp create mode 100644 src/tactic/fpa/qffplra_tactic.h diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 874f1cfcc..7ed2b0445 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -22,14 +22,14 @@ Revision History: bool smt_logics::supported_logic(symbol const & s) { - return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || + return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || logic_has_arith(s) || logic_has_bv(s) || logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) || logic_has_horn(s) || logic_has_fpa(s); } bool smt_logics::logic_has_reals_only(symbol const& s) { - return + return s == "QF_RDL" || s == "QF_LRA" || s == "UFLRA" || @@ -84,8 +84,9 @@ bool smt_logics::logic_has_arith(symbol const & s) { s == "QF_BVFP" || s == "QF_S" || s == "ALL" || - s == "QF_FD" || - s == "HORN"; + s == "QF_FD" || + s == "HORN" || + s == "QF_FPLRA"; } bool smt_logics::logic_has_bv(symbol const & s) { @@ -137,7 +138,7 @@ bool smt_logics::logic_has_str(symbol const & s) { } bool smt_logics::logic_has_fpa(symbol const & s) { - return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL"; + return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || s == "ALL"; } bool smt_logics::logic_has_uf(symbol const & s) { diff --git a/src/tactic/fpa/qffplra_tactic.cpp b/src/tactic/fpa/qffplra_tactic.cpp new file mode 100644 index 000000000..947a41111 --- /dev/null +++ b/src/tactic/fpa/qffplra_tactic.cpp @@ -0,0 +1,72 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + qffpalra_tactic.cpp + +Abstract: + + Tactic for QF_FPLRA benchmarks. + +Author: + + Christoph (cwinter) 2018-04-24 + +Notes: + +--*/ +#include "tactic/tactical.h" +#include "tactic/fpa/qffp_tactic.h" +#include "tactic/fpa/qffplra_tactic.h" + +tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p) { + tactic * st = mk_qffp_tactic(m, p); + st->updt_params(p); + return st; +} + +struct is_non_qffplra_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + fpa_util fu; + arith_util au; + + is_non_qffplra_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s)) + throw found(); + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id() || + fid == fu.get_family_id() || + fid == bu.get_family_id() || + fid == au.get_family_id()) + return; + if (is_uninterp_const(n)) + return; + if (au.is_real(s)) + return; + + throw found(); + } +}; + +class is_qffplra_probe : public probe { +public: + result operator()(goal const & g) override { + return !test(g); + } + + ~is_qffplra_probe() override {} +}; + +probe * mk_is_qffplra_probe() { + return alloc(is_qffplra_probe); +} diff --git a/src/tactic/fpa/qffplra_tactic.h b/src/tactic/fpa/qffplra_tactic.h new file mode 100644 index 000000000..b5a741ac3 --- /dev/null +++ b/src/tactic/fpa/qffplra_tactic.h @@ -0,0 +1,38 @@ +#pragma once +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + qffplra_tactic.h + +Abstract: + + Tactic for QF_FPLRA benchmarks. + +Author: + + Christoph (cwinter) 2018-04-24 + +Notes: + + +--*/ +#ifndef QFFPLRA_TACTIC_H_ +#define QFFPLRA_TACTIC_H_ + +#include "util/params.h" +class ast_manager; +class tactic; + +tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* +ADD_TACTIC("qffplra", "(try to) solve goal using the tactic for QF_FPLRA.", "mk_qffplra_tactic(m, p)") +*/ + +probe * mk_is_qffplra_probe(); +/* +ADD_PROBE("is-qffplra", "true if the goal is in QF_FPLRA.", "mk_is_qffplra_probe()") +*/ + +#endif diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 09052869b..5cf06ca86 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -28,24 +28,26 @@ Notes: #include "tactic/arith/probe_arith.h" #include "tactic/smtlogics/quant_tactics.h" #include "tactic/fpa/qffp_tactic.h" +#include "tactic/fpa/qffplra_tactic.h" #include "tactic/smtlogics/qfaufbv_tactic.h" #include "tactic/smtlogics/qfauflia_tactic.h" #include "tactic/smtlogics/qfufnra_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), - cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), - cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), + cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), + cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m), cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m), cond(mk_is_qflra_probe(), mk_qflra_tactic(m), cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m), cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), - cond(mk_is_lira_probe(), mk_lira_tactic(m, p), - cond(mk_is_nra_probe(), mk_nra_tactic(m), + cond(mk_is_lira_probe(), mk_lira_tactic(m, p), + cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), + cond(mk_is_qffplra_probe(), mk_qffplra_tactic(m, p), //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), - mk_smt_tactic()))))))))))), + mk_smt_tactic())))))))))))), p); return st; } From e13f3d92af517c6caeceec77f7bdaf4560323a17 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 24 Apr 2018 15:01:05 +0100 Subject: [PATCH 16/30] Updated CMakelists.txt --- src/tactic/fpa/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt index a54212235..c647df7fc 100644 --- a/src/tactic/fpa/CMakeLists.txt +++ b/src/tactic/fpa/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(fpa_tactics fpa2bv_model_converter.cpp fpa2bv_tactic.cpp qffp_tactic.cpp + qffplra_tactic.cpp COMPONENT_DEPENDENCIES arith_tactics bv_tactics @@ -14,4 +15,5 @@ z3_add_component(fpa_tactics TACTIC_HEADERS fpa2bv_tactic.h qffp_tactic.h + qffplra_tactic.h ) From f7bcf0fd585e3fd7c294d63307356d7357ea3383 Mon Sep 17 00:00:00 2001 From: yxliang01 <13267.okk@gmail.com> Date: Tue, 24 Apr 2018 08:17:20 -0700 Subject: [PATCH 17/30] Z3 now will also try to find libz3 in PYTHONPATH --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 8a7b33efd..78fad45be 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1657,7 +1657,7 @@ else: if hasattr(builtins, "Z3_LIB_DIRS"): _all_dirs = builtins.Z3_LIB_DIRS -for v in ('Z3_LIBRARY_PATH', 'PATH'): +for v in ('Z3_LIBRARY_PATH', 'PATH', 'PYTHONPATH'): if v in os.environ: lp = os.environ[v]; lds = lp.split(';') if sys.platform in ('win32') else lp.split(':') From ab8d3cdc447e278465563294d44c73ea29d098af Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Tue, 24 Apr 2018 17:59:21 +0100 Subject: [PATCH 18/30] WMax conflict budget bug fix --- src/opt/opt_context.cpp | 4 ++-- src/opt/opt_params.pyg | 2 +- src/opt/wmax.cpp | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 2f6bad9e8..4bbbc3865 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -398,10 +398,10 @@ namespace opt { /** \brief there is no need to use push/pop when all objectives are maxsat and engine - is maxres. + is maxres or mss. */ bool context::scoped_lex() { - if (m_maxsat_engine == symbol("maxres")) { + if (m_maxsat_engine == symbol("maxres") || m_maxsat_engine == symbol("mss")) { for (unsigned i = 0; i < m_objectives.size(); ++i) { if (m_objectives[i].m_type != O_MAXSMT) return true; } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 41548452a..e06836f61 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), - ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), + ('priority', SYMBOL, 'lex', "select how to prioritize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 52b87e536..513c68d6e 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -84,6 +84,9 @@ namespace opt { if (m.canceled()) { is_sat = l_undef; } + if (is_sat == l_undef) { + break; + } if (is_sat == l_false) { TRACE("opt", tout << "Unsat\n";); break; @@ -97,9 +100,6 @@ namespace opt { //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); } - else { - //DEBUG_CODE(verify_cores(cores);); - } update_cores(wth(), cores); wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); From b5f067bec539b6cad0987b7b0edb8a1bb721ac61 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Apr 2018 11:18:24 +0200 Subject: [PATCH 19/30] fix #1592 #1587 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_util.cpp | 3 + src/smt/theory_seq.cpp | 143 ++++++-------------------------------- src/smt/theory_seq.h | 1 - src/util/scoped_timer.cpp | 24 ++++--- 4 files changed, 42 insertions(+), 129 deletions(-) diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index 88b4c398d..87cfac04c 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -31,6 +31,9 @@ Revision History: #include "muz/base/dl_rule.h" #include "muz/base/dl_util.h" #include "util/stopwatch.h" +#ifndef __STDC_FORMAT_MACROS +#define __STDC_FORMAT_MACROS +#endif #include namespace datalog { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index db8dbd340..95f804863 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -134,8 +134,7 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) { if (num_scopes == 0) return; m_cache.reset(); unsigned start = m_limit[m_limit.size() - num_scopes]; - for (unsigned i = m_updates.size(); i > start; ) { - --i; + for (unsigned i = m_updates.size(); i-- > start; ) { if (m_updates[i] == INS) { m_map.remove(m_lhs[i].get()); } @@ -436,8 +435,8 @@ bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs if (ls.empty() || !is_var(ls[0])) { return false; } - for (unsigned i = 0; i < rs.size(); ++i) { - if (!m_util.str.is_unit(rs[i])) { + for (expr* r : rs) { + if (!m_util.str.is_unit(r)) { return false; } } @@ -482,8 +481,7 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector bool theory_seq::branch_variable_mb() { bool change = false; - for (unsigned i = 0; i < m_eqs.size(); ++i) { - eq const& e = m_eqs[i]; + for (eq const& e : m_eqs) { vector len1, len2; if (!is_complex(e)) { continue; @@ -2226,63 +2224,7 @@ void theory_seq::internalize_eq_eh(app * atom, bool_var v) { } bool theory_seq::internalize_atom(app* a, bool) { -#if 1 return internalize_term(a); -#else - if (is_skolem(m_eq, a)) { - return internalize_term(a); - } - context & ctx = get_context(); - bool_var bv = ctx.mk_bool_var(a); - ctx.set_var_theory(bv, get_id()); - ctx.mark_as_relevant(bv); - - expr* e1, *e2; - if (m_util.str.is_in_re(a, e1, e2)) { - return internalize_term(to_app(e1)) && internalize_re(e2); - } - if (m_util.str.is_contains(a, e1, e2) || - m_util.str.is_prefix(a, e1, e2) || - m_util.str.is_suffix(a, e1, e2)) { - return internalize_term(to_app(e1)) && internalize_term(to_app(e2)); - } - if (is_accept(a) || is_reject(a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) { - return true; - } - UNREACHABLE(); - return internalize_term(a); -#endif -} - -bool theory_seq::internalize_re(expr* e) { - expr* e1, *e2; - unsigned lc, uc; - if (m_util.re.is_to_re(e, e1)) { - return internalize_term(to_app(e1)); - } - if (m_util.re.is_star(e, e1) || - m_util.re.is_plus(e, e1) || - m_util.re.is_opt(e, e1) || - m_util.re.is_loop(e, e1, lc) || - m_util.re.is_loop(e, e1, lc, uc) || - m_util.re.is_complement(e, e1)) { - return internalize_re(e1); - } - if (m_util.re.is_union(e, e1, e2) || - m_util.re.is_intersection(e, e1, e2) || - m_util.re.is_concat(e, e1, e2)) { - return internalize_re(e1) && internalize_re(e2); - } - if (m_util.re.is_full_seq(e) || - m_util.re.is_full_char(e) || - m_util.re.is_empty(e)) { - return true; - } - if (m_util.re.is_range(e, e1, e2)) { - return internalize_term(to_app(e1)) && internalize_term(to_app(e2)); - } - UNREACHABLE(); - return internalize_term(to_app(e)); } bool theory_seq::internalize_term(app* term) { @@ -2346,8 +2288,8 @@ void theory_seq::add_int_string(expr* e) { bool theory_seq::check_int_string() { bool change = false; - for (unsigned i = 0; i < m_int_string.size(); ++i) { - expr* e = m_int_string[i].get(), *n; + for (expr * e : m_int_string) { + expr* n = nullptr; if (m_util.str.is_itos(e) && add_itos_val_axiom(e)) { change = true; } @@ -3448,8 +3390,8 @@ void theory_seq::add_itos_length_axiom(expr* len) { void theory_seq::propagate_in_re(expr* n, bool is_true) { TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";); - expr* e1 = nullptr, *e2 = nullptr; - VERIFY(m_util.str.is_in_re(n, e1, e2)); + expr* s = nullptr, *re = nullptr; + VERIFY(m_util.str.is_in_re(n, s, re)); expr_ref tmp(n, m); m_rewrite(tmp); @@ -3470,21 +3412,21 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { return; } - expr_ref e3(e2, m); + expr_ref e3(re, m); context& ctx = get_context(); literal lit = ctx.get_literal(n); if (!is_true) { - e3 = m_util.re.mk_complement(e2); + e3 = m_util.re.mk_complement(re); lit.neg(); } eautomaton* a = get_automaton(e3); if (!a) return; - expr_ref len(m_util.str.mk_length(e1), m); + expr_ref len(m_util.str.mk_length(s), m); for (unsigned i = 0; i < a->num_states(); ++i) { - literal acc = mk_accept(e1, len, e3, i); - literal rej = mk_reject(e1, len, e3, i); + literal acc = mk_accept(s, len, e3, i); + literal rej = mk_reject(s, len, e3, i); add_axiom(a->is_final_state(i)?acc:~acc); add_axiom(a->is_final_state(i)?~rej:rej); } @@ -3495,8 +3437,8 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { literal_vector lits; lits.push_back(~lit); - for (unsigned s : states) { - lits.push_back(mk_accept(e1, zero, e3, s)); + for (unsigned st : states) { + lits.push_back(mk_accept(s, zero, e3, st)); } if (lits.size() == 2) { propagate_lit(nullptr, 1, &lit, lits[1]); @@ -3547,8 +3489,8 @@ static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v) bool theory_seq::get_num_value(expr* e, rational& val) const { context& ctx = get_context(); expr_ref _val(m); - if (!ctx.e_internalized(e)) - return false; + if (!ctx.e_internalized(e)) + return false; enode* next = ctx.get_enode(e), *n = next; do { if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) { @@ -3945,8 +3887,8 @@ theory_seq::dependency* theory_seq::mk_join(dependency* deps, literal lit) { } theory_seq::dependency* theory_seq::mk_join(dependency* deps, literal_vector const& lits) { - for (unsigned i = 0; i < lits.size(); ++i) { - deps = mk_join(deps, lits[i]); + for (literal l : lits) { + deps = mk_join(deps, l); } return deps; } @@ -4151,53 +4093,15 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";); m_rewrite(eq); if (!m.is_false(eq)) { - literal lit = mk_eq(e1, e2, false); - if (m_util.str.is_empty(e2)) { std::swap(e1, e2); } - if (false && m_util.str.is_empty(e1)) { - expr_ref head(m), tail(m), conc(m); - mk_decompose(e2, head, tail); - conc = mk_concat(head, tail); - propagate_eq(~lit, e2, conc, true); - } -#if 0 - - // (e1 = "" & e2 = xdz) or (e2 = "" & e1 = xcy) or (e1 = xcy & e2 = xdz & c != d) or (e1 = x & e2 = xdz) or (e2 = x & e1 = xcy) - // e1 = "" or e1 = xcy or e1 = x - // e2 = "" or e2 = xdz or e2 = x - // e1 = xcy or e2 = xdz - // c != d - - sort* char_sort = 0; - expr_ref emp(m); - VERIFY(m_util.is_seq(m.get_sort(e1), char_sort)); - emp = m_util.str.mk_empty(m.get_sort(e1)); - - expr_ref x = mk_skolem(symbol("seq.ne.x"), e1, e2); - expr_ref y = mk_skolem(symbol("seq.ne.y"), e1, e2); - expr_ref z = mk_skolem(symbol("seq.ne.z"), e1, e2); - expr_ref c = mk_skolem(symbol("seq.ne.c"), e1, e2, 0, char_sort); - expr_ref d = mk_skolem(symbol("seq.ne.d"), e1, e2, 0, char_sort); - literal e1_is_emp = mk_seq_eq(e1, emp); - literal e2_is_emp = mk_seq_eq(e2, emp); - literal e1_is_xcy = mk_seq_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y)); - literal e2_is_xdz = mk_seq_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z)); - add_axiom(lit, e1_is_emp, e1_is_xcy, mk_seq_eq(e1, x)); - add_axiom(lit, e2_is_emp, e2_is_xdz, mk_seq_eq(e2, x)); - add_axiom(lit, e1_is_xcy, e2_is_xdz); - add_axiom(lit, ~mk_eq(c, d, false)); -#else - else { - dependency* dep = m_dm.mk_leaf(assumption(~lit)); - m_nqs.push_back(ne(e1, e2, dep)); - solve_nqs(m_nqs.size() - 1); - } -#endif + dependency* dep = m_dm.mk_leaf(assumption(~lit)); + m_nqs.push_back(ne(e1, e2, dep)); + solve_nqs(m_nqs.size() - 1); } } @@ -4528,8 +4432,7 @@ bool theory_seq::add_reject2reject(expr* rej, bool& change) { ensure_nth(~len_le_idx, s, idx); literal_vector eqs; bool has_undef = false; - for (unsigned i = 0; i < mvs.size(); ++i) { - eautomaton::move const& mv = mvs[i]; + for (eautomaton::move const& mv : mvs) { literal eq = mk_literal(mv.t()->accept(nth)); switch (ctx.get_assignment(eq)) { case l_false: diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index a17b29eba..b6b553dec 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -390,7 +390,6 @@ namespace smt { vector const& ll, vector const& rl); bool set_empty(expr* x); bool is_complex(eq const& e); - bool internalize_re(expr* e); bool check_extensionality(); bool check_contains(); diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index a2a0cc269..56d40c47a 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -208,14 +208,22 @@ struct scoped_timer::imp { pthread_cond_signal(&m_condition_var); pthread_mutex_unlock(&m_mutex); - if (pthread_join(m_thread_id, nullptr) != 0) - throw default_exception("failed to join thread"); - if (pthread_mutex_destroy(&m_mutex) != 0) - throw default_exception("failed to destroy pthread mutex"); - if (pthread_cond_destroy(&m_condition_var) != 0) - throw default_exception("failed to destroy pthread condition variable"); - if (pthread_attr_destroy(&m_attributes) != 0) - throw default_exception("failed to destroy pthread attributes object"); + if (pthread_join(m_thread_id, nullptr) != 0) { + warning_msg("failed to join thread"); + return; + } + if (pthread_mutex_destroy(&m_mutex) != 0) { + warning_msg("failed to destroy pthread mutex"); + return; + } + if (pthread_cond_destroy(&m_condition_var) != 0) { + warning_msg("failed to destroy pthread condition variable"); + return; + } + if (pthread_attr_destroy(&m_attributes) != 0) { + warning_msg("failed to destroy pthread attributes object"); + return; + } #elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_) // Linux & FreeBSD & NetBSD bool init = false; From cf2258a536287cb13cefb882e1277a035d715996 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Apr 2018 08:39:35 +0200 Subject: [PATCH 20/30] fix #1594 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index b592b719a..381339768 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -256,6 +256,7 @@ bool zstring::contains(zstring const& other) const { int zstring::indexof(zstring const& other, int offset) const { SASSERT(offset >= 0); + if (static_cast(offset) <= length() && other.length() == 0) return offset; if (static_cast(offset) == length()) return -1; if (other.length() + offset > length()) return -1; unsigned last = length() - other.length(); From a04921dafe04c3be3a02ca8ba2a90d8213c1309a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Apr 2018 08:47:05 +0200 Subject: [PATCH 21/30] fix #1595 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 381339768..cd8571a95 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -177,7 +177,7 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { return zstring(*this); } if (src.length() == 0) { - return zstring(*this); + return dst + zstring(*this); } bool found = false; for (unsigned i = 0; i < length(); ++i) { From 74292a48e5b8e0a6ebfa47b5f42ea67f13bd602c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Apr 2018 09:08:34 +0200 Subject: [PATCH 22/30] change order of concatentation for empty string, #1595 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e5cac969f..3ead59833 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -856,7 +856,7 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu return BR_DONE; } if (m_util.str.is_string(b, s2) && s2.length() == 0) { - result = m_util.str.mk_concat(a, c); + result = m_util.str.mk_concat(c, a); return BR_REWRITE1; } if (m_util.str.is_string(a, s1) && s1.length() == 0) { From 047f6c558c156ebe5e116c7d9f26e70026007336 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 26 Apr 2018 16:36:14 -0400 Subject: [PATCH 23/30] fix memory leak related to #1575 --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0f9d42b3d..126594b06 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8096,7 +8096,7 @@ namespace smt { rational nn1Len, nn2Len; bool nn1Len_exists = get_len_value(lhs, nn1Len); bool nn2Len_exists = get_len_value(rhs, nn2Len); - expr * emptyStr = mk_string(""); + expr_ref emptyStr(mk_string(""), m); if (nn1Len_exists && nn1Len.is_zero()) { if (!in_same_eqc(lhs, emptyStr) && rhs != emptyStr) { From 37852807b0fa0fb0ee1799dbc2c46df46b89ac47 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:39:45 +0100 Subject: [PATCH 24/30] Revert "WMax conflict budget bug fix" This reverts commit ab8d3cdc447e278465563294d44c73ea29d098af. --- src/opt/opt_context.cpp | 4 ++-- src/opt/opt_params.pyg | 2 +- src/opt/wmax.cpp | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 4bbbc3865..2f6bad9e8 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -398,10 +398,10 @@ namespace opt { /** \brief there is no need to use push/pop when all objectives are maxsat and engine - is maxres or mss. + is maxres. */ bool context::scoped_lex() { - if (m_maxsat_engine == symbol("maxres") || m_maxsat_engine == symbol("mss")) { + if (m_maxsat_engine == symbol("maxres")) { for (unsigned i = 0; i < m_objectives.size(); ++i) { if (m_objectives[i].m_type != O_MAXSMT) return true; } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index e06836f61..41548452a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), - ('priority', SYMBOL, 'lex', "select how to prioritize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), + ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 513c68d6e..52b87e536 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -84,9 +84,6 @@ namespace opt { if (m.canceled()) { is_sat = l_undef; } - if (is_sat == l_undef) { - break; - } if (is_sat == l_false) { TRACE("opt", tout << "Unsat\n";); break; @@ -100,6 +97,9 @@ namespace opt { //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); } + else { + //DEBUG_CODE(verify_cores(cores);); + } update_cores(wth(), cores); wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); From bf2a031f7bb728aaabbc2103df75f684c516c0f6 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:39:55 +0100 Subject: [PATCH 25/30] Revert "disjoint cores" This reverts commit e5aa79ba6a1f1e5e5ba38716c71247ccb70c0391. --- src/opt/mss_solver.cpp | 221 ++++++++++++----------------------------- src/opt/opt_params.pyg | 3 +- 2 files changed, 63 insertions(+), 161 deletions(-) diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index 1ac351855..d27b6300c 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -11,85 +11,45 @@ class mss_solver: public maxsmt_solver_base { private: typedef ptr_vector exprs; - typedef obj_hashtable expr_set; mss m_mss; unsigned m_index; - exprs m_asms; - unsigned m_mss_found; - vector m_cores; - unsigned m_core_idx; - model_ref m_last_model; - exprs m_mss_trail; - exprs m_mcs_trail; - unsigned_vector m_mss_trail_lim; - unsigned_vector m_mcs_trail_lim; + expr_ref_vector m_asms; unsigned m_max_mss; - bool m_disjoint_cores; public: mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft): maxsmt_solver_base(c, ws, soft), m_mss(c.get_solver(), m), m_index(id), - m_mss_found(0), - m_core_idx(0), - m_max_mss(UINT_MAX), - m_disjoint_cores(false) { + m_asms(m), + m_max_mss(UINT_MAX) { } virtual ~mss_solver() {} virtual lbool operator()() { if (!init()) return l_undef; - init_local(); - lbool is_sat = disjoint_cores(); - if (is_sat != l_true) return is_sat; - if (m_cores.size() == 0) return l_true; - update_model(); - exprs asms; - while (true) { - exprs mss, mcs; - mss.append(m_cores[m_core_idx]); - is_sat = cld(m_last_model, mss, mcs); - if (is_sat == l_undef || m.canceled()) return l_undef; - SASSERT(is_sat == l_true); - update_trails(mss, mcs); - if (m_core_idx < m_cores.size()-1) { - m_core_idx++; - } - else { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_mss_trail.size() + m_asms.size() << " :mcs " << m_mcs_trail.size() << ")\n";); - if (++m_mss_found >= m_max_mss) return l_true; - asms.push_back(relax_and_assert(m.mk_or(m_mcs_trail.size(), m_mcs_trail.c_ptr()))); - is_sat = backtrack(asms); - if (is_sat == l_false) { - SASSERT(m_core_idx == 0); - is_sat = disjoint_cores(asms); - } - if (is_sat == l_undef) return l_undef; - if (is_sat == l_false) return l_true; - } + init_asms(); + lbool is_sat = check_sat(m_asms); + if (is_sat == l_undef) return l_undef; + if (is_sat == l_true) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";); + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl.get()); + return l_true; } - return l_true; + return enumerate_mss(); } virtual void updt_params(params_ref& p) { maxsmt_solver_base::updt_params(p); opt_params _p(p); m_max_mss = _p.mss_max(); - m_disjoint_cores = _p.mss_disjoint_cores(); } private: - void init_local() { - m_cores.reset(); - m_core_idx = 0; - m_mss_found = 0; - m_last_model.reset(); - m_mss_trail.reset(); - m_mcs_trail.reset(); - m_mss_trail_lim.reset(); - m_mcs_trail_lim.reset(); + void init_asms() { m_asms.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { expr* e = m_soft[i]; @@ -114,84 +74,42 @@ private: return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); } - lbool disjoint_cores(exprs const& asms) { - expr_set asm_lits, core_lits; - for (unsigned i = 0; i < asms.size(); ++i) { - asm_lits.insert(asms[i]); + lbool enumerate_mss() { + expr_ref_vector asms(m); + for (unsigned i = 0; i < m_max_mss; ++i) { + exprs mss, mcs; + lbool is_sat = next_mss(asms, mss, mcs); + if (is_sat == l_false && i == 0) return l_false; + if (is_sat == l_undef && i == 0) return l_undef; + if (is_sat == l_false || is_sat == l_undef) return l_true; + asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr()))); } - lbool is_sat = l_false; - exprs core; - while (is_sat == l_false) { - exprs tmp_asms; - tmp_asms.append(asms); - tmp_asms.append(m_asms); - is_sat = check_sat(tmp_asms); - if (is_sat == l_true) { - update_model(); - } - else if (is_sat == l_false) { - core.reset(); - s().get_unsat_core(core); - for (unsigned i = 0; i < core.size();) { - if (asm_lits.contains(core[i])) { - core[i] = core.back(); - core.pop_back(); - } - else { - core_lits.insert(core[i]); - ++i; - } - } - if (core.empty()) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver empty core)\n";); - return l_false; - } - if (m_disjoint_cores) { - m_cores.push_back(core); - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :core-size " << core.size() << " :num-cores " << m_cores.size() << ")\n";); - for (unsigned i = 0; i < m_asms.size();) { - if (core_lits.contains(m_asms[i]) || !m_disjoint_cores) { - m_asms[i] = m_asms.back(); - m_asms.pop_back(); - } - else { - ++i; - } - } - } - else { - m_cores.push_back(m_asms); - m_asms.reset(); - } - } - } - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :num-cores " << m_cores.size() << ")\n";); - // TODO: update m_lower? - return is_sat; + return l_true; } - lbool disjoint_cores() { - return disjoint_cores(exprs()); - } - - lbool backtrack(exprs& asms) { - SASSERT(m_mss_trail_lim.size() == m_mcs_trail_lim.size()); - lbool is_sat = l_false; - while (is_sat == l_false && m_core_idx > 0) { - m_core_idx--; - m_mss_trail.resize(m_mss_trail_lim.back()); - m_mss_trail_lim.pop_back(); - m_mcs_trail.resize(m_mcs_trail_lim.back()); - m_mcs_trail_lim.pop_back(); - exprs tmp_asms; - tmp_asms.append(asms); - get_trail_asms(tmp_asms); - is_sat = check_sat(tmp_asms); - if (is_sat == l_true) { - update_model(); - } + lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) { + mss.reset(); + mcs.reset(); + lbool is_sat = check_sat(asms); + if (is_sat != l_true) return is_sat; + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl.get()); + vector dummy; + push_exprs(mss, m_asms); + push_exprs(mss, asms); + is_sat = cld(mdl.get(), mss, mcs); + if (is_sat == l_true) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); } - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";); + /*is_sat = m_mss(mdl.get(), dummy, mss, mcs); + SASSERT(is_sat != l_false); + if (is_sat == l_true) { + mdl.reset(); + m_mss.get_model(mdl); + update_assignment(mdl.get()); + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + }*/ return is_sat; } @@ -200,19 +118,19 @@ private: undef.append(mss); update_sat(initial_model, sat, undef); lbool is_sat = l_true; - while (is_sat == l_true && !undef.empty()) { + while (is_sat == l_true) { expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); - exprs asms; - asms.append(sat); - get_trail_asms(asms); - asms.push_back(asum); - is_sat = check_sat(asms); + sat.push_back(asum); + is_sat = check_sat(sat); + sat.pop_back(); if (is_sat == l_true) { - update_model(); - update_sat(m_last_model, sat, undef); + model_ref mdl; + s().get_model(mdl); + update_sat(mdl, sat, undef); + update_assignment(mdl.get()); } } - if (is_sat == l_false || undef.empty()) { + if (is_sat == l_false) { mss.reset(); mcs.reset(); mss.append(sat); @@ -222,26 +140,6 @@ private: return is_sat; } - void get_trail_asms(exprs& asms) { - asms.append(m_mss_trail); - for (unsigned i = 0; i < m_mcs_trail.size(); ++i) { - asms.push_back(m.mk_not(m_mcs_trail[i])); - } - } - - void update_trails(exprs const& mss, exprs const& mcs) { - m_mss_trail_lim.push_back(m_mss_trail.size()); - m_mcs_trail_lim.push_back(m_mcs_trail.size()); - m_mss_trail.append(mss); - m_mcs_trail.append(mcs); - } - - void update_model() { - m_last_model.reset(); - s().get_model(m_last_model); - update_assignment(m_last_model.get()); - } - void update_sat(model_ref mdl, exprs& sat, exprs& undef) { for (unsigned i = 0; i < undef.size();) { if (is_true(mdl.get(), undef[i])) { @@ -262,7 +160,12 @@ private: } lbool check_sat() { - return check_sat(exprs()); + expr_ref_vector dummy(m); + return check_sat(dummy); + } + + lbool check_sat(expr_ref_vector const& asms) { + return s().check_sat(asms); } lbool check_sat(exprs const& asms) { @@ -283,7 +186,7 @@ private: for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); } - // TODO: DEBUG verify assignment? + // TODO: DEBUG verify assignment m_upper = upper; trace_bounds("mss-solver"); } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 41548452a..4cb22389d 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -21,8 +21,7 @@ def_module_params('opt', ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'), ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'), ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'), - ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate'), - ('mss.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores') + ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate') )) From 7e8ed0762d29bbfc80716937183772e388802f1c Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:39:58 +0100 Subject: [PATCH 26/30] Revert "implemented CLD" This reverts commit 3a7efb91ae073c346716b4213c06d32fc39510a6. --- src/opt/mss.cpp | 12 ++++---- src/opt/mss_solver.cpp | 62 ++++-------------------------------------- 2 files changed, 12 insertions(+), 62 deletions(-) diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp index 47f4b6e02..cc0fa8d7d 100644 --- a/src/opt/mss.cpp +++ b/src/opt/mss.cpp @@ -155,10 +155,10 @@ namespace opt { lbool is_sat = l_true; for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) { bool has_mcs = false; - bool not_last = i + 1 < m_cores.size(); + bool is_last = i + 1 < m_cores.size(); SASSERT(check_invariant()); update_core(m_cores[i]); // remove members of mss - is_sat = process_core(1, m_cores[i], has_mcs, not_last); + is_sat = process_core(1, m_cores[i], has_mcs, is_last); } if (is_sat == l_true) { SASSERT(check_invariant()); @@ -183,7 +183,7 @@ namespace opt { // at least one literal in core is false in current model. // pick literals in core that are not yet in mss. // - lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) { + lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) { SASSERT(sz > 0); if (core.empty()) { return l_true; @@ -191,7 +191,7 @@ namespace opt { if (m.canceled()) { return l_undef; } - if (sz == 1 && core.size() == 1 && not_last && !has_mcs) { + if (sz == 1 && core.size() == 1 && is_last && !has_mcs) { // there has to be at least one false // literal in the core. TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";); @@ -214,7 +214,7 @@ namespace opt { SASSERT(m_mss_set.contains(core[i])); }); update_core(core); - return process_core(2*sz, core, has_mcs, not_last); + return process_core(2*sz, core, has_mcs, is_last); case l_false: if (sz == 1) { has_mcs = true; @@ -232,7 +232,7 @@ namespace opt { } update_core(core); } - return process_core(1, core, has_mcs, not_last); + return process_core(1, core, has_mcs, is_last); case l_undef: return l_undef; } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index d27b6300c..501b43ee4 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -98,61 +98,15 @@ private: vector dummy; push_exprs(mss, m_asms); push_exprs(mss, asms); - is_sat = cld(mdl.get(), mss, mcs); - if (is_sat == l_true) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); - } - /*is_sat = m_mss(mdl.get(), dummy, mss, mcs); - SASSERT(is_sat != l_false); - if (is_sat == l_true) { - mdl.reset(); - m_mss.get_model(mdl); - update_assignment(mdl.get()); - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); - }*/ + is_sat = m_mss(mdl.get(), dummy, mss, mcs); + SASSERT(is_sat == l_true); + mdl.reset(); + m_mss.get_model(mdl); + update_assignment(mdl.get()); + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); return is_sat; } - lbool cld(model_ref initial_model, exprs& mss, exprs& mcs) { - exprs sat, undef; - undef.append(mss); - update_sat(initial_model, sat, undef); - lbool is_sat = l_true; - while (is_sat == l_true) { - expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); - sat.push_back(asum); - is_sat = check_sat(sat); - sat.pop_back(); - if (is_sat == l_true) { - model_ref mdl; - s().get_model(mdl); - update_sat(mdl, sat, undef); - update_assignment(mdl.get()); - } - } - if (is_sat == l_false) { - mss.reset(); - mcs.reset(); - mss.append(sat); - mcs.append(undef); - is_sat = l_true; - } - return is_sat; - } - - void update_sat(model_ref mdl, exprs& sat, exprs& undef) { - for (unsigned i = 0; i < undef.size();) { - if (is_true(mdl.get(), undef[i])) { - sat.push_back(undef[i]); - undef[i] = undef.back(); - undef.pop_back(); - } - else { - ++i; - } - } - } - void push_exprs(exprs& dst, expr_ref_vector const& src) { for (unsigned i = 0; i < src.size(); ++i) { dst.push_back(src[i]); @@ -168,10 +122,6 @@ private: return s().check_sat(asms); } - lbool check_sat(exprs const& asms) { - return s().check_sat(asms.size(), asms.c_ptr()); - } - void update_assignment(model* mdl) { rational upper(0); for (unsigned i = 0; i < m_soft.size(); ++i) { From e1d7f5deba5398e8471ae53d63fce59c690c731e Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:40:00 +0100 Subject: [PATCH 27/30] Revert "MSS based MaxSMT solver" This reverts commit 3bbc09c1d2c800ea4ac646c66a886d25a87c4938. --- src/opt/maxsmt.cpp | 4 -- src/opt/mss_solver.cpp | 156 ----------------------------------------- src/opt/mss_solver.h | 12 ---- src/opt/opt_params.pyg | 8 +-- 4 files changed, 4 insertions(+), 176 deletions(-) delete mode 100755 src/opt/mss_solver.cpp delete mode 100755 src/opt/mss_solver.h diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 9bc4f4f14..91e843ca0 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -21,7 +21,6 @@ Notes: #include "opt/maxsmt.h" #include "opt/maxres.h" #include "opt/wmax.h" -#include "opt/mss_solver.h" #include "ast/ast_pp.h" #include "util/uint_set.h" #include "opt/opt_context.h" @@ -241,9 +240,6 @@ namespace opt { else if (maxsat_engine == symbol("pd-maxres")) { m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints); } - else if (maxsat_engine == symbol("mss")) { - m_msolver = mk_mss_solver(m_c, m_index, m_weights, m_soft_constraints); - } else if (maxsat_engine == symbol("wmax")) { m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints); } diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp deleted file mode 100755 index 501b43ee4..000000000 --- a/src/opt/mss_solver.cpp +++ /dev/null @@ -1,156 +0,0 @@ -#include "solver/solver.h" -#include "opt/maxsmt.h" -#include "opt/mss_solver.h" -#include "opt/mss.h" -#include "opt/opt_context.h" -#include "opt/opt_params.hpp" - -using namespace opt; - -class mss_solver: public maxsmt_solver_base { - -private: - typedef ptr_vector exprs; - mss m_mss; - unsigned m_index; - expr_ref_vector m_asms; - unsigned m_max_mss; - -public: - mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft), - m_mss(c.get_solver(), m), - m_index(id), - m_asms(m), - m_max_mss(UINT_MAX) { - } - - virtual ~mss_solver() {} - - virtual lbool operator()() { - if (!init()) return l_undef; - init_asms(); - lbool is_sat = check_sat(m_asms); - if (is_sat == l_undef) return l_undef; - if (is_sat == l_true) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";); - model_ref mdl; - s().get_model(mdl); - update_assignment(mdl.get()); - return l_true; - } - return enumerate_mss(); - } - - virtual void updt_params(params_ref& p) { - maxsmt_solver_base::updt_params(p); - opt_params _p(p); - m_max_mss = _p.mss_max(); - } - -private: - void init_asms() { - m_asms.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - expr* e = m_soft[i]; - m_asms.push_back(relax_and_assert(e)); - } - } - - expr_ref relax_and_assert(expr* e) { - expr_ref asum(m); - if (is_literal(e)) { - asum = e; - } - else { - asum = mk_fresh_bool("r"); - e = m.mk_iff(asum, e); - s().assert_expr(e); - } - return asum; - } - - bool is_literal(expr* l) { - return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); - } - - lbool enumerate_mss() { - expr_ref_vector asms(m); - for (unsigned i = 0; i < m_max_mss; ++i) { - exprs mss, mcs; - lbool is_sat = next_mss(asms, mss, mcs); - if (is_sat == l_false && i == 0) return l_false; - if (is_sat == l_undef && i == 0) return l_undef; - if (is_sat == l_false || is_sat == l_undef) return l_true; - asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr()))); - } - return l_true; - } - - lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) { - mss.reset(); - mcs.reset(); - lbool is_sat = check_sat(asms); - if (is_sat != l_true) return is_sat; - model_ref mdl; - s().get_model(mdl); - update_assignment(mdl.get()); - vector dummy; - push_exprs(mss, m_asms); - push_exprs(mss, asms); - is_sat = m_mss(mdl.get(), dummy, mss, mcs); - SASSERT(is_sat == l_true); - mdl.reset(); - m_mss.get_model(mdl); - update_assignment(mdl.get()); - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); - return is_sat; - } - - void push_exprs(exprs& dst, expr_ref_vector const& src) { - for (unsigned i = 0; i < src.size(); ++i) { - dst.push_back(src[i]); - } - } - - lbool check_sat() { - expr_ref_vector dummy(m); - return check_sat(dummy); - } - - lbool check_sat(expr_ref_vector const& asms) { - return s().check_sat(asms); - } - - void update_assignment(model* mdl) { - rational upper(0); - for (unsigned i = 0; i < m_soft.size(); ++i) { - if (!is_true(mdl, m_soft[i])) { - upper += m_weights[i]; - } - } - if (upper > m_upper) return; - if (!m_c.verify_model(m_index, mdl, upper)) return; - m_model = mdl; - m_c.model_updated(mdl); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_assignment[i] = is_true(m_soft[i]); - } - // TODO: DEBUG verify assignment - m_upper = upper; - trace_bounds("mss-solver"); - } - - bool is_true(model* mdl, expr* e) { - expr_ref tmp(m); - return mdl->eval(e, tmp, true) && m.is_true(tmp); - } - - bool is_true(expr* e) { - return is_true(m_model.get(), e); - } -}; - -maxsmt_solver_base* opt::mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { - return alloc(mss_solver, c, id, ws, soft); -} diff --git a/src/opt/mss_solver.h b/src/opt/mss_solver.h deleted file mode 100755 index 5c274cd4c..000000000 --- a/src/opt/mss_solver.h +++ /dev/null @@ -1,12 +0,0 @@ -#ifndef MSS_SOLVER_H_ -#define MSS_SOLVER_H_ - -#include "opt/maxsmt.h" - -namespace opt { - - maxsmt_solver_base* mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft); - -} - -#endif diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 4cb22389d..1d6d7ee6a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -2,13 +2,13 @@ def_module_params('opt', description='optimization parameters', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), - ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), - ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'), + ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), @@ -20,8 +20,8 @@ def_module_params('opt', ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'), ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'), - ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'), - ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate') + ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core') + )) From 24b35fb9256f2bf799cadae819334d8d52a3e686 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Thu, 26 Apr 2018 22:42:55 +0100 Subject: [PATCH 28/30] WMax conflict budget bug fix --- src/opt/wmax.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 52b87e536..513c68d6e 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -84,6 +84,9 @@ namespace opt { if (m.canceled()) { is_sat = l_undef; } + if (is_sat == l_undef) { + break; + } if (is_sat == l_false) { TRACE("opt", tout << "Unsat\n";); break; @@ -97,9 +100,6 @@ namespace opt { //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); } - else { - //DEBUG_CODE(verify_cores(cores);); - } update_cores(wth(), cores); wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); From 5dbba8bd5364b72ec9824f1c50d94b241b9cc218 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Apr 2018 17:48:04 +0200 Subject: [PATCH 29/30] fix #1599. fix #1600 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 1 - src/api/api_context.h | 5 ++--- src/ast/datatype_decl_plugin.cpp | 2 ++ src/ast/datatype_decl_plugin.h | 3 ++- src/cmd_context/basic_cmds.cpp | 2 +- src/cmd_context/cmd_context.cpp | 10 +++++++--- src/cmd_context/context_params.h | 5 ++++- src/cmd_context/tactic_cmds.cpp | 4 ++-- src/opt/opt_context.h | 14 +++++++------- 9 files changed, 27 insertions(+), 19 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c8b365f22..5993e9fdd 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -78,7 +78,6 @@ namespace api { m_bv_util(m()), m_datalog_util(m()), m_fpa_util(m()), - m_dtutil(m()), m_sutil(m()), m_last_result(m()), m_ast_trail(m()), diff --git a/src/api/api_context.h b/src/api/api_context.h index 185eb9e0f..72a0e4bbb 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -61,7 +61,6 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; - datatype_util m_dtutil; seq_util m_sutil; // Support for old solver API @@ -122,12 +121,12 @@ namespace api { bool produce_unsat_cores() const { return m_params.m_unsat_core; } bool use_auto_config() const { return m_params.m_auto_config; } unsigned get_timeout() const { return m_params.m_timeout; } - unsigned get_rlimit() const { return m_params.m_rlimit; } + unsigned get_rlimit() const { return m_params.rlimit(); } arith_util & autil() { return m_arith_util; } bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } fpa_util & fpautil() { return m_fpa_util; } - datatype_util& dtutil() { return m_dtutil; } + datatype_util& dtutil() { return m_dt_plugin->u(); } seq_util& sutil() { return m_sutil; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index f685c70d5..dfeaef9f8 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -390,6 +390,8 @@ namespace datatype { TRACE("datatype", tout << "declaring " << datatypes[i]->name() << "\n";); if (m_defs.find(datatypes[i]->name(), d)) { TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";); + sort_ref_vector srts(*m_manager); + u().reset(); dealloc(d); } m_defs.insert(datatypes[i]->name(), datatypes[i]); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index f32e9990d..88b50af82 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -239,7 +239,6 @@ namespace datatype { map m_defs; svector m_def_block; unsigned m_class_id; - util & u() const; void inherit(decl_plugin* other_p, ast_translation& tr) override; @@ -279,6 +278,8 @@ namespace datatype { def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); } def& get_def(symbol const& s) { return *(m_defs[s]); } bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); } + util & u() const; + private: bool is_value_visit(expr * arg, ptr_buffer & todo) const; diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 0c9c5360c..4e8806d62 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -503,7 +503,7 @@ public: ctx.set_random_seed(to_unsigned(val)); } else if (m_option == m_reproducible_resource_limit) { - ctx.params().m_rlimit = to_unsigned(val); + ctx.params().set_rlimit(to_unsigned(val)); } else if (m_option == m_verbosity) { set_verbosity_level(to_unsigned(val)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 11f800b25..9f93e1b93 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1328,7 +1328,8 @@ void cmd_context::push() { s.m_macros_stack_lim = m_macros_stack.size(); s.m_aux_pdecls_lim = m_aux_pdecls.size(); s.m_assertions_lim = m_assertions.size(); - if (m_solver) + m().limit().push(m_params.rlimit()); + if (m_solver) m_solver->push(); if (m_opt) m_opt->push(); @@ -1443,6 +1444,9 @@ void cmd_context::pop(unsigned n) { restore_assertions(s.m_assertions_lim); restore_psort_inst(s.m_psort_inst_stack_lim); m_scopes.shrink(new_lvl); + while (n--) { + m().limit().pop(); + } } @@ -1453,7 +1457,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions TRACE("before_check_sat", dump_assertions(tout);); init_manager(); unsigned timeout = m_params.m_timeout; - unsigned rlimit = m_params.m_rlimit; + unsigned rlimit = m_params.rlimit(); scoped_watch sw(*this); lbool r; bool was_opt = false; @@ -1530,7 +1534,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions void cmd_context::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector & conseq) { unsigned timeout = m_params.m_timeout; - unsigned rlimit = m_params.m_rlimit; + unsigned rlimit = m_params.rlimit(); lbool r; m_check_sat_result = m_solver.get(); // solver itself stores the result. m_solver->set_progress_callback(this); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index df62057fe..3d2947b7a 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -27,6 +27,8 @@ class context_params { void set_bool(bool & opt, char const * param, char const * value); void set_uint(unsigned & opt, char const * param, char const * value); + unsigned m_rlimit; + public: bool m_auto_config; bool m_proof; @@ -42,10 +44,11 @@ public: bool m_unsat_core; bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager. unsigned m_timeout; - unsigned m_rlimit; + unsigned rlimit() const { return m_rlimit; } context_params(); void set(char const * param, char const * value); + void set_rlimit(unsigned lim) { m_rlimit = lim; } void updt_params(); void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 32a92ea59..78187ebe1 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -205,7 +205,7 @@ public: tref->set_logic(ctx.get_logic()); ast_manager & m = ctx.m(); unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); - unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); + unsigned rlimit = p.get_uint("rlimit", ctx.params().rlimit()); labels_vec labels; goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); @@ -321,7 +321,7 @@ public: assert_exprs_from(ctx, *g); unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); - unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); + unsigned rlimit = p.get_uint("rlimit", ctx.params().rlimit()); goal_ref_buffer result_goals; model_converter_ref mc; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 6af106ef3..e97fabbe4 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -283,13 +283,13 @@ namespace opt { struct is_propositional_fn; bool is_propositional(expr* e); - void init_solver(); - void update_solver(); - void setup_arith_solver(); - void add_maxsmt(symbol const& id, unsigned index); - void set_simplify(tactic *simplify); - void set_pareto(pareto_base* p); - void clear_state(); + void init_solver(); + void update_solver(); + void setup_arith_solver(); + void add_maxsmt(symbol const& id, unsigned index); + void set_simplify(tactic *simplify); + void set_pareto(pareto_base* p); + void clear_state(); bool is_numeral(expr* e, rational& n) const; From f234bb348bb33dc97dce2751a241bdbf96a46814 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Apr 2018 17:49:20 +0200 Subject: [PATCH 30/30] fix #1599. fix #1600 Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index dfeaef9f8..d3704a84a 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -390,7 +390,6 @@ namespace datatype { TRACE("datatype", tout << "declaring " << datatypes[i]->name() << "\n";); if (m_defs.find(datatypes[i]->name(), d)) { TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";); - sort_ref_vector srts(*m_manager); u().reset(); dealloc(d); }