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

adding in-processing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-24 18:27:32 -07:00
parent fb84ba8c34
commit c3d29e75ef
9 changed files with 484 additions and 106 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

461
src/sat/card_extension.cpp
View file

@ -51,10 +51,17 @@ namespace sat {
m_max_sum(0) {
for (unsigned i = 0; i < wlits.size(); ++i) {
m_wlits[i] = wlits[i];
if (m_max_sum + wlits[i].first < m_max_sum) {
}
update_max_sum();
}
void card_extension::pb::update_max_sum() {
m_max_sum = 0;
for (unsigned i = 0; i < size(); ++i) {
if (m_max_sum + m_wlits[i].first < m_max_sum) {
throw default_exception("addition of pb coefficients overflows");
}
m_max_sum += wlits[i].first;
m_max_sum += m_wlits[i].first;
}
}
@ -196,13 +203,12 @@ namespace sat {
// pb:
void card_extension::copy_pb(card_extension& result) {
for (unsigned i = 0; i < m_pbs.size(); ++i) {
for (pb* p : m_pbs) {
svector<wliteral> wlits;
pb& p = *m_pbs[i];
for (unsigned i = 0; i < p.size(); ++i) {
wlits.push_back(p[i]);
for (wliteral w : *p) {
wlits.push_back(w);
}
result.add_pb_ge(p.lit(), wlits, p.k());
result.add_pb_ge(p->lit(), wlits, p->k());
}
}
@ -437,6 +443,151 @@ namespace sat {
}
}
void card_extension::unit_propagation_simplification(literal lit, literal_vector const& lits) {
if (lit == null_literal) {
for (literal l : lits) {
if (value(l) == l_undef) {
s().assign(l, justification());
}
}
}
else {
// add clauses for: p.lit() <=> conjunction of undef literals
SASSERT(value(lit) == l_undef);
literal_vector cl;
cl.push_back(lit);
for (literal l : lits) {
if (value(l) == l_undef) {
s().mk_clause(~lit, l);
cl.push_back(~l);
}
}
s().mk_clause(cl);
}
}
bool card_extension::is_cardinality(pb const& p) {
if (p.size() == 0) return false;
unsigned w = p[0].first;
for (unsigned i = 1; i < p.size(); ++i) {
if (w != p[i].first) return false;
}
return true;
}
void card_extension::simplify2(pb& p) {
if (is_cardinality(p)) {
literal_vector lits(p.literals());
unsigned k = (p.k() + p[0].first - 1) / p[0].first;
add_at_least(p.lit(), lits, k);
remove_constraint(p);
return;
}
if (p.lit() == null_literal) {
unsigned max_sum = p.max_sum();
unsigned sz = p.size();
for (unsigned i = 0; i < sz; ++i) {
wliteral wl = p[i];
if (p.k() > max_sum - wl.first) {
std::cout << "unit literal\n";
}
}
}
}
void card_extension::simplify(pb& p) {
s().pop_to_base_level();
if (p.lit() != null_literal && value(p.lit()) == l_false) {
return;
init_watch(p, !p.lit().sign());
std::cout << "pb: flip sign\n";
}
if (p.lit() != null_literal && value(p.lit()) == l_true) {
std::cout << "literal is assigned at base level " << s().at_base_lvl() << "\n";
SASSERT(lvl(p.lit()) == 0);
nullify_tracking_literal(p);
}
SASSERT(p.lit() == null_literal || value(p.lit()) == l_undef);
unsigned true_val = 0, slack = 0, num_false = 0;
for (wliteral wl : p) {
switch (value(wl.second)) {
case l_true: true_val += wl.first; break;
case l_false: ++num_false; break;
default: slack += wl.first; break;
}
}
if (true_val == 0 && num_false == 0) {
// no op
}
else if (true_val >= p.k()) {
std::cout << "tautology\n";
if (p.lit() != null_literal) {
std::cout << "tautology at level 0\n";
s().assign(p.lit(), justification());
}
remove_constraint(p);
}
else if (slack + true_val < p.k()) {
if (p.lit() != null_literal) {
s().assign(~p.lit(), justification());
}
else {
std::cout << "unsat during simplification\n";
s().set_conflict(justification());
}
remove_constraint(p);
}
else if (slack + true_val == p.k()) {
std::cout << "unit propagation\n";
literal_vector lits(p.literals());
unit_propagation_simplification(p.lit(), lits);
remove_constraint(p);
}
else {
std::cout << "pb value at base: " << true_val << " false: " << num_false << " size: " << p.size() << " k: " << p.k() << "\n";
unsigned sz = p.size();
clear_watch(p);
for (unsigned i = 0; i < sz; ++i) {
if (value(p[i].second) != l_undef) {
--sz;
p.swap(i, sz);
--i;
}
}
std::cout << "new size: " << sz << " old size " << p.size() << "\n";
p.update_size(sz);
p.update_k(p.k() - true_val);
// display(std::cout, c, true);
if (p.lit() == null_literal) {
init_watch(p, true);
}
else {
SASSERT(value(p.lit()) == l_undef);
// c will be watched once c.lit() is assigned.
}
simplify2(p);
}
}
void card_extension::nullify_tracking_literal(pb& p) {
if (p.lit() != null_literal) {
get_wlist(p.lit()).erase(watched(p.index()));
get_wlist(~p.lit()).erase(watched(p.index()));
p.nullify_literal();
}
}
void card_extension::remove_constraint(pb& p) {
clear_watch(p);
nullify_tracking_literal(p);
m_pbs[index2position(p.index())] = 0;
dealloc(&p);
}
void card_extension::display(std::ostream& out, pb const& p, bool values) const {
if (p.lit() != null_literal) out << p.lit() << " == ";
if (p.lit() != null_literal && values) {
@ -469,13 +620,10 @@ namespace sat {
// xor:
void card_extension::copy_xor(card_extension& result) {
for (unsigned i = 0; i < m_xors.size(); ++i) {
for (xor* x : m_xors) {
literal_vector lits;
xor& x = *m_xors[i];
for (literal l : x) {
lits.push_back(l);
}
result.add_xor(x.lit(), lits);
for (literal l : *x) lits.push_back(l);
result.add_xor(x->lit(), lits);
}
}
@ -872,7 +1020,7 @@ namespace sat {
for (unsigned i = 0; 0 <= slack && i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
int coeff = get_coeff(v);
lbool val = m_solver->value(v);
lbool val = s().value(v);
bool is_true = val == l_true;
bool append = coeff != 0 && val != l_undef && (coeff < 0 == is_true);
if (append) {
@ -1004,22 +1152,8 @@ namespace sat {
card_extension::~card_extension() {
m_stats.reset();
}
void card_extension::add_at_least(literal lit, literal_vector const& lits, unsigned k) {
unsigned index = 4*m_cards.size();
SASSERT(is_card_index(index));
card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
m_cards.push_back(c);
if (lit == null_literal) {
// it is an axiom.
init_watch(*c, true);
m_card_axioms.push_back(c);
}
else {
get_wlist(lit).push_back(index);
get_wlist(~lit).push_back(index);
m_index_trail.push_back(index);
while (!m_index_trail.empty()) {
clear_index_trail_back();
}
}
@ -1028,19 +1162,42 @@ namespace sat {
add_at_least(lit, lits, k);
}
void card_extension::add_at_least(literal lit, literal_vector const& lits, unsigned k) {
unsigned index = 4*m_cards.size();
SASSERT(is_card_index(index));
card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
if (lit != null_literal) s().set_external(lit.var());
m_cards.push_back(c);
init_watch(*c);
}
void card_extension::init_watch(card& c) {
unsigned index = c.index();
literal lit = c.lit();
m_index_trail.push_back(index);
if (lit == null_literal) {
// it is an axiom.
init_watch(c, true);
}
else {
get_wlist(lit).push_back(index);
get_wlist(~lit).push_back(index);
}
}
void card_extension::add_pb_ge(literal lit, svector<wliteral> const& wlits, unsigned k) {
unsigned index = 4*m_pbs.size() + 0x3;
SASSERT(is_pb_index(index));
pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
m_pbs.push_back(p);
m_index_trail.push_back(index);
if (lit == null_literal) {
init_watch(*p, true);
m_pb_axioms.push_back(p);
}
else {
s().set_external(lit.var());
get_wlist(lit).push_back(index);
get_wlist(~lit).push_back(index);
m_index_trail.push_back(index);
}
}
@ -1059,6 +1216,8 @@ namespace sat {
SASSERT(is_xor_index(index));
xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, lit, lits);
m_xors.push_back(x);
s().set_external(lit.var());
for (literal l : lits) s().set_external(l.var());
get_wlist(lit).push_back(index);
get_wlist(~lit).push_back(index);
m_index_trail.push_back(index);
@ -1069,8 +1228,9 @@ namespace sat {
TRACE("sat", tout << l << " " << idx << "\n";);
if (is_pb_index(idx)) {
pb& p = index2pb(idx);
if (l.var() == p.lit().var()) {
if (p.lit() != null_literal && l.var() == p.lit().var()) {
init_watch(p, !l.sign());
keep = true;
}
else if (p.lit() != null_literal && value(p.lit()) != l_true) {
keep = false;
@ -1081,8 +1241,9 @@ namespace sat {
}
else if (is_card_index(idx)) {
card& c = index2card(idx);
if (l.var() == c.lit().var()) {
if (c.lit() != null_literal && l.var() == c.lit().var()) {
init_watch(c, !l.sign());
keep = true;
}
else if (c.lit() != null_literal && value(c.lit()) != l_true) {
keep = false;
@ -1263,6 +1424,10 @@ namespace sat {
}
}
void card_extension::simplify(xor& x) {
// no-op
}
void card_extension::get_card_antecedents(literal l, card const& c, literal_vector& r) {
DEBUG_CODE(
bool found = false;
@ -1313,6 +1478,109 @@ namespace sat {
}
}
void card_extension::nullify_tracking_literal(card& c) {
if (c.lit() != null_literal) {
get_wlist(c.lit()).erase(watched(c.index()));
get_wlist(~c.lit()).erase(watched(c.index()));
c.nullify_literal();
}
}
void card_extension::remove_constraint(card& c) {
clear_watch(c);
nullify_tracking_literal(c);
m_cards[index2position(c.index())] = 0;
dealloc(&c);
}
void card_extension::simplify(card& c) {
SASSERT(c.lit() == null_literal || value(c.lit()) != l_false);
if (c.lit() != null_literal && value(c.lit()) == l_false) {
std::ofstream ous("unit.txt");
s().display(ous);
s().display_watches(ous);
display(ous, c, true);
exit(1);
return;
init_watch(c, !c.lit().sign());
std::cout << "card: flip sign\n";
}
if (c.lit() != null_literal && value(c.lit()) == l_true) {
std::cout << "literal is assigned at base level " << value(c.lit()) << " " << s().at_base_lvl() << "\n";
SASSERT(lvl(c.lit()) == 0);
nullify_tracking_literal(c);
}
if (c.lit() == null_literal && c.k() == 1) {
std::cout << "create clause\n";
literal_vector lits;
for (literal l : c) lits.push_back(l);
s().mk_clause(lits);
remove_constraint(c);
return;
}
SASSERT(c.lit() == null_literal || value(c.lit()) == l_undef);
unsigned num_true = 0, num_false = 0;
for (literal l : c) {
switch (value(l)) {
case l_true: ++num_true; break;
case l_false: ++num_false; break;
default: break;
}
}
if (num_false + num_true == 0) {
// no simplification
return;
}
else if (num_true >= c.k()) {
std::cout << "tautology\n";
if (c.lit() != null_literal) {
std::cout << "tautology at level 0\n";
s().assign(c.lit(), justification());
}
remove_constraint(c);
}
else if (num_false + c.k() > c.size()) {
if (c.lit() != null_literal) {
std::cout << "falsity at level 0\n";
s().assign(~c.lit(), justification());
remove_constraint(c);
}
else {
std::cout << "unsat during simplification\n";
}
}
else if (num_false + c.k() == c.size()) {
std::cout << "unit propagations : " << c.size() - num_false - num_true << "\n";
literal_vector lits(c.literals());
unit_propagation_simplification(c.lit(), lits);
remove_constraint(c);
}
else {
std::cout << "literals assigned at base: " << num_true + num_false << " " << c.size() << " k: " << c.k() << "\n";
unsigned sz = c.size();
clear_watch(c);
for (unsigned i = 0; i < sz; ++i) {
if (value(c[i]) != l_undef) {
--sz;
c.swap(i, sz);
--i;
}
}
std::cout << "new size: " << sz << " old size " << c.size() << "\n";
c.update_size(sz);
c.update_k(c.k() - num_true);
if (c.lit() == null_literal) {
init_watch(c, true);
}
else {
SASSERT(value(c.lit()) == l_undef);
// c will be watched once c.lit() is assigned.
}
}
}
lbool card_extension::add_assign(card& c, literal alit) {
// literal is assigned to false.
@ -1380,51 +1648,110 @@ namespace sat {
m_index_lim.push_back(m_index_trail.size());
}
void card_extension::clear_index_trail_back() {
unsigned index = m_index_trail.back();
m_index_trail.pop_back();
if (is_card_index(index)) {
card* c = m_cards.back();
if (c) {
SASSERT(c->index() == index);
clear_watch(*c); // can skip during finalization
dealloc(c);
}
m_cards.pop_back();
}
else if (is_pb_index(index)) {
pb* p = m_pbs.back();
if (p) {
SASSERT(p->index() == index);
clear_watch(*p); // can skip during finalization
dealloc(p);
}
m_pbs.pop_back();
}
else if (is_xor_index(index)) {
xor* x = m_xors.back();
if (x) {
SASSERT(x->index() == index);
clear_watch(*x); // can skip during finalization
dealloc(x);
}
m_xors.pop_back();
}
else {
UNREACHABLE();
}
}
void card_extension::pop(unsigned n) {
TRACE("sat_verbose", tout << "pop:" << n << "\n";);
unsigned new_lim = m_index_lim.size() - n;
unsigned sz = m_index_lim[new_lim];
while (m_index_trail.size() > sz) {
unsigned index = m_index_trail.back();
m_index_trail.pop_back();
if (is_card_index(index)) {
SASSERT(m_cards.back()->index() == index);
clear_watch(*m_cards.back());
dealloc(m_cards.back());
m_cards.pop_back();
}
else if (is_pb_index(index)) {
SASSERT(m_pbs.back()->index() == index);
clear_watch(*m_pbs.back());
dealloc(m_pbs.back());
m_pbs.pop_back();
}
else if (is_xor_index(index)) {
SASSERT(m_xors.back()->index() == index);
clear_watch(*m_xors.back());
dealloc(m_xors.back());
m_xors.pop_back();
}
else {
UNREACHABLE();
}
clear_index_trail_back();
}
m_index_lim.resize(new_lim);
m_num_propagations_since_pop = 0;
}
void card_extension::simplify() {}
void card_extension::simplify() {
s().pop_to_base_level();
for (card* c : m_cards) {
if (c) simplify(*c);
}
for (pb* p : m_pbs) {
if (p) simplify(*p);
}
for (xor* x : m_xors) {
if (x) simplify(*x);
}
gc();
}
void card_extension::gc() {
// remove constraints where indicator literal isn't used.
sat::use_list use_list;
use_list.init(s().num_vars());
svector<bool> var_used(s().num_vars(), false);
for (clause* c : s().m_clauses) if (!c->frozen()) use_list.insert(*c);
for (card* c : m_cards) if (c) for (literal l : *c) var_used[l.var()] = true;
for (pb* p : m_pbs) if (p) for (wliteral wl : *p) var_used[wl.second.var()] = true;
for (xor* x : m_xors) if (x) for (literal l : *x) var_used[l.var()] = true;
for (card* c : m_cards) {
if (c && c->lit() != null_literal && !var_used[c->lit().var()] && use_list.get(c->lit()).empty() && use_list.get(~c->lit()).empty()) {
remove_constraint(*c);
}
}
for (pb* p : m_pbs) {
if (p && p->lit() != null_literal && !var_used[p->lit().var()] && use_list.get(p->lit()).empty() && use_list.get(~p->lit()).empty()) {
remove_constraint(*p);
}
}
// take ownership of interface variables
for (card* c : m_cards) if (c && c->lit() != null_literal) var_used[c->lit().var()] = true;
for (pb* p : m_pbs) if (p && p->lit() != null_literal) var_used[p->lit().var()] = true;
// set variables to be non-external if they are not used in theory constraints.
unsigned ext = 0;
for (unsigned v = 0; v < s().num_vars(); ++v) {
if (s().is_external(v) && !var_used[v]) {
s().set_non_external(v);
++ext;
}
}
std::cout << "non-external variables " << ext << "\n";
}
void card_extension::clauses_modifed() {}
lbool card_extension::get_phase(bool_var v) { return l_undef; }
void card_extension::copy_card(card_extension& result) {
for (unsigned i = 0; i < m_cards.size(); ++i) {
for (card* c : m_cards) {
literal_vector lits;
card& c = *m_cards[i];
for (unsigned i = 0; i < c.size(); ++i) {
lits.push_back(c[i]);
}
result.add_at_least(c.lit(), lits, c.k());
for (literal l : *c) lits.push_back(l);
result.add_at_least(c->lit(), lits, c->k());
}
}
extension* card_extension::copy(solver* s) {
@ -1537,13 +1864,13 @@ namespace sat {
std::ostream& card_extension::display(std::ostream& out) const {
for (card* c : m_cards) {
display(out, *c, false);
if (c) display(out, *c, false);
}
for (pb* p : m_pbs) {
display(out, *p, false);
if (p) display(out, *p, false);
}
for (xor* x : m_xors) {
display(out, *x, false);
if (x) display(out, *x, false);
}
return out;
}

40
src/sat/card_extension.h
View file

@ -59,10 +59,16 @@ namespace sat {
unsigned index() const { return m_index; }
literal lit() const { return m_lit; }
literal operator[](unsigned i) const { return m_lits[i]; }
literal const* begin() const { return m_lits; }
literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
unsigned k() const { return m_k; }
unsigned size() const { return m_size; }
void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
void negate();
void negate();
void update_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; }
void update_k(unsigned k) { m_k = k; }
void nullify_literal() { m_lit = null_literal; }
literal_vector literals() const { return literal_vector(m_size, m_lits); }
};
typedef std::pair<unsigned, literal> wliteral;
@ -76,6 +82,7 @@ namespace sat {
unsigned m_num_watch;
unsigned m_max_sum;
wliteral m_wlits[0];
void update_max_sum();
public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(pb) + num_lits * sizeof(wliteral); }
pb(unsigned index, literal lit, svector<wliteral> const& wlits, unsigned k);
@ -83,7 +90,7 @@ namespace sat {
literal lit() const { return m_lit; }
wliteral operator[](unsigned i) const { return m_wlits[i]; }
wliteral const* begin() const { return m_wlits; }
wliteral const* end() const { return (wliteral const*)m_wlits + m_size; }
wliteral const* end() const { return static_cast<wliteral const*>(m_wlits) + m_size; }
unsigned k() const { return m_k; }
unsigned size() const { return m_size; }
@ -94,6 +101,10 @@ namespace sat {
void set_num_watch(unsigned s) { m_num_watch = s; }
void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
void negate();
void update_size(unsigned sz) { m_size = sz; update_max_sum(); }
void update_k(unsigned k) { m_k = k; }
void nullify_literal() { m_lit = null_literal; }
literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
};
class xor {
@ -109,7 +120,7 @@ namespace sat {
literal operator[](unsigned i) const { return m_lits[i]; }
unsigned size() const { return m_size; }
literal const* begin() const { return m_lits; }
literal const* end() const { return (literal const*)m_lits + m_size; }
literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
void negate() { m_lits[0].neg(); }
};
@ -131,9 +142,6 @@ namespace sat {
ptr_vector<xor> m_xors;
ptr_vector<pb> m_pbs;
scoped_ptr_vector<card> m_card_axioms;
scoped_ptr_vector<pb> m_pb_axioms;
// watch literals
unsigned_vector m_index_trail;
unsigned_vector m_index_lim;
@ -157,7 +165,14 @@ namespace sat {
void inc_parity(bool_var v);
void reset_parity(bool_var v);
void clear_index_trail_back();
solver& s() const { return *m_solver; }
void gc();
// cardinality
void init_watch(card& c);
void init_watch(card& c, bool is_true);
void init_watch(bool_var v);
void assign(card& c, literal lit);
@ -170,6 +185,10 @@ namespace sat {
void unwatch_literal(literal w, card& c);
void get_card_antecedents(literal l, card const& c, literal_vector & r);
void copy_card(card_extension& result);
void simplify(card& c);
void nullify_tracking_literal(card& c);
void remove_constraint(card& c);
void unit_propagation_simplification(literal lit, literal_vector const& lits);
// xor specific functionality
void copy_xor(card_extension& result);
@ -177,17 +196,19 @@ namespace sat {
void watch_literal(xor& x, literal lit);
void unwatch_literal(literal w, xor& x);
void init_watch(xor& x, bool is_true);
void assign(xor& x, literal lit);
void assign(xor& x, literal lit);
void set_conflict(xor& x, literal lit);
bool parity(xor const& x, unsigned offset) const;
lbool add_assign(xor& x, literal alit);
void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
void get_xor_antecedents(literal l, xor const& x, literal_vector & r);
void simplify(xor& x);
bool is_card_index(unsigned idx) const { return 0x0 == (idx & 0x3); }
bool is_xor_index(unsigned idx) const { return 0x1 == (idx & 0x3); }
bool is_pb_index(unsigned idx) const { return 0x3 == (idx & 0x3); }
unsigned index2position(unsigned idx) const { return idx >> 2; }
card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 2]; }
xor& index2xor(unsigned idx) const { SASSERT(is_xor_index(idx)); return *m_xors[idx >> 2]; }
pb& index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pbs[idx >> 2]; }
@ -205,6 +226,11 @@ namespace sat {
void assign(pb& p, literal l);
void unwatch_literal(literal w, pb& p);
void get_pb_antecedents(literal l, pb const& p, literal_vector & r);
void simplify(pb& p);
void simplify2(pb& p);
bool is_cardinality(pb const& p);
void nullify_tracking_literal(pb& p);
void remove_constraint(pb& p);
inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); }

7
src/sat/sat_model_converter.cpp
View file

@ -32,6 +32,13 @@ namespace sat {
void model_converter::reset() {
m_entries.finalize();
}
model_converter& model_converter::operator=(model_converter const& other) {
reset();
m_entries.append(other.m_entries);
return *this;
}
void model_converter::operator()(model & m) const {
vector<entry>::const_iterator begin = m_entries.begin();

1
src/sat/sat_model_converter.h
View file

@ -59,6 +59,7 @@ namespace sat {
model_converter();
~model_converter();
void operator()(model & m) const;
model_converter& operator=(model_converter const& other);
entry & mk(kind k, bool_var v);
void insert(entry & e, clause const & c);

45
src/sat/sat_simplifier.cpp
View file

@ -35,10 +35,6 @@ namespace sat {
void use_list::insert(clause & c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
if (m_use_list.size() <= c[i].index()) {
std::cout << c[i] << "\n";
std::cout << m_use_list.size() << "\n";
}
m_use_list[c[i].index()].insert(c);
}
}
@ -86,14 +82,11 @@ namespace sat {
void simplifier::register_clauses(clause_vector & cs) {
std::stable_sort(cs.begin(), cs.end(), size_lt());
clause_vector::iterator it = cs.begin();
clause_vector::iterator end = cs.end();
for (; it != end; ++it) {
clause & c = *(*it);
if (!c.frozen()) {
m_use_list.insert(c);
if (c.strengthened())
m_sub_todo.insert(c);
for (clause* c : cs) {
if (!c->frozen()) {
m_use_list.insert(*c);
if (c->strengthened())
m_sub_todo.insert(*c);
}
}
}
@ -1358,16 +1351,12 @@ namespace sat {
TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
unsigned before_clauses = num_pos + num_neg;
unsigned after_clauses = 0;
clause_wrapper_vector::iterator it1 = m_pos_cls.begin();
clause_wrapper_vector::iterator end1 = m_pos_cls.end();
for (; it1 != end1; ++it1) {
clause_wrapper_vector::iterator it2 = m_neg_cls.begin();
clause_wrapper_vector::iterator end2 = m_neg_cls.end();
for (; it2 != end2; ++it2) {
for (clause_wrapper& c1 : m_pos_cls) {
for (clause_wrapper& c2 : m_neg_cls) {
m_new_cls.reset();
if (resolve(*it1, *it2, pos_l, m_new_cls)) {
TRACE("resolution_detail", tout << *it1 << "\n" << *it2 << "\n-->\n";
for (unsigned i = 0; i < m_new_cls.size(); i++) tout << m_new_cls[i] << " "; tout << "\n";);
if (resolve(c1, c2, pos_l, m_new_cls)) {
TRACE("resolution_detail", tout << c1 << "\n" << c2 << "\n-->\n";
for (literal l : m_new_cls) tout << l << " "; tout << "\n";);
after_clauses++;
if (after_clauses > before_clauses) {
TRACE("resolution", tout << "too many after clauses: " << after_clauses << "\n";);
@ -1393,16 +1382,12 @@ namespace sat {
m_elim_counter -= num_pos * num_neg + before_lits;
it1 = m_pos_cls.begin();
end1 = m_pos_cls.end();
for (; it1 != end1; ++it1) {
clause_wrapper_vector::iterator it2 = m_neg_cls.begin();
clause_wrapper_vector::iterator end2 = m_neg_cls.end();
for (; it2 != end2; ++it2) {
for (auto & c1 : m_pos_cls) {
for (auto & c2 : m_neg_cls) {
m_new_cls.reset();
if (!resolve(*it1, *it2, pos_l, m_new_cls))
if (!resolve(c1, c2, pos_l, m_new_cls))
continue;
TRACE("resolution_new_cls", tout << *it1 << "\n" << *it2 << "\n-->\n" << m_new_cls << "\n";);
TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
if (cleanup_clause(m_new_cls))
continue; // clause is already satisfied.
switch (m_new_cls.size()) {
@ -1470,7 +1455,7 @@ namespace sat {
for (bool_var v : vars) {
checkpoint();
if (m_elim_counter < 0)
return;
break;
if (try_eliminate(v)) {
m_num_elim_vars++;
}

20
src/sat/sat_solver.cpp
View file

@ -66,6 +66,7 @@ namespace sat {
}
solver::~solver() {
m_ext = 0;
SASSERT(check_invariant());
TRACE("sat", tout << "Delete clauses\n";);
del_clauses(m_clauses.begin(), m_clauses.end());
@ -159,6 +160,7 @@ namespace sat {
m_user_scope_literals.reset();
m_user_scope_literals.append(src.m_user_scope_literals);
m_mc = src.m_mc;
}
// -----------------------
@ -198,6 +200,10 @@ namespace sat {
return v;
}
void solver::set_non_external(bool_var v) {
m_external[v] = false;
}
void solver::set_external(bool_var v) {
if (m_external[v]) return;
m_external[v] = true;
@ -1444,6 +1450,20 @@ namespace sat {
if (m_next_simplify > m_conflicts_since_init + m_config.m_simplify_max)
m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max;
}
#if 1
static unsigned file_no = 0;
#pragma omp critical (print_sat)
{
++file_no;
std::ostringstream ostrm;
ostrm << "s" << file_no << ".txt";
std::ofstream ous(ostrm.str());
display(ous);
}
#endif
}
void solver::sort_watch_lits() {

1
src/sat/sat_solver.h
View file

@ -274,6 +274,7 @@ namespace sat {
unsigned num_restarts() const { return m_restarts; }
bool is_external(bool_var v) const { return m_external[v] != 0; }
void set_external(bool_var v);
void set_non_external(bool_var v);
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; }
unsigned search_lvl() const { return m_search_lvl; }

13
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -113,6 +113,17 @@ public:
if (m_mc0.get()) result->m_mc0 = m_mc0->translate(tr);
result->m_internalized = m_internalized;
result->m_internalized_converted = m_internalized_converted;
#if 0
static unsigned file_no = 0;
#pragma omp critical (print_sat)
{
++file_no;
std::ostringstream ostrm;
ostrm << "s" << file_no << ".txt";
std::ofstream ous(ostrm.str());
result->m_solver.display(ous);
}
#endif
return result;
}
@ -538,7 +549,7 @@ private:
g = m_subgoals[0];
expr_ref_vector atoms(m);
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true, is_lemma);
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, false, is_lemma);
m_goal2sat.get_interpreted_atoms(atoms);
if (!atoms.empty()) {
std::stringstream strm;

2
src/sat/sat_watched.cpp
View file

@ -60,7 +60,7 @@ namespace sat {
out << "(" << it->get_blocked_literal() << " " << *(ca.get_clause(it->get_clause_offset())) << ")";
break;
case watched::EXT_CONSTRAINT:
out << it->get_ext_constraint_idx();
out << "ext: " << it->get_ext_constraint_idx();
break;
default:
UNREACHABLE();