Commit Graph

113 Commits

Author SHA1 Message Date
Alan Mishchenko 853222ee7b Fixed a corner-case when 'sim3 -a' does not work for costant POs. 2013-01-25 06:49:49 +07:00
Alan Mishchenko edd4b2a29c Added switch &trim -V <num> to remove const POs with specific value <num>. 2013-01-25 06:19:51 +07:00
Alan Mishchenko 4efc89d342 Enabled detecting CEXes in multiple POs without stopping (sim3 -a). 2013-01-23 16:50:45 +07:00
Alan Mishchenko 6863688789 Enabled detecting CEXes in multiple POs without stopping (sim3 -a). 2013-01-23 12:37:44 +07:00
Alan Mishchenko ac1207abea Enabled detecting CEXes in multiple POs without stopping (sim3 -a). 2013-01-23 02:07:50 +07:00
Alan Mishchenko 8287b05a09 Reintroduced the old abstraction procedure Saig_ManCexAbstractionFlops() formerly called from &abs_start for backward compatibility. 2013-01-08 14:46:13 +08:00
Alan Mishchenko a625caa17d Fixing C++ compilation issues. 2013-01-08 13:56:20 +08:00
Alan Mishchenko f26e760e9d Fixing C++ compilation issues. 2013-01-08 13:33:17 +08:00
Alan Mishchenko 2575a5d683 Unifification of custom extensions. 2012-12-10 13:56:40 -08:00
Alan Mishchenko ce63869fe7 Enabling multi-output solving in 'pdr'. 2012-12-09 17:33:44 -08:00
Alan Mishchenko 9fc1cd0b3f Enabling multi-output solving in 'pdr'. 2012-12-09 15:12:40 -08:00
Alan Mishchenko 58d4012a55 Enabling multi-output solving in 'pdr'. 2012-12-09 14:46:16 -08:00
Alan Mishchenko 8a08453af2 Corner-case bug fix in &rpm. 2012-12-09 10:05:34 -08:00
Alan Mishchenko b65ae7349a Enabling multi-output solving in 'pdr'. 2012-12-09 09:47:48 -08:00
Alan Mishchenko 8c04d9501f Making 'scorr -c' applicable to seq benchmarks without constraints. 2012-12-04 18:35:44 -08:00
Alan Mishchenko be7a4e4259 Isolating BMC code into a separate package. 2012-11-14 13:55:24 -08:00
Alan Mishchenko 30b8c3d422 Made print-out of frontier cut an option ('-c') in '&ps'. 2012-11-12 14:08:10 -08:00
Alan Mishchenko aa2c7c0546 Enabling verbose report of dumping abstraction in GLA. 2012-11-07 12:05:39 -08:00
Alan Mishchenko db7852bba7 Improvements to LMS code. 2012-11-06 18:04:23 -08:00
Niklas Een e353c4b75c Merge 2012-10-30 12:38:57 -07:00
Niklas Een c3168ba661 Replaced printfs with Abc_Print 2012-10-29 15:35:02 -07:00
Niklas Een 1e8565eee3 Replaced printfs with Abc_Print 2012-10-29 15:28:30 -07:00
Niklas Een c3a773d94f Replaced printfs with Abc_Print 2012-10-29 15:27:40 -07:00
Alan Mishchenko b733b813d6 Added switch '-q' to 'scorr' and '&scorr' to quit when PO is not a candidate constant. 2012-10-25 22:50:29 -07:00
Alan Mishchenko 6b96d9a84e Integrating GIA with LUT mapping. 2012-10-24 17:39:38 -07:00
Alan Mishchenko 5cd1396b3d Creating dedicated choice representation for GIA. 2012-10-24 12:22:46 -07:00
Alan Mishchenko daeffe791c Making report about the number of correcty covered frames consistent across the engines. 2012-10-09 15:42:25 -07:00
Alan Mishchenko da61616d84 Bug fix in &gla (incorrect reporting of proved timeframes). 2012-10-09 11:59:30 -07:00
Alan Mishchenko b882f64fa5 Bug fix in &gla (incorrect reporting of proved timeframes). 2012-10-09 11:48:28 -07:00
Alan Mishchenko 4ed89d00fe Making explicit cast to 64-bit unsigned in a few places. 2012-10-09 09:23:08 -07:00
Alan Mishchenko f66fd3f3a3 Updating readme. 2012-10-06 18:28:25 -07:00
Alan Mishchenko c7eab028a1 C++ portability changes. 2012-10-03 21:59:04 -07:00
Alan Mishchenko b532d144c8 C++ portability changes. 2012-10-03 21:56:59 -07:00
Alan Mishchenko 56d3d7cd22 C++ portability changes. 2012-10-03 21:49:18 -07:00
Alan Mishchenko aa705a9af6 Renamed reference counting APIs in GIA package. 2012-10-02 20:20:46 -07:00
Alan Mishchenko 49267fd379 Structural reparametrization. 2012-10-02 20:11:38 -07:00
Alan Mishchenko aeb7f7ea11 Combined old reparametrization command with the new one. 2012-10-02 17:27:36 -07:00
Alan Mishchenko 4aa33e7d0f Structural reparametrization. 2012-10-02 16:30:14 -07:00
Alan Mishchenko b71d4425d0 Separated truth table computation for GIA manager and added new procedures. 2012-10-02 15:20:11 -07:00
Alan Mishchenko 60ad1765ff Structural reparametrization. 2012-10-01 22:55:01 -07:00
Alan Mishchenko a287bcd2e2 Fixed several important problems in choice computation (command 'dch'). 2012-10-01 18:28:55 -07:00
Alan Mishchenko 7d29663720 Fixed several important problems in choice computation (command 'dch'). 2012-10-01 18:25:41 -07:00
Alan Mishchenko a595fa85ef Structural reparametrization. 2012-09-30 22:46:21 -07:00
Alan Mishchenko 4ab0c4b204 Correcting comment related to pthreads. 2012-09-24 20:53:26 -07:00
Alan Mishchenko 255f171f63 Improving computation of choices from equivalence classes. 2012-09-23 23:53:12 -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 b5306c1566 Added simplification before the concurrent call to PDR. 2012-09-20 20:13:40 -07:00
Alan Mishchenko 5f09917c22 Added simplification before the concurrent call to PDR. 2012-09-20 19:51:39 -07:00
Alan Mishchenko 1f9abfd7a8 Bug fix: no need to normalize const0 node. 2012-09-17 10:02:37 -07:00