Nikolaj Bjorner
f614721a92
have it create string ranges
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-06-25 20:23:09 -07:00
Copilot
8c2a425e4b
Smart constructors for regex ranges: canonical form at construction time ( #9814 )
...
Regex range expressions (`re.range`) and Boolean operations over them
were left in unsimplified form, defeating downstream optimisations
(bisimulation classical fast-path, derivative engine) and producing
semantically-empty terms not syntactically equal to `re.none`.
## Changes
### `seq_decl_plugin.h` / `seq_decl_plugin.cpp`
- **`seq_util::rex::mk_range(sort*, unsigned lo, unsigned hi)`** — new
smart constructor that normalises at call time:
- `lo > hi` → `re.empty`
- `lo == hi` → `str.to_re` (singleton string)
- `lo < hi` → `re.range`
- **`mk_info_rec` `OP_RE_RANGE`** — concrete non-empty ranges (both
bounds are single-char literals with `lo ≤ hi`) now return `classical =
true`, enabling the XOR-bisimulation `classical_distinguishing`
fast-path on character-predicate leaves. Symbolic/unknown ranges retain
`classical = false`.
### `seq_rewriter.cpp`
- **`mk_re_range`** — singleton collapse: `(re.range "a" "a")` →
`(str.to_re "a")`
- **`mk_regex_inter_normalize`** — range × range intersection: `[a,b] ∩
[c,d]` → `[max(a,c), min(b,d)]`, or `re.none` (disjoint), or `str.to_re`
(boundary singleton); now delegates to `re().mk_range(sort*, lo, hi)`
- **`mk_regex_union_normalize`** — range × range union for
overlapping/adjacent ranges: `[a,b] ∪ [c,d]` → `[min(a,c), max(b,d)]`;
disjoint ranges fall through to existing `merge_regex_sets`; now
delegates to `re().mk_range(sort*, lo, hi)`
- **`mk_re_complement`** — range complement expands to one or two
concrete ranges instead of an opaque `re.comp` node; now delegates to
`re().mk_range(sort*, lo, hi)`:
- `comp([0, b])` → `[b+1, max]`
- `comp([a, max])` → `[0, a-1]`
- `comp([a, b])` → `[0, a-1] ∪ [b+1, max]`
```
(simplify (re.range "z" "a")) ; → re.none
(simplify (re.range "a" "a")) ; → (str.to_re "a")
(simplify (re.inter (re.range "a" "z") (re.range "f" "k"))); → (re.range "f" "k")
(simplify (re.union (re.range "a" "f") (re.range "g" "k"))); → (re.range "a" "k")
(simplify (re.comp (re.range "b" "y"))) ; → (re.union [0,a] [z,max])
```
### Tests
New `src/test/seq_rewriter.cpp` with 14 cases covering all the above
reductions plus downstream propagation (star/concat/union/inter
absorbing empty ranges).
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-06-16 13:58:56 -06:00
Margus Veanes
513b81253b
Add OP_RE_XOR and union-find bisimulation for ground regex equivalence ( #9804 )
...
Implements the algorithm of Eq(p,q) = Empty(p XOR q)' using a union-find
driven bisimulation closure (per the CAV'26 ERE paper).
### What's added
* **New primitive OP_RE_XOR (re.xor)** wired through seq_decl_plugin:
parser signature, info propagation (nullable, min_length), and
pretty-printer.
* **seq_rewriter**: structural XOR rewrites ( XOR r = empty, XOR empty =
r, ull XOR r = comp(r), comp/comp absorption, complement push, AC
normalisation), nullability (Null(p XOR q) = Null(p) != Null(q)),
derivative (D_a(p XOR q) = D_a(p) XOR D_a(q)), reverse, antimirov
derivative, and `check_deriv_normal_form` coverage.
* **New class seq::regex_bisim** in
`src/ast/rewriter/seq_regex_bisim.{h,cpp}` to keep the bisim logic out
of the already-large `seq_rewriter.cpp`. Uses `basic_union_find` from
`util/union_find.h`, an `obj_map` for the node assignment, and a
50000-step bound (returns `l_undef` on overrun).
* **Integration** in `seq_rewriter::reduce_re_eq` (with a re-entry
guard) and in `seq_regex::propagate_eq` / `propagate_ne` for ground
regexes; on `l_undef` we fall back to the existing axiomatisation.
* **`sls_seq_plugin`**: extend `OP_RE_DIFF` switch arms to also cover
`OP_RE_XOR`.
### Validation
* Full release build with MSVC + Ninja.
* `./test-z3 /a` -- 89/89 tests passing.
* `./test-z3 /seq smt2print_parse` -- PASS.
* Smoke tests with `(a|b)*` vs `(a*b*)*` (equal) and `a*` vs `(a|b)*`
(not equal) return the expected `sat`/`unsat` quickly.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-10 14:58:20 -07:00
Copilot
d415ead6a2
Port is_classical attribute to seq_util::rex::info ( #9796 )
...
`is_classical` (tracks whether a regex uses only classical operators —
no complement, intersection, diff, or empty-language/fail) was only
available on `euf::snode`. Moving it into `seq_util::rex::info` makes it
accessible to all regex-handling code without going through the snode
layer.
### Changes
**`seq_decl_plugin.h`**
- Added `bool classical { true }` to `seq_util::rex::info`
- The general `info` constructor requires `bool is_classical` explicitly
(no default)
**`seq_decl_plugin.cpp`**
- `mk_info_rec`: `OP_RE_EMPTY_SET` (fail) sets `classical=false`
- `mk_info_rec`: `OP_RE_RANGE`, `OP_RE_FULL_CHAR_SET`, `OP_RE_OF_PRED`
set `classical=false`
- `complement()`, `conj()` (intersection), `diff()`: always produce
`classical=false`
- `star()`, `plus()`, `opt()`, `concat()`, `disj()`, `orelse()`,
`loop()`: propagate `classical` via logical AND over operands
- `operator=` and `display()` updated to include `classical`
### Semantics
| Operation | `classical` |
|-----------|-------------|
| `re.empty` (fail) | `false` |
| `re.range`, `re.allchar`, `re.of.pred` | `false` |
| `re.comp` (complement) | `false` |
| `re.inter` (intersection) | `false` |
| `re.diff` | `false` |
| `re.all` (full sequence set) | `true` |
| `str.to.re` (string literal) | `true` |
| `re.*`, `re.+`, `re.opt`, `re.++`, `re.union`, `re.loop` | inherited
from operands |
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
2026-06-09 14:35:48 -07:00
Copilot
6e68911cbb
Reapply PR #8190 : Replace std::ostringstream with C++20 std::format ( #8204 )
...
* Initial plan
* Reapply PR #8190 : Replace std::ostringstream with C++20 std::format
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-01-15 21:30:29 -08:00
Copilot
2436943794
Standardize for-loop increments to prefix form (++i) ( #8199 )
...
* Initial plan
* Convert postfix to prefix increment in for loops
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix member variable increment conversion bug
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update API generator to produce prefix increments
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-01-14 19:55:31 -08:00
Lev Nachmanson
d5e0216070
Revert "Merge pull request #8190 from Z3Prover/copilot/fix-std-format-usage"
...
This reverts commit d9bdb6b83c8b188621a5
2026-01-13 18:18:07 -10:00
copilot-swe-agent[bot]
64957e2b0e
Modernize more files to use std::format: bv_decl_plugin, dl_decl_plugin, datatype_decl_plugin, seq_decl_plugin
...
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
2026-01-13 21:34:47 +00:00
LeeYoungJoon
0a93ff515d
Centralize and document TRACE tags using X-macros ( #7657 )
...
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros
* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md
* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled
* trace: improve trace tag handling system with hierarchical tagging
- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
(class names and descriptions to be refined in a future update)
* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals
* trace : add cstring header
* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py
* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.
* trace : Add TODO comment for future implementation of tag_class activation
* trace : Disable code related to tag_class until implementation is ready (#7663 ).
2025-05-28 14:31:25 +01:00
Nikolaj Bjorner
24c3cd38d1
add v0 of equality solver
2024-11-30 17:25:49 -08:00
Nikolaj Bjorner
a6b502779b
fix #7252
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-06-13 17:52:17 -07:00
Nikolaj Bjorner
02d48adae5
fix #6573
2023-02-08 08:24:52 -08:00
Nikolaj Bjorner
1e0f71c971
add way to access range bounds directly #6186
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 09:35:37 -07:00
Nikolaj Bjorner
1e8f9078e3
fix unsoundness in explanation handling for nested datatypes and sequences
2022-07-03 17:00:39 -07:00
Nikolaj Bjorner
004139b320
rewrites for characters
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-02 11:37:21 -07:00
Nikolaj Bjorner
5a685ba9b5
expose maxdiff
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-04 08:52:42 -07:00
Nikolaj Bjorner
367bfedab0
add min/max diff in final check
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-04 07:39:38 -07:00
Nikolaj Bjorner
87d2a3b4e5
map/mapi/foldl/foldli
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-04 01:10:18 -07:00
Nikolaj Bjorner
e1929ca9b9
add regex power to API and for Java per request
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-15 19:18:33 -07:00
Margus Veanes
be38b256c8
fixed bug in is_char_const_range ( #5724 )
2021-12-19 17:46:42 -08:00
Margus Veanes
a7b1db611c
State graph dgml update and fixes in condition simplifier ( #5721 )
...
* improved generated dgml graph
* fixed simplification of negated ranges and did some code cleanup
* do not make loops with lower=upper=0, this is epsilon
* do not add loops with lower=upper=1
* bug fix in normalization: forgotten eps case
2021-12-19 11:09:55 -08:00
Margus Veanes
2be93870c8
Cleanup regex info and some fixes in Derivative code ( #5709 )
...
* removed unused regex info fields
* cleanup of info and fixes in antimirov derivatives
* removed extra qualification on operator
2021-12-15 10:59:34 -08:00
Nikolaj Bjorner
96e871c826
add stub for testing updates to scoped_timer
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-12 12:31:23 -08:00
Nikolaj Bjorner
51fa40ece5
fix spelling
2021-12-09 10:23:37 -08:00
Nikolaj Bjorner
518ef9f916
fix #5674
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-18 21:14:50 -08:00
Margus Veanes
efcad5ff35
fixed nullability bug in the if-then-else info ( #5620 )
2021-10-26 09:11:07 +02:00
Nikolaj Bjorner
fb9fa1b7d2
updated printer
2021-10-15 17:56:54 -07:00
Margus Veanes
cb120c93f4
Regex range bug fix ( #5601 )
...
* added a missing derivative case for nonground range
* further missing cases and a bug fix in re.to_str
2021-10-15 15:30:55 -07:00
Nikolaj Bjorner
0fc9f1d46a
fix max/min length to handle concatenation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-09 16:20:32 -07:00
Margus Veanes
146f4621c5
Updated regex derivative engine ( #5567 )
...
* updated derivative engine
* some edit
* further improvements in derivative code
* more deriv code edits and re::to_str update
* optimized mk_deriv_accept
* fixed PR comments
* small syntax fix
* updated some simplifications
* bugfix:forgot to_re before reverse
* fixed PR comments
* more PR comment fixes
* more PR comment fixes
* forgot to delete
* deleting unused definition
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-08 13:04:49 -07:00
Nikolaj Bjorner
f13ccf8969
bv2char and char2bv with Clemens
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-13 16:09:03 +02:00
Nikolaj Bjorner
3eb849ad9e
rewrite equality too
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-08-09 15:32:04 -07:00
Margus Veanes
225204e2f4
updates related to issue #5140 ( #5463 )
...
* updates related to issue #5140
* updated/simplified some cases
* fixing feedback comments
* fixed comments and added missing case for get_re_head_tail_reversed
* two bug fixes and some other code improvements
2021-08-09 10:48:56 -07:00
CEisenhofer
0fa4b63d26
Added sbv2s ( #5413 )
...
* Added sbv2s
* Fixed indention
Co-authored-by: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
2021-07-16 17:58:28 +02:00
Nikolaj Bjorner
e5c5caea45
add call to function
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 09:19:20 +02:00
Nikolaj Bjorner
1bc10cebc5
add ubv2s step 1
2021-07-12 12:53:00 +02:00
Nikolaj Bjorner
5d3f48cc8d
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-06-07 09:51:39 -07:00
Nikolaj Bjorner
92ec81d108
#5140
...
@veanes
mk_bool_app_helper has a bug:
When it simplifies a disjunction or conjunction of regex membership constraints of the form (and (str.in_re "" R) (str.in_re x Q))
then the first term (str.in_re "" R) is omitted in the result.
You have a test here
3da9d91866/src/ast/rewriter/seq_rewriter.cpp (L438)3da9d91866/src/ast/rewriter/seq_rewriter.cpp (L485)
2021-06-06 20:30:09 -07:00
Nikolaj Bjorner
262daf5151
symbol/zstring transition
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-22 13:54:21 -07:00
Nikolaj Bjorner
20a67e47ca
remove symbol -> zstring -> symbol round-trips
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-22 13:12:49 -07:00
Margus Veanes
8ca6f567d3
fixing issue #5140 ( #5268 )
2021-05-16 13:53:08 -07:00
Nikolaj Bjorner
8263d20e0d
add code review comment
2021-04-20 11:30:25 -07:00
Nikolaj Bjorner
9098084217
reduce overhead of creating seq-plugin, enable parameter cleanup for #5095
2021-03-15 11:54:44 -07:00
Nikolaj Bjorner
612cc5cfba
fix #5014
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-02-12 16:01:33 -08:00
Nikolaj Bjorner
8fffc03263
remove bv dependencies
2021-02-08 10:57:50 -08:00
Nikolaj Bjorner
0f29fff836
remove bit-vector dependencies in seq theory
2021-02-08 10:57:50 -08:00
Nikolaj Bjorner
4455f6caf8
move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail
2021-02-02 03:58:19 -08:00
Nikolaj Bjorner
520b24aab4
string escaping
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-30 04:58:58 -08:00
Nikolaj Bjorner
909257f856
remove family id externals
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-27 06:48:24 -08:00
Nikolaj Bjorner
d3564f5b50
move unicode toggle to char-plugin
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-27 06:42:19 -08:00
