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

264 commits

Author SHA1 Message Date
Thomas Haas
d2706bab64
Fixes in Java's User Propagator (#7088) 
* Fixed decide callback for Java user propagators

* Java User Prop:
- Added return value to conflict
- Added consequence method
- Added missing access modifier to decideWrapper

* Removed type parameters of expressions in UserPropagatorBase

* Renamed propagateConflict to propagateConsequence
 2024-01-18 09:29:15 -08:00
Michał Górny
9ad4d50b5d
Use built-in importlib.resources on Python 3.9+ (#7042) 
Use built-in `importlib.resources` module rather than the external
`importlib_resources` package on Python 3.9 and newer.  The latter
is only intended as a backport for old Python versions, and since modern
Linux distributions may no longer support such old Python versions,
they also no longer provide importlib_resources (this is the case
on Gentoo).
 2023-12-05 07:49:32 -08:00
Rui Chen
4d4359f78a
fix shebang syntax issue (#7044) 2023-12-05 07:48:15 -08:00
Bruce Mitchener
3422f44cea
Fix syntax warning when using Python 3.12. (#7022) 
This happens when generating the Python API and you are using
Python 3.12 in the build environment:

```
.../z3/scripts/update_api.py:1828: SyntaxWarning: invalid escape sequence '\#'
```

This was a `DeprecationWarning` previously, but Python 3.12 changed
it to a `SyntaxWarning` to make it more visible. The release notes
indicate that this will be a syntax error in the future.
 2023-11-28 07:55:25 -08:00
Nikolaj Bjorner
f6c9ead10c #6964 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-27 13:17:20 -07:00
rsetaluri
d5fe4b0d78
Update script to use importlib_resources (#6949) 
To avoid a deprecation warning, this change updates scripts/update_api.py
to use 'importlib_resources' instead of 'pkg_resources'.

See https://setuptools.pypa.io/en/latest/pkg_resources.html and
https://importlib-resources.readthedocs.io/en/latest/migration.html for
more information.
 2023-10-24 13:19:44 -07:00
Sijmen
0a444f357a
Slightly improve Z3_LIBRARY_PATH error message (#6895) 2023-09-11 12:58:03 -07:00
Nikolaj Bjorner
e8a38c5482 build fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 19:14:45 -07:00
Nikolaj Bjorner
3d8f75b3d8 enable on-clause with dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 16:59:02 -07:00
Jerry James
f5c069f899
Fix regular expression strings with escapes (#6797) 2023-07-07 09:57:07 -07:00
Nikolaj Bjorner
81068981aa fix #6746, fix type errors in java bindings 2023-06-03 09:41:29 +02:00
Clemens Eisenhofer
82667bd86b
Fix UP's decide callback (#6707) 
* Query Boolean Assignment in the UP

* UP's decide ref arguments => next_split

* Fixed wrapper

* More fixes
 2023-06-02 09:52:54 +02:00
ditto
11264c38d8
Java user propagator interface (#6733) 
* Java API: user propagator interface

* Java API: improved user propagator interface

* Java API: Add UserPropagatorBase.java

* Remove redundant header file

* Initialize `JavaInfo` object and error handling

* Native.UserPropagatorBase implements AutoCloseable

* Add Override annotation
 2023-05-24 18:27:28 +01:00
Nikolaj Bjorner
6aaaa3b015 fix #6660 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-03-31 09:58:28 -07:00
Kevin Phoenix
1a9990a92f
Use sys.getdefaultencoding() instead of sys.stdout.encoding (#6612) 2023-02-28 11:46:10 -08:00
Nikolaj Bjorner
550619bfcf add API for creating and attaching simplifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 17:06:03 -08:00
Nikolaj Bjorner
07dd1065db added API to monitor clause inferences 
See RELEASE_NOTES for more information
examples pending.
 2022-10-19 08:34:55 -07:00
Thomas Pani
adf6e98cdf
Handle _out(STRING) parameters in Java API (#6325) 2022-09-06 15:29:12 -07:00
Bruce Mitchener
a3161bdc15 update_api.py: Remove usage of MKException. 
This wasn't working as it was being accessed from a function object
rather than the module.

Instead, let's just print the error and exit.
 2022-08-04 07:54:42 +03:00
Nikolaj Bjorner
cd7ef11593 add decide callbacks to propagator API 
this is an intermediary state. The decide_eh is only partially implemented.
 2022-07-27 04:28:41 +02:00
Stefan Muenzel
99212a2726
Use int64 for ocaml api functions that require it (#6150) 
* Use int64 for ocaml api functions that require it

Signed-off-by: Stefan Muenzel <source@s.muenzel.net>

* Use elif

Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
 2022-07-11 09:25:05 -07:00
Nikolaj Bjorner
e6e0c74324
Update update_api.py 
fix typo
 2022-07-02 13:17:14 -07:00
Nikolaj Bjorner
c35d0d1e49
Update update_api.py 
add automation!
 2022-07-02 13:05:35 -07:00
Nikolaj Bjorner
5ba8231d07 make it work with old pythons 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-21 09:10:38 -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
Clemens Eisenhofer
2fa60aa43c
Added function to select the next variable to split on (User-Propagator) (#6096) 
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int
 2022-06-19 10:49:25 -07:00
Nuno Lopes
73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places 
It's harmful to have iostream everywhere as it injects functions in the compiled files
 2022-06-17 14:10:19 +01:00
Nikolaj Bjorner
363b69f588 fix #6034 2022-05-16 16:44:13 -07:00
Nikolaj Bjorner
f6b2874d7c update to take effect of def_API for callback functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-16 10:30:54 -07:00
Nikolaj Bjorner
8218f25222 add decide callback 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 15:30:03 -07:00
Nikolaj Bjorner
3b441137c0 ocaml build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 11:01:23 -07:00
Nikolaj Bjorner
d58de2f8e4 java build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 10:20:32 -07:00
Nikolaj Bjorner
a71ce54c34 freeze functions with callbacks for ocaml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 10:04:50 -07:00
Nikolaj Bjorner
cf4149d53e freeze functions with callbacks for ocaml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 10:02:41 -07:00
Nikolaj Bjorner
1ab7be67d0 java build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 09:58:43 -07:00
Nikolaj Bjorner
a3b066f0b4 ml: VOIDP -> ptr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-07 12:49:05 -07:00
Nikolaj Bjorner
b633947762 don't log function pointers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-07 12:41:51 -07:00
Nikolaj Bjorner
6d40e6f401 java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-07 11:24:46 -07:00
Nikolaj Bjorner
14214c5a07 exposing user propagators over .Net 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-07 11:08:40 -07:00
Nikolaj Bjorner
c996a66da0 separate pre-processing, add callback parameter to push/pop in python API 2022-04-11 17:05:59 +02:00
Nikolaj Bjorner
fd1f5cdd0f fix callback type declarations for propagators 2022-03-19 12:24:46 -07:00
Nikolaj Bjorner
5ec7a66a45 change class name, add comment 2022-01-04 22:02:14 -08:00
Nikolaj Bjorner
964a5cd761 lump java together 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:48:05 -08:00
Nikolaj Bjorner
ef3dd32364 some cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:21:53 -08:00
Nuno Lopes
9b5ec6d004 logging cleanup 
move everything out-of-line as common path doesn't log
fix some race conditions on file ptr vs enable_logging vars
 2021-08-29 12:24:19 +01:00
Nuno Lopes
1f4a7c5101 logging: don't call the returned function twice (one for log, one for return) 
Z3_simplify() does RETURN_Z3(simplify(...)), hence the function was being called twice
it turns out simplify is not idempotent, so calling it twice can result in different results
thus breaking the log.
 2021-08-29 11:06:19 +01:00
Karlheinz Friedberger
764e033bf4
Specify and document value for environment variable for loading native library in Java bindings (#5477) 
* limit range of environment variable for loading the native library in Java to "true".

This change specifies the range of values that are allowed to set the environment
variable "z3.skipLibraryLoad".
Only the value "true" (in upper-, lower-, and mixed-case is accepted as valid value.
Other values, such as "false", "0", "1", "foo", an empty or a missing value are
evaluated to "false" and cause the default loading of the native library.

* adding documentation about environment variable for (not) loading the native library in Java.

This is a follow-up commit for #4667 to provide a publicly visible documentation.
 2021-08-13 14:54:02 -07:00
Nikolaj Bjorner
34885562e0 try without #!/bin/env python #5397 2021-07-10 15:20:56 +02:00
Nikolaj Bjorner
16448104eb add new model event handler for incremental optimization 2021-02-05 17:11:04 -08:00
Nikolaj Bjorner
d2abc9ed0f remove comment #4956 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-21 22:18:24 -08:00