summaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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-284-0/+144
* 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-256-35/+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-213-124/+263
* 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-205-59/+372
* 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 P...Alan Mishchenko2012-07-202-3/+66
* 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 ta...Alan Mishchenko2012-07-193-6/+10
|/
* 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-152-0/+5
* 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-145-8/+735
* Fixing assertion mismatch in bmc2.Alan Mishchenko2012-07-141-1/+1
* Fixing the integer print-out problem.Alan Mishchenko2012-07-131-13/+13
* Fixing the integer print-out problem.Alan Mishchenko2012-07-131-12/+18
* Debugging a proof error.Alan Mishchenko2012-07-132-12/+7
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+2
* Debugging a proof error.Alan Mishchenko2012-07-132-50/+26
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+7
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+1
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-3/+3
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+1
* Debugging a proof error.Alan Mishchenko2012-07-131-1/+1
* Debugging a proof error.Alan Mishchenko2012-07-131-1/+2
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+5
* Debugging a proof error.Alan Mishchenko2012-07-131-1/+3