Alan Mishchenko
|
f1dba69c57
|
Improved memory management of proof-logging and propagated changes.
|
2012-02-16 14:23:52 -08:00 |
Alan Mishchenko
|
59ea100dbf
|
Variable timeframe abstraction.
|
2012-02-13 20:40:38 -08:00 |
Alan Mishchenko
|
d931de7feb
|
Variable timeframe abstraction.
|
2012-02-13 20:03:55 -08:00 |
Alan Mishchenko
|
6f4bb33ce1
|
Variable timeframe abstraction.
|
2012-02-13 14:35:00 -08:00 |
Alan Mishchenko
|
f80841a5fd
|
Variable timeframe abstraction.
|
2012-02-13 14:17:01 -08:00 |
Alan Mishchenko
|
d9edb7e549
|
Variable timeframe abstraction.
|
2012-02-12 02:16:36 -08:00 |
Alan Mishchenko
|
309ab1c12b
|
Variable timeframe abstraction.
|
2012-02-11 20:48:23 -08:00 |
Alan Mishchenko
|
a2df331852
|
Variable timeframe abstraction.
|
2012-01-28 13:48:48 -08:00 |
Alan Mishchenko
|
ce0e8caf79
|
Variable timeframe abstraction.
|
2012-01-27 00:48:06 -08:00 |
Alan Mishchenko
|
c7e855619a
|
Variable timeframe abstraction.
|
2012-01-24 14:39:49 -08:00 |
Alan Mishchenko
|
94d35a2592
|
Variable timeframe abstraction.
|
2012-01-24 01:04:56 -08:00 |
Alan Mishchenko
|
fb918249ca
|
Variable timeframe abstraction.
|
2012-01-21 22:57:18 -08:00 |
Alan Mishchenko
|
8014f25f6d
|
Major restructuring of the code.
|
2012-01-21 04:30:10 -08:00 |
Alan Mishchenko
|
719b06f912
|
Variable timeframe abstraction.
|
2012-01-20 17:55:34 -08:00 |
Alan Mishchenko
|
37b8a190ba
|
Improving printout in the SAT solver.
|
2012-01-13 20:57:26 -08:00 |
Alan Mishchenko
|
56cc5734a4
|
Bug fix related to not properly resizing SAT solver's model array.
|
2012-01-12 07:28:01 -08:00 |
Alan Mishchenko
|
10ad89490a
|
Bug fix related to not properly resizing SAT solver's model array.
|
2012-01-06 11:34:06 +07:00 |
Alan Mishchenko
|
5a45a75dca
|
APIs to represent simple gates in CNF.
|
2012-01-05 19:19:13 +07:00 |
Alan Mishchenko
|
32e7b75829
|
APIs to represent simple gates in CNF.
|
2012-01-05 13:15:05 +07:00 |
Alan Mishchenko
|
c59e2e9c96
|
Transforming the solver to use different clause representation.
|
2011-12-23 21:45:23 -08:00 |
Alan Mishchenko
|
7facbc3cc9
|
Transforming the solver to use different clause representation.
|
2011-12-23 10:23:45 -08:00 |
Alan Mishchenko
|
94174d0f04
|
Transforming the solver to use different clause representation.
|
2011-12-23 00:43:31 -08:00 |
Alan Mishchenko
|
9d2893040e
|
Transforming the solver to use different clause representation.
|
2011-12-23 00:29:26 -08:00 |
Alan Mishchenko
|
844c385e2b
|
Transforming the solver to use different clause representation.
|
2011-12-22 15:38:06 -08:00 |
Alan Mishchenko
|
d0da3a8258
|
Computing interpolants as truth tables.
|
2011-12-22 14:26:47 -08:00 |
Alan Mishchenko
|
8404ecda54
|
Undoing temporary change to the solver.
|
2011-12-15 17:05:38 -08:00 |
Alan Mishchenko
|
4d000265f6
|
Temporary change to the solver.
|
2011-12-15 16:47:28 -08:00 |
Alan Mishchenko
|
bc2f199bd3
|
Started SAT-based reparameterization.
|
2011-12-13 23:38:41 -08:00 |
Alan Mishchenko
|
c2a1a9ef37
|
Implementing rollback in the updated solver.
|
2011-12-10 14:55:33 -08:00 |
Alan Mishchenko
|
a2228ee09b
|
Implementing rollback in the updated solver.
|
2011-12-10 14:45:35 -08:00 |
Alan Mishchenko
|
871171ffa4
|
Implemented rollback in the main SAT solver and updated PDR to use it (saves about 5% of runtime).
|
2011-12-10 14:06:01 -08:00 |
Alan Mishchenko
|
6c766b4f1a
|
Implementing rollback in the updated solver.
|
2011-12-10 13:11:28 -08:00 |
Alan Mishchenko
|
dea5708d4e
|
Removing unused files.
|
2011-12-10 11:30:29 -08:00 |
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
|
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
|
e84dcb7862
|
g++ portability changes.
|
2011-12-06 16:06:59 -08:00 |
Alan Mishchenko
|
b743298cd5
|
Proof-logging in the updated solver.
|
2011-12-05 20:02:46 -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
|
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 |