mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

smt: restore direct quantifier internalization in theory::mk_literal

Browse source 
Commit 382abb786 routed theory::mk_literal through the new
context::non_ground_internalize helper. For a top-level quantifier
literal (e.g. the universally-quantified emptiness condition produced
by the sequence/regex solver), that helper takes the non-ground proxy
path — it allocates a fresh proxy constant, asserts proxy = quantifier
and internalizes assertions — instead of internalizing the quantifier
directly. This engages quantifier instantiation on a goal the seq
theory previously discharged instantly as incomplete, turning a fast
'unknown (incomplete (theory seq))' answer into a -T: timeout.

Restore the previous behavior for quantifier expressions by
internalizing them directly, while keeping non_ground_internalize for
all other (non-quantifier) expressions.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-12 01:29:30 -07:00 • committed by GitHub
parent ba7b12c18c
commit 9b8bfe6a26
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_theory.cpp
View file

@ -152,8 +152,12 @@ namespace smt {
expr_ref e(_e, m);
bool is_not = m.is_not(_e, _e);
if (!ctx.e_internalized(_e)) {
auto n = ctx.non_ground_internalize(_e);
_e = n->get_expr();
if (is_quantifier(_e))
ctx.internalize(_e, true);
else {
auto n = ctx.non_ground_internalize(_e);
_e = n->get_expr();
}
}
literal lit = ctx.get_literal(_e);
ctx.mark_as_relevant(lit);