mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity
16271 commits 23 branches 48 tags 157 MiB
Commit graph

13772 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
545341e699 fix #5895 2022-03-12 09:17:13 -08:00
Nikolaj Bjorner
c51ca86203 add another constant folding case 2022-03-10 17:39:40 -08:00
Nikolaj Bjorner
e839e18381 minimal addition to rewrite bit-vector to character conversion using constant folding. 2022-03-10 17:31:17 -08:00
Nikolaj Bjorner
8f2ea90db1 Merge branch 'master' of https://github.com/Z3Prover/z3 2022-03-10 17:09:36 -08:00
Nikolaj Bjorner
081c62d006 allow range comparison for bit-vectors and int/real 2022-03-10 17:08:49 -08:00
Nikolaj Bjorner
580012e19f fix #5894 
expp is not implemented. This is the second time a fuzz bug reports it. Instead of closing the bug, just disable code path as fuzzers are not considering the comment from previous bug.
 2022-03-10 09:45:09 -08:00
Hari Govind V K
f26c12a9ad
fix #5882. Use model true when inlining (#5892) 2022-03-09 12:31:39 -08:00
Nuno Lopes
43f7636826 remove some copies/moves 2022-03-09 12:46:41 +00:00
Nikolaj Bjorner
1d224d1bcd na 2022-03-08 08:51:00 -08:00
Nikolaj Bjorner
c6f8ee33d4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-08 08:36:19 -08:00
Nikolaj Bjorner
3293aeb7c7 na 2022-03-08 08:36:19 -08: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
Lorenzo Veronese
e3568d5b47
Handle additional cases in rule_properties::check_accessor (#5821) 
* Handle additional cases in rule_properties::check_accessor

* Walk parents depth first in rule_properties::check_accessor
 2022-03-07 07:49:59 -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
bbadd17d56 fix #5874 2022-03-02 08:46:28 -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
Nikolaj Bjorner
2b6dadcbc6 fix #5869 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-28 17:02:13 -08:00
Nikolaj Bjorner
302c0d178c fix #5867 2022-02-26 09:52:23 -08:00
Clemens Eisenhofer
412b05076c
User-functions fix (#5868) 2022-02-26 09:21:01 -08:00
Nuno Lopes
689e2d41de remove a bunch of unneeded memory allocations 2022-02-25 16:08:23 +00:00
Nikolaj Bjorner
7f149a36d7 refining model update rules for del_rule #5865 #5866 2022-02-25 08:03:46 -08:00
Nikolaj Bjorner
30a2f2fd9d initial stab at NativeContext 2022-02-25 07:56:36 -08:00
Nikolaj Bjorner
f2e712b0d6 throttle is_compatible to check variables at most once 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-23 08:45:22 -08:00
Nikolaj Bjorner
7b4f1ed530 missing initialization of m_user_propagator, disable unsound in-processing in pb_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-23 04:49:42 -08:00