diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp index 37f708009..dfc15636c 100644 --- a/src/muz/pdr/pdr_dl_interface.cpp +++ b/src/muz/pdr/pdr_dl_interface.cpp @@ -145,6 +145,11 @@ lbool dl_interface::query(expr * query) { query_pred = rules.get_output_predicate(); + TRACE("pdr", + tout << "rules:\n"; + m_ctx.display_rules(tout); + ); + IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); m_pdr_rules.replace_rules(rules); m_pdr_rules.close(); @@ -152,6 +157,7 @@ lbool dl_interface::query(expr * query) { m_ctx.reopen(); m_ctx.replace_rules(old_rules); + scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode. m_context->set_proof_converter(m_ctx.get_proof_converter()); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index e6b452603..016f1ee0e 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -192,9 +192,8 @@ public: lbool mus_solver() { lbool is_sat = l_true; if (!init()) return l_undef; - init_local(); + is_sat = init_local(); trace(); - is_sat = process_mutex(); if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { if (m_lower >= m_upper) break; @@ -233,10 +232,9 @@ public: lbool primal_dual_solver() { if (!init()) return l_undef; - init_local(); + lbool is_sat = init_local(); trace(); exprs cs; - lbool is_sat = process_mutex(); if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { is_sat = check_sat_hill_climb(m_asms); @@ -274,54 +272,6 @@ public: return l_true; } - lbool process_mutex() { - vector mutexes; - lbool is_sat = s().find_mutexes(m_asms, mutexes); - if (is_sat != l_true) { - return is_sat; - } - for (unsigned i = 0; i < mutexes.size(); ++i) { - process_mutex(mutexes[i]); - } - if (!mutexes.empty()) { - trace(); - } - return l_true; - } - - void process_mutex(expr_ref_vector& mutex) { - TRACE("opt", - for (unsigned i = 0; i < mutex.size(); ++i) { - tout << mk_pp(mutex[i].get(), m) << " |-> " << get_weight(mutex[i].get()) << "\n"; - }); - if (mutex.size() <= 1) { - return; - } - sort_assumptions(mutex); - ptr_vector core(mutex.size(), mutex.c_ptr()); - remove_soft(core, m_asms); - rational weight(0), sum1(0), sum2(0); - vector weights; - for (unsigned i = 0; i < mutex.size(); ++i) { - rational w = get_weight(mutex[i].get()); - weights.push_back(w); - sum1 += w; - m_asm2weight.remove(mutex[i].get()); - } - for (unsigned i = mutex.size(); i > 0; ) { - --i; - expr_ref soft(m.mk_or(i+1, mutex.c_ptr()), m); - rational w = weights[i]; - weight = w - weight; - m_lower += weight*rational(i); - sum2 += weight*rational(i+1); - add_soft(soft, weight); - for (; i > 0 && weights[i-1] == w; --i) {} - weight = w; - } - SASSERT(sum1 == sum2); - } - lbool check_sat_hill_climb(expr_ref_vector& asms1) { expr_ref_vector asms(asms1); lbool is_sat = l_true; @@ -854,12 +804,18 @@ public: m_dump_benchmarks = _p.dump_benchmarks(); } - void init_local() { + lbool init_local() { m_upper.reset(); m_lower.reset(); m_trail.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - add_soft(m_soft[i], m_weights[i]); + obj_map new_soft; + lbool is_sat = find_mutexes(new_soft); + if (is_sat != l_true) { + return is_sat; + } + obj_map::iterator it = new_soft.begin(), end = new_soft.end(); + for (; it != end; ++it) { + add_soft(it->m_key, it->m_value); } m_max_upper = m_upper; m_found_feasible_optimum = false; @@ -867,6 +823,7 @@ public: add_upper_bound_block(); m_csmodel = 0; m_correction_set_size = 0; + return l_true; } virtual void commit_assignment() { diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 7d3e8eda9..97ce28166 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -38,7 +38,8 @@ namespace opt { m_c(c), m_soft(soft), m_weights(ws), - m_assertions(m) { + m_assertions(m), + m_trail(m) { c.get_base_model(m_model); SASSERT(m_model); updt_params(c.params()); @@ -152,6 +153,67 @@ namespace opt { verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";); } + lbool maxsmt_solver_base::find_mutexes(obj_map& new_soft) { + m_lower.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + new_soft.insert(m_soft[i], m_weights[i]); + } + vector mutexes; + lbool is_sat = s().find_mutexes(m_soft, mutexes); + if (is_sat != l_true) { + return is_sat; + } + for (unsigned i = 0; i < mutexes.size(); ++i) { + process_mutex(mutexes[i], new_soft); + } + return l_true; + } + + struct maxsmt_compare_soft { + obj_map const& m_soft; + maxsmt_compare_soft(obj_map const& soft): m_soft(soft) {} + bool operator()(expr* a, expr* b) const { + return m_soft.find(a) > m_soft.find(b); + } + }; + + void maxsmt_solver_base::process_mutex(expr_ref_vector& mutex, obj_map& new_soft) { + TRACE("opt", + for (unsigned i = 0; i < mutex.size(); ++i) { + tout << mk_pp(mutex[i].get(), m) << " |-> " << new_soft.find(mutex[i].get()) << "\n"; + }); + if (mutex.size() <= 1) { + return; + } + maxsmt_compare_soft cmp(new_soft); + ptr_vector _mutex(mutex.size(), mutex.c_ptr()); + std::sort(_mutex.begin(), _mutex.end(), cmp); + mutex.reset(); + mutex.append(_mutex.size(), _mutex.c_ptr()); + + rational weight(0), sum1(0), sum2(0); + vector weights; + for (unsigned i = 0; i < mutex.size(); ++i) { + rational w = new_soft.find(mutex[i].get()); + weights.push_back(w); + sum1 += w; + new_soft.remove(mutex[i].get()); + } + for (unsigned i = mutex.size(); i > 0; ) { + --i; + expr_ref soft(m.mk_or(i+1, mutex.c_ptr()), m); + m_trail.push_back(soft); + rational w = weights[i]; + weight = w - weight; + m_lower += weight*rational(i); + sum2 += weight*rational(i+1); + new_soft.insert(soft, weight); + for (; i > 0 && weights[i-1] == w; --i) {} + weight = w; + } + SASSERT(sum1 == sum2); + } + maxsmt::maxsmt(maxsat_context& c, unsigned index): @@ -310,4 +372,5 @@ namespace opt { } + }; diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 57fe12b59..5ecb023f6 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -62,6 +62,7 @@ namespace opt { const expr_ref_vector m_soft; vector m_weights; expr_ref_vector m_assertions; + expr_ref_vector m_trail; rational m_lower; rational m_upper; model_ref m_model; @@ -95,12 +96,17 @@ namespace opt { ~scoped_ensure_theory(); smt::theory_wmaxsat& operator()(); }; + + lbool find_mutexes(obj_map& new_soft); protected: void enable_sls(bool force); void trace_bounds(char const* solver); + void process_mutex(expr_ref_vector& mutex, obj_map& new_soft); + + }; /** diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index ef4989cee..d3ceb9a3b 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -40,19 +40,28 @@ namespace opt { lbool operator()() { TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); - lbool is_sat = l_true; - bool was_sat = false; - for (unsigned i = 0; i < m_soft.size(); ++i) { - wth().assert_weighted(m_soft[i], m_weights[i]); + obj_map soft; + lbool is_sat = find_mutexes(soft); + if (is_sat != l_true) { + return is_sat; } - while (l_true == is_sat) { - is_sat = s().check_sat(0,0); + rational offset = m_lower; + m_upper = offset; + bool was_sat = false; + obj_map::iterator it = soft.begin(), end = soft.end(); + for (; it != end; ++it) { + wth().assert_weighted(it->m_key, it->m_value); + m_upper += it->m_value; + } + trace_bounds("wmax"); + while (l_true == is_sat && m_lower < m_upper) { + is_sat = s().check_sat(0, 0); if (m.canceled()) { is_sat = l_undef; } if (is_sat == l_true) { if (wth().is_optimal()) { - m_upper = wth().get_min_cost(); + m_upper = offset + wth().get_min_cost(); s().get_model(m_model); } expr_ref fml = wth().mk_block(); @@ -63,11 +72,11 @@ namespace opt { } if (was_sat) { wth().get_assignment(m_assignment); + m_upper = offset + wth().get_min_cost(); } if (is_sat == l_false && was_sat) { is_sat = l_true; } - m_upper = wth().get_min_cost(); if (is_sat == l_true) { m_lower = m_upper; } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 35652608c..739af8bfe 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -16,7 +16,7 @@ def_module_params(module_name='smt', ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), - ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (0 means immediate timeout)'), + ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 1c1d236ad..667411be5 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -369,7 +369,7 @@ namespace smt { lbool context::find_mutexes(expr_ref_vector const& vars, vector& mutexes) { - index_set lits; + uint_set lits; for (unsigned i = 0; i < vars.size(); ++i) { expr* n = vars[i]; bool neg = m_manager.is_not(n, n); @@ -379,11 +379,11 @@ namespace smt { } while (!lits.empty()) { literal_vector mutex; - index_set other(lits); + uint_set other(lits); while (!other.empty()) { - index_set conseq; + uint_set conseq; literal p = to_literal(*other.begin()); - other.erase(p.index()); + other.remove(p.index()); mutex.push_back(p); if (other.empty()) { break; @@ -407,11 +407,12 @@ namespace smt { return l_true; } - void context::get_reachable(literal p, index_set& goal, index_set& reachable) { - index_set seen; + void context::get_reachable(literal p, uint_set& goal, uint_set& reachable) { + uint_set seen; literal_vector todo; todo.push_back(p); while (!todo.empty()) { + // std::cout << "todo: " << todo.size() << "\n"; p = todo.back(); todo.pop_back(); if (seen.contains(p.index())) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index d9f24ddf6..84459d272 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1371,7 +1371,7 @@ namespace smt { \brief Auxiliry function for mutex finding. */ - void get_reachable(literal p, index_set& goal, index_set& reached); + void get_reachable(literal p, uint_set& goal, uint_set& reached); public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 73e427b0b..a2f8ceba9 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1289,7 +1289,7 @@ namespace smt { m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars; m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses; - IF_VERBOSE(1, verbose_stream() + IF_VERBOSE(2, verbose_stream() << "(smt.pb compile sorting network bound: " << k << " literals: " << in.size() << " clauses: " << sortnw.m_stats.m_num_compiled_clauses diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index bf3ca9b67..335b2c3bb 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -231,7 +231,7 @@ struct scoped_timer::imp { }; scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { - if (ms != UINT_MAX) + if (ms != UINT_MAX && ms != 0) m_imp = alloc(imp, ms, eh); else m_imp = 0;