From 25ad9d2ee126b7ad262d8e3505485e151fcb9f5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 May 2014 14:43:06 -0700 Subject: [PATCH] tuning based on benchmarks from Robert White Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/expr_safe_replace.cpp | 52 +++++++++++++------------- src/ast/rewriter/expr_safe_replace.h | 7 +++- src/opt/pb_sls.cpp | 7 ++++ src/opt/weighted_maxsat.cpp | 34 ++++++++++------- src/tactic/arith/elim01_tactic.cpp | 5 +++ 5 files changed, 65 insertions(+), 40 deletions(-) diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index a4886ad1a..37fcdfe6a 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -29,43 +29,39 @@ void expr_safe_replace::insert(expr* src, expr* dst) { } void expr_safe_replace::operator()(expr* e, expr_ref& res) { - obj_map cache; - ptr_vector todo, args; - expr_ref_vector refs(m); - todo.push_back(e); + m_todo.push_back(e); expr* a, *b, *d; - todo.push_back(e); - while (!todo.empty()) { - a = todo.back(); - if (cache.contains(a)) { - todo.pop_back(); + while (!m_todo.empty()) { + a = m_todo.back(); + if (m_cache.contains(a)) { + m_todo.pop_back(); } else if (m_subst.find(a, b)) { - cache.insert(a, b); - todo.pop_back(); + m_cache.insert(a, b); + m_todo.pop_back(); } else if (is_var(a)) { - cache.insert(a, a); - todo.pop_back(); + m_cache.insert(a, a); + m_todo.pop_back(); } else if (is_app(a)) { app* c = to_app(a); unsigned n = c->get_num_args(); - args.reset(); + m_args.reset(); for (unsigned i = 0; i < n; ++i) { - if (cache.find(c->get_arg(i), d)) { - args.push_back(d); + if (m_cache.find(c->get_arg(i), d)) { + m_args.push_back(d); } else { - todo.push_back(c->get_arg(i)); + m_todo.push_back(c->get_arg(i)); } } - if (args.size() == n) { - b = m.mk_app(c->get_decl(), args.size(), args.c_ptr()); - refs.push_back(b); - cache.insert(a, b); - todo.pop_back(); + if (m_args.size() == n) { + b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr()); + m_refs.push_back(b); + m_cache.insert(a, b); + m_todo.pop_back(); } } else { @@ -93,12 +89,16 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { } replace(q->get_expr(), new_body); b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body); - refs.push_back(b); - cache.insert(a, b); - todo.pop_back(); + m_refs.push_back(b); + m_cache.insert(a, b); + m_todo.pop_back(); } } - res = cache.find(e); + res = m_cache.find(e); + m_cache.reset(); + m_todo.reset(); + m_args.reset(); + m_refs.reset(); } void expr_safe_replace::reset() { diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h index ad626d18f..1f21d35e9 100644 --- a/src/ast/rewriter/expr_safe_replace.h +++ b/src/ast/rewriter/expr_safe_replace.h @@ -29,9 +29,12 @@ class expr_safe_replace { expr_ref_vector m_src; expr_ref_vector m_dst; obj_map m_subst; + obj_map m_cache; + ptr_vector m_todo, m_args; + expr_ref_vector m_refs; public: - expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m) {} + expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m), m_refs(m) {} void insert(expr* src, expr* dst); @@ -42,6 +45,8 @@ public: void apply_substitution(expr* s, expr* def, expr_ref& t); void reset(); + + bool empty() const { return m_subst.empty(); } }; #endif /* __EXPR_SAFE_REPLACE_H__ */ diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index c62c79c6a..f04301c06 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -90,6 +90,8 @@ namespace smt { struct stats { stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } + unsigned m_num_flips; + unsigned m_num_improvements; }; ast_manager& m; @@ -116,6 +118,7 @@ namespace smt { unsigned m_non_greedy_percent; // percent of moves to do non-greedy style random_gen m_rng; scoped_mpz one; + stats m_stats; imp(ast_manager& m): m(m), @@ -238,6 +241,8 @@ namespace smt { } void collect_statistics(::statistics& st) const { + st.update("sls.num_flips", m_stats.m_num_flips); + st.update("sls.num_improvements", m_stats.m_num_improvements); } void updt_params(params_ref& p) { @@ -347,6 +352,7 @@ namespace smt { } literal flip() { + m_stats.m_num_flips++; literal result; if (m_hard_false.empty()) { result = flip_soft(); @@ -359,6 +365,7 @@ namespace smt { m_best_assignment.reset(); m_best_assignment.append(m_assignment); m_best_penalty = m_penalty; + m_stats.m_num_improvements++; init_max_flips(); } if (!m_assignment[result.var()]) { diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 7a19e00af..42a1c8ce3 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -60,17 +60,24 @@ namespace opt { params_ref m_params; // config bool m_enable_sls; // config bool m_enable_sat; // config + bool m_sls_enabled; + bool m_sat_enabled; public: maxsmt_solver_base(solver* s, ast_manager& m): m_s(s), m(m), m_cancel(false), m_soft(m), - m_enable_sls(false), m_enable_sat(false) {} + m_enable_sls(false), m_enable_sat(false), + m_sls_enabled(false), m_sat_enabled(false) {} virtual ~maxsmt_solver_base() {} virtual rational get_lower() const { return m_lower; } virtual rational get_upper() const { return m_upper; } virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); } - virtual void collect_statistics(statistics& st) const { } + virtual void collect_statistics(statistics& st) const { + if (m_sls_enabled || m_sat_enabled) { + m_s->collect_statistics(st); + } + } virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } virtual void updt_params(params_ref& p) { m_params.copy(p); @@ -121,7 +128,6 @@ namespace opt { fid != pb.get_family_id() && fid != bv.get_family_id() && !is_uninterp_const(n)) { - std::cout << mk_pp(n, m) << "\n"; throw found(); } } @@ -147,7 +153,7 @@ namespace opt { } void enable_bvsat() { - if (probe_bv()) { + if (m_enable_sat && !m_sat_enabled && probe_bv()) { tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); @@ -159,15 +165,17 @@ namespace opt { unsigned lvl = m_s->get_scope_level(); while (lvl > 0) { sat_solver->push(); --lvl; } m_s = sat_solver; + m_sat_enabled = true; } } void enable_sls() { - if (m_enable_sls && probe_bv()) { + if (m_enable_sls && !m_sls_enabled && probe_bv()) { m_params.set_uint("restarts", 20); unsigned lvl = m_s->get_scope_level(); m_s = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params); while (lvl > 0) { m_s->push(); --lvl; } + m_sls_enabled = true; } } @@ -249,19 +257,18 @@ namespace opt { m_soft_aux(m), m_trail(m), m_soft_constraints(m), - m_enable_lazy(false) { + m_enable_lazy(true) { m_enable_lazy = true; - enable_sls(); } virtual ~bcd2() {} - virtual lbool operator()() { expr_ref fml(m), r(m); lbool is_sat = l_undef; expr_ref_vector asms(m); bool first = true; + enable_sls(); solver::scoped_push _scope1(s()); init(); init_bcd(); @@ -557,13 +564,14 @@ namespace opt { public: pbmax(solver* s, ast_manager& m, bool use_aux): maxsmt_solver_base(s, m), m_use_aux(use_aux) { - enable_bvsat(); - enable_sls(); } virtual ~pbmax() {} lbool operator()() { + enable_bvsat(); + enable_sls(); + TRACE("opt", s().display(tout); tout << "\n"; for (unsigned i = 0; i < m_soft.size(); ++i) { tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n"; @@ -636,12 +644,12 @@ namespace opt { public: wpm2(solver* s, ast_manager& m, maxsmt_solver_base* _maxs): maxsmt_solver_base(s, m), maxs(_maxs) { - enable_sls(); } virtual ~wpm2() {} lbool operator()() { + enable_sls(); IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 solve)\n";); solver::scoped_push _s(s()); pb_util u(m); @@ -839,12 +847,12 @@ namespace opt { public: sls(solver* s, ast_manager& m): maxsmt_solver_base(s, m) { - enable_bvsat(); - enable_sls(); } virtual ~sls() {} lbool operator()() { IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";); + enable_bvsat(); + enable_sls(); init(); lbool is_sat = s().check_sat(0, 0); if (is_sat == l_true) { diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index 300291cb2..53fa948ce 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -185,6 +185,11 @@ public: << bounds.has_upper(x, hi, s2) << " " << hi << "\n";); } } + + if (sub.empty()) { + result.push_back(g.get()); + return; + } expr_ref new_curr(m), tmp_curr(m); proof_ref new_pr(m);