Alan Mishchenko
|
f67c0c173d
|
Changes to the main SAT solver: fixing performance bug (resetting decay params after each restart), making the SAT solver platform- and runtime-independent (by using interger-based activity).
|
2011-12-09 23:49:30 -08:00 |
Alan Mishchenko
|
eb35f0ef65
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 01:05:18 -08:00 |
Alan Mishchenko
|
36a80c7579
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 00:38:49 -08:00 |
Alan Mishchenko
|
beb29257bf
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 00:38:16 -08:00 |
Alan Mishchenko
|
200c5cc659
|
Added support for generating a library of real-life truth-tables.
|
2011-12-09 00:37:05 -08:00 |
Alan Mishchenko
|
07405ca1c5
|
Integrated new proof-logging into proof-based gate-level abstraction.
|
2011-12-08 22:42:50 -08:00 |
Alan Mishchenko
|
b5c3992b6b
|
Proof-logging in the updated solver.
|
2011-12-08 19:43:08 -08:00 |
Alan Mishchenko
|
c985e17d1f
|
Proof-logging in the updated solver.
|
2011-12-08 15:06:26 -08:00 |
Alan Mishchenko
|
d1fa7f7a61
|
Proof-logging in the updated solver.
|
2011-12-07 22:26:50 -08:00 |
Alan Mishchenko
|
565fefec7a
|
Proof-logging in the updated solver.
|
2011-12-06 21:11:18 -08:00 |
Alan Mishchenko
|
35733eb1a1
|
Added/renamed useful APIs.
|
2011-12-06 21:10:58 -08:00 |
Alan Mishchenko
|
68baf03809
|
Another attempt to make CUDD platform- and runtime-independent.
|
2011-12-06 18:58:41 -08:00 |
Alan Mishchenko
|
780321cf54
|
Another attempt to make CUDD platform- and runtime-independent.
|
2011-12-06 17:48:31 -08:00 |
Alan Mishchenko
|
7cce97b4b3
|
Added new switch to the LUT matching code.
|
2011-12-06 16:50:04 -08:00 |
Alan Mishchenko
|
e84dcb7862
|
g++ portability changes.
|
2011-12-06 16:06:59 -08:00 |
Alan Mishchenko
|
ef37d14bc6
|
Added recording of AIG subgraphs.
|
2011-12-06 15:37:09 -08:00 |
Alan Mishchenko
|
f95e73c40b
|
Added recording of AIG subgraphs.
|
2011-12-06 14:29:32 -08:00 |
Alan Mishchenko
|
0f8b68aef8
|
Performance bug fix in SOP balancing.
|
2011-12-06 13:15:53 -08:00 |
Alan Mishchenko
|
360c705fc4
|
Added recording of AIG subgraphs.
|
2011-12-06 12:42:00 -08:00 |
Alan Mishchenko
|
b4a46eb688
|
Bug fixes in CUDD 2.4.2.
|
2011-12-06 07:39:55 -08:00 |
Alan Mishchenko
|
a24e678a79
|
Bug fixes in CUDD 2.4.2.
|
2011-12-06 07:32:17 -08:00 |
Alan Mishchenko
|
b743298cd5
|
Proof-logging in the updated solver.
|
2011-12-05 20:02:46 -08:00 |
Alan Mishchenko
|
df8b636169
|
Fixed performance bug in matching code.
|
2011-12-05 18:27:03 -08:00 |
Alan Mishchenko
|
72404d1fdf
|
Proof-logging in the updated solver.
|
2011-12-05 18:00:49 -08:00 |
Alan Mishchenko
|
bb96fa361c
|
Proof-logging in the updated solver.
|
2011-12-05 11:53:57 -08:00 |
Alan Mishchenko
|
7a19593d3f
|
Proof-logging in the updated solver.
|
2011-12-04 23:30:09 -08:00 |
Alan Mishchenko
|
f0d44a4a93
|
Proof-logging in the updated solver.
|
2011-12-04 22:58:24 -08:00 |
Alan Mishchenko
|
09d3e1ff77
|
Proof-logging in the updated solver.
|
2011-12-04 16:10:11 -08:00 |
Alan Mishchenko
|
a7031bb3f7
|
Removing redundant function declarations.
|
2011-12-02 10:11:39 -05:00 |
Alan Mishchenko
|
12869de14b
|
Previusly forgotten debug printout.
|
2011-12-02 01:08:48 -05:00 |
Alan Mishchenko
|
5161978d05
|
Started proof transformations.
|
2011-12-01 01:14:32 -05:00 |
Alan Mishchenko
|
1c16c45679
|
Started experiments with a new solver.
|
2011-11-27 16:28:57 -08:00 |
Alan Mishchenko
|
fc4ab6bd39
|
Started experiments with a new solver.
|
2011-11-26 18:17:39 -08:00 |
Alan Mishchenko
|
0cfc97b940
|
Started experiments with a new solver.
|
2011-11-26 11:54:01 -08:00 |
Alan Mishchenko
|
8ac9515d36
|
Started experiments with a new solver.
|
2011-11-26 11:37:27 -08:00 |
Alan Mishchenko
|
06416a981f
|
Started experiments with a new solver.
|
2011-11-26 11:33:37 -08:00 |
Alan Mishchenko
|
d2db956a61
|
Started experiments with a new solver.
|
2011-11-25 18:08:48 -08:00 |
Alan Mishchenko
|
0f594b78fa
|
Commented out the default call to UNSAT core verification.
|
2011-11-25 18:07:41 -08:00 |
Alan Mishchenko
|
9726d5a85e
|
Improvement to the SAT solver (skipping binary clauses).
|
2011-11-25 18:06:36 -08:00 |
Alan Mishchenko
|
7a0a4d4d79
|
Added a warning to Makefile about setting compilation flags when compiling on 32-bit Linux.
|
2011-11-24 14:25:47 -08:00 |
Alan Mishchenko
|
0a5d856cec
|
Making GLA PBA and GLA CBA communicate information.
|
2011-11-22 19:07:00 -08:00 |
Alan Mishchenko
|
ff938c7141
|
Modifications to the matching procedure
|
2011-11-22 18:48:03 -08:00 |
Alan Mishchenko
|
24408a483c
|
Bug fix in GLA PBA.
|
2011-11-13 00:17:00 -08:00 |
Alan Mishchenko
|
c7a7444211
|
Bug fix in GLA PBA.
|
2011-11-13 00:10:34 -08:00 |
Alan Mishchenko
|
21de666005
|
Bug fix in GLA PBA.
|
2011-11-13 00:01:16 -08:00 |
Alan Mishchenko
|
e43c0d8708
|
Setting the number of completed time frames.
|
2011-11-12 23:44:38 -08:00 |
Alan Mishchenko
|
b695e3334c
|
Setting the number of completed time frames.
|
2011-11-12 23:42:19 -08:00 |
Alan Mishchenko
|
30ea50a3b4
|
Temporary debugging change.
|
2011-11-12 23:21:41 -08:00 |
Alan Mishchenko
|
ca33481f1e
|
Temporary debugging change.
|
2011-11-12 23:10:08 -08:00 |
Alan Mishchenko
|
bf97e901d7
|
Temporary debugging change.
|
2011-11-12 23:07:19 -08:00 |