ada/z3
0
0
Fork 0
mirror of https://github.com/AdaCore/z3.git synced 2026-02-12 12:40:40 -08:00
Code Issues Packages Projects Releases Wiki Activity
20,121 Commits 55 Branches 6 Tags
master
Commit Graph

86 Commits

Author SHA1 Message Date
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
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
Nikolaj Bjorner
791ca02ab1 formula simplification example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-11 09:33:36 +03: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
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
rainoftime
b5deba8426 add EFSMT solving example (#5654) 
Co-authored-by: rainoftime <rainoftime@gmail.com>
 2021-11-09 11:05:10 -08: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
Nikolaj Bjorner
7fab0f5923 updated experiment 2021-03-26 14:58: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