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 |
|
Matteo Nicoli
|
785fab74f4
|
Create bubble_sort.py (#4976)
|
2021-01-26 09:42:17 -08: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 |
|
Bruce Mitchener
|
0edd587e5a
|
Fix typos in examples.
|
2019-08-14 22:00:50 -07: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 |
|
Nikolaj Bjorner
|
e0a49dd556
|
html pages for z3 python tutorial
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-07 19:14:54 -07:00 |
|
Charlie Barto
|
167f968fa8
|
Change from BINARY_DIR to PROJECT_BINARY_DIR
|
2019-05-15 11:25:40 -07:00 |
|
Nikolaj Bjorner
|
56ac3f86a5
|
fix justification for implied equalities in special relations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-04-03 17:08:10 -07:00 |
|
Titus Barik
|
2f0d2ec385
|
PYTHON_PATH should say PYTHONPATH.
|
2019-01-18 16:18:16 -08:00 |
|
Huanyi Chen
|
19471f9fa3
|
Implement mini_quip
|
2019-01-04 18:30:02 -05:00 |
|
Huanyi Chen
|
83e3a79bd1
|
Remove testcase that takes long time to finish
|
2019-01-04 17:31:47 -05:00 |
|
Huanyi Chen
|
4b29b208ad
|
Add few more testcases
|
2018-12-28 13:28:15 -05:00 |
|
Huanyi Chen
|
300e99b67a
|
Make sure init is included when generalize
|
2018-12-28 13:21:40 -05:00 |
|
Huanyi Chen
|
b083c7546e
|
Substitue Vars in queries
Replace Vars that are representing primary inputs as "i#" when query
solvers.
|
2018-12-28 13:21:35 -05:00 |
|
Nikolaj Bjorner
|
f591e0948a
|
fix #1841
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-22 15:28:33 -08:00 |
|
Nikolaj Bjorner
|
498fa87993
|
seq rewriting fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-22 10:48:49 -08:00 |
|
Nikolaj Bjorner
|
37ef3cbeb2
|
add rc2 sample
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-20 14:32:01 -08:00 |
|