Commit Graph

711 Commits

Author SHA1 Message Date
Alan Mishchenko 9f71a9f67b Isomorphism checking code. 2012-02-20 16:09:20 -08:00
Alan Mishchenko 2377ae60e9 Isomorphism checking code. 2012-02-19 14:52:43 -08:00
Alan Mishchenko ea13085fe3 Added printout of BMC tents in &ps. 2012-02-19 13:33:21 -08:00
Alan Mishchenko c9147d76cc Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity). 2012-02-19 09:55:52 -08:00
Alan Mishchenko 7ca9c116df Isomorphism checking code. 2012-02-18 19:20:02 -08:00
Alan Mishchenko 5d7c568589 Changes to properly save current GIA after &miter -t and not erase the comb cex after &put. 2012-02-17 15:51:12 -08:00
Alan Mishchenko ee9f66e2c4 Isomorphism checking code. 2012-02-17 13:19:09 -08:00
Alan Mishchenko f2a413029c Silencing some of the gcc warnings. 2012-02-17 12:46:08 -08:00
Alan Mishchenko 97856d021a Silencing some of the gcc warnings. 2012-02-16 23:40:23 -08:00
Alan Mishchenko 791b107e7a Silencing some of the gcc warnings. 2012-02-16 21:53:16 -08:00
Alan Mishchenko 8587ebe797 Variable timeframe abstraction. 2012-02-16 00:11:09 -08:00
Alan Mishchenko a9980135a0 Isomorphism checking code. 2012-02-14 22:15:49 -08:00
Alan Mishchenko 77b5dc261e Added restarts to PDR. 2012-02-13 23:31:01 -08:00
Alan Mishchenko d0713831a0 Lazy man's logic synthesis. 2012-02-12 17:30:05 -08:00
Alan Mishchenko d9edb7e549 Variable timeframe abstraction. 2012-02-12 02:16:36 -08:00
Alan Mishchenko 862ebb214d Variable timeframe abstraction. 2012-02-11 22:54:59 -08:00
Alan Mishchenko 49c5beefd4 Variable timeframe abstraction. 2012-02-11 22:30:04 -08:00
Alan Mishchenko 95d7b478fd Variable timeframe abstraction. 2012-02-11 21:56:05 -08:00
Alan Mishchenko 112f797c73 Added switch -f to 'print_io' to suppress printing flops. 2012-02-11 00:43:37 -08:00
Alan Mishchenko c5067f7d04 Graph isomorphism checking code. 2012-02-11 00:22:05 -08:00
Alan Mishchenko 71891354b4 Bug fixes in &cec command. 2012-02-10 00:07:31 -08:00
Alan Mishchenko 25859eefb6 Graph isomorphism checking code. 2012-02-02 15:45:48 -08:00
Alan Mishchenko 61211df4ff Lazy man's logic synthesis. 2012-02-01 12:24:04 -08:00
Alan Mishchenko 044149593d Graph isomorphism checking code. 2012-01-30 23:11:38 -08:00
Alan Mishchenko 7ea40494eb Graph isomorphism checking code. 2012-01-29 21:22:54 -08:00
Alan Mishchenko e511b87237 Moving Vec_IntPrint to where it belongs. 2012-01-29 21:22:26 -08:00
Alan Mishchenko 99b408fcb1 Generation of dual-rail miter. 2012-01-28 20:10:34 -08:00
Alan Mishchenko 5aeab257ed Generation of dual-rail miter. 2012-01-28 15:05:33 -08:00
Alan Mishchenko 7a87f20c18 Variable timeframe abstraction. 2012-01-27 00:57:42 -08:00
Alan Mishchenko ce0e8caf79 Variable timeframe abstraction. 2012-01-27 00:48:06 -08:00
Alan Mishchenko 94d35a2592 Variable timeframe abstraction. 2012-01-24 01:04:56 -08:00
Alan Mishchenko f8e933c718 Variable timeframe abstraction. 2012-01-23 13:45:46 -08:00
Alan Mishchenko c39fd3741a Added returning counter-example after BMC, which was recently added to 'dprove'. 2012-01-23 12:41:55 -08:00
Alan Mishchenko 8014f25f6d Major restructuring of the code. 2012-01-21 04:30:10 -08:00
Alan Mishchenko c44cc5de94 Deleting file added by mistake. 2012-01-20 20:30:24 -08:00
Alan Mishchenko 2c50c2c5c0 Preserving CI/CO varible names when moving between the main space and &-space. 2012-01-20 19:54:26 -08:00
Alan Mishchenko 7d4545126d Variable timeframe abstraction. 2012-01-20 19:04:01 -08:00
Alan Mishchenko b9163754b7 New hierarchy manager. 2012-01-20 09:52:38 -08:00
Alan Mishchenko ec1c45fb64 New hierarchy manager. 2012-01-19 21:09:49 -08:00
Alan Mishchenko 215d62f41f New hierarchy manager. 2012-01-19 17:18:11 -08:00
Alan Mishchenko fffd733f94 Replaced 'bmc' by 'bmc2' in 'dprove'. Added switches to 'dprove' to control BMC frames and conflicts. 2012-01-19 14:24:56 -08:00
Alan Mishchenko 0111d43b54 New hierarchy manager. 2012-01-19 12:02:07 -08:00
Alan Mishchenko 8c62c9db6c Added switch 'write_counter -f' to output flop values in each time frame. 2012-01-18 17:49:13 -08:00
Alan Mishchenko debe445063 New hierarchy manager. 2012-01-18 17:28:59 -08:00
Alan Mishchenko fe6d1ff7da New hierarchy manager. 2012-01-18 02:25:12 -08:00
Alan Mishchenko 2a236864ab Changes to the lazy man's synthesis code. 2012-01-17 23:38:11 -08:00
Alan Mishchenko d8d705c717 New hierarchy manager. 2012-01-17 23:19:47 -08:00
Alan Mishchenko 6bff2986a2 New hierarchy manager. 2012-01-17 15:02:25 -08:00
Alan Mishchenko be5256c926 New hierarchy manager. 2012-01-16 22:06:59 -08:00
Alan Mishchenko 0695ec5473 New hierarchy manager plus additional printout in the GIA package. 2012-01-16 13:07:51 -08:00
Alan Mishchenko ca28f77f3a Variable timeframe abstraction. 2012-01-16 12:21:53 -08:00
Alan Mishchenko 10478a9cbf Variable timeframe abstraction. 2012-01-15 20:47:58 -08:00
Alan Mishchenko bb4897aba6 Changes to the lazy man's synthesis code. 2012-01-15 12:35:04 -08:00
Alan Mishchenko 1f0e5533dc Several small bug fixes in the mapper. 2012-01-15 09:15:10 -08:00
Alan Mishchenko 60a84f7350 Changes to the lazy man's synthesis code. 2012-01-14 23:39:53 -08:00
Alan Mishchenko 868ed19469 Changes to the lazy man's synthesis code. 2012-01-14 22:37:25 -08:00
Alan Mishchenko ac7e665bf6 Bug fixes in the Verilog parser. 2012-01-14 22:21:23 -08:00
Alan Mishchenko c7e215ca31 New hierarchy manager. 2012-01-14 18:05:12 -08:00
Alan Mishchenko 9c409addca Support computation experiments with different network data-structures. 2012-01-14 18:04:47 -08:00
Alan Mishchenko 7a3c33e169 New hierarchy manager. 2012-01-13 22:49:08 -08:00
Alan Mishchenko 5fff8354ce New hierarchy manager. 2012-01-13 22:02:04 -08:00
Alan Mishchenko b7ba9aa8dc New hierarchy manager. 2012-01-13 20:58:28 -08:00
Alan Mishchenko 4bd7efa6cd Added counting hits and misses during structural hashing. 2012-01-13 19:31:13 -08:00
Alan Mishchenko edbff75fff New hierarchy manager. 2012-01-13 18:10:00 -08:00
Alan Mishchenko eecbbea24b New hierarchy manager. 2012-01-13 17:50:21 -08:00
Alan Mishchenko 095345fc4a Added new name manager and modified hierarchy manager to use it. 2012-01-13 15:43:09 -08:00
Alan Mishchenko cb2d12bb04 New hierarchy manager. 2012-01-13 00:34:13 -08:00
Alan Mishchenko 2e1dcdd239 Added model ID inside the design. 2012-01-12 23:29:47 -08:00
Alan Mishchenko fadde52dc6 Changes to the lazy man's synthesis code. 2012-01-11 22:08:35 -08:00
Alan Mishchenko 564a3553f0 Gate level abstraction. 2012-01-08 13:15:03 +07:00
Alan Mishchenko 376bf3a703 Bug fix: changing output number to 0 in the CEX after ORing POs. 2012-01-07 11:19:03 +07:00
Alan Mishchenko 26b87c8c55 Added warning when the network from file has no primary inputs. 2012-01-06 01:36:08 +07:00
Alan Mishchenko aec5d33889 Backward reachability using circuit cofactoring. 2012-01-01 15:58:17 +07:00
Alan Mishchenko 1e20e2ccbc Delay optimization using precomputed library. 2011-12-30 13:11:52 +07:00
Alan Mishchenko 655d452cbb Delay optimization using precomputed library. 2011-12-30 11:36:25 +07:00
Alan Mishchenko 6ed8340226 Delay optimization using precomputed library. 2011-12-30 11:27:12 +07:00
Alan Mishchenko 64b8aa51e9 Delay optimization using precomputed library. 2011-12-30 09:54:30 +07:00
Alan Mishchenko 6c19c1dfed Delay optimization using precomputed library. 2011-12-29 21:14:01 +07:00
Alan Mishchenko ed13bd16fd New variable-time frame abstraction. 2011-12-29 10:13:25 +07:00
Alan Mishchenko 21df8bf021 Experiments with flattening hierarchy. 2011-12-28 22:16:04 +07:00
Alan Mishchenko 1c51d9577d Added switch -n to 'miter' to ignore PI/PO names. 2011-12-22 14:55:10 -08:00
Alan Mishchenko d0da3a8258 Computing interpolants as truth tables. 2011-12-22 14:26:47 -08:00
Alan Mishchenko 82a2495ce9 Improvements to hierarchical BLIF parser. 2011-12-22 14:26:03 -08:00
Alan Mishchenko b3c9609e82 Improvements to hierarchical BLIF parser. 2011-12-21 12:56:28 -08:00
Alan Mishchenko 3418a8820a Fixed a bug in matching code. 2011-12-17 17:51:13 -08:00
Alan Mishchenko f67cb76dff Added optional printout of the hierarchy structure before collapsing. 2011-12-15 19:32:05 -08:00
Alan Mishchenko 2bb95a97d0 Adding switch '-W' to fx to control the quality of extracted divisors. 2011-12-15 15:44:56 -08:00
Alan Mishchenko b63b332bac Trying to make sorting of nodes platform-indendent. 2011-12-15 12:42:42 -08:00
Alan Mishchenko 40ddda3edd Trying to make sorting of nodes platform-indendent. 2011-12-15 12:27:35 -08:00
Alan Mishchenko bc2f199bd3 Started SAT-based reparameterization. 2011-12-13 23:38:41 -08:00
Alan Mishchenko 8fdc5d220f g++ portability changes. 2011-12-13 12:17:03 -08:00
Alan Mishchenko 23af7f9036 Added command &read_blif to read hierarchical BLIF directly into the &-space. 2011-12-12 19:10:33 -08:00
Alan Mishchenko be874a7abe Added command &read_blif to read hierarchical BLIF directly into the &-space. 2011-12-12 18:43:49 -08:00
Alan Mishchenko ed4f4adeee Added the hierarchy printout. 2011-12-11 17:29:25 -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 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 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 d2db956a61 Started experiments with a new solver. 2011-11-25 18:08:48 -08:00
Alan Mishchenko 0a5d856cec Making GLA PBA and GLA CBA communicate information. 2011-11-22 19:07:00 -08:00
Alan Mishchenko 30ea50a3b4 Temporary debugging change. 2011-11-12 23:21:41 -08:00
Alan Mishchenko df3e23ae3a Enabled skipping random decisions in PBA, which are performed by default. 2011-11-12 17:50:41 -08:00
Alan Mishchenko fa96b8d798 Do not allow interpolation with constraints. 2011-11-12 17:18:49 -08:00
Alan Mishchenko c1ac6b9b3e Dump inductive invariant or last interpolant after interpolation. 2011-11-12 16:56:41 -08:00
Alan Mishchenko 3beb36778e Enabled counter-example minimization in 'write_counter'. 2011-11-11 20:56:05 -08:00
Alan Mishchenko 0b73c76380 Preventing scripts from aborting if reading has failed. 2011-11-08 17:58:51 -08:00
Alan Mishchenko 55e9c4d0fa Corner case bug in deriving truth table from SOP. 2011-11-08 11:36:35 -08:00
Alan Mishchenko 9a89e3f9f5 Changing defaults in gate-level abstraction. 2011-11-06 23:35:15 -08:00
Alan Mishchenko d2ced9f82e Changes to read multi-output testcases described using AIGER 1.9. 2011-11-06 23:15:27 -08:00
Alan Mishchenko 5b75410a5e Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc. 2011-10-31 15:04:47 -05:00
Alan Mishchenko f08be2742e C++ portability changes. 2011-10-27 23:34:11 -07:00
Alan Mishchenko bc81cf2dae Improvements to the new abstraction code. 2011-10-27 14:20:47 -07:00
Alan Mishchenko 0f77840520 New proof-based abstraction code. 2011-10-25 18:32:06 +08:00
Alan Mishchenko f7fd329787 Improvements to the QBF solver. 2011-10-25 17:22:33 +08:00
Alan Mishchenko a8e1ba40b9 The result of merging with recent PyABC changes. 2011-10-25 14:05:50 +08:00
Alan Mishchenko f96f3fa583 Improvements to the QBF solver. 2011-10-24 18:05:45 +08:00
Alan Mishchenko 9ec9d9f315 New abstraction code. 2011-10-19 23:45:11 +07:00
Alan Mishchenko 19ce8396f0 New abstraction code. 2011-10-19 16:03:15 +07:00
Alan Mishchenko 397bebf8a5 New abstraction code. 2011-10-19 15:42:55 +07:00
Alan Mishchenko 12b70d4946 Changes to CNF generation code. 2011-10-17 10:39:05 +03:00
Alan Mishchenko 6f0b87dd5c New abstraction code. 2011-10-15 22:04:05 +03:00
Alan Mishchenko ad5ee9ff46 Changes to the matching procedure. 2011-10-12 15:04:41 +03:00
Alan Mishchenko 924ec940fe Changes to the matching procedure. 2011-10-06 15:48:27 +07:00
Alan Mishchenko d66b586330 Modified write_blif to output LUT structures. 2011-10-04 18:43:23 +07:00
Alan Mishchenko e6e6a3cf9e Changes to the matching procedure. 2011-10-01 17:00:59 +07:00
Baruch Sterin ef0fbf0372 completely silence the "source" command when the -s option is given 2011-10-24 15:21:08 -07:00
Alan Mishchenko 519b03e8e8 Changes to the matching procedure and new abstraction code. 2011-09-27 15:10:53 +07:00
Alan Mishchenko 976f5f5a12 Changes to Boolean matching. 2011-09-24 20:15:54 -07:00
Alan Mishchenko d080336bb5 Added new feature to bmc3. 2011-09-23 22:35:03 -07:00
Alan Mishchenko 8f74276edb Initial changes to enable gate-level abstraction. 2011-09-22 09:37:44 -07:00
Alan Mishchenko c1edeccc60 64-bit portability changes. 2011-09-17 16:24:40 -07:00
Alan Mishchenko 8248691d84 Added limit on the number of flops to add in one iteration of &abs_refine. 2011-09-12 16:46:37 -05:00
Alan Mishchenko 583bc4d71a Added limit on the number of flops to add in one iteration of &abs_cba. 2011-09-11 20:31:25 -05:00
Alan Mishchenko a7acb2f104 Fixed the problem with blackboxes not preserving their names after duplication. 2011-09-08 21:10:36 +07:00
Alan Mishchenko 11ed724766 Added timeout to &abc_pba. 2011-09-02 17:09:07 +07:00
Alan Mishchenko f8fb154229 Change 'testcex' to modify the PO number. 2011-08-27 22:44:21 +07:00
Alan Mishchenko 2adf8dc2fd Sequential cleanup with symbolic/ternary simulation. 2011-08-25 17:21:17 +07:00
Alan Mishchenko df6d509023 Sequential cleanup with symbolic/ternary simulation. 2011-08-25 14:14:50 +07:00
Alan Mishchenko 3469b605e1 Sequential cleanup with symbolic/ternary simulation. 2011-08-24 17:39:57 +07:00
Alan Mishchenko c913fd8849 Other changes to enable new features in the mapper (bug fix). 2011-08-24 09:33:40 +07:00
Alan Mishchenko d79cd4db44 Experiments with SPFD-based decomposition. 2011-08-21 15:05:44 +07:00
Alan Mishchenko 21dfaedebd Experiments with SPFD-based decomposition + new K-map print-out. 2011-08-20 20:18:31 +07:00
Alan Mishchenko b71b5bbc23 Bug fix in CBA and PBA. 2011-08-18 14:38:02 +07:00
Alan Mishchenko 48ae2c448f Bug fix in CBA and PBA. 2011-08-17 20:49:41 +07:00
Alan Mishchenko 3344a46b26 Added switch '-t' to 'miter' to create regular miter from dual-output miter. 2011-08-14 19:22:30 +07:00
Alan Mishchenko 94726c981b Other changes to enable new features in the mapper (bug fix). 2011-08-06 13:28:22 +08:00
Alan Mishchenko b9dea5d674 Other changes to enable new features in the mapper (bug fix). 2011-08-06 01:31:07 +08:00
Alan Mishchenko 49df91f071 Several bug fixes. 2011-08-02 12:58:37 +07:00
Alan Mishchenko 64f31f98bf Added API to access the CEX vector. 2011-08-02 12:01:49 +07:00
Alan Mishchenko 6c6c0b0686 Enabled saving vector of counter-examples in the ABC framework. 2011-08-02 00:31:03 +07:00
Alan Mishchenko 4e9f972489 Changes to enable CEX minimization. 2011-08-01 20:44:13 +07:00
Alan Mishchenko 961f7532d7 Changing the ordering of arguments in two iterators. 2011-08-01 13:47:51 +07:00
Alan Mishchenko 820a147ef1 Removed useless typecasts related to changes in Vec_VecEntry(). 2011-08-01 12:35:34 +07:00
Alan Mishchenko 81620f2e92 Changes to enable CEX minimization. 2011-08-01 12:13:49 +07:00
Alan Mishchenko 34811655f2 Minor bug fix in 'testcex'. 2011-07-31 20:37:38 +07:00
Alan Mishchenko 0d65c49048 Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when 2^nRegs frames are completed). 2011-07-31 20:22:57 +07:00
Alan Mishchenko 340e4380e9 Changes to enable smarter simulation (bug fix). 2011-07-30 20:26:17 +07:00
Alan Mishchenko 43d8b8bece Changes to enable smarter simulation. 2011-07-30 20:19:28 +07:00
Alan Mishchenko 02711b6392 Added generation of counter-examples to induction in 'ind'. 2011-07-30 19:18:26 +07:00
Alan Mishchenko c60852f4a9 Changes to enable smarter simulation. 2011-07-30 13:37:02 +07:00
Alan Mishchenko 2ea0ded0bc Changes to enable smarter simulation. 2011-07-30 13:30:04 +07:00
Alan Mishchenko e4f15dd003 Changes to enable smarter simulation. 2011-07-30 02:04:54 +07:00
Alan Mishchenko badf8e4742 Improving and updating the abstraction code. 2011-07-29 18:57:54 +07:00
Alan Mishchenko dac71e9b33 Added deriving abstraction in GIA from the precomputed flop map. 2011-07-29 16:21:25 +07:00
Alan Mishchenko ce38474c74 Improving and updating the abstraction code. 2011-07-29 15:38:44 +07:00
Alan Mishchenko 9e6d0664cb Other changes to enable new features in the mapper (bug fix). 2011-07-28 15:27:07 +07:00
Alan Mishchenko fddff7a55b Other changes to enable new features in the mapper (bug fix). 2011-07-28 13:50:34 +07:00
Alan Mishchenko 8ed6d8e05f Adding procedures to find the care bits of a counter-example (update). 2011-07-27 20:18:14 +07:00
Alan Mishchenko 7184003b42 Adding procedures to find the care bits of a counter-example (update). 2011-07-25 20:52:15 +07:00
Alan Mishchenko e7a5a74b4c Adding procedures to find the care bits of a counter-example. 2011-07-25 20:35:06 +07:00
Alan Mishchenko 76447062cc Adding &equiv3, a new way of refining equivalence classes. 2011-07-22 20:20:19 +07:00
Alan Mishchenko 9a2a0f2912 Changes to enable smarter simulation. 2011-07-21 17:55:44 +07:00
Alan Mishchenko fdf79ed471 Other changes to enable new features in the mapper (bug fix). 2011-07-21 12:02:07 +07:00
Alan Mishchenko ee261ef3f2 Other changes to enable new features in the mapper (bug fix). 2011-07-20 18:23:10 +07:00
Alan Mishchenko bb86d9142e New demitering features. 2011-07-20 13:52:54 +07:00
Alan Mishchenko 4ca6612821 Fixed assertion failure when mitering with choices. 2011-07-20 11:01:12 +07:00
Alan Mishchenko bc63966e4a Corner case bug fix in 'speedup'. 2011-07-20 10:55:58 +07:00
Alan Mishchenko fbd6a08e73 Other changes to enable new features in the mapper (bug fix). 2011-07-16 17:49:35 +07:00
Alan Mishchenko 302f7d7a97 Other changes to enable new features in the mapper (bug fix). 2011-07-15 18:50:58 +07:00
Alan Mishchenko 96e44e313e Other changes to enable new features in the mapper (bug fix). 2011-07-15 12:27:40 +07:00
Alan Mishchenko 6a020d6f69 Added switch to PDR to disable expensive generalization step. 2011-07-13 15:13:08 +07:00
Alan Mishchenko 669f390c6d Other changes to enable new features in the mapper (bug fix). 2011-07-13 12:48:51 +07:00
Alan Mishchenko 73702835c6 Added equivalence class computation for flop outputs only in &equiv2. 2011-07-13 10:13:24 +07:00
Alan Mishchenko 204fac4dca Other changes to enable new features in the mapper. 2011-07-10 13:56:05 +07:00
Alan Mishchenko ebfd70cdf4 Initial changes to enable new features in the mapper 2011-07-08 19:40:07 -07:00
Alan Mishchenko a37de7cc4d Printing out the path/name of the resource file that is being sourced. 2011-07-02 17:17:55 -07:00
Alan Mishchenko 10953634c9 Fixing a typo, which led to not printing delay in 'ps' after SC mapping. 2011-07-02 17:05:14 -07:00
Alan Mishchenko f866920eb5 Added a new demitering feature for dual-output miters. 2011-07-02 13:58:12 -07:00
Alan Mishchenko 6c2ac7661d Added another specialized check to the mapper. 2011-06-27 20:17:52 -07:00
Alan Mishchenko 0985eaca6c Updated 'iprove' to generate seq CEX when CEC fails (small fix). 2011-06-25 09:48:23 -07:00
Alan Mishchenko 49869d08ec Merged two last changes. 2011-06-25 09:45:04 -07:00
Alan Mishchenko 15cc374fe3 Updated 'iprove' to generate seq CEX when CEC fails. 2011-06-25 09:23:44 -07:00
Alan Mishchenko 5b639818e9 Added dumping CEXes in AIGER format. 2011-06-21 19:54:31 -07:00
Alan Mishchenko 4669839b24 Added new mapping feature. 2011-06-20 22:23:32 -07:00
Alan Mishchenko 6fd29922d3 Added permute/unpermute. 2011-06-20 13:16:23 -07:00