mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

We need to reset local conflicts

Browse source
This commit is contained in:
CEisenhofer 2026-04-08 18:24:11 +02:00
parent 26ededa891
commit 86dc9d3268
4 changed files with 57 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1315,6 +1315,11 @@ namespace seq {
SASSERT(depth <= cur_path.size());
m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
if (node->is_general_conflict()) {
++m_stats.m_num_simplify_conflict;
return search_result::unsat;
}
// check for external cancellation (timeout, user interrupt)
if (!m.inc())
return search_result::unknown;
@ -1336,10 +1341,18 @@ namespace seq {
return search_result::unknown;
}
node->set_eval_idx(m_run_idx);
SASSERT(!node->is_general_conflict());
node->clear_local_conflict(); // clear local conflicts from previous runs
// we might need to tell the SAT solver about the new integer inequalities
// that might have been added by an extension step
assert_node_new_int_constraints(node);
if (node->is_currently_conflict()) {
++m_stats.m_num_simplify_conflict;
return search_result::unsat;
}
// simplify constraints (idempotent after first call)
const simplify_result sr = node->simplify_and_init(cur_path);

7
src/smt/seq/seq_nielsen.h
View file

@ -611,6 +611,13 @@ namespace seq {
(reason() != backtrack_reason::unevaluated && m_is_extended);
}
void clear_local_conflict() {
SASSERT(!is_general_conflict());
m_reason = backtrack_reason::unevaluated;
m_conflict_internal = nullptr;
m_conflict_external_literal = sat::null_literal;
}
backtrack_reason reason() const { return m_reason; }
void set_child_conflict() {

4
src/smt/seq/seq_nielsen_pp.cpp
View file

@ -589,10 +589,10 @@ namespace seq {
out << ", color=green";
else if (n->is_general_conflict())
out << ", color=darkred";
else if (n->eval_idx() != m_run_idx) // inactive, not visited this run
out << ", color=blue";
else if (n->is_currently_conflict())
out << ", color=red";
else if (n->eval_idx() != m_run_idx) // inactive, not visited this run
out << ", color=blue";
out << "];\n";
}

64
src/smt/theory_nseq.cpp
View file

@ -741,6 +741,36 @@ namespace smt {
p.m_string_solver = "seq";
kernel kernel(m, p);
auto model_out = [&]() {
model_ref model;
kernel.get_model(model);
for (unsigned i = 0; i < model->get_num_constants(); i++) {
func_decl* f = model->get_constant(i);
expr_ref v(m);
VERIFY(model->eval(f, v));
std::cout << f->get_name() << ": " << mk_pp(v, m) << std::endl;
}
for (unsigned i = 0; i < model->get_num_functions(); i++) {
func_decl* f = model->get_function(i);
func_interp* fi = model->get_func_interp(f);
auto entries = fi->get_entries();
std::cout << f->get_name() << ":\n";
for (unsigned j = 0; j < fi->num_entries(); j++) {
auto& e = entries[j];
auto* args = e->get_args();
std::cout << "\n(";
for (unsigned k = 0; k < fi->get_arity(); k++) {
if (k > 0)
std::cout << ", ";
std::cout << mk_pp(args[k], m);
}
std::cout << "): ";
expr* r = e->get_result();
std::cout << mk_pp(r, m) << std::endl;
}
}
};
for (seq::dep_source const& d : m_nielsen.conflict_sources()) {
if (std::holds_alternative<enode_pair>(d))
kernel.assert_expr(
@ -763,6 +793,7 @@ namespace smt {
}
auto dot = m_nielsen.to_dot();
std::cout << std::endl;
model_out();
kernel.reset();
auto& lits = ctx.assigned_literals();
for (literal l : lits) {
@ -772,44 +803,19 @@ namespace smt {
th_rewriter th(m);
expr_ref r(m);
th(e, r);
std::cout << mk_pp(r, m) << std::endl;
kernel.assert_expr(r);
}
auto res2 = kernel.check();
if (res2 == l_true) {
// the algorithm is unsound
std::cout << "Original input is SAT" << std::endl;
model_ref model;
kernel.get_model(model);
for (unsigned i = 0; i < model->get_num_constants(); i++) {
func_decl* f = model->get_constant(i);
expr_ref v(m);
VERIFY(model->eval(f, v));
std::cout << f->get_name() << ": " << mk_pp(v, m) << std::endl;
}
for (unsigned i = 0; i < model->get_num_functions(); i++) {
func_decl* f = model->get_function(i);
func_interp* fi = model->get_func_interp(f);
auto entries = fi->get_entries();
std::cout << f->get_name() << ":\n";
for (unsigned j = 0; j < fi->num_entries(); j++) {
auto& e = entries[j];
auto* args = e->get_args();
std::cout << "\n(";
for (unsigned k = 0; k < fi->get_arity(); k++) {
if (k > 0)
std::cout << ", ";
std::cout << mk_pp(args[k], m);
}
std::cout << "): ";
expr* r = e->get_result();
std::cout << mk_pp(r, m) << std::endl;
}
}
model_out();
}
else if (res == l_false)
else if (res2 == l_false)
// the justification is too narrow
std::cout << "Original input is UNSAT" << std::endl;
else
std::cout << "Original input is UNKNOWN" << std::endl;
}
VERIFY(res != l_true);
}