mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

Enforce all power terms are internalized at model construction phase

Browse source
This commit is contained in:
CEisenhofer 2026-07-20 18:01:31 +02:00
parent 386f8528b6
commit d885580633
3 changed files with 43 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/seq_model.cpp
View file

@ -134,6 +134,8 @@ namespace smt {
return alloc(expr_wrapper_proc, to_app(e));
}
std::cout << mk_pp(n->get_expr(), m) << std::endl;
// For nth_u (underspecified nth): the Nielsen character-peel /
// regex-if-split records the chosen character as a relevant
// equality literal (e.g. (= (seq.nth_u x 0) (_ Char 65))), so the
@ -239,12 +241,11 @@ namespace smt {
if (seen.contains(curr->id()))
continue;
seen.insert(curr->id());
if (m.is_value(curr->get_expr()))
;
else if (curr->is_empty())
;
else if (curr->is_char_or_unit()) {
expr *e = curr->arg(0)->get_expr();
if (m.is_value(curr->get_expr()) || curr->is_empty())
continue;
if (curr->is_char_or_unit()) {
expr* e = curr->arg(0)->get_expr();
if (m_ctx.e_internalized(e))
deps.push_back(m_ctx.get_enode(e));
}
@ -283,14 +284,9 @@ namespace smt {
expr_ref seq_model::snode_to_value(euf::snode const* n, enode_vector const &deps, expr_ref_vector const &values) {
// var2value: leaf deps keyed by expression ID (populated from `deps`/`values`).
// node2value: computed nodes keyed by (snode_id * 2 + is_recursive).
// The recursion flag is part of the key because the SAME variable snode
// appears in two distinct roles in a Nielsen substitution such as D -> "cc" D:
// the outer variable (is_recursive == false, value == value of its replacement)
// and the inner "leftover" remainder (is_recursive == true, value == "").
u_map<expr *> var2value;
u_map<expr *> node2value;
// resolve: check leaf deps by expression ID, computed nodes by (snode,recursive) key.
// resolve: check leaf deps by expression ID, computed nodes by snode key.
auto resolve = [&](euf::snode const* s, expr*& out) -> bool {
if (var2value.find(s->get_expr()->get_id(), out))
return true;
@ -307,6 +303,7 @@ namespace smt {
expr *val = nullptr;
while (!todo.empty()) {
auto curr = todo.back();
// std::cout << "processing: " << mk_pp(curr->get_expr(), m) << std::endl;
// Early exit: already computed (as leaf dep or computed node).
expr* cached = nullptr;
if (resolve(curr, cached)) {
@ -445,7 +442,8 @@ namespace smt {
if (a.is_numeral(e, val))
return val;
bool has_val = get_arith_value(e, val);
bool has_val = get_arith_value(_e, val);
CTRACE(seq, !has_val, tout << "no value associated with " << mk_pp(e, m) << "\n";);
return val;
}

30
src/smt/theory_nseq.cpp
View file

@ -920,6 +920,8 @@ namespace smt {
m_nielsen.reset();
m_nielsen.create_root();
m_nielsen.set_sat_node(m_nielsen.root());
if (!ensure_model_internalized())
return FC_CONTINUE;
TRACE(seq, display(tout << "empty nielsen\n"));
return FC_DONE;
}
@ -939,6 +941,8 @@ namespace smt {
m_nielsen.reset();
m_nielsen.create_root();
m_nielsen.set_sat_node(m_nielsen.root());
if (!ensure_model_internalized())
return FC_CONTINUE;
TRACE(seq, display(tout << "empty nielsen\n"));
return FC_DONE;
}
@ -962,9 +966,10 @@ namespace smt {
all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) {
++m_num_sat_revalidations;
TRACE(seq, tout << "nseq final_check: revalidated cached SAT path, skipping rebuild\n");
if (!check_length_coherence()) return FC_CONTINUE;
if (!check_stoi_coherence()) return FC_CONTINUE;
if (!has_unhandled_preds()) return FC_DONE;
if (!check_length_coherence()) return FC_CONTINUE;
if (!check_stoi_coherence()) return FC_CONTINUE;
if (!ensure_model_internalized()) return FC_CONTINUE;
if (!has_unhandled_preds()) return FC_DONE;
return FC_GIVEUP;
}
// fall through - no reason to rebuild the Nielsen graph
@ -1071,6 +1076,8 @@ namespace smt {
if (!check_stoi_coherence())
return FC_CONTINUE;
TRACE(seq, tout << "pre-check done\n");
if (!ensure_model_internalized())
return FC_CONTINUE;
return FC_DONE;
default:
break;
@ -1116,6 +1123,8 @@ namespace smt {
if (!all_sat)
return FC_CONTINUE;
if (!ensure_model_internalized())
return FC_CONTINUE;
if (!has_unhandled_preds())
return FC_DONE;
@ -1160,7 +1169,7 @@ namespace smt {
bool all_sat = true;
ctx.push_trail(reset_vector(m_nielsen_literals));
for (const auto& c : m_nielsen.sat_node()->constraints()) {
// std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
auto lit = mk_literal(c.fml);
m_nielsen_literals.push_back(lit);
// Ensure Nielsen assumptions participate in SAT search instead of
@ -2293,6 +2302,19 @@ namespace smt {
return true;
}
bool theory_nseq::ensure_model_internalized() const {
bool all_internalized = true;
for (const auto * n : m_nielsen.sat_path()) {
for (const auto& subst : n->subst()) {
if (ctx.e_internalized(subst.m_replacement->get_expr()))
continue;
ctx.internalize(subst.m_replacement->get_expr(), false);
all_internalized = false;
}
}
return all_internalized;
}
// -----------------------------------------------------------------------
// Use theory assumptions to bound search depth and force literal assignments
// m_assumption_lit gets added as an assumption to the set of existing assumptions.

6
src/smt/theory_nseq.h
View file

@ -208,6 +208,12 @@ namespace smt {
bool check_length_coherence();
// Has to be called before model construction
// otw. some terms required for model construction would be not initialized
// e.g., X = a^{2 + n}
// term "2 + n" would not necessarily be internalized
bool ensure_model_internalized() const;
// stoi axiom helpers
void add_stoi_nseq_axioms(expr* stoi_e);
bool check_stoi_coherence();