mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity
21844 commits 48 branches 58 tags 222 MiB
Commit graph

21844 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
5f92d3344d Define eq_ref and eq_refs types in ast.h and use them in nseq_ne 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-01 02:35:32 +00:00
copilot-swe-agent[bot]
63a3674bbd Initial plan 2026-03-01 02:06:09 +00:00
Nikolaj Bjorner
03cf706eb5 include partial plan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-28 14:00:29 -08:00
Nikolaj Bjorner
9557c5500b first rounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-28 12:19:22 -08:00
Nikolaj Bjorner
636b3b0a6b Add Phase 5: regex membership checking via derivatives 
- check_regex_memberships: iterate regex constraints in final_check
- check_regex_mem: for ground strings, compute Brzozowski derivatives and check nullable
- derive_regex: step-by-step derivative of regex w.r.t. string prefix
- is_ground_string: resolve string value through e-graph roots
- Handles positive (str.in_re) and negative (not str.in_re) memberships
- Uses seq_rewriter::mk_derivative and is_nullable (existing Z3 infrastructure)
- No regressions on string-concat.smt2 (36/62 correct, 0 wrong)

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-28 10:06:36 -08:00
Nikolaj Bjorner
4b58d57b61 Add Phase 4: length reasoning and canonize fix 
- Length axiom generation: concat decomposition, unit=1, empty=0, string=k
- Bidirectional len(x)=0 <-> x="" axioms
- check_zero_length: propagate zero-length variables to empty
- propagate_length_eqs: equate lengths of equation sides
- Fixed canonize: decompose structurally first, then follow e-graph roots
  Prevents both equation sides resolving to same root expression
- Fixed branch_var_prefix: skip cyclic candidates (containing variable itself)
  and ground candidates with wrong length
- check_length_conflict prevents e-graph corruption from incompatible merges
- Fresh value pinning for model generation (m_fresh_values)
- Regression: 36/62 correct, 0 wrong, 26 unknown on string-concat.smt2

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 22:48:58 -08:00
Nikolaj Bjorner
f48040d809 Add Phase 3: Nielsen transformation engine and equation solving 
- New nseq_nielsen.h/cpp in src/ast/rewriter/: self-contained Nielsen
  transformation engine for word equations
  - simplify(): strip common prefix/suffix, empty elimination, variable
    stripping, single-var assignment detection
  - split(): case analysis for var vs constant, var vs var
  - is_conflict(): mismatch detection (different constants, one side
    has constants while other is empty)

- Wire Nielsen into theory_nseq:
  - solve_eqs()/solve_eq(): process word equations using Nielsen
    transformations with e-graph canonization
  - branch_eq()/branch_var_prefix(): binary empty/non-empty decisions
    and prefix enumeration (no fresh variable creation)
  - canonize(): rewrite equation sides using current e-graph equivalences
  - all_eqs_solved(): check if all equations are satisfied
  - mk_value(): basic model generation (walk e-class for string constants)

- Passes basic tests: simple equalities, concat equations, unsat detection

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 18:01:08 -08:00
Nikolaj Bjorner
58b57b2632 Add Phase 2: core data structures for theory_nseq 
- nseq_constraint.h: constraint types (nseq_eq, nseq_ne, nseq_mem,
  nseq_pred) with dependency tracking via scoped_dependency_manager
- nseq_state.h/cpp: backtrackable state management with scoped_vector
  collections, axiom queue, length tracking, linearization for
  conflict/propagation justifications, statistics, display
- theory_nseq.h/cpp: full internalization (term/atom/bool), equality
  and disequality handling with union-find, literal assignment dispatch
  (prefix/suffix/contains/in_re), axiom management, propagation
  helpers (propagate_eq/lit, set_conflict), scope push/pop wired
  to nseq_state

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 17:26:10 -08:00
Nikolaj Bjorner
c325c56de4 Add theory_nseq skeleton: new string solver selectable via smt.string_solver=nseq 
Phase 1 of the theory_nseq implementation: a stub theory solver for
strings based on Nielsen transformations and lazy regex membership.

