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

Log to file

Browse source
This commit is contained in:
CEisenhofer 2026-04-14 11:47:26 +02:00
parent acae332b13
commit ed4387c70e
2 changed files with 65 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1371,6 +1371,27 @@ namespace seq {
return search_result::unsat;
}
str_mem* mem = nullptr;
for (auto& m : node->m_str_mem) {
if (m.m_id == 28) {
mem = &m;
break;
}
}
if (mem) {
static int cnt = 0;
std::cout << "search cnt: " << cnt << std::endl;
vector<dep_manager::value, false> deps;
m_dep_mgr.linearize(mem->m_dep, deps);
for (auto& dep : deps) {
if (std::holds_alternative<enode_pair>(dep))
std::cout << "eq: " << mk_pp(std::get<enode_pair>(dep).first->get_expr(), m) << " = " << mk_pp(std::get<enode_pair>(dep).second->get_expr(), m) << std::endl;
else
std::cout << "mem literal: " << std::get<sat::literal>(dep) << std::endl;
}
}
// simplify constraints (idempotent after first call)
const simplify_result sr = node->simplify_and_init(cur_path);
@ -4151,6 +4172,21 @@ namespace seq {
SASSERT(dep);
static unsigned cnt = 0;
std::cout << cnt << std::endl;
cnt++;
std::cout << "Dep:\n";
vector<dep_manager::value, false> deps;
m_dep_mgr.linearize(dep, deps);
for (auto& dep : deps) {
if (std::holds_alternative<enode_pair>(dep))
std::cout << "eq: " << mk_pp(std::get<enode_pair>(dep).first->get_expr(), m) << " = " << mk_pp(std::get<enode_pair>(dep).second->get_expr(), m) << std::endl;
else
std::cout << "mem literal: " << std::get<sat::literal>(dep) << std::endl;
}
euf::snode* approx = nullptr;
for (euf::snode* tok : tokens) {
euf::snode* tok_re = nullptr;
@ -4164,6 +4200,20 @@ namespace seq {
else if (tok->is_var()) {
// Variable → intersection of primitive regex constraints, or Σ*
euf::snode* x_range = m_seq_regex->collect_primitive_regex_intersection(tok, node, m_dep_mgr, dep);
std::cout << "Primitives for " << mk_pp(tok->get_expr(), m) << ":\n";
if (x_range)
std::cout << mk_pp(x_range->get_expr(), m) << std::endl;
else
std::cout << "null" << std::endl;
std::cout << "Dep:\n";
deps.reset();
m_dep_mgr.linearize(dep, deps);
for (auto& dep : deps) {
if (std::holds_alternative<enode_pair>(dep))
std::cout << "eq: " << mk_pp(std::get<enode_pair>(dep).first->get_expr(), m) << " = " << mk_pp(std::get<enode_pair>(dep).second->get_expr(), m) << std::endl;
else
std::cout << "mem literal: " << std::get<sat::literal>(dep) << std::endl;
}
if (x_range)
tok_re = x_range;
else {

27
src/smt/theory_nseq.cpp
View file

@ -589,7 +589,7 @@ namespace smt {
// Always assert non-negativity for all string theory vars,
// even when there are no string equations/memberships.
if (assert_nonneg_for_all_vars()) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: nonneg assertions added, FC_CONTINUE\n";);
TRACE(seq, tout << "nseq final_check: nonneg assertions added, FC_CONTINUE\n");
return FC_CONTINUE;
}
@ -600,7 +600,7 @@ namespace smt {
// there is nothing to do for the string solver, as there are no string constraints
if (!has_eq_or_mem && m_ho_terms.empty() && !has_unhandled_preds()) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state+ho, FC_DONE (no solve)\n";);
TRACE(seq, tout << "nseq final_check: empty state+ho, FC_DONE (no solve)\n");
m_nielsen.reset();
m_nielsen.create_root();
m_nielsen.set_sat_node(m_nielsen.root());
@ -612,20 +612,20 @@ namespace smt {
// There is an existing nielsen graph with a satisfying assignment.
if (!m_nielsen_literals.empty() && m_nielsen.sat_node() != nullptr &&
all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: satifiable state revisited\n");
TRACE(seq, tout << "nseq final_check: satifiable state revisited\n");
// Re-run solving/model extraction instead of early exiting on a
// cached SAT node. This avoids stale sat paths after additional
// SAT assignments were introduced in prior FC_CONTINUE rounds.
}
}
// unfold higher-order terms when sequence structure is known
if (unfold_ho_terms()) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: unfolded ho_terms, FC_CONTINUE\n";);
TRACE(seq, tout << "nseq final_check: unfolded ho_terms, FC_CONTINUE\n");
return FC_CONTINUE;
}
if (!has_eq_or_mem && !has_unhandled_preds()) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state (after ho), FC_DONE (no solve)\n";);
TRACE(seq, tout << "nseq final_check: empty state (after ho), FC_DONE (no solve)\n");
m_nielsen.reset();
m_nielsen.create_root();
m_nielsen.set_sat_node(m_nielsen.root());
@ -637,7 +637,7 @@ namespace smt {
// assert length constraints derived from string equalities
if (assert_length_constraints()) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: length constraints asserted, FC_CONTINUE\n";);
TRACE(seq, tout << "nseq final_check: length constraints asserted, FC_CONTINUE\n");
return FC_CONTINUE;
}
@ -656,15 +656,15 @@ namespace smt {
switch (check_regex_memberships_precheck()) {
case l_true:
// conflict was asserted inside check_regex_memberships_precheck
IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck UNSAT\n";);
TRACE(seq, tout << "nseq final_check: regex precheck UNSAT\n");
return FC_CONTINUE;
case l_false:
// all regex constraints satisfiable, no word eqs → SAT
IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck SAT\n";);
TRACE(seq, tout << "nseq final_check: regex precheck SAT\n");
m_nielsen.set_sat_node(m_nielsen.root());
if (!check_length_coherence())
return FC_CONTINUE;
TRACE(seq, display(tout << "pre-check done\n"));
TRACE(seq, tout << "pre-check done\n");
return FC_DONE;
default:
break;
@ -674,7 +674,7 @@ namespace smt {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: calling solve()\n";);
// here the actual Nielsen solving happens
auto result = m_nielsen.solve();
auto result = m_nielsen.solve(); std::cout << "Solve returned " << (int)result << std::endl;
#ifdef Z3DEBUG
// Examining the Nielsen graph is probably the best way of debugging
@ -685,6 +685,7 @@ namespace smt {
if (result == seq::nielsen_graph::search_result::unsat) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNSAT\n";);
TRACE(seq, tout << "nseq final_check: solve UNSAT\n");
explain_nielsen_conflict();
return FC_CONTINUE;
}
@ -692,6 +693,8 @@ namespace smt {
if (result == seq::nielsen_graph::search_result::sat) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve SAT, sat_node="
<< (m_nielsen.sat_node() ? "set" : "null") << "\n";);
TRACE(seq, tout << "nseq final_check: solve SAT, sat_node="
<< (m_nielsen.sat_node() ? "set" : "null") << "\n");
// Nielsen found a consistent assignment for positive constraints.
SASSERT(has_eq_or_mem); // we should have axiomatized them
@ -699,7 +702,7 @@ namespace smt {
// If assumptions remain undefined, returning SAT can yield
// unsound/invalid models because the chosen Nielsen branch
// is not yet committed in the outer SAT core.
IF_VERBOSE(1, verbose_stream() << "nseq final_check: unresolved assumptions, FC_GIVEUP\n";);
TRACE(seq, tout << "nseq final_check: unresolved assumptions, FC_GIVEUP\n");
return FC_GIVEUP;
}