Alan Mishchenko
|
4507a5d3ed
|
Correcting the report of completed timeframes in &gla.
|
2012-09-04 14:19:19 -07:00 |
Alan Mishchenko
|
b08aca5c1e
|
Make switches -d (-m) by default dump abstracted model (miter with abstraction map) into files whose names are derived from the names of the input file by adding _abs (_gla).
|
2012-09-04 14:09:39 -07:00 |
Alan Mishchenko
|
05f51cbb2a
|
Enabled recording the name of the file GIA is coming from.
|
2012-09-04 13:52:42 -07:00 |
Alan Mishchenko
|
b9ed304236
|
Correcting the report of completed timeframes in &gla.
|
2012-09-04 13:38:52 -07:00 |
Alan Mishchenko
|
b26d698ff8
|
Uniqifying status file name in &gla.
|
2012-09-03 19:06:01 -07:00 |
Alan Mishchenko
|
201cb24596
|
Several minor changes.
|
2012-09-03 17:15:44 -07:00 |
Alan Mishchenko
|
fe1a16e9b4
|
Changes to allow &gla to run with fSimple = 1 (useful for debugging).
|
2012-08-31 18:45:10 -07:00 |
Alan Mishchenko
|
e63c603e92
|
Fixing assert which failes when SAT solver returns after a timeout.
|
2012-08-31 00:52:08 -07:00 |
Alan Mishchenko
|
329831bdac
|
Bug fix: abstraction commands not properly updating status when dumping intermediate abstraction.
|
2012-08-28 12:12:24 -07:00 |
Alan Mishchenko
|
c25f5dee05
|
Bug fix in &gla.
|
2012-08-27 13:49:53 -07:00 |
Alan Mishchenko
|
137f0347f0
|
Added switch '&gla -m' to dump original miter with the abstraction map.
|
2012-08-26 09:21:45 -07:00 |
Alan Mishchenko
|
5da7102f55
|
Fixing undesirable effect of recent refinement code on older code in &gla -n.
|
2012-08-11 11:47:22 -07:00 |
Alan Mishchenko
|
528c8e0bba
|
Enabling -S <num> for &gla to not check the first <num> frames.
|
2012-08-10 23:56:46 -07:00 |
Alan Mishchenko
|
d22b3d055b
|
Fixing problem with max limit on the number of abstracted objects in &gla.
|
2012-08-10 11:16:23 -07:00 |
Alan Mishchenko
|
65b652fadb
|
Added purification of UNSAT core in &gla.
|
2012-08-10 09:31:03 -07:00 |
Alan Mishchenko
|
409ce39b61
|
Improved abstraction refinement.
|
2012-08-09 19:44:40 -07:00 |
Alan Mishchenko
|
a019dd216e
|
Improved abstraction refinement.
|
2012-08-09 19:16:25 -07:00 |
Alan Mishchenko
|
8ad4a10fae
|
Compiler warnings.
|
2012-08-09 18:07:00 -07:00 |
Alan Mishchenko
|
5b80d704a1
|
Improved abstraction refinement.
|
2012-08-09 17:53:38 -07:00 |
Alan Mishchenko
|
bf35ed1b86
|
New cut-based refinement.
|
2012-08-08 12:33:48 -07:00 |
Alan Mishchenko
|
ca75e118e7
|
Added generation of values of internal nodes for GIA manager.
|
2012-08-08 11:47:06 -07:00 |
Alan Mishchenko
|
a8e59b2c42
|
Added generation of values of internal nodes for GIA manager.
|
2012-08-08 09:43:57 -07:00 |
Alan Mishchenko
|
094bdc0572
|
New command 'testnpn' to compare semi-canonical forms.
|
2012-08-08 01:41:42 -07:00 |
Alan Mishchenko
|
f9b032ee02
|
Scalable gate-level abstraction.
|
2012-08-07 11:46:50 -07:00 |
Alan Mishchenko
|
c35471dac4
|
Scalable gate-level abstraction.
|
2012-08-07 10:43:01 -07:00 |
Alan Mishchenko
|
173303b464
|
Scalable gate-level abstraction.
|
2012-08-06 22:03:35 -07:00 |
Alan Mishchenko
|
8e31b4c047
|
Scalable gate-level abstraction.
|
2012-08-06 22:02:50 -07:00 |
Alan Mishchenko
|
b3dd1f82f1
|
New cut-based refinement.
|
2012-08-06 21:59:50 -07:00 |
Alan Mishchenko
|
ca9803fc98
|
Scalable gate-level abstraction.
|
2012-08-06 21:59:14 -07:00 |
Alan Mishchenko
|
1917321c4e
|
Scalable gate-level abstraction.
|
2012-08-06 09:58:34 -07:00 |
Alan Mishchenko
|
294c06f162
|
Scalable gate-level abstraction.
|
2012-08-04 09:37:49 -07:00 |
Alan Mishchenko
|
a01b479013
|
Scalable gate-level abstraction.
|
2012-08-03 21:44:00 -07:00 |
Alan Mishchenko
|
5760c3225d
|
Scalable gate-level abstraction.
|
2012-08-03 18:31:16 -07:00 |
Alan Mishchenko
|
30ae05f0a5
|
Scalable gate-level abstraction.
|
2012-08-03 18:25:47 -07:00 |
Alan Mishchenko
|
e9af6c3cec
|
Scalable gate-level abstraction.
|
2012-08-02 23:44:48 -07:00 |
Alan Mishchenko
|
cb66aa429d
|
Scalable gate-level abstraction.
|
2012-08-02 10:54:21 -07:00 |
Alan Mishchenko
|
b939e16006
|
Scalable gate-level abstraction.
|
2012-08-02 09:44:48 -07:00 |
Alan Mishchenko
|
352060122b
|
Scalable gate-level abstraction.
|
2012-08-02 09:40:19 -07:00 |
Alan Mishchenko
|
fe93162114
|
Scalable gate-level abstraction.
|
2012-08-02 01:05:14 -07:00 |
Alan Mishchenko
|
8822e811ca
|
Scalable gate-level abstraction.
|
2012-08-02 00:29:57 -07:00 |
Alan Mishchenko
|
68c70bcb8e
|
Scalable gate-level abstraction.
|
2012-08-01 13:46:46 -07:00 |
Alan Mishchenko
|
99e8ef14cb
|
Scalable gate-level abstraction.
|
2012-08-01 13:43:33 -07:00 |
Alan Mishchenko
|
e7ddde3f5a
|
Scalable gate-level abstraction.
|
2012-08-01 08:59:02 -07:00 |
Alan Mishchenko
|
e3e4a98792
|
Scalable gate-level abstraction.
|
2012-07-31 21:18:39 -07:00 |
Alan Mishchenko
|
dc56a65582
|
Scalable gate-level abstraction.
|
2012-07-31 14:51:48 -07:00 |
Alan Mishchenko
|
7517c78522
|
Scalable gate-level abstraction.
|
2012-07-31 12:02:06 -07:00 |
Alan Mishchenko
|
a457cf496a
|
Scalable gate-level abstraction.
|
2012-07-31 10:36:03 -07:00 |
Alan Mishchenko
|
b20ca62e00
|
Scalable gate-level abstraction.
|
2012-07-31 00:00:34 -07:00 |
Alan Mishchenko
|
ed564664f1
|
Disabling learned clause removal when incremental proof-logging is running (tends to generate smaller abstarctions).
|
2012-07-30 11:31:26 -07:00 |
Alan Mishchenko
|
cd39fd6b05
|
Fixing performance bug with old proof-logging (adding clauses multiple times).
|
2012-07-30 11:05:54 -07:00 |