From 94dae2da3a8e3571637707cb5a1c34357ee83bd2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Jan 2019 18:11:18 -0800 Subject: [PATCH 1/3] fix fourth bug produced by repros by Mark Dunlop Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 18 +++++++++++------- src/smt/smt_conflict_resolution.cpp | 4 ++-- src/smt/smt_context.h | 2 +- src/smt/smt_context_pp.cpp | 15 ++++++++------- src/smt/theory_pb.cpp | 2 ++ src/smt/theory_seq.cpp | 15 ++++++++++++--- 6 files changed, 36 insertions(+), 20 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 789aaf8db..25b51372e 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -375,7 +375,7 @@ public: get_mus_model(mdl); is_sat = minimize_core(_core); core.append(_core.size(), _core.c_ptr()); - verify_core(core); + DEBUG_CODE(verify_core(core);); ++m_stats.m_num_cores; if (is_sat != l_true) { IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";); @@ -738,7 +738,7 @@ public: m_correction_set_size = correction_set_size; } - TRACE("opt", tout << *mdl;); + TRACE("opt_verbose", tout << *mdl;); rational upper(0); @@ -761,7 +761,7 @@ public: m_model = mdl; m_c.model_updated(mdl.get()); - TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;); + TRACE("opt", tout << "updated upper: " << upper << "\n";); for (soft& s : m_soft) { s.set_value(m_model->is_true(s.s)); @@ -838,16 +838,17 @@ public: void commit_assignment() override { if (m_found_feasible_optimum) { - TRACE("opt", tout << "Committing feasible solution\ndefs:" << m_defs << "\nasms:" << m_asms << "\n";); add(m_defs); add(m_asms); + TRACE("opt", tout << "Committing feasible solution\ndefs:" << m_defs << "\nasms:" << m_asms << "\n";); + } // else: there is only a single assignment to these soft constraints. } void verify_core(exprs const& core) { return; - IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";); + IF_VERBOSE(1, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); _solver->assert_expr(core); @@ -855,8 +856,11 @@ public: IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << " core size " << core.size() << "\n"); CTRACE("opt", is_sat != l_false, for (expr* c : core) tout << "core: " << mk_pp(c, m) << "\n"; - _solver->display(tout);); - VERIFY(is_sat == l_false); + _solver->display(tout); + tout << "other solver\n"; + s().display(tout); + ); + VERIFY(is_sat == l_false || m.canceled()); } void verify_assumptions() { diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 7fdfbf9aa..9a3ae7728 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1372,7 +1372,7 @@ namespace smt { } while (true) { - TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";); + TRACE("unsat_core_bug", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";); switch (js.get_kind()) { case b_justification::CLAUSE: { clause * cls = js.get_clause(); @@ -1417,7 +1417,7 @@ namespace smt { } while (idx >= 0) { literal l = m_assigned_literals[idx]; - TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";); + CTRACE("unsat_core_bug", m_ctx.is_marked(l.var()), tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << "\n";); if (m_ctx.get_assign_level(l) < search_lvl) goto end_unsat_core; if (m_ctx.is_marked(l.var())) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6f382a5f6..ef018b895 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1358,7 +1358,7 @@ namespace smt { void display_profile(std::ostream & out) const; - void display(std::ostream& out, b_justification j) const; + std::ostream& display(std::ostream& out, b_justification j) const; // ----------------------------------- // diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 72cc2404c..c40b829a7 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -356,9 +356,9 @@ namespace smt { } void context::display_unsat_core(std::ostream & out) const { - unsigned sz = m_unsat_core.size(); - for (unsigned i = 0; i < sz; i++) - out << mk_pp(m_unsat_core.get(i), m_manager) << "\n"; + for (expr* c : m_unsat_core) { + out << mk_pp(c, m_manager) << "\n"; + } } void context::collect_statistics(::statistics & st) const { @@ -563,13 +563,14 @@ namespace smt { } out << "\n"; if (is_app(n)) { - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) - todo.push_back(to_app(n)->get_arg(i)); + for (expr* arg : *to_app(n)) { + todo.push_back(arg); + } } } } - void context::display(std::ostream& out, b_justification j) const { + std::ostream& context::display(std::ostream& out, b_justification j) const { switch (j.get_kind()) { case b_justification::AXIOM: out << "axiom"; @@ -593,7 +594,7 @@ namespace smt { UNREACHABLE(); break; } - out << "\n"; + return out << "\n"; } void context::trace_assign(literal l, b_justification j, bool decision) const { diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 86d84c60a..875fe8de4 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1924,6 +1924,7 @@ namespace smt { process_antecedent(~js.get_literal(), offset); break; case b_justification::AXIOM: + bound = 0; break; case b_justification::JUSTIFICATION: { justification* j = js.get_justification(); @@ -1934,6 +1935,7 @@ namespace smt { } if (pbj == nullptr) { TRACE("pb", tout << "skip justification for " << conseq << "\n";); + bound = 0; // this is possible when conseq is an assumption. // The justification of conseq is itself, // don't increment the cofficient here because it assumes diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2864182eb..37297997a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2905,17 +2905,26 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) { TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";); } else if (is_skolem(m_tail, e)) { - // e = tail(s, l), len(s) > l => - // len(tail(s, l)) = len(s) - l - 1 + // e = tail(s, l), len(s) > l => len(tail(s, l)) = len(s) - l - 1 + // e = tail(s, l), len(s) <= l => len(tail(s, l)) = 0 + s = to_app(e)->get_arg(0); l = to_app(e)->get_arg(1); expr_ref len_s = mk_len(s); literal len_s_gt_l = mk_simplified_literal(m_autil.mk_ge(mk_sub(len_s, l), m_autil.mk_int(1))); - if (ctx.get_assignment(len_s_gt_l) == l_true) { + switch (ctx.get_assignment(len_s_gt_l)) { + case l_true: len = mk_sub(len_s, mk_sub(l, m_autil.mk_int(1))); TRACE("seq", tout << len_s << " " << len << " " << len_s_gt_l << "\n";); lits.push_back(len_s_gt_l); return true; + case l_false: + len = m_autil.mk_int(0); + TRACE("seq", tout << len_s << " " << len << " " << len_s_gt_l << "\n";); + lits.push_back(~len_s_gt_l); + return true; + default: + break; } } else if (m_util.str.is_unit(e)) { From 4f988595c7800dafd63e81015cbce1e0cd32ec3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Jan 2019 19:45:19 -0800 Subject: [PATCH 2/3] fix #2107 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c8b8d27de..9d4c9f852 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3244,8 +3244,13 @@ namespace smt { proof * pr = m_manager.mk_asserted(curr_assumption); internalize_assertion(curr_assumption, pr, 0); literal l = get_literal(curr_assumption); + if (l == true_literal) + continue; + if (l == false_literal) { + set_conflict(b_justification::mk_axiom()); + break; + } m_literal2assumption.insert(l.index(), orig_assumption); - // mark_as_relevant(l); <<< not needed // internalize_assertion marked l as relevant. SASSERT(is_relevant(l)); TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";); From 58f5531cfff1324aa001cd1da6c750669510a87b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Jan 2019 08:18:03 -0800 Subject: [PATCH 3/3] fix #2114 introduced while working on #2095 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 125 ++++++++++++++++++++++------------------- src/sat/sat_solver.h | 1 + src/solver/solver.cpp | 7 ++- 3 files changed, 72 insertions(+), 61 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index fa1d9352d..dd25c9d2b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1664,6 +1664,7 @@ namespace sat { if (m_conflicts_since_init < m_next_simplify) { return; } + log_stats(); m_simplifications++; IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";); @@ -1890,75 +1891,81 @@ namespace sat { m_config.m_restart_margin * m_slow_glue_avg <= m_fast_glue_avg; } + void solver::log_stats() { + m_restart_logs++; + + std::stringstream strm; + strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " " + << std::setw(6) << m_stats.m_decision << " " + << std::setw(4) << m_stats.m_restart + << mk_stat(*this) + << " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n"; + std::string str(strm.str()); + svector nums; + for (size_t i = 0; i < str.size(); ++i) { + while (i < str.size() && str[i] != ' ') ++i; + while (i < str.size() && str[i] == ' ') ++i; + // position of first character after space + if (i < str.size()) { + nums.push_back(i); + } + } + bool same = m_last_positions.size() == nums.size(); + size_t diff = 0; + for (unsigned i = 0; i < nums.size() && same; ++i) { + if (m_last_positions[i] > nums[i]) diff += m_last_positions[i] - nums[i]; + if (m_last_positions[i] < nums[i]) diff += nums[i] - m_last_positions[i]; + } + if (m_last_positions.empty() || + m_restart_logs >= 20 + m_last_position_log || + (m_restart_logs >= 6 + m_last_position_log && (!same || diff > 3))) { + m_last_position_log = m_restart_logs; + // conflicts restarts learned gc time + // decisions clauses units memory + int adjust[9] = { -3, -3, -3, -1, -3, -2, -1, -2, -1 }; + char const* tag[9] = { ":conflicts ", ":decisions ", ":restarts ", ":clauses/bin ", ":learned/bin ", ":units ", ":gc ", ":memory ", ":time" }; + std::stringstream l1, l2; + l1 << "(sat.stats "; + l2 << "(sat.stats "; + size_t p1 = 11, p2 = 11; + SASSERT(nums.size() == 9); + for (unsigned i = 0; i < 9 && i < nums.size(); ++i) { + size_t p = nums[i]; + if (i & 0x1) { + // odd positions + for (; p2 < p + adjust[i]; ++p2) l2 << " "; + p2 += strlen(tag[i]); + l2 << tag[i]; + } + else { + // even positions + for (; p1 < p + adjust[i]; ++p1) l1 << " "; + p1 += strlen(tag[i]); + l1 << tag[i]; + } + } + for (; p1 + 2 < str.size(); ++p1) l1 << " "; + for (; p2 + 2 < str.size(); ++p2) l2 << " "; + l1 << ")\n"; + l2 << ")\n"; + IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str()); + m_last_positions.reset(); + m_last_positions.append(nums); + } + IF_VERBOSE(1, verbose_stream() << str); + } + void solver::restart(bool to_base) { m_stats.m_restart++; m_restarts++; if (m_conflicts_since_init >= m_restart_next_out && get_verbosity_level() >= 1) { - m_restart_logs++; if (0 == m_restart_next_out) { m_restart_next_out = 1; } else { m_restart_next_out = (3*m_restart_next_out)/2 + 1; } - - std::stringstream strm; - strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " " - << std::setw(6) << m_stats.m_decision << " " - << std::setw(4) << m_stats.m_restart - << mk_stat(*this) - << " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n"; - std::string str(strm.str()); - svector nums; - for (size_t i = 0; i < str.size(); ++i) { - while (i < str.size() && str[i] != ' ') ++i; - while (i < str.size() && str[i] == ' ') ++i; - // position of first character after space - if (i < str.size()) { - nums.push_back(i); - } - } - bool same = m_last_positions.size() == nums.size(); - size_t diff = 0; - for (unsigned i = 0; i < nums.size() && same; ++i) { - if (m_last_positions[i] > nums[i]) diff += m_last_positions[i] - nums[i]; - if (m_last_positions[i] < nums[i]) diff += nums[i] - m_last_positions[i]; - } - if (m_last_positions.empty() || m_restart_logs >= 20 + m_last_position_log || (m_restart_logs >= 6 + m_last_position_log && (!same || diff > 3))) { - m_last_position_log = m_restart_logs; - // conflicts restarts learned gc time - // decisions clauses units memory - int adjust[9] = { -3, -3, -3, -1, -3, -2, -1, -2, -1 }; - char const* tag[9] = { ":conflicts ", ":decisions ", ":restarts ", ":clauses/bin ", ":learned/bin ", ":units ", ":gc ", ":memory ", ":time" }; - std::stringstream l1, l2; - l1 << "(sat.stats "; - l2 << "(sat.stats "; - size_t p1 = 11, p2 = 11; - SASSERT(nums.size() == 9); - for (unsigned i = 0; i < 9 && i < nums.size(); ++i) { - size_t p = nums[i]; - if (i & 0x1) { - // odd positions - for (; p2 < p + adjust[i]; ++p2) l2 << " "; - p2 += strlen(tag[i]); - l2 << tag[i]; - } - else { - // even positions - for (; p1 < p + adjust[i]; ++p1) l1 << " "; - p1 += strlen(tag[i]); - l1 << tag[i]; - } - } - for (; p1 + 2 < str.size(); ++p1) l1 << " "; - for (; p2 + 2 < str.size(); ++p2) l2 << " "; - l1 << ")\n"; - l2 << ")\n"; - IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str()); - m_last_positions.reset(); - m_last_positions.append(nums); - } - IF_VERBOSE(1, verbose_stream() << str); + log_stats(); } IF_VERBOSE(30, display_status(verbose_stream());); pop_reinit(restart_level(to_base)); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 48fc54598..96cc53b4a 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -425,6 +425,7 @@ namespace sat { unsigned m_last_position_log; unsigned m_restart_logs; unsigned restart_level(bool to_base); + void log_stats(); bool should_restart() const; void set_next_restart(); bool reached_max_conflicts(); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 6f4880d38..9126ab1a2 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -338,8 +338,11 @@ lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) { } void solver::dump_state(unsigned sz, expr* const* assumptions) { - std::string file = m_cancel_backup_file.str(); - if (file != "") { + if ((symbol::null != m_cancel_backup_file) && + !m_cancel_backup_file.is_numerical() && + m_cancel_backup_file.c_ptr() && + m_cancel_backup_file.bare_str()[0]) { + std::string file = m_cancel_backup_file.str(); std::ofstream ous(file); display(ous, sz, assumptions); }