mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
working on new clause organization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
7b9156dd5b
commit
1149955893
2 changed files with 67 additions and 6 deletions
|
|
@ -337,7 +337,9 @@ namespace sat {
|
|||
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
|
||||
literal lit = to_literal(idx);
|
||||
if (is_false(lit)) {
|
||||
unsigned sz = m_ternary_count[lit.index()];
|
||||
for (binary const& b : m_ternary[lit.index()]) {
|
||||
if (sz-- == 0) break;
|
||||
if (is_false(b.m_u) && is_false(b.m_v))
|
||||
return true;
|
||||
}
|
||||
|
|
@ -402,7 +404,9 @@ namespace sat {
|
|||
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
|
||||
literal lit = to_literal(idx);
|
||||
if (!is_true(lit)) {
|
||||
unsigned sz = m_ternary_count[lit.index()];
|
||||
for (binary const& b : m_ternary[lit.index()]) {
|
||||
if (sz-- == 0) break;
|
||||
if (!is_true(b.m_u) && !is_true(b.m_v))
|
||||
return false;
|
||||
}
|
||||
|
|
@ -474,6 +478,27 @@ namespace sat {
|
|||
for (literal lit : m_binary[l.index()]) {
|
||||
if (is_undef(lit)) sum += literal_occs(lit) / 4.0;
|
||||
}
|
||||
#ifdef NEW_CLAUSE
|
||||
unsigned sz = m_ternary_count[(~l).index()];
|
||||
for (binary const& b : m_ternary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
sum += (literal_occs(b.m_u) + literal_occs(b.m_v)) / 8.0;
|
||||
}
|
||||
sz = m_clause_count[(~l).index()];
|
||||
for (unsigned idx : m_clauses[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
literal lit;
|
||||
unsigned j = idx;
|
||||
double to_add = 0;
|
||||
while ((lit = to_literal(m_clause_literals[++j])) != null_literal) {
|
||||
if (!is_fixed(lit) && lit != ~l) {
|
||||
to_add += literal_occs(lit);
|
||||
}
|
||||
}
|
||||
unsigned len = m_clause_literals[idx];
|
||||
sum += pow(0.5, len) * to_add / len;
|
||||
}
|
||||
#else
|
||||
watch_list& wlist = m_watches[l.index()];
|
||||
for (auto & w : wlist) {
|
||||
switch (w.get_kind()) {
|
||||
|
|
@ -506,6 +531,7 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
return sum;
|
||||
}
|
||||
|
||||
|
|
@ -521,8 +547,16 @@ namespace sat {
|
|||
double lookahead::heule_unit_score(literal l) {
|
||||
double sum = 0;
|
||||
for (literal lit : m_binary[l.index()]) {
|
||||
if (is_undef(lit)) sum += 0.25;
|
||||
if (is_undef(lit)) sum += 0.5;
|
||||
}
|
||||
#ifdef NEW_CLAUSE
|
||||
sum += 0.25 * m_ternary_count[(~l).index()];
|
||||
unsigned sz = m_clause_count[(~l).index()];
|
||||
for (unsigned cls_idx : m_clauses[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
sum += pow(0.5, m_clause_literals[cls_idx]);
|
||||
}
|
||||
#else
|
||||
watch_list& wlist = m_watches[l.index()];
|
||||
for (auto & w : wlist) {
|
||||
switch (w.get_kind()) {
|
||||
|
|
@ -553,6 +587,7 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
return sum;
|
||||
}
|
||||
|
||||
|
|
@ -590,6 +625,13 @@ namespace sat {
|
|||
if (is_undef(lit)) sum += h[lit.index()];
|
||||
// if (m_freevars.contains(lit.var())) sum += h[lit.index()];
|
||||
}
|
||||
#ifdef NEW_CLAUSE
|
||||
unsigned sz = m_ternary_count[(~l).index()];
|
||||
for (binary const& b : m_ternary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
tsum += h[b.m_u.index()] * h[b.m_v.index()];
|
||||
}
|
||||
#else
|
||||
watch_list& wlist = m_watches[l.index()];
|
||||
for (auto & w : wlist) {
|
||||
switch (w.get_kind()) {
|
||||
|
|
@ -621,6 +663,7 @@ namespace sat {
|
|||
}
|
||||
// std::cout << "tsum: " << tsum << "\n";
|
||||
}
|
||||
#endif
|
||||
// std::cout << "sum: " << sum << " afactor " << afactor << " sqfactor " << sqfactor << " tsum " << tsum << "\n";
|
||||
sum = (double)(0.1 + afactor*sum + sqfactor*tsum);
|
||||
// std::cout << "sum: " << sum << " max score " << m_config.m_max_score << "\n";
|
||||
|
|
@ -990,8 +1033,10 @@ namespace sat {
|
|||
m_binary.push_back(literal_vector());
|
||||
m_watches.push_back(watch_list());
|
||||
m_watches.push_back(watch_list());
|
||||
#ifndef NEW_CLAUSE
|
||||
m_full_watches.push_back(clause_vector());
|
||||
m_full_watches.push_back(clause_vector());
|
||||
#endif
|
||||
m_bstamp.push_back(0);
|
||||
m_bstamp.push_back(0);
|
||||
m_stamp.push_back(0);
|
||||
|
|
@ -1238,6 +1283,7 @@ namespace sat {
|
|||
m_wstack.reset();
|
||||
}
|
||||
|
||||
#ifndef NEW_CLAUSE
|
||||
clause const& lookahead::get_clause(watch_list::iterator it) const {
|
||||
clause_offset cls_off = it->get_clause_offset();
|
||||
return *(m_cls_allocator.get_clause(cls_off));
|
||||
|
|
@ -1248,7 +1294,7 @@ namespace sat {
|
|||
DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(is_false(c[j])););
|
||||
return r;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
//
|
||||
// The current version is modeled after CDCL SAT solving data-structures.
|
||||
|
|
@ -1386,11 +1432,15 @@ namespace sat {
|
|||
}
|
||||
|
||||
void lookahead::restore_ternary(literal l) {
|
||||
unsigned sz = m_ternary_count[(~l).index()];
|
||||
for (binary const& b : m_ternary[(~l).index()]) {
|
||||
if (sz-- == 0) break;
|
||||
m_ternary_count[b.m_u.index()]++;
|
||||
m_ternary_count[b.m_v.index()]++;
|
||||
}
|
||||
sz = m_ternary_count[l.index()];
|
||||
for (binary const& b : m_ternary[l.index()]) {
|
||||
if (sz-- == 0) break;
|
||||
m_ternary_count[b.m_u.index()]++;
|
||||
m_ternary_count[b.m_v.index()]++;
|
||||
}
|
||||
|
|
@ -2020,6 +2070,7 @@ namespace sat {
|
|||
|
||||
bool lookahead::check_autarky(literal l, unsigned level) {
|
||||
return false;
|
||||
#if 0
|
||||
// no propagations are allowed to reduce clauses.
|
||||
for (clause * cp : m_full_watches[l.index()]) {
|
||||
clause& c = *cp;
|
||||
|
|
@ -2049,6 +2100,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
return true;
|
||||
#endif
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -2061,9 +2113,11 @@ namespace sat {
|
|||
++m_stats.m_autarky_propagations;
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";);
|
||||
|
||||
#ifdef NEW_CLAUSE
|
||||
TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()]
|
||||
<< " "
|
||||
<< (!m_binary[l.index()].empty() || !m_full_watches[l.index()].empty()) << "\n";);
|
||||
<< (!m_binary[l.index()].empty() || m_clause_count[l.index()] != 0) << "\n";);
|
||||
#endif
|
||||
reset_lookahead_reward();
|
||||
assign(l);
|
||||
propagate();
|
||||
|
|
@ -2341,7 +2395,9 @@ namespace sat {
|
|||
|
||||
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
|
||||
literal lit = to_literal(idx);
|
||||
unsigned sz = m_ternary_count[idx];
|
||||
for (binary const& b : m_ternary[idx]) {
|
||||
if (sz-- == 0) break;
|
||||
if (idx < b.m_u.index() && idx << b.m_v.index()) {
|
||||
out << lit << " " << b.m_u << " " << b.m_v << "\n";
|
||||
}
|
||||
|
|
@ -2555,10 +2611,11 @@ namespace sat {
|
|||
out << "free vars: ";
|
||||
for (bool_var b : m_freevars) out << b << " ";
|
||||
out << "\n";
|
||||
clause_allocator dummy_allocator;
|
||||
for (unsigned i = 0; i < m_watches.size(); ++i) {
|
||||
watch_list const& wl = m_watches[i];
|
||||
if (!wl.empty()) {
|
||||
sat::display_watch_list(out << to_literal(i) << " -> ", m_cls_allocator, wl);
|
||||
sat::display_watch_list(out << to_literal(i) << " -> ", dummy_allocator, wl);
|
||||
out << "\n";
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -125,10 +125,12 @@ namespace sat {
|
|||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
||||
#ifndef NEW_CLAUSE
|
||||
struct ternary {
|
||||
ternary(literal u, literal v, literal w): m_u(u), m_v(v), m_w(w) {}
|
||||
literal m_u, m_v, m_w;
|
||||
};
|
||||
#endif
|
||||
|
||||
#ifdef NEW_CLAUSE
|
||||
struct binary {
|
||||
|
|
@ -172,10 +174,10 @@ namespace sat {
|
|||
clause_vector m_clauses; // non-binary clauses
|
||||
clause_vector m_retired_clauses; // clauses that were removed during search
|
||||
unsigned_vector m_retired_clause_lim;
|
||||
#endif
|
||||
svector<ternary> m_retired_ternary; // ternary removed during search
|
||||
unsigned_vector m_retired_ternary_lim;
|
||||
clause_allocator m_cls_allocator;
|
||||
clause_allocator m_cls_allocator;
|
||||
#endif
|
||||
bool m_inconsistent;
|
||||
unsigned_vector m_bstamp; // literal: timestamp for binary implication
|
||||
vector<svector<double> > m_H; // literal: fitness score
|
||||
|
|
@ -188,7 +190,9 @@ namespace sat {
|
|||
const unsigned c_fixed_truth = UINT_MAX - 1;
|
||||
vector<watch_list> m_watches; // literal: watch structure
|
||||
svector<lit_info> m_lits; // literal: attributes.
|
||||
#ifndef NEW_CLAUSE
|
||||
vector<clause_vector> m_full_watches; // literal: full watch list, used to ensure that autarky reduction is sound
|
||||
#endif
|
||||
double m_lookahead_reward; // metric associated with current lookahead1 literal.
|
||||
literal_vector m_wstack; // windofall stack that is populated in lookahead1 mode
|
||||
uint64 m_prefix; // where we are in search tree
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue