3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

394 commits

Author SHA1 Message Date
Henrich Lauko 96671cfc73
Add and fix a few general compiler warnings. (#5628)
* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings
2021-10-29 15:42:32 +02:00
Alexander Traud f5f35f87d0
fix grouping for latest doxygen (#5626)
Since doxygen 1.8.16, opening and closing a group must not be done as
C comment but as doxygen command. In other words, not one but two
asterisk characters are required so that doxygen finds a group.
2021-10-27 23:46:31 +02:00
Nikolaj Bjorner eb8c8da8a7 ex handler
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-27 09:38:36 +02:00
Nikolaj Bjorner 7f41d6140f use some suggestions from #5615
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-22 12:39:55 -04:00
Nikolaj Bjorner f05ac8a429 updated C++ API for escaped and unescaped strings #5615
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-21 14:52:59 -04:00
Kartik Singhal 1dcbd2d86c
Correct capitalization of package (#5569)
See https://stackoverflow.com/a/50004273/1167061
2021-09-25 09:04:06 -07:00
Nikolaj Bjorner 55285b2193 make it easier to iterate over arguments of an application
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-09-02 09:51:59 -07: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
Kiwamu Okabe 81b8f397b3
Need -thread option to compile OCaml example (#5440)
I can compile the OCaml example with `-thread` option at Linux.

```
$ ocaml --version
The OCaml toplevel, version 4.05.0
```
2021-07-28 16:57:26 -07:00
Nikolaj Bjorner a1b036a4fa
Update README.md 2021-04-25 17:02:34 -07:00
Nikolaj Bjorner 3ff5d4226a
Update README.md 2021-04-25 16:59:53 -07:00
Tias Guns a52b485d9c
marco: immediately shrink to core if not subset (#5203)
Small improvement, found while translating it in another system
2021-04-20 12:29:52 -07:00
Rolf Eike Beer 7f8e2a9f75
clean up CMake code (#5182)
* CMake: simplify FindGMP.cmake

Remove printing of all the different variables, and let FPHSA output the library
name. Add an imported target, which bundles the library and the include
directories for easier usage.

* fix build: vector::c_ptr() now is vector::data()

* CMake: use Threads::Threads imported module

Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect.

* CMake: remove needless policy setting

The minimum required version is CMake 3.4, where these policies are already set
to new because they were introduced earlier.

* CMake: remove needless variable expansion
2021-04-14 10:29:15 -07:00
Nikolaj Bjorner 4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner 7fab0f5923 updated experiment 2021-03-26 14:58:23 -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 7eceeff349 move branch of unit variable 2021-03-08 10:09:04 -08:00
Nikolaj Bjorner 3c26a965e1 updated script, add comment to mk_eq_empty 2021-03-07 06:59:58 -08:00
Nikolaj Bjorner 8de96009cd na 2021-03-06 12:36:19 -08:00
Nikolaj Bjorner 8d54e83567 updated hitting set sample 2021-03-06 10:18:52 -08:00
Nikolaj Bjorner 022a1fd3dd fix #5080 assertion is violated on legal input, add an example 2021-03-05 15:01:39 -08:00
Nuno Lopes 1bb9a02160 travis timeouts 2021-02-21 13:13:19 +00:00
Matteo Nicoli 785fab74f4
Create bubble_sort.py (#4976) 2021-01-26 09:42:17 -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 5c2f07df09 max lex less chatty
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-29 19:47:17 -08:00
Nikolaj Bjorner eacef5f3f9 deal with warnings over unused variables and procedures
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-11-29 19:45:35 -08:00
Nuno Lopes 9c08b60b5a c++ example: call Z3_finalize_memory() so that the buildbot leak checker doesnt complain about reachable memory 2020-10-24 15:35:56 +01:00
Nikolaj Bjorner 85b4fc1865 void
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-23 10:47:39 -07:00
Andrew V. Jones bb9cd5dd49
Ensure that the 'OUTPUT' locations in CMake for Python examples is accurate (#4499)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
2020-06-04 15:04:01 -07:00
Nikolaj Bjorner 59e388ece1 handle bind proof constructor and print lambda
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-06-04 11:59:59 -07:00
Nikolaj Bjorner 773b27296f translate optimize from c++ API #2859
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-15 04:24:51 -08:00
Nikolaj Bjorner 8973c18856 require c++11 on TPTP #2738
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-25 09:54:23 -08:00
Nikolaj Bjorner c7248a65e4 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 22:31:45 -08:00
Nikolaj Bjorner 31a6788859 comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-11 12:39:57 -07:00
Nikolaj Bjorner a990e7f02e add visitor example, fix double conversion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-11 12:37:26 -07:00
Nikolaj Bjorner 3eac4a4aa1 clean up examples for unused variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-09-22 10:24:05 -07:00
Bruce Mitchener 0edd587e5a Fix typos in examples. 2019-08-14 22:00:50 -07:00
Bruce Mitchener 0eafeb9342 Fix confusing tabs mixed in with spaces in C examples. 2019-08-13 09:26:44 -07:00
Richard Bradley 04e0b767c3 Fix sudoku Java example 2019-07-31 23:32:38 +01: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
Nikolaj Bjorner 807095a344 fix #2375
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-03 10:04:00 +07:00
Nikolaj Bjorner e5dffeace4 fix #2365
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-30 08:40:41 +03:00
Nikolaj Bjorner b4bbe12ca1 set kernel to 3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-11 10:41:51 -07:00
Nikolaj Bjorner 7bfb730fee fix traffic jam
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-10 17:45:55 -07:00
Nikolaj Bjorner b4daf8dcd8 adding advanced port
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-10 12:33:20 -07:00
Nikolaj Bjorner 9f426443ca saving strategies tutorial from notebooks.azure.com
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-10 10:30:11 -07:00
Nikolaj Bjorner 6cd7169665 readme and link
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-09 11:10:35 -07:00
Nikolaj Bjorner 2861b10d58 update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-08 09:26:15 -07:00
Nikolaj Bjorner 08528b3526 ported guide
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-08 09:20:55 -07:00
Nikolaj Bjorner 36e03db0f3 png
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-07 19:29:14 -07:00