mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity
19575 commits 22 branches 48 tags 155 MiB
Commit graph

439 commits

Author SHA1 Message Date
Josh Berdine 934455a24b
Remove vestiges of old ml api (#7597) 2025-03-27 16:41:31 -07:00
Nikolaj Bjorner ec14ef765e Update Ubuntu job name in Azure pipeline and add string variable creation in C API example 2024-09-23 17:42:39 +01:00
Nikolaj Bjorner f7691d34fd fix generic example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-02-21 08:16:01 -08:00
Bruce Mitchener 53f89a81c1
Fix some typos. (#7115) 2024-02-07 23:06:43 -08:00
Nikolaj Bjorner ebe5ebf0ae Add branch and bound solver, for fun 2023-12-23 11:58:29 -08:00
Nikolaj Bjorner 4fe423482a bugfix on slack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-21 15:36:26 -08:00
Nikolaj Bjorner ae1d9270b5 improve add bin/item functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-21 15:27:11 -08:00
Nikolaj Bjorner b09c237775 rudimentary bin cover solver using the user propagator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-21 15:18:26 -08:00
Christoph M. Wintersteiger 68a2c08d5e
Add Z3_get_estimated_alloc_size to OCaml API (#7068) 2023-12-21 12:54:30 -08:00
Christoph M. Wintersteiger 16753e43f1
Add accessors for RCF numeral internals (#7013) 2023-11-23 17:54:23 +01:00
Christoph M. Wintersteiger 23de8056d7
Add RCF functions to OCaml API (#6932) 2023-10-06 11:49:22 +09:00
Nikolaj Bjorner 5b385bd2fe fix #6665 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-02 10:58:21 -07:00
Nikolaj Bjorner ce09c2ea6d fix build 2023-03-27 09:56:09 -07:00
Nikolaj Bjorner b4ad747e0b fix #6644 2023-03-27 09:00:38 -07:00
Nikolaj Bjorner fa72ec5405 switch to expose fresh function instead of changing legacy function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:05:34 -08:00
Nikolaj Bjorner 47c7ed3b17 update ml example to 64 bit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 04:33:52 -08:00
Nikolaj Bjorner f3d6856736 remove msf example, add option to make model converter not reduce models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-19 20:24:31 -08:00
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