mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity
18495 commits 24 branches 48 tags 158 MiB
Commit graph

18495 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
f81180173b remove optional Julia build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-30 14:41:10 -08:00
Nikolaj Bjorner
5d4303f268 build Julia for x64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-30 13:27:16 -08:00
Nikolaj Bjorner
e0bed3bcfa build Julia for x64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-30 13:26:22 -08:00
Nikolaj Bjorner
680b0f523f add download stage for arm64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-30 12:32:09 -08:00
Nikolaj Bjorner
b3b95dbc5c move installation directories to under bin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-30 11:06:27 -08:00
Nikolaj Bjorner
9bd8e35581 adapt paths to new distribution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-30 10:07:38 -08:00
Nikolaj Bjorner
f7ed4adfbb update path for win distributions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-29 19:47:05 -08:00
Nikolaj Bjorner
bef67f8523 special purpose dotnet copy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-29 19:32:31 -08:00
Nikolaj Bjorner
4be8b7d88c update win-dist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-29 18:47:29 -08:00
Nikolaj Bjorner
908aaa06f7 fix #7101 2024-01-29 12:26:51 -08:00
Nikolaj Bjorner
2b683941b7 fix #7103 2024-01-27 17:46:23 -08:00
Nikolaj Bjorner
f8a3b6f521 fix #7102 2024-01-27 17:05:55 -08:00
Nikolaj Bjorner
2af1cff11f updating java cmake scrip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-27 16:29:19 -08:00
Nikolaj Bjorner
527f824adf update java install/build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-25 15:07:54 -08:00
Nikolaj Bjorner
c8c2e3a7b7 update java install/build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-25 15:05:33 -08:00
Nikolaj Bjorner
637ffcd491 Update mk_win_dist_cmake.py 2024-01-25 12:23:15 -08:00
Yisu Remy Wang
dec5715f03
Expose forall and exists to Julia (#7099) 2024-01-25 09:49:01 -08:00
Nikolaj Bjorner
9d59d86a1c update cmake build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-25 09:42:28 -08:00
Nikolaj Bjorner
ee2be7d642 attempting to build ARM 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-25 08:41:37 -08:00
Nikolaj Bjorner
bdb9106f99
Api (#7097) 
* rename ul_pair to column

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* t

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* simple test passed

* remove an assert

* relax an assertion

* remove an obsolete function

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* access a term by the term column

* remove the column index from colunm.h

* remove an unused method

* remove debug code

* fix the build of lp_tst

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-24 16:05:18 -08:00
Nikolaj Bjorner
133546625c update minor version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-24 09:24:46 -08:00
Nikolaj Bjorner
1b94d43a8b fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-24 08:52:56 -08:00
Nikolaj Bjorner
fad428381a prepare for integer intervals 2024-01-23 15:33:48 -08:00
Nikolaj Bjorner
98c9fa7faf prepare for handling integer intervals 2024-01-23 15:29:11 -08:00
Nikolaj Bjorner
36453c5949 use while (true) in do loops with continue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-23 14:56:57 -08:00
Nikolaj Bjorner
be7856c57d fix #7027 
TODO: review old nlsat bugs for effect of this fix.
 2024-01-23 14:56:15 -08:00
Nikolaj Bjorner
125a82bea5 improved diagnostics 2024-01-22 16:23:55 -08:00
Nikolaj Bjorner
8d4e7fac6b add diagnostics option to new arithmetic solver 2024-01-22 16:23:55 -08:00
Nikolaj Bjorner
839b7101ae add ability to multiply term 2024-01-22 15:48:45 -08:00
Nikolaj Bjorner
0ebd8d655b prepare for printing more cases of root objects in SMT 2024-01-22 15:48:45 -08:00
Nikolaj Bjorner
69f118e77f use assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-22 15:48:45 -08:00
dependabot[bot]
414c33f92d
Bump mymindstorm/setup-emsdk from 13 to 14 (#7095) 
Bumps [mymindstorm/setup-emsdk](https://github.com/mymindstorm/setup-emsdk) from 13 to 14.
- [Release notes](https://github.com/mymindstorm/setup-emsdk/releases)
- [Commits](https://github.com/mymindstorm/setup-emsdk/compare/v13...v14)

---
updated-dependencies:
- dependency-name: mymindstorm/setup-emsdk
  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>
 2024-01-22 14:50:06 -08:00
Nikolaj Bjorner
a7b564cafe update release scripts and notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-21 10:06:38 -08:00
Nikolaj Bjorner
7486e8724f track quantifier instantiation method in proof hint #7080 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-20 17:44:07 -08:00
Nikolaj Bjorner
302ebff704 prepare for release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-20 16:46:13 -08:00
Nikolaj Bjorner
e722dc7777 add status badge for windows build, remove windows build from Azure pipelines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-20 16:30:08 -08:00
Nikolaj Bjorner
2dd45f8c19 add Windows build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-20 16:28:04 -08:00
Nikolaj Bjorner
910b3023c2 free memory the clean way 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-20 14:01:01 -08:00
Nikolaj Bjorner
d32dcfc4a4 free memory the clean way 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-20 13:54:50 -08:00
Nikolaj Bjorner
17545233e6 encapsulate anum functionality 2024-01-20 12:59:58 -08:00
Nikolaj Bjorner
548be4c1f9 add explicit move constructor to deal with unit test regression test-z3 algebraic on Windows/debug - 
it uses copy constructor instead of move when returning a scoped_anum in functions such as power and root.
This leads to freeing memory that gets passed as return value.

The copy constructor for scoped_numeral is also suspicious because it doesn't ensure memory ownership.
 2024-01-20 12:59:58 -08:00
Nikolaj Bjorner
a2993f7457 encapsulate mpz a bit more 2024-01-20 12:59:58 -08:00
Thomas Haas
d2706bab64
Fixes in Java's User Propagator (#7088) 
* Fixed decide callback for Java user propagators

* Java User Prop:
- Added return value to conflict
- Added consequence method
- Added missing access modifier to decideWrapper

* Removed type parameters of expressions in UserPropagatorBase

* Renamed propagateConflict to propagateConsequence
 2024-01-18 09:29:15 -08:00
Nikolaj Bjorner
2c55aa5466 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-17 18:04:08 -08:00
Lev Nachmanson
d084a19630 take care of strategy undecided, Nikolaj's comments 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-17 14:17:07 -10:00
Lev Nachmanson
6e9a938533 Merge branch 'master' of https://github.com/z3prover/z3 2024-01-17 14:02:38 -10:00
Lev Nachmanson
c591a7a3e7 force int bound on int columns, call term_is_int() after subst 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-17 13:53:59 -10:00
Nikolaj Bjorner
fef1596c81 pin expression passed to validate_eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-17 15:11:06 -08:00
Nikolaj Bjorner
4f75153186
Update z3_api.h 
Updated doc https://github.com/Z3Prover/z3/discussions/7087
 2024-01-17 13:53:38 -08:00
Nikolaj Bjorner
c340233df6 fix #7081 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-16 10:31:31 -08:00