mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3 into lev

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-07-03 13:42:50 -07:00
commit c7e1d59b19
9 changed files with 263 additions and 299 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_pb.cpp
View file

@ -962,11 +962,11 @@ namespace smt {
m_stats.m_num_conflicts++;
context& ctx = get_context();
justification* js = 0;
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
c.inc_propagations(*this);
if (!resolve_conflict(c, lits)) {
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
}
SASSERT(ctx.inconsistent());

26
src/smt/theory_seq.cpp
View file

@ -522,31 +522,25 @@ bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
}
// exists x, y, rs' != empty s.t. (ls = x ++ rs' ++ y & rs = rs') || (ls = rs' ++ x && rs = y ++ rs')
// TBD: spec comment above doesn't seem to match what this function does.
unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector const& rs) {
SASSERT(!ls.empty() && !rs.empty());
unsigned_vector res;
unsigned_vector result;
expr_ref l = mk_concat(ls);
expr_ref r = mk_concat(rs);
expr_ref pair(m.mk_eq(l,r), m);
if (m_overlap.find(pair, res)) {
return res;
if (m_overlap.find(pair, result)) {
return result;
}
unsigned_vector result;
result.reset();
for (unsigned i = 0; i < ls.size(); ++i) {
if (eq_unit(ls[i], rs.back())) {
bool same = true;
if (i >= 1) {
for (unsigned j = i - 1; rs.size() + j >= 1 + i; --j) {
if (!eq_unit(ls[j], rs[rs.size()+j-i-1])) {
same = false;
break;
}
}
if (same)
result.push_back(i+1);
bool same = rs.size() > i;
for (unsigned j = 0; same && j < i; ++j) {
same = eq_unit(ls[j], rs[rs.size() - 1 - i + j]);
}
else
result.push_back(1);
if (same)
result.push_back(i+1);
}
}
m_overlap.insert(pair, result);