mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-28 14:08:55 +00:00
Code Activity

set clean shutdown for local search and re-enable local search when it parallelizes with PB solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-06-30 16:06:44 -07:00
parent b2b3bab246
commit 8de2544abb
4 changed files with 24 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/sat_local_search.cpp
View file

@ -362,7 +362,7 @@ namespace sat {
set_phase(i, phase[i]);
}
void local_search::import(solver const& s, bool _init) {
void local_search::import(solver const& s, bool _init) {
flet<bool> linit(m_initializing, true);
m_is_pb = false;
m_vars.reset();
@ -412,9 +412,10 @@ namespace sat {
[&](unsigned sz, literal const* c, unsigned k) { add_cardinality(sz, c, k); };
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)> pb =
[&](unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { add_pb(sz, c, coeffs, k); };
if (ext && (!ext->is_pb() || !ext->extract_pb(card, pb)))
if (ext && (!ext->is_pb() || !ext->extract_pb(card, pb))) {
IF_VERBOSE(0, verbose_stream() << (ext) << " is-pb " << (!ext && ext->is_pb()) << "\n");
throw default_exception("local search is incomplete with extensions beyond PB");
}
if (_init)
init();
}