Generalize semi-linear length constraints for regex union and concatenation in theory_seq_len#8932
Draft
Generalize semi-linear length constraints for regex union and concatenation in theory_seq_len#8932
Conversation
…nation
Replace the old single-period (base, period) schema in theory_seq_len with a
richer svector<len_arm> representation where each arm captures one arithmetic
progression via an existential linear constraint:
∃ k_0,...,k_{n-1} ≥ 0 : |s| = base + ∑ periods[i] * k_i
Key improvements:
- Union R1|R2: recurse on both sides, return the concatenated arm sets.
When asserting, fresh guard Booleans are introduced so the SAT solver
case-splits between the two sets of length constraints.
- General concatenation R1++R2: compute the Minkowski product of arm sets.
Combined arms carry the merged period lists so, e.g., (aa)*++(bbb)* yields
|s| = 2*k1 + 3*k2 with k1,k2 ≥ 0, immediately ruling out length 1.
A MAX_LEN_ARMS=16 cap prevents combinatorial explosion.
- Option (R)?: now produces two precise fixed arms {0} and {n} instead of
the over-approximate single progression {0, n, 2n, …}.
- Each arm is encoded via fresh non-negative Int Skolem constants, letting
the linear arithmetic solver find counting witnesses directly.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
sgraph::mk_var(symbol const& name) silently hardcoded m_str_sort (always
String), which is wrong when sequences of other element sorts are in play.
Changes:
- euf_snode.h: add get_sort() convenience accessor (SASSERT that expr is
non-null, then return expr->get_sort()) so call sites are readable and the
precondition is checked in one place.
- euf_sgraph.h / euf_sgraph.cpp: make sort a required parameter of mk_var;
remove the implicit use of m_str_sort.
- seq_nielsen.h / seq_nielsen.cpp: make sort a required parameter of
mk_fresh_var; forward it to mk_var.
- All mk_fresh_var() call sites in seq_nielsen.cpp updated to derive the sort
from the adjacent contextual snode via ->get_sort():
lhead/rhead: sort of the variable being substituted
lhs_toks[0]: sort of the equation's leading token (padding case)
first: sort of the string membership variable
base: sort of the power's base sequence
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Contributor
|
@copilot - fix the build |
Contributor
|
@copilot fix the build |
m_len_vars(sg.get_manager()) was incorrectly placed inside the constructor
body after the opening { instead of being part of the initializer list.
Move it to the correct position in the initializer list.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Contributor
Author
Contributor
Author
The build fix was committed in 572e8a7. The constructor initializer for |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
sgraph::mk_var(symbol const& name, sort* s)— add requiredsort*parameter, remove use ofm_str_sortsnode::get_sort()convenience accessor withSASSERT(m_expr)ineuf_snode.hnielsen_graph::mk_fresh_var(sort* s)— add requiredsort*parameter, forward tomk_varmk_fresh_var()call sites inseq_nielsen.cppto pass the sort via->get_sort()from the adjacent contextual snodem_len_vars(sg.get_manager())moved from body to initializer list✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.