From da0c12cdba94deb6d5044120e484e525b0b67793 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Aug 2015 18:29:36 -0700 Subject: [PATCH 1/2] move display method to before first SAT call Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 10 ---------- src/opt/opt_context.cpp | 15 ++++++++++++++- src/opt/opt_context.h | 2 ++ 3 files changed, 16 insertions(+), 11 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 8784cf80a..827f211e6 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -186,7 +186,6 @@ public: init(); init_local(); trace(); - display(); while (m_lower < m_upper) { TRACE("opt", display_vec(tout, m_asms); @@ -220,7 +219,6 @@ public: init(); init_local(); trace(); - display(); exprs cs; while (m_lower < m_upper) { lbool is_sat = check_sat_hill_climb(m_asms); @@ -253,14 +251,6 @@ public: return l_true; } - void display() { - if (m_dump_benchmarks && m_c.sat_enabled()) { - unsigned sz = m_soft.size(); - inc_sat_display(verbose_stream(), s(), sz, - m_soft.c_ptr(), m_weights.c_ptr()); - } - } - lbool check_sat_hill_climb(expr_ref_vector& asms1) { expr_ref_vector asms(asms1); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 4ae4b0112..f3d0e9bd0 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -41,6 +41,7 @@ Notes: #include "ast_smt_pp.h" #include "filter_model_converter.h" #include "ast_pp_util.h" +#include "inc_sat_solver.h" namespace opt { @@ -220,7 +221,7 @@ namespace opt { TRACE("opt", tout << "Hard constraint: " << mk_ismt2_pp(m_hard_constraints[i].get(), m) << std::endl;); s.assert_expr(m_hard_constraints[i].get()); } - + display_benchmark(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); lbool is_sat = s.check_sat(0,0); TRACE("opt", tout << "initial search result: " << is_sat << "\n";); @@ -1069,6 +1070,18 @@ namespace opt { } } + void context::display_benchmark() { + if (opt_params(m_params).dump_benchmarks() && + sat_enabled() && + m_objectives.size() == 1 && + m_objectives[0].m_type == O_MAXSMT + ) { + objective& o = m_objectives[0]; + unsigned sz = o.m_terms.size(); + inc_sat_display(verbose_stream(), get_solver(), sz, o.m_terms.c_ptr(), o.m_weights.c_ptr()); + } + } + void context::display(std::ostream& out) { display_assignment(out); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index f872d70b5..aa8c0a69a 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -280,6 +280,8 @@ namespace opt { void validate_lex(); + void display_benchmark(); + // pareto void yield(); From 546a9b8f0318b72dddf4d7b6f13c91201093ea52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Aug 2015 10:53:39 -0700 Subject: [PATCH 2/2] revising pd-maxres Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 2 +- src/opt/maxsls.cpp | 14 +++- src/sat/sat_sls.cpp | 1 + src/sat/sat_sls.h | 1 - src/sat/sat_solver.cpp | 12 +-- src/sat/sat_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 110 +++++++++----------------- src/tactic/arith/card2bv_tactic.cpp | 1 + src/tactic/core/simplify_tactic.cpp | 5 +- 9 files changed, 65 insertions(+), 82 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 827f211e6..42c73f8d0 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -171,7 +171,7 @@ public: } void new_assumption(expr* e, rational const& w) { - IF_VERBOSE(3, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";); + IF_VERBOSE(13, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";); TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n";); m_asm2weight.insert(e, w); m_asms.push_back(e); diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp index e1cf90fb1..4e59cfdfd 100644 --- a/src/opt/maxsls.cpp +++ b/src/opt/maxsls.cpp @@ -20,6 +20,8 @@ Notes: #include "maxsls.h" #include "ast_pp.h" #include "model_smt2_pp.h" +#include "opt_context.h" +#include "inc_sat_solver.h" namespace opt { @@ -34,7 +36,7 @@ namespace opt { IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";); init(); enable_sls(true); - lbool is_sat = s().check_sat(0, 0); + lbool is_sat = check(); if (is_sat == l_true) { s().get_model(m_model); m_upper.reset(); @@ -49,6 +51,16 @@ namespace opt { } return is_sat; } + + lbool check() { + if (m_c.sat_enabled()) { + return inc_sat_check_sat( + s(), m_soft.size(), m_soft.c_ptr(), m_weights.c_ptr(), m_upper); + } + else { + return s().check_sat(0, 0); + } + } }; diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp index ad26554af..24f952ea9 100644 --- a/src/sat/sat_sls.cpp +++ b/src/sat/sat_sls.cpp @@ -386,6 +386,7 @@ namespace sat { m_best_value = val; m_best_model.reset(); m_best_model.append(m_model); + s.set_model(m_best_model); IF_VERBOSE(1, verbose_stream() << "new value: " << val << " @ " << i << "\n";); if (i*2 > m_max_tries) { m_max_tries *= 2; diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h index 6f9d89e41..7ea472083 100644 --- a/src/sat/sat_sls.h +++ b/src/sat/sat_sls.h @@ -97,7 +97,6 @@ namespace sat { void set_soft(unsigned sz, literal const* lits, double const* weights); bool has_soft() const { return !m_soft.empty(); } void opt(unsigned sz, literal const* tabu, bool reuse_model); - model const& get_model() { return m_best_model; } virtual void display(std::ostream& out) const; double evaluate_model(model& mdl); private: diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3d6130d5e..9af35d9b3 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1105,6 +1105,12 @@ namespace sat { } } + void solver::set_model(model const& mdl) { + m_model.reset(); + m_model.append(mdl); + m_model_is_current = !m_model.empty(); + } + void solver::mk_model() { m_model.reset(); m_model_is_current = true; @@ -1117,8 +1123,6 @@ namespace sat { TRACE("sat_mc_bug", m_mc.display(tout);); if (m_config.m_optimize_model) { m_wsls.opt(0, 0, false); - m_model.reset(); - m_model.append(m_wsls.get_model()); } m_mc(m_model); TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); @@ -1808,9 +1812,7 @@ namespace sat { // apply optional clause minimization by detecting subsumed literals. // initial experiment suggests it has no effect. m_mus(); // ignore return value on cancelation. - m_model.reset(); - m_model.append(m_mus.get_model()); - m_model_is_current = !m_model.empty(); + set_model(m_mus.get_model()); } } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c7f6cc235..c656465ed 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -280,6 +280,7 @@ namespace sat { bool model_is_current() const { return m_model_is_current; } literal_vector const& get_core() const { return m_core; } model_converter const & get_model_converter() const { return m_mc; } + void set_model(model const& mdl); protected: unsigned m_conflicts; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index aace703d0..94917e190 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -56,7 +56,7 @@ class inc_sat_solver : public solver { proof_converter_ref m_pc; model_converter_ref m_mc2; expr_dependency_ref m_dep_core; - + svector m_weights; typedef obj_map dep2asm_t; public: @@ -82,8 +82,6 @@ public: simp2_p.set_bool("hoist_mul", false); // required by som m_preprocess = and_then(mk_card2bv_tactic(m, m_params), - //mk_simplify_tactic(m), - //mk_propagate_values_tactic(m), using_params(mk_simplify_tactic(m), simp2_p), mk_max_bv_sharing_tactic(m), mk_bit_blaster_tactic(m), @@ -100,25 +98,32 @@ public: } void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) { + m_weights.reset(); + if (weights != 0) { + for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]); + } m_solver.pop_to_base_level(); dep2asm_t dep2asm; VERIFY(l_true == internalize_formulas()); - VERIFY(l_true == internalize_assumptions(sz, assumptions, 0 != weights, dep2asm)); + VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm)); m_solver.display_wcnf(out, sz, m_asms.c_ptr(), weights); } lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) { - + m_weights.reset(); + if (weights != 0) { + m_weights.append(sz, weights); + } + SASSERT(m_weights.empty() == (m_weights.c_ptr() == 0)); m_solver.pop_to_base_level(); dep2asm_t dep2asm; m_model = 0; lbool r = internalize_formulas(); if (r != l_true) return r; - r = internalize_assumptions(sz, assumptions, 0 != weights, dep2asm); + r = internalize_assumptions(sz, assumptions, dep2asm); if (r != l_true) return r; - //m_solver.display_dimacs(std::cout); - r = m_solver.check(m_asms.size(), m_asms.c_ptr(), weights, max_weight); + r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight); switch (r) { case l_true: if (sz > 0 && !weights) { @@ -179,7 +184,7 @@ public: } } virtual void assert_expr(expr * t) { - TRACE("opt", tout << mk_pp(t, m) << "\n";); + TRACE("sat", tout << mk_pp(t, m) << "\n";); m_fmls.push_back(t); } virtual void set_produce_models(bool f) {} @@ -238,9 +243,10 @@ private: m_pc.reset(); m_dep_core.reset(); m_subgoals.reset(); + m_preprocess->reset(); SASSERT(g->models_enabled()); SASSERT(!g->proofs_enabled()); - TRACE("opt", g->display(tout);); + TRACE("sat", g->display(tout);); try { (*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core); } @@ -254,61 +260,26 @@ private: return l_undef; } g = m_subgoals[0]; - TRACE("opt", g->display_with_dependencies(tout);); + TRACE("sat", g->display_with_dependencies(tout);); m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true); return l_true; } - lbool internalize_assumptions(unsigned sz, expr* const* asms, bool is_weighted, dep2asm_t& dep2asm) { + lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { if (sz == 0) { return l_true; } - if (is_weighted) { - return internalize_weighted(sz, asms, dep2asm); - } - return internalize_unweighted(sz, asms, dep2asm); - } - - lbool internalize_unweighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. - lbool res = l_undef; for (unsigned i = 0; i < sz; ++i) { g->assert_expr(asms[i], m.mk_leaf(asms[i])); } - res = internalize_goal(g, dep2asm); + lbool res = internalize_goal(g, dep2asm); if (res == l_true) { - extract_assumptions(dep2asm); + extract_assumptions(sz, asms, dep2asm); } return res; } - /* - \brief extract weighted assumption literals in the same order as the weights. - For this purpose we enforce tha assumptions are literals. - */ - lbool internalize_weighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { - goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. - lbool res = l_undef; - m_asms.reset(); - expr_ref_vector lits(m); - filter_model_converter_ref fmc = alloc(filter_model_converter, m); - for (unsigned i = 0; i < sz; ++i) { - expr_ref lit = ensure_literal(g, asms[i], fmc.get()); - lits.push_back(lit); - g->assert_expr(lit, m.mk_leaf(lit)); - } - m_mc = concat(m_mc.get(), fmc.get()); - res = internalize_goal(g, dep2asm); - if (res == l_true) { - for (unsigned i = 0; i < lits.size(); ++i) { - sat::literal l; - VERIFY (dep2asm.find(lits[i].get(), l)); - m_asms.push_back(l); - } - } - return res; - } - lbool internalize_formulas() { if (m_fmls_head == m_fmls.size()) { return l_true; @@ -321,39 +292,31 @@ private: return internalize_goal(g, dep2asm); } - expr_ref ensure_literal(goal_ref& g, expr* e, filter_model_converter* fmc) { - expr_ref result(m), fml(m); - expr* e1; - if (is_uninterp_const(e) || (m.is_not(e, e1) && is_uninterp_const(e1))) { - result = e; - } - else { - // TBD: need a filter_model_converter to remove - result = m.mk_fresh_const("soft", m.mk_bool_sort()); - fmc->insert(to_app(result)->get_decl()); - fml = m.mk_implies(result, e); - g->assert_expr(fml); - } - return result; - } - - void extract_assumptions(dep2asm_t& dep2asm) { + void extract_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { m_asms.reset(); - dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); - for (; it != end; ++it) { - m_asms.push_back(it->m_value); + unsigned j = 0; + sat::literal lit; + for (unsigned i = 0; i < sz; ++i) { + if (dep2asm.find(asms[i], lit)) { + m_asms.push_back(lit); + if (i != j && !m_weights.empty()) { + m_weights[j] = m_weights[i]; + } + ++j; + } } - //IF_VERBOSE(0, verbose_stream() << asms << "\n";); + SASSERT(dep2asm.size() == m_asms.size()); } void extract_core(dep2asm_t& dep2asm) { u_map asm2dep; dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); for (; it != end; ++it) { - asm2dep.insert(it->m_value.index(), it->m_key); + expr* e = it->m_key; + asm2dep.insert(it->m_value.index(), e); } sat::literal_vector const& core = m_solver.get_core(); - TRACE("opt", + TRACE("sat", dep2asm_t::iterator it2 = dep2asm.begin(); dep2asm_t::iterator end2 = dep2asm.end(); for (; it2 != end2; ++it2) { @@ -426,7 +389,7 @@ private: for (unsigned i = 0; i < m_fmls.size(); ++i) { expr_ref tmp(m); VERIFY(m_model->eval(m_fmls[i].get(), tmp)); - CTRACE("opt", !m.is_true(tmp), + CTRACE("sat", !m.is_true(tmp), tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) << " to " << tmp << "\n"; model_smt2_pp(tout, m, *(m_model.get()), 0);); @@ -461,3 +424,4 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof } return s.display_weighted(out, sz, soft, weights.c_ptr()); } + diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index b4be4b862..3ef1d786d 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -24,6 +24,7 @@ Notes: #include"card2bv_tactic.h" #include"pb_rewriter.h" #include"ast_util.h" +#include"ast_pp.h" namespace pb { unsigned card2bv_rewriter::get_num_bits(func_decl* f) { diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 80be97b0b..227a34b51 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include"simplify_tactic.h" #include"th_rewriter.h" -#include"ast_smt2_pp.h" +#include"ast_pp.h" struct simplify_tactic::imp { ast_manager & m_manager; @@ -65,6 +65,9 @@ struct simplify_tactic::imp { proof * pr = g.pr(idx); new_pr = m().mk_modus_ponens(pr, new_pr); } + if (m_manager.is_false(new_curr)) { + std::cout << mk_pp(curr, m_manager) << " => " << new_curr << "\n"; + } g.update(idx, new_curr, new_pr, g.dep(idx)); } TRACE("after_simplifier_bug", g.display(tout););