mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
16289 commits 24 branches 48 tags 158 MiB
Commit graph

2214 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
2e00f2f32d
Propagator (#5845) 
* user propagator without ids

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* user propagator without ids

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix signature

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* references #5818

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix c++ build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* switch to vs 2022

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* switch 2022

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Update propagator example (I) (#5835)

* fix #5829

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* switch to vs 2022

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Adapted the example to the changes in the propagator

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* context goes out of scope in stack allocation, so can't used scoped context when passing objects around

* parameter check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add rewriter

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Fixed bug in user-propagator "created" (#5843)

Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
 2022-02-17 09:21:41 +02:00
mbergen
2e15e2aa4d
Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API (#5832) 
* Add mkLinearOrder

* reorder arguments to match definition, add short comment

* add partial order

* add comments
 2022-02-16 23:37:20 +02:00
Nikolaj Bjorner
33985ebcf5 update expected 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 19:14:54 +02:00
Nikolaj Bjorner
07d02ea415 fix #5829 2022-02-09 12:08:36 +02:00
Nikolaj Bjorner
1c10ce4070 #5815 - surface multi-arity arrays over python API 2022-02-06 08:40:56 +02:00
Nikolaj Bjorner
8a84cacfea add tuple support for __getitem__ #5815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-06 04:02:12 +02:00
Nikolaj Bjorner
e9dad84b85 update documentation comments 2022-02-06 03:35:32 +02:00
Nikolaj Bjorner
a189ca8b60 truncation directive #5805 2022-01-31 10:50:46 -08:00
Nikolaj Bjorner
a621041308 fix #5795 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 10:45:38 -08:00
Hennadii Chernyshchyk
85f6456655
Add missing constness (#5787) 2022-01-21 15:32:25 +01:00