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

sls updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-12 22:14:57 -07:00
parent 1412c183d4
commit cafb31ff94
3 changed files with 45 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/sat/sat_mus.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include "sat_solver.h" #include "sat_solver.h"
#include "sat_mus.h" #include "sat_mus.h"
#include "sat_sls.h"
namespace sat { namespace sat {
@ -76,11 +77,11 @@ namespace sat {
if (core.empty()) { if (core.empty()) {
break; break;
} }
sz = core.size(); // sz = core.size();
core.append(mus); // measure_mr();
measure_mr(); // core.append(mus);
// rmr(); // rmr();
core.resize(sz); // core.resize(sz);
break; break;
} }
case l_false: case l_false:
@ -115,6 +116,25 @@ namespace sat {
} }
m_model.reset(); m_model.reset();
m_model.append(m2); m_model.append(m2);
sls sls(s);
literal_vector tabu;
tabu.append(m_mus);
tabu.append(m_core);
for (unsigned i = m_mus.size(); i < tabu.size(); ++i) {
tabu[i] = ~tabu[i];
lbool is_sat = sls(tabu.size(), tabu.c_ptr());
tabu[i] = ~tabu[i];
switch (is_sat) {
case l_true:
//m_mus.push_back(tabu[i]);
//m_core.erase(tabu[i]);
std::cout << "in core " << tabu[i] << "\n";
break;
default:
break;
}
}
} }
// //

20
src/sat/sat_sls.cpp
View file

@ -64,13 +64,13 @@ namespace sat {
lbool sls::operator()(unsigned sz, literal const* tabu) { lbool sls::operator()(unsigned sz, literal const* tabu) {
init(sz, tabu); init(sz, tabu);
for (unsigned i = 0; i < m_max_tries; ++i) { for (unsigned i = 0; !m_false.empty() && i < m_max_tries; ++i) {
flip(); flip();
}
if (m_false.empty()) { if (m_false.empty()) {
SASSERT(s.check_model(m_model)); SASSERT(s.check_model(m_model));
return l_true; return l_true;
} }
}
return l_undef; return l_undef;
} }
@ -84,6 +84,7 @@ namespace sat {
for (unsigned i = 0; i < m_bin_clauses.size(); ++i) { for (unsigned i = 0; i < m_bin_clauses.size(); ++i) {
m_alloc.del_clause(m_bin_clauses[i]); m_alloc.del_clause(m_bin_clauses[i]);
} }
m_bin_clauses.reset();
m_clauses.reset(); m_clauses.reset();
clause * const * it = s.begin_clauses(); clause * const * it = s.begin_clauses();
clause * const * end = s.end_clauses(); clause * const * end = s.end_clauses();
@ -108,6 +109,7 @@ namespace sat {
m_tabu.resize(s.num_vars(), false); m_tabu.resize(s.num_vars(), false);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
m_model[tabu[i].var()] = tabu[i].sign()?l_false:l_true; m_model[tabu[i].var()] = tabu[i].sign()?l_false:l_true;
SASSERT(value_at(tabu[i], m_model) == l_true);
} }
sz = m_clauses.size(); sz = m_clauses.size();
@ -116,8 +118,18 @@ namespace sat {
unsigned n = 0; unsigned n = 0;
unsigned csz = c.size(); unsigned csz = c.size();
for (unsigned j = 0; j < csz; ++j) { for (unsigned j = 0; j < csz; ++j) {
if (value_at(c[j], m_model) == l_true) { lbool val = value_at(c[j], m_model);
switch (val) {
case l_true:
++n; ++n;
break;
case l_undef:
++n;
m_model[c[j].var()] = c[j].sign()?l_false:l_true;
SASSERT(value_at(c[j], m_model) == l_true);
break;
default:
break;
} }
} }
m_num_true.push_back(n); m_num_true.push_back(n);
@ -196,7 +208,7 @@ namespace sat {
literal lit; literal lit;
if (!pick_flip(lit)) return; if (!pick_flip(lit)) return;
SASSERT(value_at(lit, m_model) == l_false); SASSERT(value_at(lit, m_model) == l_false);
m_model[lit.var()] = lit.sign()?l_true:l_false; m_model[lit.var()] = lit.sign()?l_false:l_true;
SASSERT(value_at(lit, m_model) == l_true); SASSERT(value_at(lit, m_model) == l_true);
unsigned_vector const& use1 = get_use(lit); unsigned_vector const& use1 = get_use(lit);
unsigned sz = use1.size(); unsigned sz = use1.size();