mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

redoing pd-maxres

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-20 18:09:43 -07:00
parent a9807878ea
commit 954e612188
2 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_justification.h
View file

@ -30,9 +30,9 @@ namespace sat {
justification(ext_justification_idx idx, kind k):m_val1(idx), m_val2(k) {} justification(ext_justification_idx idx, kind k):m_val1(idx), m_val2(k) {}
public: public:
justification():m_val1(0), m_val2(NONE) {} justification():m_val1(0), m_val2(NONE) {}
justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {} explicit justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {}
justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {} justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {} explicit justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {}
justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); } justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
kind get_kind() const { return static_cast<kind>(m_val2 & 7); } kind get_kind() const { return static_cast<kind>(m_val2 & 7); }

11
src/sat/sat_solver.cpp
View file

@ -925,7 +925,6 @@ namespace sat {
else { else {
svector<literal> blocker; svector<literal> blocker;
if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) { if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) {
++m_stats.m_blocked_corr_sets;
pop_to_base_level(); pop_to_base_level();
mk_clause(blocker.size(), blocker.c_ptr()); mk_clause(blocker.size(), blocker.c_ptr());
goto retry_init_assumptions; goto retry_init_assumptions;
@ -952,6 +951,7 @@ namespace sat {
literal lit = lits[i]; literal lit = lits[i];
SASSERT(is_external(lit.var())); SASSERT(is_external(lit.var()));
m_assumption_set.insert(lit); m_assumption_set.insert(lit);
TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";);
switch(value(lit)) { switch(value(lit)) {
case l_undef: case l_undef:
@ -959,13 +959,15 @@ namespace sat {
assign(lit, justification()); assign(lit, justification());
break; break;
case l_false: { case l_false: {
set_conflict(lit); SASSERT(!inconsistent());
set_conflict(justification(), ~lit);
flet<bool> _min1(m_config.m_minimize_core, false); flet<bool> _min1(m_config.m_minimize_core, false);
flet<bool> _min2(m_config.m_minimize_core_partial, false); flet<bool> _min2(m_config.m_minimize_core_partial, false);
resolve_conflict_for_unsat_core(); resolve_conflict_for_unsat_core();
weight += weights[i]; weight += weights[i];
blocker.push_back(~lit); blocker.push_back(lit);
SASSERT(m_core.size() <= m_assumptions.size()); TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";);
SASSERT(m_core.size() <= m_assumptions.size() + 1);
SASSERT(m_assumptions.size() <= i); SASSERT(m_assumptions.size() <= i);
if (m_core.size() <= 3 || m_core.size() < blocker.size()) { if (m_core.size() <= 3 || m_core.size() < blocker.size()) {
TRACE("opt", tout << "found small core: " << m_core.size() << "\n";); TRACE("opt", tout << "found small core: " << m_core.size() << "\n";);
@ -973,6 +975,7 @@ namespace sat {
} }
m_inconsistent = false; m_inconsistent = false;
if (weight >= max_weight) { if (weight >= max_weight) {
++m_stats.m_blocked_corr_sets;
TRACE("opt", tout << "blocking soft correction set: " << blocker.size() << "\n";); TRACE("opt", tout << "blocking soft correction set: " << blocker.size() << "\n";);
// block the current correction set candidate. // block the current correction set candidate.
return false; return false;