mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
19786 commits 49 branches 53 tags 182 MiB
Commit graph

2624 commits

Author SHA1 Message Date
Clemens Eisenhofer
b0d8b27f37
Fixed registering expressions in push/pop (#5964) 
* Fixed registering expressions in push/pop

* Reused existing function
 2022-04-11 16:50:13 +02:00
Frédéric Bour
f43d9d00d4
Z3_add_rec_def body is not a macro (#5963) 2022-04-11 13:38:20 +02:00
Nikolaj Bjorner
011c1b2dd2 remove refs to bare_str 2022-04-09 12:06:27 +02:00
Nikolaj Bjorner
005b8e3cf8 arc -> arch 2022-04-09 08:28:22 +02:00
Nikolaj Bjorner
c98eda03f7 nightly osx arm64 wheel 2022-04-09 06:55:31 +02:00
Nikolaj Bjorner
f3789e21a3 id doesn't use mk_util 2022-04-08 14:42:18 +02:00
fleisherdev
ac2523af82
Fix null ref on access of Entry[] contents (#5947) 
Co-authored-by: jfleisher <jofleish@microsoft.com>
 2022-04-06 05:37:51 +02:00
Nikolaj Bjorner
3828130791 fix #5922 use 0u to help type inference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-24 14:05:14 -10:00
John Fleisher
ce04c16a6f
Jfleisher/nightlynuget (#5916) 
* WiP: Test nightly version number change

* Fix debug assert

* WiP: test nuget publish to AzDo feed for nightly build

* WiP: Make Nuget deploy separate stage

* WiP: fix nightly stage name

* change nuget push to vstsfeed

* Try case sensitive name for artifacts

* WiP: use artifact folder names

* add Rev version to package

* WiP: build def variation on nightly build version

* WiP: use Build_BuildNumber and Build_DefinitionName

* WiP: using hyphen in nightly version

* Tag nightly packages with datetime

* fix commit

* Build.BuildId and Build.DefinitionName

* WiP: change suffix format to lead with alpha

* test z3public feed publish

* revert public publish test

* WiP: test build# versioning scheme

* WiP: another variant on version number for nightly

Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-22 12:19:58 -07:00
Nikolaj Bjorner
bbb27775ed ensure that objects in callback are of sort Ast. 2022-03-20 11:24:42 -07:00
Nikolaj Bjorner
b5b9c85c40 call it UbuntuBuild 2022-03-19 15:24:53 -07:00
Nikolaj Bjorner
cfe02edda5 remove stale return 2022-03-19 12:26:48 -07:00
Nikolaj Bjorner
86af723db7 remove left-over debug output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-19 09:40:29 -07:00
Nikolaj Bjorner
41d1c34067 remove else case 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-17 12:33:15 -07:00
Nikolaj Bjorner
1fa373d6c2 old bug: unit of xor is false 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-17 08:21:22 -07:00
Matt Thornton
4e0a2f5968
Dispose of intermediate Z3Objects created in dotnet api. (#5901) 
* Dispose of intermediate Z3Objects created in dotnet api.

* Set C# LangVersion to 8.0.

* Fix build errors.

* Fix warning about empty using statement.

* Fix Xor to only dispose of objects that it creates internally.
 2022-03-17 08:08:05 -07:00
Nikolaj Bjorner
0b230ee703 move some functions to using var pattern #5900 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-16 16:29:54 -07:00
Nikolaj Bjorner
a1517251dd call dispose on sorts #5900, missing charSort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-16 07:28:05 -07:00
Nikolaj Bjorner
cd5e114ed3 call dispose on sorts #5900 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-16 07:24:33 -07:00
Nikolaj Bjorner
cb9dcb799f add regex power to API and for Java per request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-16 06:17:31 -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
Nikolaj Bjorner
706d7ea893 native context uses legacy mk_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-15 16:01:05 -07:00
John Fleisher
97c7ce63b5
Clean up build warnings (#5884) 
* Clean up warnings in compile for documentation notes

* remove snk from local build

Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-07 12:55:30 -08:00
Nikolaj Bjorner
882fc31aea doc strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 15:25:05 -08:00
Nikolaj Bjorner
b0c0f4d1f4 fix #5876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 15:07:45 -08:00
Nikolaj Bjorner
3e51b69a9a no fun! 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 15:03:02 -08:00
Nikolaj Bjorner
87e6f103c6 commenting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 14:00:07 -08:00
Nikolaj Bjorner
676ba78600 fix else case: it is first argument of const array 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 13:10:02 -08:00
John Fleisher
35d26bc282
NativeModel: TryGetArrayValue (#5881) 
* WiP:  Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort

* WiP: Native z3 mk_ functions

* WiP: mk_ functions for NativeContext

* WiP: add utility functions for getting values

* WiP: Adding more native utility functions

* native model pull

* WiP: NativeContext additions for array access

* WiP: use Z3_symbol in place of managed Symbol

* WiP: add solver, model, and array methods

* WiP: MkSimpleSolver, MkReal

* WiP: GetDomain GetRange

* WiP: MkExists

* Override for MkFuncDecl

* MkConstArray, MkSelect

* WiP: code cleanup

* migrate Context reference to NativeContext

* remove local signing from PR

* minor code cleanup

* Sorts to properties, fix usings,

* make IntSort property

* sort using

* IntSort, RealSort - properties

* WiP: get array value update

Co-authored-by: jfleisher <jofleish@microsoft.com>
 2022-03-03 13:06:30 -08:00
Nikolaj Bjorner
248a3676af na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:40:29 -08:00
Nikolaj Bjorner
e1e8d15827 stub out array serialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:38:23 -08:00
Nikolaj Bjorner
cd324a4734 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:07:00 -08:00
Nikolaj Bjorner
8d1276fa60 using directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:03:31 -08:00
John Fleisher
a08be497f7
NativeContext, NativeSolver, NativeModel - updates for Pex (#5878) 
* WiP:  Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort

* WiP: Native z3 mk_ functions

* WiP: mk_ functions for NativeContext

* WiP: add utility functions for getting values

* WiP: Adding more native utility functions

* native model pull

* WiP: NativeContext additions for array access

* WiP: use Z3_symbol in place of managed Symbol

* WiP: add solver, model, and array methods

* WiP: MkSimpleSolver, MkReal

* WiP: GetDomain GetRange

* WiP: MkExists

* Override for MkFuncDecl

* MkConstArray, MkSelect

* WiP: code cleanup

* migrate Context reference to NativeContext

* remove local signing from PR

* minor code cleanup

Co-authored-by: jfleisher <jofleish@microsoft.com>
 2022-03-03 10:41:12 -08:00
Nikolaj Bjorner
811cd9d48d add example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 09:14:47 -08:00
Nikolaj Bjorner
ee18c5070c add stubs for injective function axioms, add some parameter functions 2022-03-03 09:09:03 -08:00
Nikolaj Bjorner
757cf7622d sketch ArrayValue, add statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-02 10:59:19 -08:00
Nikolaj Bjorner
80506dfdfa sketch ArrayValue, add statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-02 10:55:39 -08:00
Nikolaj Bjorner
bf14aeb1bd stub out nativesolver 2022-03-02 10:06:38 -08:00
Nikolaj Bjorner
5f79a977fb use conventions from Context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 14:27:57 -08:00
Nikolaj Bjorner
c812d1e890 update native func interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 14:07:20 -08:00
Nikolaj Bjorner
61d2654770 quantifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 13:18:18 -08:00
Nikolaj Bjorner
deeb5e9921 finish NativeModel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 12:40:03 -08:00
Nikolaj Bjorner
c0826d58bf add stubs for native model and func interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 12:11:10 -08:00
Nikolaj Bjorner
deaad86d6a nit 2022-03-01 12:11:10 -08:00
Clemens Eisenhofer
412b05076c
User-functions fix (#5868) 2022-02-26 09:21:01 -08:00
Nikolaj Bjorner
30a2f2fd9d initial stab at NativeContext 2022-02-25 07:56:36 -08:00
Nikolaj Bjorner
ff5d210e81 na 2022-02-20 10:33:15 +02:00
Nikolaj Bjorner
9a1a72867c Add str.<= and str.< to Java API 2022-02-20 10:29:38 +02:00
Nikolaj Bjorner
7091b1c856 add additional regex operators to API 2022-02-20 10:29:18 +02:00