mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 16:54:11 +00:00
Code Activity

We need to check local consistency over and over again

Browse source
This commit is contained in:
CEisenhofer 2026-04-09 15:56:00 +02:00
parent 09572b20ed
commit e6ef0d29c4
2 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/seq/seq_nielsen.cpp
View file

@ -268,6 +268,7 @@ namespace seq {
for (const auto f : *to_app(c.fml)) {
add_constraint(constraint(f, c.dep, m));
}
return;
}
expr* l, *r;
if (m.is_eq(c.fml, l, r)) {
@ -275,10 +276,6 @@ namespace seq {
return;
}
m_constraints.push_back(c);
SASSERT(m_graph.m_literal_if_false);
auto lit = m_graph.m_literal_if_false(c.fml);
if (lit != sat::null_literal)
set_external_conflict(lit, c.dep);
}
void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
@ -1334,7 +1331,7 @@ namespace seq {
return search_result::unknown;
#ifdef Z3DEBUG
if (m_stats.m_num_dfs_nodes % 1000 == 0) {
if (m_stats.m_num_dfs_nodes % 200 == 0) {
std::string dot = to_dot();
dot = dot;
}
@ -4006,8 +4003,13 @@ nielsen_graph::generate_length_constraints(vector<length_constraint>& constraint
// already present in the enclosing solver scope; asserting them again would
// be redundant (though harmless). This is called by search_dfs right after
// simplify_and_init, which is where new constraints are produced.
SASSERT(m_literal_if_false);
for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) {
m_solver.assert_expr(node->constraints()[i].fml);
auto& c = node->constraints()[i];
m_solver.assert_expr(c.fml);
auto lit = m_literal_if_false(c.fml);
if (lit != sat::null_literal)
node->set_external_conflict(lit, c.dep);
}
}

6
src/smt/theory_nseq.cpp
View file

@ -248,7 +248,7 @@ namespace smt {
void theory_nseq::assign_eh(bool_var v, bool is_true) {
try {
expr* e = ctx.bool_var2expr(v);
std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
// std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
expr *s = nullptr, *re = nullptr, *a = nullptr, *b = nullptr;
TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";);
if (m_seq.str.is_in_re(e, s, re)) {
@ -737,7 +737,7 @@ namespace smt {
case l_true:
break;
case l_undef:
//std::cout << "Undef: " << mk_pp(c.fml, m) << "\n";
//std::cout << "Undef [" << lit << "]: " << mk_pp(c.fml, m) << "\n";
has_undef = true;
ctx.force_phase(lit);
IF_VERBOSE(2, verbose_stream() <<
@ -751,7 +751,7 @@ namespace smt {
ctx.force_phase(lit);
has_undef = true;
ctx.force_phase(lit);
//std::cout << "False: " << mk_pp(c.fml, m) << "\n";
//std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
break;
}
}