- New files: theory_nseq.h/cpp with all required theory virtual methods
- Add 'nseq' to smt.string_solver parameter validation and documentation
- Wire into smt_setup.cpp dispatch (setup_QF_S, setup_seq_str, setup_nseq)
- Currently returns FC_GIVEUP for non-trivial string constraints

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 17:00:59 -08:00
Nikolaj Bjorner
d1468bc09d initial spec 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-27 16:25:58 -08:00
Nikolaj Bjorner
d906a0cc2d fix bug reported by Maria Novoszel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-27 12:02:55 -08:00
Lev Nachmanson
5ff5b075b2
Merge pull request #8789 from Z3Prover/succ_int_mult 
Fix #7507: simplify (>= product_of_consecutive_ints 0) to true
 2026-02-27 09:45:26 -10:00
Lev Nachmanson
21c23e78db Fix #7507: simplify (>= product_of_consecutive_ints 0) to true 
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.

Two changes:
1. is_non_negative: detect products where unpaired factors are
   consecutive integer expressions (differ by exactly 1), handling
   both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
   to multiplication expressions to avoid disrupting other theories

Also adds regression tests for the new simplification.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-02-27 06:37:07 -10:00
Nikolaj Bjorner
fda8b4175f
Merge pull request #8793 from Z3Prover/copilot/fix-missing-api-functions 
Add missing array and FP API functions to Go, OCaml, and TypeScript bindings
 2026-02-27 03:14:18 -08:00
copilot-swe-agent[bot]
282db840de Add missing API functions to Go, OCaml, and TypeScript bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-27 02:55:37 +00:00
copilot-swe-agent[bot]
3f6acc45ed Initial plan 2026-02-27 02:48:36 +00:00
Nikolaj Bjorner
ea873672c3
Merge pull request #8788 from Z3Prover/copilot/simplify-fpa-test-code 
refactor(test): extract run_fp_test helper in fpa.cpp
 2026-02-26 16:29:42 -08:00
copilot-swe-agent[bot]
cf0ffa2673 refactor: extract run_fp_test helper in fpa.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 23:54:17 +00:00
copilot-swe-agent[bot]
f2e00b3589 Initial plan 2026-02-26 23:52:54 +00:00
Nikolaj Bjorner
aeded4d721
Merge pull request #8787 from Z3Prover/dependabot/npm_and_yarn/src/api/js/multi-770cfcd984 
Bump minimatch in /src/api/js
 2026-02-26 15:52:39 -08:00
Nikolaj Bjorner
828e4a7ef7
Merge pull request #8779 from Z3Prover/copilot/convert-bv1-blast-to-simplifier 
Convert bv1-blast tactic to a dependent_expr_simplifier
 2026-02-26 15:52:18 -08:00
