summaryrefslogtreecommitdiffstats
path: root/src/sat
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* Silencing warnings.Alan Mishchenko2012-07-112-7/+6
|
* Changes to clause mapping.Alan Mishchenko2012-07-114-30/+36
|
* Changes to clause mapping.Alan Mishchenko2012-07-111-1/+1
|
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-118-455/+498
|
* Improving print-outs of &vta and &gla.Alan Mishchenko2012-07-103-1/+9
|
* Performance bug fix in the SAT solver (clearing variable activity after ↵Alan Mishchenko2012-07-101-10/+0
| | | | rollback).
* Performance bug fix in the SAT solver (clearing variable activity after ↵Alan Mishchenko2012-07-091-0/+7
| | | | rollback).
* Performance bug fix in the SAT solver (clearing variable activity after ↵Alan Mishchenko2012-07-091-0/+3
| | | | rollback).
* Replacing Mb/Gb to be MB/GB.Alan Mishchenko2012-07-099-11/+11
|
* Bug fix in the recent changes to the SAT solver.Alan Mishchenko2012-07-091-0/+3
|
* Removing print-out message.Alan Mishchenko2012-07-091-1/+1
|
* Adding several command-line arguments to 'dsat'.Alan Mishchenko2012-07-092-6/+15
|
* Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, ↵Alan Mishchenko2012-07-097-262/+706
| | | | dsat, etc).
* Updating memory print-out of &vta and &gla.Alan Mishchenko2012-07-082-4/+5
|
* Updating project settings to have simpler include paths.Alan Mishchenko2012-07-0717-26/+26
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-073-3/+5
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-0719-73/+72
|
* Various changes to enable sensitization-based refinement in &gla.Alan Mishchenko2012-07-042-5/+5
|
* Performance improvement in &gla.Alan Mishchenko2012-07-043-0/+3
|
* Added memory reporting to &vta.Alan Mishchenko2012-06-224-4/+57
|