Nikolaj Bjorner
147fb0d9c1
fix tptp5 build
2022-11-30 21:41:44 -08:00
Nikolaj Bjorner
cfc8e19baf
add more simplifiers, fix model reconstruction order for elim_unconstrained
...
- enable sat.smt in smt_tactic that
is invoked by default on first goals
add flatten-clauses
add push-ite
have tptp5 front-end pretty print SMT2 formulas a little nicer.
2022-12-01 02:35:43 +09:00
Nikolaj Bjorner
f6595c161f
add examples with proof replay
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-19 17:43:56 -07:00
Nikolaj Bjorner
88d10f7fe4
add example for monitoring proof logs
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-19 13:37:51 -07:00
Nuno Lopes
87e45221fd
add missing break stmt to example
...
Reported by Henrique Preto
2022-10-14 09:43:18 +01:00
Nikolaj Bjorner
9b7c66ea7b
revert update to netcoreapp version
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-12 08:41:43 -07:00
Nikolaj Bjorner
ff679e0fce
increment version number
2022-09-11 19:02:44 -07:00
Nikolaj Bjorner
5322d4f241
fix #6326
2022-09-06 23:48:21 -07:00
Nikolaj Bjorner
791ca02ab1
formula simplification example
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-11 09:33:36 +03:00
Bruce Mitchener
6835522a7f
z3++.h: No longer include unused sstream.
...
This makes some code using the C++ API have to include `<sstream>`
if they used the functionality but didn't include it themselves.
2022-08-05 09:41:49 +03:00
Bruce Mitchener
7eb1e6dd23
userPropagator: Compile as C++20.
...
Using std::unordered_map::contains requires C++20.
2022-08-05 07:41:14 +03:00
Bruce Mitchener
fb1d0bc899
cmake: Remove ExternalProject BUILD_ALWAYS workaround.
...
This was only needed for cmake < 3.1, but we require later
than that.
2022-08-02 09:27:11 +03:00
Nikolaj Bjorner
5b219aab76
add mutual recursive datatypes to c++ API #6179
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 20:32:00 -07:00
Nikolaj Bjorner
2e13c0bf41
add API and example for one dimensional algebraic datatype #6179
2022-07-20 19:43:18 -07:00
Nikolaj Bjorner
393c63fe0c
fix #6114
2022-07-18 09:33:39 -07:00
Nuno Lopes
fcbbf7ba76
fix build warning+error in c++ example
2022-06-17 16:43:34 +01:00
Nikolaj Bjorner
dd46224a1d
use structured proof hints
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-28 09:37:41 -07:00
Nikolaj Bjorner
a5d588ce09
add example for #5933
2022-04-05 04:26:40 +02:00
Nikolaj Bjorner
053cb72cc2
handle return status
2022-04-04 20:19:15 +02:00
Nikolaj Bjorner
4f6811a6a2
with simplification
2022-04-03 21:10:53 -07:00
Nikolaj Bjorner
a24a922688
fix #5915
2022-03-22 16:03:44 -07:00
Clemens Eisenhofer
35fb95648b
Updated user-propagator example ( #5879 )
2022-03-03 10:42:06 -08:00
Nikolaj Bjorner
2e00f2f32d
Propagator ( #5845 )
...
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* user propagator without ids
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix signature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* references #5818
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix c++ build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update propagator example (I) (#5835 )
* fix #5829
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* switch to vs 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Adapted the example to the changes in the propagator
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* context goes out of scope in stack allocation, so can't used scoped context when passing objects around
* parameter check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Fixed bug in user-propagator "created" (#5843 )
Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
2022-02-17 09:21:41 +02:00
Nikolaj Bjorner
53f72d9cbe
updated mini
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-26 15:44:49 -08:00
Matteo Nicoli
cbdd7b0696
three smt2 examples added and one python example updated ( #5690 )
2021-12-01 16:21:12 -08:00
Brenton Bostick
5351640e97
Fix stray semicolon in examples ( #5669 )
2021-11-18 10:35:22 -08:00
rainoftime
b5deba8426
add EFSMT solving example ( #5654 )
...
Co-authored-by: rainoftime <rainoftime@gmail.com>
2021-11-09 11:05:10 -08:00
Clemens Eisenhofer
091079e58c
Added user propagator example ( #5625 )
...
* Added user propagator example
* User propagator example code refactoring
(+ removed unused parameter warning)
* Moved user-propagator example to its own directory
2021-11-02 15:03:02 -07:00
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