summaryrefslogtreecommitdiffstats
path: root/src/sat
Commit message (Collapse)AuthorAgeFilesLines
* Counter-example analysis and optimization.Alan Mishchenko2012-11-301-3/+1
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-301-17/+21
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-301-12/+78
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-291-0/+590
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-281-1/+2
|
* Added switch 'cexcut -m' to generate bad states for all frames after G.Alan Mishchenko2012-11-152-10/+139
|
* Added switch 'cexcut -n' to generate only one bad state.Alan Mishchenko2012-11-152-24/+238
|
* Added command 'cexcut' and 'cexmerge'.Alan Mishchenko2012-11-142-12/+15
|
* Added command 'cexcut' and 'cexmerge'.Alan Mishchenko2012-11-142-16/+52
|
* Added command 'cexcut' and 'cexmerge'.Alan Mishchenko2012-11-141-2/+102
|
* Added command 'cexsave' and 'cexload'.Alan Mishchenko2012-11-146-8/+12
|
* Isolating BMC code into a separate package.Alan Mishchenko2012-11-149-0/+3941
|
* Increasing memory page limit in the main SAT solver.Alan Mishchenko2012-10-311-1/+1
|
* Making explicit cast to 64-bit unsigned in a few places.Alan Mishchenko2012-10-091-2/+2
|
* C++ portability changes.Alan Mishchenko2012-10-032-2/+3
|
* Added delay multipliers to 'map'.Alan Mishchenko2012-09-161-1/+1
|
* Prepared &gla to try abstracting and proving concurrently.Alan Mishchenko2012-09-142-51/+47
|
* Reversed to a buggy version of reduceDB in complete proof-logging, because ↵Alan Mishchenko2012-09-121-2/+2
| | | | it works with rollback and it is not used in &gla -pn -L 0.
* Changes to allow &gla to run with fSimple = 1 (useful for debugging).Alan Mishchenko2012-08-311-0/+1
|
* Bug fix in &gla.Alan Mishchenko2012-08-273-5/+16
|
* Scalable gate-level abstraction.Alan Mishchenko2012-08-021-0/+12
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-311-1/+1
|
* 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-301-1/+1
| | | | (tends to generate smaller abstarctions).
* Fixing performance bug with old proof-logging (adding clauses multiple times).Alan Mishchenko2012-07-301-0/+1
|
* Fixed compiler warnings.Alan Mishchenko2012-07-291-2/+2
|
* Reducing memory usage in proof-based abstraction.Alan Mishchenko2012-07-293-30/+393
|
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-281-37/+49
|
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-282-65/+89
|
* Recording and reusing learned util clauses in bmc2.Alan Mishchenko2012-07-221-0/+1
|
* Recording and reusing learned util clauses in bmc3.Alan Mishchenko2012-07-222-1/+19
|
* 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-131-25/+9
|
* 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-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
|
* Debugging a proof error.Alan Mishchenko2012-07-131-3/+21
|
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+6
|
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+3
|
* Several small changes and fixes.Alan Mishchenko2012-07-133-5/+11
|
* Removed useless file.Alan Mishchenko2012-07-121-5/+6
|
* Added procedure for checking satisfied clauses.Alan Mishchenko2012-07-121-0/+37
|
* Silencing warnings.Alan Mishchenko2012-07-111-1/+1
|