Nikolaj Bjorner
|
fc3cbcbe02
|
remove deprecated options
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-02 10:16:35 -08:00 |
|
Nikolaj Bjorner
|
b98c864d76
|
fixes to inprocessing code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-01 18:06:26 -08:00 |
|
Nikolaj Bjorner
|
c8e655830f
|
add statistics to cubing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-01 10:13:54 -08:00 |
|
Nikolaj Bjorner
|
a4dc68766d
|
preparing for more efficient asymmetric branching
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-29 17:16:15 -08:00 |
|
Nikolaj Bjorner
|
53e36c9cf9
|
re-organize iterators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-16 09:29:44 -08:00 |
|
Nikolaj Bjorner
|
d8a2e9d008
|
initialize glue in constructor to ensure it gets set
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-15 15:57:07 -08:00 |
|
Nikolaj Bjorner
|
f7e14b3283
|
add global autarky option, update translation of solvers to retain vsids, remove stale code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-14 18:19:21 -08:00 |
|
Nikolaj Bjorner
|
6f273e7b8f
|
bug fixes in uninitialized variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-11 12:09:33 -08:00 |
|
Nikolaj Bjorner
|
d7f9a3b37d
|
fix crash bugs in sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-11 11:27:10 -08:00 |
|
Nikolaj Bjorner
|
a6da207b65
|
fix crash bugs in sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-11 11:25:43 -08:00 |
|
Nikolaj Bjorner
|
75b8d10f48
|
add backtrack level to cuber interface
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-08 21:44:21 -08:00 |
|
Nikolaj Bjorner
|
2746528aab
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-07 17:16:36 -08:00 |
|
Nikolaj Bjorner
|
9a4fb4ff76
|
remove ad-hoc parameters, deprecating dimacs cube mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-05 14:08:55 -08:00 |
|
Nikolaj Bjorner
|
70ee030228
|
updates to parallel tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-05 10:53:25 -08:00 |
|
Nikolaj Bjorner
|
fd49a0c89c
|
added facility to persist model transformations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-02 00:05:52 -05:00 |
|
Nikolaj Bjorner
|
caaf0ba33c
|
model-add/del
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-01 22:32:22 -05:00 |
|
Nikolaj Bjorner
|
829c140087
|
ensure that bca takes also lemmas into account
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-27 15:40:25 -07:00 |
|
Nikolaj Bjorner
|
0919fd4075
|
fix bca condition for tautology check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-25 16:46:22 -07:00 |
|
Nikolaj Bjorner
|
ee6cfb8eef
|
updates to simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-23 01:00:06 -04:00 |
|
Nikolaj Bjorner
|
76eed064eb
|
bug fixes, prepare for retaining blocked clauses
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-19 22:19:05 -07:00 |
|
Nikolaj Bjorner
|
9f9ae4427d
|
add cce
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-15 15:13:43 -07:00 |
|
Nikolaj Bjorner
|
c12439fe1e
|
fix #1306
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-13 07:29:16 -07:00 |
|
Nikolaj Bjorner
|
81ad69214c
|
fixing lookahead/ba + parallel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-11 17:06:28 -07:00 |
|
Nikolaj Bjorner
|
79ceaa1d13
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-11 13:17:57 -07:00 |
|
Nikolaj Bjorner
|
1a6f8c2fad
|
working on parallel solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-10 16:35:05 -07:00 |
|
Nikolaj Bjorner
|
f85c02600f
|
remove verificaiton code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-08 16:07:58 -07:00 |
|
Nikolaj Bjorner
|
10e4235b4c
|
bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-08 14:35:31 -07:00 |
|
Nikolaj Bjorner
|
d6327d69d2
|
bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-29 15:35:11 -07:00 |
|
Nikolaj Bjorner
|
e507a6ccd1
|
adding incremental cubing from API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-28 09:06:17 -07:00 |
|
Miguel Angelo Da Terra Neves
|
ff2cdc0e3f
|
local updates
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
|
2017-09-27 17:18:28 -07:00 |
|
Nikolaj Bjorner
|
a1e4fc3e98
|
fix new clause encoding
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-27 11:13:35 -07:00 |
|
Nikolaj Bjorner
|
82922d92f7
|
add cube functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-24 13:29:46 -07:00 |
|
Nikolaj Bjorner
|
ae9a6664d4
|
add cube mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-24 10:53:57 -07:00 |
|
Nikolaj Bjorner
|
9cd974e334
|
remove display
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-24 09:40:35 -07:00 |
|
Nikolaj Bjorner
|
2751cbc270
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-23 22:36:36 -05:00 |
|
Nikolaj Bjorner
|
cab4e4b461
|
add feature to display benchmark in format seen by SAT solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-21 18:32:46 -05:00 |
|
Nikolaj Bjorner
|
651587ce01
|
merge with master branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-19 09:39:22 -07:00 |
|
Nikolaj Bjorner
|
431d318958
|
experiments with ccc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-09-19 08:19:08 -07:00 |
|
Nikolaj Bjorner
|
b19f94ae5b
|
make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-31 13:24:11 -07:00 |
|
Nikolaj Bjorner
|
b482dbd589
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-27 17:02:27 -07:00 |
|
Christoph M. Wintersteiger
|
da34de340d
|
Fixed bug in sat model converter. Fixes #1148.
|
2017-07-15 20:25:13 +01:00 |
|
Nikolaj Bjorner
|
da263601e6
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-05 19:19:36 -07:00 |
|
Nikolaj Bjorner
|
b419a0e4a4
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-05 14:32:13 -07:00 |
|
Nikolaj Bjorner
|
5262248823
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-04 11:13:05 -07:00 |
|
Nikolaj Bjorner
|
9b631f982b
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-30 17:48:04 -07:00 |
|
Nikolaj Bjorner
|
bcf0ee7709
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-29 18:53:58 -07:00 |
|
Nikolaj Bjorner
|
7580644d15
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-29 08:11:27 -07:00 |
|
Nikolaj Bjorner
|
6fad478a18
|
reorg
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-28 17:46:29 -07:00 |
|
Nikolaj Bjorner
|
6f4c873b29
|
debugging
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-27 13:18:20 -07:00 |
|
Nikolaj Bjorner
|
66f0de6785
|
added in-processing features to card/pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-25 16:26:47 -07:00 |
|