mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 17:06:14 +00:00
Code Activity

fix #3558

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 16:47:40 -07:00
parent 7945d42e5e
commit 35c59e3ca0
2 changed files with 42 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/sat/ba_solver.cpp
View file

@ -2048,7 +2048,40 @@ namespace sat {
return lit; return lit;
} }
ba_solver::constraint* ba_solver::add_xr(literal_vector const& lits, bool learned) { ba_solver::constraint* ba_solver::add_xr(literal_vector const& _lits, bool learned) {
struct parity {
bool sign; bool lit;
parity(): sign(false), lit(false) {}
// {false, false}, p => {false, true}
// {false, false}, !p => {true, true}
// {false, true}, p => {true, false}
// {false, true}, !p => {true, false}
void add(literal l) {
lit = !lit;
sign = sign != l.sign();
}
};
literal_vector lits;
u_map<parity> var2parity;
for (literal lit : _lits) {
var2parity.insert_if_not_there2(lit.var(), parity())->get_data().m_value.add(lit);
}
bool polarity = false;
for (auto const& kv : var2parity) {
bool lit = kv.m_value.lit;
bool sign = kv.m_value.sign;
if (lit)
lits.push_back(literal(kv.m_key, sign));
else
polarity = polarity ^ sign;
}
if (lits.empty()) {
throw default_exception("empty xor is TBD");
}
if (polarity) {
lits[0].neg();
}
void * mem = m_allocator.allocate(xr::get_obj_size(lits.size())); void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
xr* x = new (mem) xr(next_id(), lits); xr* x = new (mem) xr(next_id(), lits);
x->set_learned(learned); x->set_learned(learned);

16
src/smt/theory_utvpi_def.h
View file

@ -759,8 +759,8 @@ namespace smt {
int_vector zero_v; int_vector zero_v;
m_graph.compute_zero_succ(v1, zero_v); m_graph.compute_zero_succ(v1, zero_v);
for (unsigned j = 0; j < zero_v.size(); ++j) { for (auto v0 : zero_v) {
if (zero_v[j] == v2) { if (v0 == v2) {
zero_v.reset(); zero_v.reset();
m_graph.compute_zero_succ(v2, zero_v); m_graph.compute_zero_succ(v2, zero_v);
break; break;
@ -769,13 +769,13 @@ namespace smt {
TRACE("utvpi", TRACE("utvpi",
tout << "Disparity: " << v1 << "\n"; tout << "Disparity: " << v1 << "\n";
for (unsigned j = 0; j < zero_v.size(); ++j) { for (auto v : zero_v) {
tout << "decrement: " << zero_v[j] << "\n"; tout << "decrement: " << v << "\n";
}); }
display(tout);
);
for (unsigned j = 0; j < zero_v.size(); ++j) { for (auto v : zero_v) {
int v = zero_v[j];
m_graph.inc_assignment(v, numeral(-1)); m_graph.inc_assignment(v, numeral(-1));
th_var k = from_var(v); th_var k = from_var(v);
if (!is_parity_ok(k)) { if (!is_parity_ok(k)) {