mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

#5467

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-10-12 10:16:15 -07:00
parent c3549ec784
commit 52032b9ef8
9 changed files with 38 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/seq_eq_solver.cpp
View file

@ -684,11 +684,12 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
cond = true;
}
// xs and ys cannot align
else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys))
else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys) && !can_align_from_lhs(ys, xs) && !can_align_from_rhs(ys, xs))
cond = true;
if (!cond)
return false;
literal_vector lits;
if (xs == ys) {
@ -724,7 +725,7 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
}
}
else {
TRACE("seq", tout << mk_pp(x1, m) << " > " << mk_pp(y1, m) << "\n";);
TRACE("seq", tout << mk_pp(x1, m) << " >\n" << mk_pp(y1, m) << "\n";);
if (ctx.get_assignment(lit3) == l_undef) {
ctx.mark_as_relevant(lit3);
return true;

4
src/smt/smt_conflict_resolution.cpp
View file

@ -474,7 +474,8 @@ namespace smt {
TRACE("conflict",
tout << "new scope level: " << m_new_scope_lvl << "\n";
tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";);
tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";
tout << "lemma: " << m_lemma << "\n";);
if (m.proofs_enabled())
mk_conflict_proof(conflict, not_l);
@ -761,6 +762,7 @@ namespace smt {
m_lemma .shrink(j);
m_lemma_atoms.shrink(j);
m_ctx.m_stats.m_num_minimized_lits += sz - j;
TRACE("conflict", tout << "lemma: " << m_lemma << "\n";);
}
/**

12
src/smt/smt_context_pp.cpp
View file

@ -113,9 +113,17 @@ namespace smt {
}
std::ostream& context::display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const {
for (unsigned i = 0; i < num_lits; ++i) {
out << literal_vector(num_lits, lits) << ":\n";
#if 1
expr_ref_vector fmls(m);
for (unsigned i = 0; i < num_lits; ++i)
fmls.push_back(literal2expr(lits[i]));
expr_ref c = mk_or(fmls);
out << c << "\n";
#else
for (unsigned i = 0; i < num_lits; ++i)
display_literal_smt2(out, lits[i]) << "\n";
}
#endif
return out;
}

2
src/smt/smt_internalizer.cpp
View file

@ -1387,7 +1387,7 @@ namespace smt {
default:
break;
}
TRACE("mk_clause", display_literals_verbose(tout << "after simplification:\n", num_lits, lits) << "\n";);
TRACE("mk_clause", display_literals_verbose(tout << "after simplification: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
unsigned activity = 1;
bool lemma = is_lemma(k);

11
src/smt/theory_seq.cpp
View file

@ -726,7 +726,7 @@ void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect
svector<assumption> assumptions;
const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
for (assumption const& a : assumptions) {
if (a.lit != null_literal) {
if (a.lit != null_literal && a.lit != true_literal) {
lits.push_back(a.lit);
SASSERT(ctx.get_assignment(a.lit) == l_true);
}
@ -743,7 +743,7 @@ bool theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
return false;
if (ctx.get_assignment(lit) == l_true)
return false;
literal_vector lits(n, _lits);
if (lit == false_literal) {
@ -2858,7 +2858,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
}
void theory_seq::add_axiom(literal_vector & lits) {
TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";);
TRACE("seq", ctx.display_literals_verbose(tout << "assert " << lits << " :", lits) << "\n";);
for (literal lit : lits)
ctx.mark_as_relevant(lit);
@ -2898,6 +2898,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
if (n1->get_root() == n2->get_root()) {
return false;
}
ctx.mark_as_relevant(n1);
ctx.mark_as_relevant(n2);
@ -2979,8 +2980,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
m_rewrite(se1);
m_rewrite(se2);
if (is_true) {
expr_ref f1 = m_sk.mk_indexof_left(se1, se2);
expr_ref f2 = m_sk.mk_indexof_right(se1, se2);
expr_ref f1 = m_sk.mk_contains_left(se1, se2);
expr_ref f2 = m_sk.mk_contains_right(se1, se2);
f = mk_concat(f1, se2, f2);
propagate_eq(lit, f, e1, true);
propagate_eq(lit, mk_len(f), mk_len(e1), false);