mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-06 10:58:47 -07:00
parent eed87807c5
commit c388d99c35
4 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_extension.h
View file

@ -128,6 +128,7 @@ namespace sat {
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) { std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {
return false; return false;
} }
virtual bool is_pb() { return false; }
}; };
}; };

11
src/sat/sat_local_search.cpp
View file

@ -380,16 +380,14 @@ namespace sat {
if (m_config.phase_sticky()) { if (m_config.phase_sticky()) {
unsigned v = 0; unsigned v = 0;
for (var_info& vi : m_vars) { for (var_info& vi : m_vars)
vi.m_bias = s.m_phase[v++] ? 98 : 2; vi.m_bias = s.m_phase[v++] ? 98 : 2;
}
} }
// copy units // copy units
unsigned trail_sz = s.init_trail_size(); unsigned trail_sz = s.init_trail_size();
for (unsigned i = 0; i < trail_sz; ++i) { for (unsigned i = 0; i < trail_sz; ++i)
add_clause(1, s.m_trail.data() + i); add_clause(1, s.m_trail.data() + i);
}
// copy binary clauses // copy binary clauses
{ {
@ -410,9 +408,8 @@ namespace sat {
} }
// copy clauses // copy clauses
for (clause* c : s.m_clauses) { for (clause* c : s.m_clauses)
add_clause(c->size(), c->begin()); add_clause(c->size(), c->begin());
}
m_num_non_binary_clauses = s.m_clauses.size(); m_num_non_binary_clauses = s.m_clauses.size();
@ -422,7 +419,7 @@ namespace sat {
[&](unsigned sz, literal const* c, unsigned k) { add_cardinality(sz, c, k); }; [&](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 = 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); }; [&](unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { add_pb(sz, c, coeffs, k); };
if (ext && !ext->extract_pb(card, pb)) if (ext && (!ext->is_pb() || !ext->extract_pb(card, pb)))
throw default_exception("local search is incomplete with extensions beyond PB"); throw default_exception("local search is incomplete with extensions beyond PB");
if (_init) { if (_init) {

3
src/sat/sat_solver.cpp
View file

@ -1396,7 +1396,8 @@ namespace sat {
} }
}; };
scoped_ls _ls(*this); scoped_ls _ls(*this);
if (inconsistent()) return l_false; if (inconsistent())
return l_false;
scoped_limits scoped_rl(rlimit()); scoped_limits scoped_rl(rlimit());
SASSERT(m_local_search); SASSERT(m_local_search);
m_local_search->add(*this); m_local_search->add(*this);

1
src/sat/smt/pb_solver.h
View file

@ -211,6 +211,7 @@ namespace pb {
unsigned next_id() { return m_constraint_id++; } unsigned next_id() { return m_constraint_id++; }
void set_non_learned(constraint& c); void set_non_learned(constraint& c);
double get_reward(literal l, sat::ext_justification_idx idx, sat::literal_occs_fun& occs) const override; double get_reward(literal l, sat::ext_justification_idx idx, sat::literal_occs_fun& occs) const override;
bool is_pb() override { return true; }
// cardinality // cardinality
lbool add_assign(card& c, literal lit); lbool add_assign(card& c, literal lit);