From 76c9abada2405442e511d370b98bb7ad6ed353b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Aug 2015 11:00:19 -0700 Subject: [PATCH 1/2] remove dbg pp Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 6 +++++- src/tactic/core/simplify_tactic.cpp | 3 --- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 94917e190..1b4063b17 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -106,7 +106,11 @@ public: dep2asm_t dep2asm; VERIFY(l_true == internalize_formulas()); VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm)); - m_solver.display_wcnf(out, sz, m_asms.c_ptr(), weights); + svector nweights; + for (unsigned i = 0; i < m_asms.size(); ++i) { + nweights.push_back((unsigned) m_weights[i]); + } + m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr()); } lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) { diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 227a34b51..fea5ac86e 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -65,9 +65,6 @@ 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);); From ee458fa60113f19b0137e6bea8f92b7427846ec3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Aug 2015 12:09:07 -0700 Subject: [PATCH 2/2] revising pd-maxres Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 4 ++++ src/sat/sat_solver.cpp | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 42c73f8d0..0e08886f5 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -247,6 +247,7 @@ public: break; } } + m_lower = m_upper; trace(); return l_true; } @@ -468,6 +469,9 @@ public: fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr())); s().assert_expr(fml); m_lower += w; + if (m_st == s_primal_dual) { + m_lower = std::min(m_lower, m_upper); + } trace(); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 9af35d9b3..a27a1a4d2 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -959,11 +959,13 @@ namespace sat { assign(lit, justification()); break; case l_false: { + m_assumptions.push_back(lit); SASSERT(!inconsistent()); set_conflict(justification(), ~lit); flet _min1(m_config.m_minimize_core, false); flet _min2(m_config.m_minimize_core_partial, false); resolve_conflict_for_unsat_core(); + m_assumptions.pop_back(); weight += weights[i]; blocker.push_back(lit); TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";);