mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-02 21:37:02 +00:00
Code Activity
15246 commits 25 branches 48 tags 158 MiB
Commit graph

254 commits

Author SHA1 Message Date
Alexander Kreuzer
dc5fa89de3
Mixing Integers and Rational in the new Java API #5085 (#5098) 
* Added covariance to arithmetic operations

* Added distillSort

* Update JavaGenericExample.java

Co-authored-by: Alexander Kreuzer <alexander.kreuzer@sap.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-16 05:24:23 -07:00
Nikolaj Bjorner
be68456c06 java compilation? 2021-02-26 05:04:46 -08:00
Nikolaj Bjorner
06caf57a86 fix #5033 2021-02-26 03:42:13 -08:00
Malte Mues
5d8d42b1fa
Update the mkConstant parameter type (#4996) 2021-02-04 16:17:49 -08:00
Nikolaj Bjorner
e61949059d compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 19:50:34 -08:00
Addison Crump
b0cecf7747
Make multi-index arrays not so bad (#4857) 2020-12-05 15:45:46 -08:00
Addison Crump
3bca1fbcd8
Java type generics (#4832) 
* Generify, needs some testing and review

* Remove unnecessary change

* Whoops, ? capture that type

* Misread the docs, whoops

* More permissible arithmetic operations

* Implement believed Optimize generics

* Missed a few generics

* More permissible expr for arrays in parameters

* More permissible expr for bitvecs in parameters

* More permissible expr for bools in parameters

* More permissible expr for fps in parameters

* More permissible expr for fprms in parameters

* More permissible expr for ints in parameters

* More permissible expr for reals in parameters

* Undo breaking name conflict due to type erasure; see notes

* Whoops, fix typing of ReExpr

* Sort corrections for Re, Seq

* More permissible expr for regular expressions in parameters

* Fix name conflict between sequences and regular expressions; see notes

* Minor typo, big implications!

* Make Constructor consistent, associate captured types with other unknown capture types for datatype consistency

* More expressive; outputs of multiple datatype definitions are only known to be sort, not capture, and Constructor.of should make a capture

* Be less dumb and just type it a little differently

* Update examples, make sure to type Expr and FuncDecl sort returns

* General fixups

* Downgrade java version, make it only for the generic support, remove var and Expr[]::new construction

* Turns out Java 8 hadn't figured out how to do stream generics yet. Didn't even show up in my IDE, weird
 2020-11-30 10:04:54 -08:00
Nikolaj Bjorner
f58618aa04 fix java compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-26 08:09:48 -08:00
Nikolaj Bjorner
d6a5ef4343 add recfuns to Java #4820 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-25 12:25:20 -08:00
Nikolaj Bjorner
4e77984c57 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:59:20 -07:00
Nikolaj Bjorner
4b346ef693 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:58:42 -07:00
Nikolaj Bjorner
0bc33e9c9d correct the type returned by mkNth #4454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 09:10:58 -07:00
Nikolaj Bjorner
04829e6b7a fix #4437, not really interesting bug as debug assertion is really for non-interrupted flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:41:26 -07:00
Nikolaj Bjorner
df75792e9c fix #4454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-02 18:35:38 -07:00
Imran Settuba
be998c308c
Allow different parsing strategies (#4205) 
* modifiers

* modifiers and function

* revert

* .
 2020-05-04 12:28:50 -07:00
Nikolaj Bjorner
0f5cc2ec70 add missing API call for solverInterrupt to Java. Fix #3382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 14:52:59 -07:00
Nikolaj Bjorner
a7b3dfb3af try now #3202 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-08 14:17:04 +01:00
Nikolaj Bjorner
dd5744a357 fix #3202 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-07 15:12:20 +01:00
Nikolaj Bjorner
53a01a07bd rename additional build options #2709 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 21:32:35 -08:00
Nikolaj Bjorner
27765ee0f4 add stub for #2522 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 09:54:07 -07:00
Nikolaj Bjorner
000e485794 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-01 12:17:19 -07:00
Nikolaj Bjorner
3147d2351d fix #2460 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-03 08:06:38 -07:00
Nikolaj Bjorner
728139599c unfinalize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-26 16:43:42 -07:00
Nikolaj Bjorner
00a4f6ad3d throw 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-26 15:28:38 -07:00
Nikolaj Bjorner
1d223b0403 setting ctx to null after close 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-26 14:59:19 -07:00
Nikolaj Bjorner
2d4e9a0f67 update managed APIs for lambda-based array models #2400 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-13 16:20:36 -04:00
Charlie Barto
167f968fa8 Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
Nikolaj Bjorner
40e329fc92 remove push/pop for fixedpoint objects from API #2249 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-27 10:13:15 -07:00
Nikolaj Bjorner
d2a3b53d92 fix remaining incorrect uses of new BoolExpr related to #2125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 12:28:17 -08:00
Nikolaj Bjorner
77942a35dc fix #2125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-07 11:20:53 -08:00
Bruce Mitchener
51a947b73d Change how 64 bit builds are detected. 
Instead of doing this at configure time, we look at the actual
compile time status. This also avoids hardcoding checks based on
what CPU architecture is present, which doesn't work when Z3 is
being built on non-x86_64 platforms.
 2018-12-09 16:16:20 +07:00
Bruce Mitchener
afc9de960c Improve JavaDoc. 2018-11-30 08:42:28 +07:00
Bruce Mitchener
38ca9ddfeb Swapped significand and exponent in call to Context.mkFPNumeral. 
Fixes #973.
 2018-11-30 08:42:01 +07:00
Nikolaj Bjorner
1603075189 add empty/full to java #1944 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-17 15:46:06 -08:00
Nikolaj Bjorner
f14a2b9a7c fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 16:13:23 -07:00
Nikolaj Bjorner
44a0dbbc61 fix #1864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 08:06:51 -07:00
Nikolaj Bjorner
2097983db3 fix java bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 14:05:38 -07:00
Nikolaj Bjorner
3bc2213d54 fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:43:42 -07:00
Sosuke MORIGUCHI
22fc5ad771 Modify javadoc directive and mis-capitalization of method name 2018-07-31 21:39:02 +09:00
Nikolaj Bjorner
605dcc40a3 fix #1741 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 09:19:13 -07:00
Nikolaj Bjorner
648a531950 update java example to bypass bit-rot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:50:29 -07:00
Nikolaj Bjorner
370abf602c fix java API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:32:58 -07:00
Nikolaj Bjorner
1f5d182f6a update java bindings for arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:09:57 -07:00
Nikolaj Bjorner
0d4b4b30b1 change storage layout of .Net binding Z3_bool to byte to deal with uninitialized memory reads on larger allocation sizes. Bug introduced when switching from defining Z3_bool as int to the bool type from stdbool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 02:58:06 -07:00
Nikolaj Bjorner
fad1e611aa build warnings, updates to reduce-invertible, change is_algebraic tester to use int return type 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 12:34:55 -07:00
Nikolaj Bjorner
ea4218a192 add upper-case files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:52:38 -07:00
Nikolaj Bjorner
1c1357af7d remove lower case files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:52:02 -07:00
Nikolaj Bjorner
a8e864a3e6 add missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:36:36 -07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
4f5775c531 remove interpolation and duality dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-24 08:33:48 -07:00