mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-24 20:16:00 +00:00
Code Activity

mus logging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-11 08:06:29 -07:00
parent 1652c16163
commit 470b5c11b9
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/sat_mus.cpp
View file

@ -59,7 +59,7 @@ namespace sat {
literal lit = core.back(); literal lit = core.back();
core.pop_back(); core.pop_back();
unsigned sz = mus.size(); unsigned sz = mus.size();
//mus.push_back(~lit); // TBD: measure mus.push_back(~lit); // TBD: measure
mus.append(core); mus.append(core);
lbool is_sat = s.check(mus.size(), mus.c_ptr()); lbool is_sat = s.check(mus.size(), mus.c_ptr());
mus.resize(sz); mus.resize(sz);
@ -78,7 +78,6 @@ namespace sat {
core.append(mus); core.append(mus);
rmr(); rmr();
core.resize(sz); core.resize(sz);
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << mus << " " << core << ")\n";);
break; break;
} }
case l_false: case l_false:
@ -86,7 +85,6 @@ namespace sat {
if (new_core.contains(~lit)) { if (new_core.contains(~lit)) {
break; break;
} }
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << new_core << ")\n";);
core.reset(); core.reset();
for (unsigned i = 0; i < new_core.size(); ++i) { for (unsigned i = 0; i < new_core.size(); ++i) {
literal lit = new_core[i]; literal lit = new_core[i];
@ -99,10 +97,13 @@ namespace sat {
} }
TRACE("sat", tout << "new core: " << mus << "\n";); TRACE("sat", tout << "new core: " << mus << "\n";);
set_core(); set_core();
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << core << ")\n";);
return l_true; return l_true;
} }
void mus::rmr() { void mus::rmr() {
return;
#if 0
model& model = s.m_model; model& model = s.m_model;
literal lit = m_mus.back(); literal lit = m_mus.back();
literal assumption_lit; literal assumption_lit;
@ -122,6 +123,7 @@ namespace sat {
model[lit.var()] = ~model[lit.var()]; // swap assignment back model[lit.var()] = ~model[lit.var()]; // swap assignment back
} }
m_toswap.resize(sz); m_toswap.resize(sz);
#endif
} }
bool mus::has_single_unsat(literal& assumption_lit) { bool mus::has_single_unsat(literal& assumption_lit) {
@ -138,7 +140,7 @@ namespace sat {
// //
void mus::find_swappable(literal lit) { void mus::find_swappable(literal lit) {
IF_VERBOSE(2, verbose_stream() << "(sat.mus swap " << lit << ")\n";); IF_VERBOSE(3, verbose_stream() << "(sat.mus swap " << lit << ")\n";);
unsigned sz = m_toswap.size(); unsigned sz = m_toswap.size();
literal lit2, lit3; literal lit2, lit3;
model const& model = s.get_model(); model const& model = s.get_model();