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

274 commits

Author SHA1 Message Date
Bruce Mitchener
8a3556e5ba cmake: Remove dep on mk_util.py for update_api.py calls. 
update_api.py doesn't depend on mk_util.py any longer, so these
dependencies can go away.
 2022-08-04 07:54:26 +03:00
Bruce Mitchener
42f5047463 cmake: Cleanup remnants of workaround for USES_TERMINAL. 
In older versions, this was dependent upon the version of cmake,
but when it was updated for newer cmake, these remnants were
left.
 2022-08-02 17:39:10 +03:00
Nikolaj Bjorner
54b16f0496
Update NativeStatic.txt 
not so automatically generated
 2022-07-02 13:04:09 -07:00
Nikolaj Bjorner
3c94083a23 fix doc errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-01 15:29:44 -07:00
Nikolaj Bjorner
3189544050 next split 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-22 09:03:32 -07:00
Nikolaj Bjorner
b254f4086b Separate out native static content for Java 
Make it easier to add native methods for callbacks (for user propagator) #6097

The Java User propagator wrapper should define a base class with virtual methods that can be invoked from functions defined in NativeStatic.txt
 2022-06-21 09:09:42 -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
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
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
6013d5da47 #5755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 14:05:06 -08:00
Nikolaj Bjorner
7a6070506d #5727 
Expose diff function,
expose allchar in Java API
expose op codes for replace/re/all
 2021-12-20 10:17:06 -08:00
Nikolaj Bjorner
0d055b83eb update input for doxygen #5400 2021-12-05 09:04:18 -08:00
CEisenhofer
c58b2f4a9c
Added character functions to API (#5549) 
* Added character functions to API

* Changed names of c++ functions
 2021-09-15 13:34:58 +01:00
intrigus-lgtm
35698c650d
Add AssertSoft String overload for Java Api (#5475) 
This adds a String overload for AssertSoft.
Previously only integer weights could have been used,
limiting the user. With Strings the user can now use
e.g. Java's BigInteger class converted to a String instead.
 2021-08-12 09:18:18 -07:00
CEisenhofer
0fa4b63d26
Added sbv2s (#5413) 
* Added sbv2s

* Fixed indention

Co-authored-by: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
 2021-07-16 17:58:28 +02:00
Nikolaj Bjorner
a3010c8875 version inc, bvsort->bitvecsort 2021-07-13 17:14:47 +02:00
Nikolaj Bjorner
7ae78da850 adding access to characters over API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 15:56:08 +02:00
Marc Mosko
8a33391708
Expose optimize.assertAndTrack to Java (#5387) 
Co-authored-by: Marc Mosko <mmosko@parc.com>
 2021-07-06 01:22:00 -07:00
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