mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-19 05:25:48 +00:00
Code Activity
22957 commits 110 branches 59 tags 206 MiB
Commit graph

151 commits

Author SHA1 Message Date
Margus Veanes
8992d5fc53 seq_split: add behaviour-neutral perf counters, surfaced via nseq -st 
Adds a split_stats struct to seq_split (make/sigma-expand/materialize/splits/pushes/oracle-prunes/intersect/intersect-pairs/complement/giveups/threshold-overruns/max-split-set/simplify) and reports them in nielsen_graph::collect_statistics as 'nseq split *'. Read-only counters; solver behaviour is unchanged (verified: L11 sat, L14 unsat, gen cssfunc sat). Diagnosis on gen-lb L15 negcount: the De Morgan complement -> intersect cross-product blows up to 2^16 split-set pairs (1.3M intersect-pairs) while simplify() and the oracle never fire on that path.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-07-03 16:05:31 +03:00
CEisenhofer
706f62286e Merge remote-tracking branch 'origin/master' into c3 2026-07-01 17:18:21 +02:00
CEisenhofer
f5baba1068 Lazy regex factorization via iterator 2026-06-30 22:22:33 +02:00
Clemens Eisenhofer
b3143e759b
Porting seq_split to master (#9840) 
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-30 10:18:28 -07:00
CEisenhofer
ccfc355edb Merge remote-tracking branch 'origin/port_seq_split_to_master' into c3 2026-06-30 13:25:27 +02:00
Nikolaj Bjorner
15f33f458d
Derive with ranges (#9965) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Margus Veanes <margus@microsoft.com>
Co-authored-by: Margus Veanes <veanes@users.noreply.github.com>
 2026-06-26 08:44:13 -06:00
CEisenhofer
bbe473cb8e Bug fixes 2026-06-26 16:12:52 +02:00
Nikolaj Bjorner
f034616950
Revert "Derive with ranges" (#9964) 
Reverts Z3Prover/z3#9963
 2026-06-25 19:57:30 -06:00
Nikolaj Bjorner
22c2635786
Derive with ranges (#9963) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Margus Veanes <margus@microsoft.com>
Co-authored-by: Margus Veanes <veanes@users.noreply.github.com>
 2026-06-25 19:47:25 -06:00
Nikolaj Bjorner
cb3fe3167f rewrite replace_all constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-23 10:45:28 -07:00
CEisenhofer
1feb610daa Probably quite instable, but included the splitting into the legacy solver 2026-06-12 17:05:38 +02:00
CEisenhofer
871a2b3bc8 Porting seq_split to master 2026-06-12 15:18:14 +02:00
CEisenhofer
671dfedebe Merge branch 'master' into c3 2026-06-11 11:04:51 +02: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
CEisenhofer
2dbefbcd56 Lookahead for regex splits applied to membership constraints 
Rewriting constraint/prefix/suffix with constant strings to regexes
 2026-06-10 20:35:36 +02:00
CEisenhofer
dbb3f70873 Moved the regex splitting into rewriter 
Added some simplifications
 2026-06-10 15:00:58 +02:00
CEisenhofer
e3b80fc578 Merge branch 'master' into c3 2026-06-10 13:41:31 +02:00
Copilot
f0956a622f
Refactor regex subset logic into seq_subset with depth-bounded recursion and optimized concat traversal (#9777) 
`seq_rewriter::is_subset` was too localized and missed key subset
implications for regex concatenations. This change extracts subset
reasoning into a dedicated component and adds heuristic
closure/monotonicity rules, then tunes the recursion strategy based on
profiling feedback.

- **Architecture: isolate subset reasoning**
  - Introduce `seq_subset` in `src/ast/rewriter` (`seq_subset.h/.cpp`).
- Add `seq_subset` as an attribute on `seq_rewriter` and route
`seq_rewriter::is_subset` through it.
- Keep `seq_rewriter` focused on rewrite orchestration while subset
logic evolves independently.

- **Subset rules: broaden inferable cases**
- Add derive-style subset decomposition across `union`, `intersection`,
`complement`, `concat`, and bounded `loop`.
  - Add E3-style closure rules:
    - `R ⊆ R*`
    - `R1* ⊆ R2*  ⇐  R1 ⊆ R2`
    - `R1+ ⊆ R2+  ⇐  R1 ⊆ R2`
  - Add missing cheap cases:
    - `ε ⊆ R` when `R` is nullable
    - `R ⊆ R+`
    - `R+ ⊆ R*`
    - Range containment: `[c1–c2] ⊆ [c3–c4]` when `c3 ≤ c1 ∧ c2 ≤ c4`
    - `to_re(s) ⊆ range` for single-character string constants
    - Difference monotonicity: `a1 \ a2 ⊆ b` when `a1 ⊆ b`
- Star absorption checks for concat/star combinations (`R·R* ⊆ R*`,
`R*·R ⊆ R*`)
- Preserve nullable-based `. +` handling and top/bottom regular-language
shortcuts.

- **Concatenation reasoning and traversal tuning**
- Remove `flatten_concat` and assume right-associative concatenation
traversal.
- Keep containment shortcuts for both `R ⊆ Σ*·R'` and `R ⊆ R'·Σ*` when
`R ⊆ R'`.
  - Make concat/concat handling tail-recursive on second arguments.

- **Depth-bounded recursion (profiling follow-up)**
- Replace visited-pair hash-table recursion state with an explicit depth
parameter in `is_subset_rec`.
  - Add `m_max_depth = 3` and return `false` when the bound is reached.
- Increment depth on recursive calls, except for the tail-recursive
concat-second-argument step.

- **Build integration**
  - Register `seq_subset.cpp` in `src/ast/rewriter/CMakeLists.txt`.

```cpp
// seq_rewriter.cpp
bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
    return m_subset.is_subset(r1, r2);
}
```

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-06-09 13:42:28 -07:00
Nikolaj Bjorner
8cc85a7d7b code simplification, fix conflict in new_diseq_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-04-21 10:17:43 +02:00
Copilot
2212f59704
seq_model: address NSB review comments (#8995) 
* Initial plan

* Address NSB review comments in seq_model.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback: improve null-sort handling in seq_model and some_seq_in_re

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-03-14 21:55:32 -07:00
Nikolaj Bjorner
fcd3a70c92 remove theory_str and classes that are only used by it 2025-08-07 21:05:12 -07:00
Nikolaj Bjorner
99ec42c0d7 additional simplifications to seq 2025-03-19 08:57:31 -10:00
Nikolaj Bjorner
c6f58c8bf7 updates to some_string_in_re per code review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-11 17:47:27 -08:00
Clemens Eisenhofer
c572fc2e4f
Regex membership (#7506) 
* Make finding a word in the regex iterative

* Fixed gc problem
 2025-01-11 17:41:37 -08:00
Nikolaj Bjorner
2dd4faf598 sketch expr_inverter approach for eliminating unconstrained regex containment. 2025-01-07 16:53:57 -08:00
Bruce Mitchener
53f89a81c1
Fix some typos. (#7115) 2024-02-07 23:06:43 -08:00
Nikolaj Bjorner
d1c7ff1a36 add unconstrained elimination for sequences 2023-03-20 17:07:04 +01:00
Nikolaj Bjorner
a409a4a677 enforce flat within QF_BV tactic, cap in-processing var-elim loops 2022-10-27 20:10:55 -07:00
Bruce Mitchener
5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Nikolaj Bjorner
4d8e4b5bd3 fix #6052 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-25 17:21:01 -04:00
Nikolaj Bjorner
c850259f89 rw 2022-05-22 07:54:27 -04: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
773e829c58 #5804 2022-01-31 10:16:09 -08:00
Margus Veanes
5afb95b34a
improved subset checking for regexes with counters (#5731) 2021-12-22 17:53:34 -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
a288f9048a
Update regex union and intersection to maintain ANF (#5717) 
* added merge for unions and intersections

* added normalization rules to ensure ANF

* fixing PR comments related to merge
 2021-12-16 19:19:36 -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
51fa40ece5 fix spelling 2021-12-09 10:23:37 -08: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
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
1bc10cebc5 add ubv2s step 1 2021-07-12 12:53:00 +02:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
804f065215 fixes for #4688 
https://github.com/Z3Prover/z3/issues/4866#issuecomment-778721073
 2021-04-11 17:42:12 -07:00
Nuno Lopes
c47ab023e5 remove a few trivial destructors so they get inlined 2021-04-04 17:13:59 +01:00
Nikolaj Bjorner
377d060036 move to separate axiom management 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-23 18:09:45 -08:00
Nikolaj Bjorner
27584d68db more rewrite rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 22:14:53 -08:00
Nikolaj Bjorner
b2eb248bad fixes, fix #5034 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 16:47:44 -08:00
Nikolaj Bjorner
9ae3339c33 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-18 12:33:17 -08:00
Nikolaj Bjorner
e63dc7efc2 more rewrite rules 2021-02-17 17:32:00 -08:00