Alan Mishchenko
|
8a91a9afe8
|
Experiments with mini AIG manager.
|
2012-09-29 19:44:45 -04:00 |
Alan Mishchenko
|
71bdfae941
|
Replacing 'st_table' by 'st__table' to resolve linker problems.
|
2012-09-29 17:11:03 -04:00 |
Alan Mishchenko
|
255f171f63
|
Improving computation of choices from equivalence classes.
|
2012-09-23 23:53:12 -07:00 |
Alan Mishchenko
|
40d9b5853b
|
Testing GIA with time manager.
|
2012-09-23 18:34:10 -07:00 |
Alan Mishchenko
|
f7caf84f21
|
Modified structural constraint extraction (unfold -s) to work for multi-output testcases.
|
2012-09-23 14:30:17 -07:00 |
Alan Mishchenko
|
6e774ef541
|
Cleaing AIG manager by removing pointers to HAIG.
|
2012-09-23 12:01:59 -07:00 |
Alan Mishchenko
|
a50a38155c
|
Integrating time manager into choice computation.
|
2012-09-22 17:57:06 -07:00 |
Alan Mishchenko
|
26f3427a1e
|
Added GIA normalization using timing manager.
|
2012-09-22 00:06:09 -07:00 |
Alan Mishchenko
|
fdd043ca34
|
Upgrading hierarchy timing manager.
|
2012-09-21 22:00:39 -07:00 |
Alan Mishchenko
|
6dc3a0a246
|
Bug fix in bmc3.
|
2012-09-17 17:39:42 -07:00 |
Alan Mishchenko
|
819b41bb59
|
Fixed timeout problem in bmc3 -s.
|
2012-09-17 09:54:45 -07:00 |
Alan Mishchenko
|
69bbfa9856
|
Created new abstraction package from the code that was all over the place.
|
2012-09-15 23:27:46 -07:00 |
Alan Mishchenko
|
ec95f569dd
|
Corrected &gla -a to work as expected.
|
2012-09-15 21:18:32 -07:00 |
Alan Mishchenko
|
152aaedcb2
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 22:45:51 -07:00 |
Alan Mishchenko
|
080c325500
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 21:22:31 -07:00 |
Alan Mishchenko
|
117bc0dbcd
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 21:20:37 -07:00 |
Alan Mishchenko
|
f64bb36fd5
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:33:23 -07:00 |
Alan Mishchenko
|
3b14c7b490
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 13:31:29 -07:00 |
Alan Mishchenko
|
19c28cae94
|
Prepared &gla to try abstracting and proving concurrently.
|
2012-09-14 10:27:48 -07:00 |
Alan Mishchenko
|
606341dca6
|
Added code to collect experimental results.
|
2012-09-11 22:36:38 -07:00 |
Alan Mishchenko
|
e95844c0af
|
Added code to collect experimental results.
|
2012-09-11 22:35:27 -07:00 |
Alan Mishchenko
|
087ec9eb1f
|
Added code to collect experimental results.
|
2012-09-11 22:34:49 -07:00 |
Alan Mishchenko
|
825bcd823c
|
Added code to collect experimental results.
|
2012-09-11 22:33:47 -07:00 |
Alan Mishchenko
|
759b7c0855
|
Added code to collect experimental results.
|
2012-09-11 16:26:01 -07:00 |
Alan Mishchenko
|
d257fce824
|
Added code to collect experimental results.
|
2012-09-11 16:25:00 -07:00 |
Alan Mishchenko
|
d40af538e2
|
Unified print-out of property failures produced by all engines.
|
2012-09-09 20:46:34 -07:00 |
Alan Mishchenko
|
71d7c9e66d
|
Disable printing refinement statistics by default.
|
2012-09-09 20:25:55 -07:00 |
Alan Mishchenko
|
56117d56e8
|
Added switch '-p' to '&gla -n' to use full proof for UNSAT core computation (for experiments).
|
2012-09-09 15:28:31 -07:00 |
Alan Mishchenko
|
4333fd24d2
|
Started CEX minimization procedure.
|
2012-09-08 18:28:13 -07:00 |
Alan Mishchenko
|
9efe9579f9
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 15:04:44 -07:00 |
Alan Mishchenko
|
519b9fdf7c
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 15:04:00 -07:00 |
Alan Mishchenko
|
002117c0e9
|
Started CEX minimization procedure.
|
2012-09-08 14:56:25 -07:00 |
Alan Mishchenko
|
cc6da1f905
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 00:19:46 -07:00 |
Alan Mishchenko
|
e1b76633dc
|
Updating &gla_refine to perform suffix refinement.
|
2012-09-08 00:14:49 -07:00 |
Alan Mishchenko
|
5ca4f3cf9f
|
Updating &gla_refine to perform suffic refinement.
|
2012-09-07 23:26:23 -07:00 |
Alan Mishchenko
|
548e04192b
|
Updating &gla_refine to perform suffic refinement.
|
2012-09-07 20:44:12 -07:00 |
Alan Mishchenko
|
9c8be56ccd
|
Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.
|
2012-09-06 15:32:07 -07:00 |
Alan Mishchenko
|
c1f4545e07
|
Added error message when the user is trying 'dsat' for multi-output comb miters.
|
2012-09-05 18:53:21 -07:00 |
Alan Mishchenko
|
9cb16d654a
|
Added new command &gla_shrink.
|
2012-09-05 00:55:33 -07:00 |
Alan Mishchenko
|
f6b67d7846
|
Added new command &gla_shrink.
|
2012-09-04 23:57:58 -07:00 |
Alan Mishchenko
|
2071d9a732
|
Enabling additinal printouts.
|
2012-09-04 21:14:47 -07:00 |
Alan Mishchenko
|
acc3abe9cc
|
Correcting the report of completed timeframes in &gla.
|
2012-09-04 14:22:06 -07:00 |
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 |