mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3632

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 20:53:10 -07:00
parent fe267803d1
commit ddc77b1100
2 changed files with 17 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/sat/sat_local_search.cpp
View file

@ -31,7 +31,9 @@ namespace sat {
for (unsigned i = 0; i < m_assumptions.size(); ++i) { for (unsigned i = 0; i < m_assumptions.size(); ++i) {
add_clause(1, m_assumptions.c_ptr() + i); add_clause(1, m_assumptions.c_ptr() + i);
} }
if (m_is_unsat)
return;
// add sentinel variable. // add sentinel variable.
m_vars.push_back(var_info()); m_vars.push_back(var_info());
@ -334,7 +336,12 @@ namespace sat {
void local_search::add_unit(literal lit, literal exp) { void local_search::add_unit(literal lit, literal exp) {
bool_var v = lit.var(); bool_var v = lit.var();
if (is_unit(lit)) return; if (is_unit(lit)) {
if (m_vars[v].m_value == lit.sign()) {
m_is_unsat = true;
}
return;
}
SASSERT(!m_units.contains(v)); SASSERT(!m_units.contains(v));
if (m_vars[v].m_value == lit.sign() && !m_initializing) { if (m_vars[v].m_value == lit.sign() && !m_initializing) {
flip_walksat(v); flip_walksat(v);
@ -575,8 +582,11 @@ namespace sat {
m_assumptions.append(sz, assumptions); m_assumptions.append(sz, assumptions);
unsigned num_units = m_units.size(); unsigned num_units = m_units.size();
init(); init();
if (m_is_unsat)
return l_false;
walksat(); walksat();
TRACE("sat", tout << m_units << "\n";);
// remove unit clauses // remove unit clauses
for (unsigned i = m_units.size(); i-- > num_units; ) { for (unsigned i = m_units.size(); i-- > num_units; ) {
m_vars[m_units[i]].m_unit = false; m_vars[m_units[i]].m_unit = false;

5
src/sat/sat_solver.cpp
View file

@ -1282,7 +1282,10 @@ namespace sat {
struct scoped_ls { struct scoped_ls {
solver& s; solver& s;
scoped_ls(solver& s): s(s) {} scoped_ls(solver& s): s(s) {}
~scoped_ls() { dealloc(s.m_local_search); s.m_local_search = nullptr; } ~scoped_ls() {
dealloc(s.m_local_search);
s.m_local_search = nullptr;
}
}; };
scoped_ls _ls(*this); scoped_ls _ls(*this);
if (inconsistent()) return l_false; if (inconsistent()) return l_false;