Alan Mishchenko
|
4cbc97a464
|
Compiler warnings.
|
2017-09-07 19:57:29 -07:00 |
Alan Mishchenko
|
8a11c911ab
|
Compiler warnings.
|
2017-09-07 19:54:12 -07:00 |
Alan Mishchenko
|
7ce7e9ec31
|
Compiler warnings.
|
2017-09-07 19:45:02 -07:00 |
Alan Mishchenko
|
af4c76e21a
|
Disabling CNF simplification in &bmcs -g.
|
2017-09-07 19:37:46 -07:00 |
Alan Mishchenko
|
ba0d855fd4
|
Trying to enable CNF simplification in &bmcs -g.
|
2017-09-07 19:16:13 -07:00 |
Alan Mishchenko
|
68b59b8a1e
|
Bug fix: forgot to init the runtime limit in Glucose.
|
2017-09-06 20:55:16 -07:00 |
Alan Mishchenko
|
3ffb098d64
|
Adding global conflict counter to Satoko (to make it apple-to-apple with other solvers).
|
2017-09-06 20:33:53 -07:00 |
Alan Mishchenko
|
97dd6019bf
|
Integrating Glucose into bmc3 -g.
|
2017-09-06 19:56:53 -07:00 |
Alan Mishchenko
|
b1bf802fda
|
More renaming.
|
2017-09-06 18:46:12 -07:00 |
Alan Mishchenko
|
bd6d95fa2c
|
Renaming Glucose namespace to avoid collisions with external solvers.
|
2017-09-06 18:43:15 -07:00 |
Alan Mishchenko
|
f68bd519c6
|
Integrating Glucose into &bmcs -g.
|
2017-09-06 17:57:44 -07:00 |
Alan Mishchenko
|
8063887ffe
|
Compiler warning.
|
2017-09-06 16:40:38 -07:00 |
Alan Mishchenko
|
16a9c21c80
|
Adding Glucose 3.0 as a separate package.
|
2017-09-06 16:36:54 -07:00 |
Alan Mishchenko
|
1ca80e1f6c
|
Adding Glucose 3.0 as a separate package.
|
2017-09-06 16:32:15 -07:00 |
Alan Mishchenko
|
9e0184c11e
|
Adding Glucose 3.0 as a separate package.
|
2017-09-06 16:31:24 -07:00 |
Alan Mishchenko
|
9e46ebe3f8
|
Adding Glucose 3.0 as a separate package.
|
2017-09-06 16:28:00 -07:00 |
Alan Mishchenko
|
7857b7fd8b
|
Renaming command-line option '-s' to be '-q' in 'pdr'.
|
2017-09-06 08:39:23 -07:00 |
Alan Mishchenko
|
be49b0fa18
|
Changes to 'pdr' to run with updated Satoko.
|
2017-09-06 08:34:58 -07:00 |
Alan Mishchenko
|
f06056d85d
|
Changes to 'pdr' to run with updated Satoko.
|
2017-09-06 08:34:04 -07:00 |
Alan Mishchenko
|
0fa4c86899
|
Small bug in a recently added Satoko API.
|
2017-09-06 08:33:34 -07:00 |
Alan Mishchenko
|
4b286febe0
|
Several small changes.
|
2017-09-06 07:29:12 -07:00 |
Alan Mishchenko
|
5a9fded57f
|
Several small changes.
|
2017-09-05 21:54:27 -07:00 |
Alan Mishchenko
|
c1c6e90d3e
|
Useful AIG duplication procedure.
|
2017-09-05 20:17:21 -07:00 |
Alan Mishchenko
|
ecae67e3bf
|
Several changes to various packages.
|
2017-09-04 15:57:00 -07:00 |
Alan Mishchenko
|
2f95a58c01
|
Fixed a memory leak in 'fxch'.
|
2017-09-03 13:08:10 -07:00 |
Alan Mishchenko
|
5e2bfe36ff
|
Adding minimize_assumptions to Satoko.
|
2017-09-03 08:07:28 -07:00 |
Alan Mishchenko
|
1d44f42039
|
Change in Satoko to make assumption var values appear in satisfiable assignments produced.
|
2017-09-03 07:28:04 -07:00 |
Alan Mishchenko
|
f991498890
|
Improvements to minimize_assumptions.
|
2017-09-03 07:25:58 -07:00 |
Alan Mishchenko
|
f77af1a44d
|
Corner-case sitution in truth-table computation.
|
2017-08-30 13:43:25 +08:00 |
Alan Mishchenko
|
a321d4cb4d
|
Small changes to printouts in &bmcs.
|
2017-08-30 11:57:45 +08:00 |
Alan Mishchenko
|
d103c4e286
|
Small changes to printouts in &bmcs.
|
2017-08-30 11:39:21 +08:00 |
Bruno Schmitt
|
ba8112ff3a
|
Fixing bronken C++ build; Satoko internal header, solver.h, should not be used in other packages
|
2017-08-29 09:40:51 +02:00 |
Bruno Schmitt
|
d0f81fcf29
|
[Satoko] Small fix.
|
2017-08-28 11:15:00 +02:00 |
Bruno Schmitt
|
3df049f37d
|
[Satoko] Correcting bug found when integrating with pdr.
The head of the propagation queue was not begin properly reset.
Adding some debugging functions.
|
2017-08-28 10:59:30 +02:00 |
Alan Mishchenko
|
d80bbe7400
|
Adding runtime profile to &bmcs.
|
2017-08-16 15:46:02 +07:00 |
Alan Mishchenko
|
efa9654634
|
Bug fix in &bmcs.
|
2017-08-16 15:20:34 +07:00 |
Alan Mishchenko
|
7365052411
|
Adding an option to bmc3 to use Satoko intead of the default SAT solver.
|
2017-08-16 15:02:47 +07:00 |
Alan Mishchenko
|
85eee2ea96
|
Bug fix in &bmcs.
|
2017-08-16 14:59:36 +07:00 |
Alan Mishchenko
|
e6dd7cb5ff
|
Bug fix in &bmcs.
|
2017-08-16 14:51:43 +07:00 |
Alan Mishchenko
|
c5131ca85f
|
Changing enconding of the SAT solver return value in &bmcs.
|
2017-08-16 14:41:36 +07:00 |
Alan Mishchenko
|
23d36a8d56
|
Integrating Satoko into 'bmc' and 'bmc2'.
|
2017-08-16 14:20:52 +07:00 |
Alan Mishchenko
|
d2747fb281
|
Adding an option to bmc3 to use Satoko intead of the default SAT solver.
|
2017-08-16 13:18:26 +07:00 |
Alan Mishchenko
|
29cb71f98b
|
Integrating Satoko into pdr.
|
2017-08-16 12:08:55 +07:00 |
Alan Mishchenko
|
6ff66ed49e
|
Changing enconding of the SAT solver return value in &bmcs.
|
2017-08-16 11:55:10 +07:00 |
Alan Mishchenko
|
443776fed7
|
Additional changes to Satoko to enable various integrations.
|
2017-08-16 11:54:14 +07:00 |
Alan Mishchenko
|
2280c2e8fe
|
Trying &bmcs with external solvers.
|
2017-08-15 18:13:31 +07:00 |
Alan Mishchenko
|
2a0289f97b
|
Trying &bmcs with external solvers.
|
2017-08-15 17:07:31 +07:00 |
Alan Mishchenko
|
7747f21fe6
|
Added several helpful APIs to Satoko.
|
2017-08-15 17:07:12 +07:00 |
Alan Mishchenko
|
ca87c1a6a0
|
Unfold several timeframes at the same time in &bmcs.
|
2017-08-15 11:36:15 +07:00 |
Alan Mishchenko
|
1f5ab6d751
|
Bug fix in &bmcs.
|
2017-08-15 10:16:17 +07:00 |