mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 13:41:27 +00:00
Code Activity
20171 commits 55 branches 53 tags 185 MiB
Commit graph

20171 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
ed84b14e6c fixing coi bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-20 17:55:37 -08:00
Nikolaj Bjorner
7b265ba162 fix poly model bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-20 14:24:08 -08:00
Nikolaj Bjorner
b3f7d16606 fix memory leaks and handling of non-integer term coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-20 11:59:12 -08:00
Nikolaj Bjorner
2578218b6f add new option for adding tangent lemmas for integer monomials 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-20 11:30:07 -08:00
Nikolaj Bjorner
fc96f827a1 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-20 10:32:51 -08:00
Nikolaj Bjorner
823800541e updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-19 14:02:27 -08:00
Nikolaj Bjorner
5d316a51d1 enable bound tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-19 10:53:42 -08:00
Nikolaj Bjorner
5de01e5d1d add stubs for bounds refinement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-19 10:42:28 -08:00
Nikolaj Bjorner
179601ffac testing model repair 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-18 14:14:54 -08:00
Nikolaj Bjorner
4df7ee67f5 updated sketch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-17 22:06:29 -08:00
Nikolaj Bjorner
92bc39dab5 add toggle to use polynomial translation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-17 20:52:34 -08:00
Nikolaj Bjorner
33709d3abb add toggle to use polynomial translation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-17 17:28:28 -08:00
Nikolaj Bjorner
2eca05e59a fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-17 09:57:17 -08:00
Nikolaj Bjorner
12df8f593e reshuffle if conditions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-16 17:24:31 -08:00
Nikolaj Bjorner
e9905c05b1 fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-16 17:21:23 -08:00
Nikolaj Bjorner
711572e73c fix crash on arie branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-16 16:58:33 -08:00
Nikolaj Bjorner
b835bd4c92 self-contained tracking of values 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-16 12:55:58 -08:00
Nikolaj Bjorner
f347c24e04 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 13:09:25 -08:00
Nikolaj Bjorner
072f1deccc update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-14 16:37:00 -08:00
Nikolaj Bjorner
d081321384 add substitution and division 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-14 16:26:10 -08:00
Nikolaj Bjorner
f55bdd923a remove mul saturate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-13 15:43:44 -08:00
Nikolaj Bjorner
5ea25dcf60 v2 running 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-13 13:59:12 -08:00
Nikolaj Bjorner
c7084e9998 revamp stellensatz to use polynomals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-12 20:21:42 -08:00
Nikolaj Bjorner
21b36868b5 revamping stellensatz 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-12 10:13:09 -08:00
Nikolaj Bjorner
b8f5e1d646 small rewrite update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-10 15:01:30 -08:00
Nikolaj Bjorner
9f848847c7 remove debug out from euf-completion 2025-11-07 08:06:13 -08:00
Nikolaj Bjorner
f4c5e14b6b add fold-unfold simplification 
this substitutes solve-eqs by including fold-unfold reductions.
 2025-11-07 08:04:41 -08:00
Nikolaj Bjorner
5d36f53cd3 add rewrite to eliminate quot-rem tautologies 2025-11-07 08:04:03 -08:00
Nikolaj Bjorner
a3ec6a0f1b add delayed diseq check 2025-11-07 08:03:37 -08:00
Nikolaj Bjorner
daf66e63c6 add more pre-processing for band 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-04 09:45:40 -08:00
Nikolaj Bjorner
4828ed97be tweak bound propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-03 12:41:33 -08:00
Nikolaj Bjorner
88269edd4b fixup bv operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-03 07:56:42 -08:00
Nikolaj Bjorner
919ac515bc fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-02 16:05:09 -08:00
Nikolaj Bjorner
ceb424dc64 update clang format 2025-10-31 08:43:50 -07:00
Nikolaj Bjorner
1b48ec27e0 update format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:43:50 -07:00
Nikolaj Bjorner
e3ef97e24d propagate value initialization to atoms 2025-10-31 08:43:50 -07:00
Nikolaj Bjorner
e709885e72 gcd reduce and use c().val for sign constraints 2025-10-31 08:43:46 -07:00
Nikolaj Bjorner
018cb3c734 generate more proper proof format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:41:14 -07:00
Nikolaj Bjorner
fdac93fff3 v0.1 of nla saturation 2025-10-31 08:36:15 -07:00
Nikolaj Bjorner
3e9afb30af disable nuget 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:33 -07:00
Nikolaj Bjorner
7c28d936fb bump version for release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:33 -07:00
Nikolaj Bjorner
a75602b7e5 update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:32 -07:00
Nikolaj Bjorner
bc28de931b fix C++ example and add polymorphic interface for C++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:32 -07:00
Nikolaj Bjorner
67dcb8bcc1 renemable Centos AMD nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:32 -07:00
Nikolaj Bjorner
d8862f8f6a fix build break introduced when adding support for polymorphic datatypes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:32 -07:00
dependabot[bot]
cf6a1ceb0e Bump actions/upload-artifact from 4 to 5 (#7998) 
Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 4 to 5.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](https://github.com/actions/upload-artifact/compare/v4...v5)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-version: '5'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-10-31 08:32:32 -07:00
dependabot[bot]
df8bca4db6 Bump actions/download-artifact from 5 to 6 (#7999) 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 5 to 6.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v5...v6)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-10-31 08:32:32 -07:00
Copilot
0ebc1070da Add missing mkLastIndexOf method and CharSort case to Java API (#8002) 
* Initial plan

* Add mkLastIndexOf method and CharSort support to Java API

- Added mkLastIndexOf method to Context.java for extracting last index of sub-string
- Added Z3_CHAR_SORT case to Sort.java's create() method switch statement
- Added test file to verify both fixes work correctly

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

* Fix author field in test file

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

* Delete examples/java/TestJavaAPICompleteness.java

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:32 -07:00
Nikolaj Bjorner
4a8a2adbb1 update centos version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:32 -07:00
Nikolaj Bjorner
20235af97b disable centos build until resolved 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-31 08:32:32 -07:00