mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix xor processing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-13 19:53:50 -08:00
parent 7e0920e362
commit 3047d930e1
3 changed files with 46 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

65
src/sat/ba_solver.cpp
View file

@ -189,8 +189,8 @@ namespace sat {
// ----------------------------------- // -----------------------------------
// xor // xor
ba_solver::xor::xor(unsigned id, literal lit, literal_vector const& lits): ba_solver::xor::xor(unsigned id, literal_vector const& lits):
constraint(xor_t, id, lit, lits.size(), get_obj_size(lits.size())) { constraint(xor_t, id, null_literal, lits.size(), get_obj_size(lits.size())) {
for (unsigned i = 0; i < size(); ++i) { for (unsigned i = 0; i < size(); ++i) {
m_lits[i] = lits[i]; m_lits[i] = lits[i];
} }
@ -959,17 +959,19 @@ namespace sat {
lbool ba_solver::add_assign(xor& x, literal alit) { lbool ba_solver::add_assign(xor& x, literal alit) {
// literal is assigned // literal is assigned
unsigned sz = x.size(); unsigned sz = x.size();
TRACE("ba", tout << "assign: " << x.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";); TRACE("ba", tout << "assign: " << ~alit << "@" << lvl(~alit) << " " << x << "\n"; display(tout, x, true); );
SASSERT(x.lit() == null_literal || value(x.lit()) == l_true); SASSERT(x.lit() == null_literal);
SASSERT(value(alit) != l_undef); SASSERT(value(alit) != l_undef);
unsigned index = 0; unsigned index = 0;
for (; index <= 2; ++index) { for (; index < 2; ++index) {
if (x[index].var() == alit.var()) break; if (x[index].var() == alit.var()) break;
} }
if (index == 2) { if (index == 2) {
// literal is no longer watched. // literal is no longer watched.
UNREACHABLE(); // this can happen as both polarities of literals
// are put in watch lists and they are removed only
// one polarity at a time.
return l_undef; return l_undef;
} }
SASSERT(x[index].var() == alit.var()); SASSERT(x[index].var() == alit.var());
@ -979,7 +981,10 @@ namespace sat {
literal lit2 = x[i]; literal lit2 = x[i];
if (value(lit2) == l_undef) { if (value(lit2) == l_undef) {
x.swap(index, i); x.swap(index, i);
// unwatch_literal(alit, x);
watch_literal(lit2, x); watch_literal(lit2, x);
watch_literal(~lit2, x);
TRACE("ba", tout << "swap in: " << lit2 << " " << x << "\n";);
return l_undef; return l_undef;
} }
} }
@ -1627,13 +1632,13 @@ namespace sat {
add_pb_ge(lit, wlits, k, false); add_pb_ge(lit, wlits, k, false);
} }
void ba_solver::add_xor(bool_var v, literal_vector const& lits) { void ba_solver::add_xor(literal_vector const& lits) {
add_xor(literal(v, false), lits, false); add_xor(lits, false);
} }
ba_solver::constraint* ba_solver::add_xor(literal lit, literal_vector const& lits, bool learned) { ba_solver::constraint* ba_solver::add_xor(literal_vector const& lits, bool learned) {
void * mem = m_allocator.allocate(xor::get_obj_size(lits.size())); void * mem = m_allocator.allocate(xor::get_obj_size(lits.size()));
xor* x = new (mem) xor(next_id(), lit, lits); xor* x = new (mem) xor(next_id(), lits);
x->set_learned(learned); x->set_learned(learned);
add_constraint(x); add_constraint(x);
for (literal l : lits) s().set_external(l.var()); // TBD: determine if goal2sat does this. for (literal l : lits) s().set_external(l.var()); // TBD: determine if goal2sat does this.
@ -1740,20 +1745,24 @@ namespace sat {
unsigned level = lvl(l); unsigned level = lvl(l);
bool_var v = l.var(); bool_var v = l.var();
SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION); SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION);
TRACE("ba", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";); TRACE("ba", tout << l << ": " << js << "\n";
for (unsigned i = 0; i <= index; ++i) tout << s().m_trail[i] << " "; tout << "\n";
s().display_units(tout);
);
unsigned num_marks = 0; unsigned num_marks = 0;
unsigned count = 0; unsigned count = 0;
while (true) { while (true) {
TRACE("ba", tout << "process: " << l << "\n";);
++count; ++count;
if (js.get_kind() == justification::EXT_JUSTIFICATION) { if (js.get_kind() == justification::EXT_JUSTIFICATION) {
constraint& c = index2constraint(js.get_ext_justification_idx()); constraint& c = index2constraint(js.get_ext_justification_idx());
TRACE("ba", tout << c << "\n";);
if (!c.is_xor()) { if (!c.is_xor()) {
r.push_back(l); r.push_back(l);
} }
else { else {
xor& x = c.to_xor(); xor& x = c.to_xor();
if (x.lit() != null_literal && lvl(x.lit()) > 0) r.push_back(x.lit());
if (x[1].var() == l.var()) { if (x[1].var() == l.var()) {
x.swap(0, 1); x.swap(0, 1);
} }
@ -1762,6 +1771,7 @@ namespace sat {
literal lit(value(x[i]) == l_true ? x[i] : ~x[i]); literal lit(value(x[i]) == l_true ? x[i] : ~x[i]);
inc_parity(lit.var()); inc_parity(lit.var());
if (lvl(lit) == level) { if (lvl(lit) == level) {
TRACE("ba", tout << "mark: " << lit << "\n";);
++num_marks; ++num_marks;
} }
else { else {
@ -1773,24 +1783,25 @@ namespace sat {
else { else {
r.push_back(l); r.push_back(l);
} }
bool found = false;
while (num_marks > 0) { while (num_marks > 0) {
l = s().m_trail[index]; l = s().m_trail[index];
v = l.var(); v = l.var();
unsigned n = get_parity(v); unsigned n = get_parity(v);
if (n > 0) { if (n > 0) {
reset_parity(v); reset_parity(v);
num_marks -= n;
if (n % 2 == 1) { if (n % 2 == 1) {
found = true;
break; break;
} }
--num_marks;
} }
--index; --index;
} }
if (num_marks == 0) { if (!found) {
break; break;
} }
--index; --index;
--num_marks;
js = s().m_justification[v]; js = s().m_justification[v];
} }
@ -2492,6 +2503,11 @@ namespace sat {
m_lits.append(n, lits); m_lits.append(n, lits);
s.s().mk_clause(n, m_lits.c_ptr()); s.s().mk_clause(n, m_lits.c_ptr());
} }
std::ostream& ba_solver::ba_sort::pp(std::ostream& out, literal l) const {
return out << l;
}
// ------------------------------- // -------------------------------
// set literals equivalent // set literals equivalent
@ -3299,7 +3315,7 @@ namespace sat {
xor const& x = cp->to_xor(); xor const& x = cp->to_xor();
lits.reset(); lits.reset();
for (literal l : x) lits.push_back(l); for (literal l : x) lits.push_back(l);
result->add_xor(x.lit(), lits, x.learned()); result->add_xor(lits, x.learned());
break; break;
} }
default: default:
@ -3427,19 +3443,8 @@ namespace sat {
} }
void ba_solver::display(std::ostream& out, xor const& x, bool values) const { void ba_solver::display(std::ostream& out, xor const& x, bool values) const {
out << "xor " << x.lit(); out << "xor: ";
if (x.lit() != null_literal && values) { for (literal l : x) {
out << "@(" << value(x.lit());
if (value(x.lit()) != l_undef) {
out << ":" << lvl(x.lit());
}
out << "): ";
}
else {
out << ": ";
}
for (unsigned i = 0; i < x.size(); ++i) {
literal l = x[i];
out << l; out << l;
if (values) { if (values) {
out << "@(" << value(l); out << "@(" << value(l);

7
src/sat/ba_solver.h
View file

@ -178,7 +178,7 @@ namespace sat {
literal m_lits[0]; literal m_lits[0];
public: public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(xor) + num_lits * sizeof(literal); } static size_t get_obj_size(unsigned num_lits) { return sizeof(xor) + num_lits * sizeof(literal); }
xor(unsigned id, literal lit, literal_vector const& lits); xor(unsigned id, literal_vector const& lits);
literal operator[](unsigned i) const { return m_lits[i]; } literal operator[](unsigned i) const { return m_lits[i]; }
literal const* begin() const { return m_lits; } literal const* begin() const { return m_lits; }
literal const* end() const { return begin() + m_size; } literal const* end() const { return begin() + m_size; }
@ -246,6 +246,7 @@ namespace sat {
literal mk_max(literal l1, literal l2); literal mk_max(literal l1, literal l2);
literal mk_min(literal l1, literal l2); literal mk_min(literal l1, literal l2);
void mk_clause(unsigned n, literal const* lits); void mk_clause(unsigned n, literal const* lits);
std::ostream& pp(std::ostream& out, literal l) const;
}; };
ba_sort m_ba; ba_sort m_ba;
psort_nw<ba_sort> m_sort; psort_nw<ba_sort> m_sort;
@ -458,7 +459,7 @@ namespace sat {
constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned); constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned); constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
constraint* add_xor(literal l, literal_vector const& lits, bool learned); constraint* add_xor(literal_vector const& lits, bool learned);
void copy_core(ba_solver* result); void copy_core(ba_solver* result);
public: public:
@ -469,7 +470,7 @@ namespace sat {
virtual void set_unit_walk(unit_walk* u) { m_unit_walk = u; } virtual void set_unit_walk(unit_walk* u) { m_unit_walk = u; }
void add_at_least(bool_var v, literal_vector const& lits, unsigned k); void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k); void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
void add_xor(bool_var v, literal_vector const& lits); void add_xor(literal_vector const& lits);
virtual bool propagate(literal l, ext_constraint_idx idx); virtual bool propagate(literal l, ext_constraint_idx idx);
virtual lbool resolve_conflict(); virtual lbool resolve_conflict();

10
src/sat/tactic/goal2sat.cpp
View file

@ -392,11 +392,15 @@ struct goal2sat::imp {
return; return;
} }
sat::literal_vector lits; sat::literal_vector lits;
convert_pb_args(num, lits);
sat::bool_var v = m_solver.mk_var(true); sat::bool_var v = m_solver.mk_var(true);
lits.push_back(sat::literal(v, true));
convert_pb_args(num, lits);
// ensure that = is converted to xor
for (unsigned i = 1; i + 1 < lits.size(); ++i) {
lits[i].neg();
}
ensure_extension(); ensure_extension();
if (lits.size() % 2 == 0) lits[0].neg(); m_ext->add_xor(lits);
m_ext->add_xor(v, lits);
sat::literal lit(v, sign); sat::literal lit(v, sign);
if (root) { if (root) {
m_result_stack.reset(); m_result_stack.reset();