mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

support self-subsumption, remove verbose log 0

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-11 21:21:55 -08:00
parent 8fb7fb9f98
commit bb4888ce31
2 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/sat/ba_solver.cpp
View file

@ -3439,7 +3439,7 @@ namespace sat {
- A >= k subsumes A + B >= k' for k' <= k - A >= k subsumes A + B >= k' for k' <= k
- A + A' >= k subsumes A + B >= k' for k' + |A'| <= k - A + A' >= k subsumes A + B >= k' for k' + |A'| <= k
- A + lit >= k self subsumes A + ~lit + B >= k' into A + B >= k' for k' <= k - A + lit >= k self subsumes A + ~lit + B >= k' into A + B >= k' for k' <= k
- TBD: consider version that generalizes self-subsumption to more than one literal - version that generalizes self-subsumption to more than one literal
A + ~L + B >= k' => A + B >= k' if A + A' + L >= k and k' + |L| + |A'| <= k A + ~L + B >= k' => A + B >= k' if A + A' + L >= k and k' + |L| + |A'| <= k
*/ */
bool ba_solver::subsumes(card& c1, card& c2, literal_vector & comp) { bool ba_solver::subsumes(card& c1, card& c2, literal_vector & comp) {
@ -3480,12 +3480,14 @@ namespace sat {
} }
} }
if (!comp.empty()) { unsigned c1_exclusive = c1.size() - common - comp.size();
// self-subsumption is TBD. bool result = c1_exclusive + 1 <= c1.k();
if (!comp.empty() && result) {
IF_VERBOSE(10, verbose_stream() << "self-subsume clause " << c2 << " is TBD\n";);
return false; return false;
} }
unsigned c1_exclusive = c1.size() - common - comp.size(); return result;
return c1_exclusive + 1 <= c1.k();
} }
/* /*
@ -3559,22 +3561,20 @@ namespace sat {
} }
else { else {
TRACE("ba", tout << "self subsume cardinality\n";); TRACE("ba", tout << "self subsume cardinality\n";);
IF_VERBOSE(0, IF_VERBOSE(11,
verbose_stream() << "self-subsume cardinality is TBD\n"; verbose_stream() << "self-subsume cardinality\n";
verbose_stream() << c1 << "\n"; verbose_stream() << c1 << "\n";
verbose_stream() << c2 << "\n";); verbose_stream() << c2 << "\n";);
#if 0
clear_watch(c2); clear_watch(c2);
unsigned j = 0;
for (unsigned i = 0; i < c2.size(); ++i) { for (unsigned i = 0; i < c2.size(); ++i) {
if (slit == c2[i]) { if (!is_marked(~c2[i])) {
c2.swap(i, c2.size() -1); c2[j++] = c2[i];
break;
} }
} }
c2.set_size(c2.size() - 1); c2.set_size(j);
init_watch(c2); init_watch(c2);
m_simplify_change = true; m_simplify_change = true;
#endif
} }
} }
} }
@ -3594,7 +3594,7 @@ namespace sat {
c1.set_learned(false); c1.set_learned(false);
} }
else { else {
IF_VERBOSE(0, verbose_stream() << "self-subsume clause is TBD\n";); IF_VERBOSE(11, verbose_stream() << "self-subsume clause is TBD\n";);
// remove literal slit from c2. // remove literal slit from c2.
TRACE("ba", tout << "TBD remove literals " << slit << " from " << c2 << "\n";); TRACE("ba", tout << "TBD remove literals " << slit << " from " << c2 << "\n";);
} }

2
src/sat/sat_solver.cpp
View file

@ -1860,7 +1860,7 @@ namespace sat {
void solver::gc_half(char const * st_name) { void solver::gc_half(char const * st_name) {
TRACE("sat", tout << "gc\n";); TRACE("sat", tout << "gc\n";);
unsigned sz = m_learned.size(); unsigned sz = m_learned.size();
unsigned new_sz = sz/2; unsigned new_sz = sz/2; // std::min(sz/2, m_clauses.size()*2);
unsigned j = new_sz; unsigned j = new_sz;
for (unsigned i = new_sz; i < sz; i++) { for (unsigned i = new_sz; i < sz; i++) {
clause & c = *(m_learned[i]); clause & c = *(m_learned[i]);