summaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Scalable gate-level abstraction.Alan Mishchenko2012-08-012-73/+267
|
* Scalable gate-level abstraction.Alan Mishchenko2012-08-011-5/+16
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-313-23/+21
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-311-51/+79
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-312-102/+108
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-312-23/+62
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-311-51/+160
|
* Saving variable activity during rollback.Alan Mishchenko2012-07-302-0/+7
|
* Saving variable activity during rollback.Alan Mishchenko2012-07-302-1/+10
|
* Disabling learned clause removal when incremental proof-logging is running ↵Alan Mishchenko2012-07-303-16/+21
| | | | (tends to generate smaller abstarctions).
* Fixing performance bug with old proof-logging (adding clauses multiple times).Alan Mishchenko2012-07-303-17/+32
|
* Fixing a problem with printing out factored forms.Alan Mishchenko2012-07-301-12/+12
|
* Fixed compiler warnings.Alan Mishchenko2012-07-292-4/+4
|
* Reducing memory usage in proof-based abstraction.Alan Mishchenko2012-07-297-85/+524
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-294-330/+221
|
* Adding memory reporting to vectors.Alan Mishchenko2012-07-297-118/+120
|
* Adding command 'testdec'.Alan Mishchenko2012-07-286-22/+630
|
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-281-37/+49
|
* Started implementing command 'testdec'.Alan Mishchenko2012-07-283-0/+140
|
* 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-283-66/+90
|
* 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
|
* Fixing interpolation to run without resource limits by default.Alan Mishchenko2012-07-252-3/+3
|
* Removed unused files from the project.Alan Mishchenko2012-07-255-7/+3
|
* Allow for skipping structural hashing when reading GIA from file.Alan Mishchenko2012-07-252-6/+10
|
* Updated code for lazy man's synthesis.Alan Mishchenko2012-07-251-34/+46
|
* Allow for skipping structural hashing when reading GIA from file.Alan Mishchenko2012-07-255-20/+25
|
* Recording and reusing learned util clauses in bmc2.Alan Mishchenko2012-07-225-3/+22
|
* Recording and reusing learned util clauses in bmc3.Alan Mishchenko2012-07-225-16/+78
|
* 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-204-59/+368
|
* Updated code for lazy man's synthesis.Alan Mishchenko2012-07-205-90/+155
|
* Added switch &trim -c to additionally remove direct connections (POs fed by ↵Alan Mishchenko2012-07-202-3/+66
| | | | PIs).
* Updated code for lazy man's synthesis.Alan Mishchenko2012-07-203-309/+76
|
* New procedures to generate NPN-classes for a library of 6-input functions.Alan Mishchenko2012-07-201-8/+16
|
* Merging recent changes.Alan Mishchenko2012-07-203-0/+295
|\
| * New procedures to generate NPN-classes for a library of 6-input functions.Alan Mishchenko2012-07-193-0/+295
| |
* | 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-183-22/+13
|
* Adding new file to the build file.Alan Mishchenko2012-07-171-0/+1
|
* Small bug in bmc2 timeout.Alan Mishchenko2012-07-161-1/+1
|
* Updated code for lazy man's synthesis.Alan Mishchenko2012-07-151-0/+1
|
* Updated code for lazy man's synthesis.Alan Mishchenko2012-07-158-30/+3020
|
* 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
|
* Fixing assertion mismatch in bmc2.Alan Mishchenko2012-07-141-1/+1
|