summaryrefslogtreecommitdiffstats
path: root/src/aig
Commit message (Collapse)AuthorAgeFilesLines
* Fixing performance bug with old proof-logging (adding clauses multiple times).Alan Mishchenko2012-07-301-17/+9
|
* Reducing memory usage in proof-based abstraction.Alan Mishchenko2012-07-293-55/+129
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-293-325/+207
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-281-24/+72
|
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-281-1/+1
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-271-211/+319
|
* Minor updates to the BMC engines.Alan Mishchenko2012-07-274-3/+51
|
* Changes in command 'bm' to report timeout (thanks to S.W.)Alan Mishchenko2012-07-261-92/+89
|
* Allow for skipping structural hashing when reading GIA from file.Alan Mishchenko2012-07-251-2/+2
|
* Allow for skipping structural hashing when reading GIA from file.Alan Mishchenko2012-07-253-14/+18
|
* Recording and reusing learned util clauses in bmc2.Alan Mishchenko2012-07-223-2/+20
|
* Recording and reusing learned util clauses in bmc3.Alan Mishchenko2012-07-223-15/+59
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-212-124/+259
|
* Correcting &gla to update status as 'sat' after CEX is found.Alan Mishchenko2012-07-202-8/+2
|
* Updated code for lazy man's synthesis (memory optimization).Alan Mishchenko2012-07-202-6/+6
|
* Updated code for lazy man's synthesis.Alan Mishchenko2012-07-203-85/+102
|
* Added switch &trim -c to additionally remove direct connections (POs fed by ↵Alan Mishchenko2012-07-201-0/+52
| | | | PIs).
* Making GIA use independent truth table number storage when computing truth ↵Alan Mishchenko2012-07-193-6/+10
| | | | tables.
* Scalable gate-level abstraction.Alan Mishchenko2012-07-181-0/+1021
|
* Enabling &gla for combinational miters.Alan Mishchenko2012-07-182-8/+9
|
* Small bug in bmc2 timeout.Alan Mishchenko2012-07-161-1/+1
|
* Updated code for lazy man's synthesis.Alan Mishchenko2012-07-151-3/+8
|
* Added new refinement manager for &gla and &abs_refine.Alan Mishchenko2012-07-141-0/+2
|
* Added new refinement manager for &gla and &abs_refine.Alan Mishchenko2012-07-144-8/+727
|
* Several small changes and fixes.Alan Mishchenko2012-07-133-15/+24
|
* Removed useless file.Alan Mishchenko2012-07-121-1/+0
|
* Fixing temporary linker problem.Alan Mishchenko2012-07-121-1/+2
|
* Handling the trivial case when PO is driven by a constant.Alan Mishchenko2012-07-112-0/+25
|
* Changes to clause mapping.Alan Mishchenko2012-07-114-104/+39
|
* Changes to clause mapping.Alan Mishchenko2012-07-112-5/+5
|
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-114-77/+34
|
* Fixed several problems when CEX is detected by &vta/&gla.Alan Mishchenko2012-07-112-3/+7
|
* Enabling refinement in &gla_refine even if CEX is invalid.Alan Mishchenko2012-07-111-2/+2
|
* Replacing printf() by Abc_Print().Alan Mishchenko2012-07-102-41/+41
|
* Improving print-outs of &vta and &gla.Alan Mishchenko2012-07-102-9/+27
|
* Improving print-outs of &vta and &gla.Alan Mishchenko2012-07-102-8/+59
|
* Replacing Mb/Gb to be MB/GB.Alan Mishchenko2012-07-0922-38/+38
|
* Performance bug fix in &gla.Alan Mishchenko2012-07-091-1/+3
|
* Adding several command-line arguments to 'dsat'.Alan Mishchenko2012-07-092-3/+3
|
* Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, ↵Alan Mishchenko2012-07-091-11/+11
| | | | dsat, etc).
* Added command &gla_purify.Alan Mishchenko2012-07-085-181/+251
|
* Updating truth table computation for GIA to work for internal nodes as well.Alan Mishchenko2012-07-082-16/+20
|
* Updating memory print-out of &vta and &gla.Alan Mishchenko2012-07-082-5/+5
|
* Adding flushing stdout after printing verbose stats.Alan Mishchenko2012-07-072-0/+3
|
* Updating project settings to have simpler include paths.Alan Mishchenko2012-07-0770-133/+133
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-072-2/+4
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-072-2/+3
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-079-9/+12
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-0778-253/+280
|
* Changing the default value of &vta -t to reduce proof memory usage.Alan Mishchenko2012-07-071-1/+1
|