dependabot[bot]
e097a98019
Bump minimatch in /src/api/js 
Bumps  and [minimatch](https://github.com/isaacs/minimatch). These dependencies needed to be updated together.

Updates `minimatch` from 3.1.2 to 3.1.5
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

Updates `minimatch` from 9.0.5 to 9.0.9
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

---
updated-dependencies:
- dependency-name: minimatch
  dependency-version: 3.1.5
  dependency-type: indirect
- dependency-name: minimatch
  dependency-version: 9.0.9
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-26 23:51:30 +00:00
Nikolaj Bjorner
c70f902b53
Merge pull request #8780 from Z3Prover/copilot/convert-blast-term-ite-to-simplifier 
Convert `blast-term-ite` tactic to a `dependent_expr_simplifier`
 2026-02-26 15:51:30 -08:00
Nikolaj Bjorner
fadf045df0
Merge pull request #8781 from Z3Prover/copilot/fix-ts-ocaml-issues 
Add register_on_clause to OCaml and TypeScript bindings
 2026-02-26 15:49:40 -08:00
copilot-swe-agent[bot]
ff7cc0f59e Remove old blast-term-ite tactic class, rename blast-term-ite2 to blast-term-ite 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 20:07:42 +00:00
copilot-swe-agent[bot]
668dd7a0a1 Rename bv1-blast2 to bv1-blast, remove old tactic source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 20:06:14 +00:00
Nikolaj Bjorner
a384e464e3
Merge pull request #8782 from Z3Prover/copilot/update-csa-workflow-discussion 
CSA workflow: embed raw report content directly into GitHub Discussion
 2026-02-26 09:27:56 -08:00
Nikolaj Bjorner
2105e95f30
Merge pull request #8785 from filipeom/filipe/expose-re_allchar 
Expose `mk_re_allchar` in OCaml API
 2026-02-26 09:26:51 -08:00
Filipe Marques
f0421879bb
Expose mk_re_allchar in OCaml API 2026-02-26 16:22:55 +00:00
Nikolaj Bjorner
070f760501
Merge pull request #8748 from Z3Prover/copilot/fix-floating-point-model-validation 
Fix fp.to_real bitvector encoding for denormal floating-point values
 2026-02-26 02:21:20 -08:00
copilot-swe-agent[bot]
234913bf56 Implement register_on_clause for OCaml and TypeScript bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 04:04:27 +00:00
copilot-swe-agent[bot]
033ea50a5d Convert bv1-blast tactic to a simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 04:01:11 +00:00
copilot-swe-agent[bot]
7390a9b856 Convert blast-term-ite tactic to also expose as a simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:51:42 +00:00
copilot-swe-agent[bot]
ddb8e35560 Update CSA workflow to integrate CSA report content directly into GitHub Discussion 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:41:55 +00:00
copilot-swe-agent[bot]
99d8db8ba8 initial plan 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:39:40 +00:00
copilot-swe-agent[bot]
31a9cbd3f7 Initial plan 2026-02-26 03:36:50 +00:00
copilot-swe-agent[bot]
c4f85493a7 Initial plan 2026-02-26 03:33:58 +00:00
copilot-swe-agent[bot]
0318762600 Initial plan 2026-02-26 03:31:18 +00:00
copilot-swe-agent[bot]
72411ce5b9 Initial plan 2026-02-26 03:31:08 +00:00
copilot-swe-agent[bot]
b4f7d057d3 Add model_validate and invalid-check to fpa regression tests 
Add (set-option :model_validate true) to each SMT-LIB2 spec in
src/test/fpa.cpp, and add ENSURE checks that the output does not
contain the string "invalid".

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:21:33 +00:00
Nikolaj Bjorner
4361b704df
Merge pull request #8774 from Z3Prover/copilot/simplify-code-in-context-and-solver 
Fix malformed JavaDoc in Context.java and extract ternary in Solver.cs
 2026-02-25 18:17:23 -08:00
copilot-swe-agent[bot]
add65451fd Add fpa regression test for fp.to_real denormal encoding fix 
Adds src/test/fpa.cpp with test_fp_to_real_denormal() exercising the
bug reported in the issue: denormal floating-point values in
(_ FloatingPoint 2 24) were getting wrong fp.to_real values because
mk_to_real was not subtracting the normalization shift lz from the
exponent.

Tests verify:
- The specific denormal from the bug report is NOT > 1.0
- Two other denormals have correct real values (0.5 and 0.125)
- A normal value is correctly identified as > 1.0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 22:04:03 +00:00
copilot-swe-agent[bot]
af2e60c069 code-simplifier: fix JavaDoc formatting in Context.java and extract ternary in Solver.cs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 21:49:23 +00:00
copilot-swe-agent[bot]
db98f1e2f7 Initial plan 2026-02-25 21:45:23 +00:00
Nikolaj Bjorner
fba1e4b648
Merge pull request #8737 from Z3Prover/copilot/fix-refutational-soundness-bug 
Fix soundness bug: RNE/RNA overflow to ±infinity in symbolic Real-to-FP conversion
 2026-02-25 13:34:59 -08:00
Nikolaj Bjorner
412c56ecc8
Merge pull request #8767 from Z3Prover/copilot/fix-ubv-to-int-bug 
Fix intblast: assert ubv_to_int(compound) = translation equality
 2026-02-25 13:32:40 -08:00
Nikolaj Bjorner
c51f45bf5e
Merge pull request #8766 from Z3Prover/copilot/fix-critical-bugs-from-discussion 
Fix critical static-analysis true positives: null deref, division by zero, dangling pointer
 2026-02-25 09:22:45 -08:00
Lev Nachmanson
a7ea22f24f remove an unnecessary template from levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-25 07:03:23 -10:00
Lev Nachmanson
66d19c4d3f
Merge pull request #8770 from Z3Prover/lws 
Optimizes the substitution of a non-nullified witness by an lc or a disc if they are added to the projection and do not vanish.
 2026-02-25 06:25:58 -10:00
Lev Nachmanson
0835420cc1 change the default of param lws_subs_witness_disc to true 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-24 15:24:35 -10:00