Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | C++ portability changes. | Alan Mishchenko | 2012-10-03 | 2 | -2/+3 |
| | |||||
* | Added delay multipliers to 'map'. | Alan Mishchenko | 2012-09-16 | 1 | -1/+1 |
| | |||||
* | Prepared &gla to try abstracting and proving concurrently. | Alan Mishchenko | 2012-09-14 | 2 | -51/+47 |
| | |||||
* | Reversed to a buggy version of reduceDB in complete proof-logging, because ↵ | Alan Mishchenko | 2012-09-12 | 1 | -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 Mishchenko | 2012-08-31 | 1 | -0/+1 |
| | |||||
* | Bug fix in &gla. | Alan Mishchenko | 2012-08-27 | 3 | -5/+16 |
| | |||||
* | Scalable gate-level abstraction. | Alan Mishchenko | 2012-08-02 | 1 | -0/+12 |
| | |||||
* | Scalable gate-level abstraction. | Alan Mishchenko | 2012-07-31 | 1 | -1/+1 |
| | |||||
* | Saving variable activity during rollback. | Alan Mishchenko | 2012-07-30 | 2 | -0/+7 |
| | |||||
* | Saving variable activity during rollback. | Alan Mishchenko | 2012-07-30 | 2 | -1/+10 |
| | |||||
* | Disabling learned clause removal when incremental proof-logging is running ↵ | Alan Mishchenko | 2012-07-30 | 1 | -1/+1 |
| | | | | (tends to generate smaller abstarctions). | ||||
* | Fixing performance bug with old proof-logging (adding clauses multiple times). | Alan Mishchenko | 2012-07-30 | 1 | -0/+1 |
| | |||||
* | Fixed compiler warnings. | Alan Mishchenko | 2012-07-29 | 1 | -2/+2 |
| | |||||
* | Reducing memory usage in proof-based abstraction. | Alan Mishchenko | 2012-07-29 | 3 | -30/+393 |
| | |||||
* | Fixed the problem with 'write_cnf' after recent changes to the SAT solver. | Alan Mishchenko | 2012-07-28 | 1 | -37/+49 |
| | |||||
* | Fixed the problem with 'write_cnf' after recent changes to the SAT solver. | Alan Mishchenko | 2012-07-28 | 2 | -65/+89 |
| | |||||
* | Recording and reusing learned util clauses in bmc2. | Alan Mishchenko | 2012-07-22 | 1 | -0/+1 |
| | |||||
* | Recording and reusing learned util clauses in bmc3. | Alan Mishchenko | 2012-07-22 | 2 | -1/+19 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 2 | -12/+7 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -2/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -25/+9 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -3/+3 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+1 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -1/+1 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -1/+2 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -2/+5 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -1/+3 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -3/+21 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -2/+6 |
| | |||||
* | Debugging a proof error. | Alan Mishchenko | 2012-07-13 | 1 | -0/+3 |
| | |||||
* | Several small changes and fixes. | Alan Mishchenko | 2012-07-13 | 3 | -5/+11 |
| | |||||
* | Removed useless file. | Alan Mishchenko | 2012-07-12 | 1 | -5/+6 |
| | |||||
* | Added procedure for checking satisfied clauses. | Alan Mishchenko | 2012-07-12 | 1 | -0/+37 |
| | |||||
* | Silencing warnings. | Alan Mishchenko | 2012-07-11 | 1 | -1/+1 |
| | |||||
* | Silencing warnings. | Alan Mishchenko | 2012-07-11 | 2 | -7/+6 |
| | |||||
* | Changes to clause mapping. | Alan Mishchenko | 2012-07-11 | 4 | -30/+36 |
| | |||||
* | Changes to clause mapping. | Alan Mishchenko | 2012-07-11 | 1 | -1/+1 |
| | |||||
* | Improvements in the proof-logging SAT solver. | Alan Mishchenko | 2012-07-11 | 8 | -455/+498 |
| | |||||
* | Improving print-outs of &vta and &gla. | Alan Mishchenko | 2012-07-10 | 3 | -1/+9 |
| | |||||
* | Performance bug fix in the SAT solver (clearing variable activity after ↵ | Alan Mishchenko | 2012-07-10 | 1 | -10/+0 |
| | | | | rollback). | ||||
* | Performance bug fix in the SAT solver (clearing variable activity after ↵ | Alan Mishchenko | 2012-07-09 | 1 | -0/+7 |
| | | | | rollback). | ||||
* | Performance bug fix in the SAT solver (clearing variable activity after ↵ | Alan Mishchenko | 2012-07-09 | 1 | -0/+3 |
| | | | | rollback). | ||||
* | Replacing Mb/Gb to be MB/GB. | Alan Mishchenko | 2012-07-09 | 9 | -11/+11 |
| | |||||
* | Bug fix in the recent changes to the SAT solver. | Alan Mishchenko | 2012-07-09 | 1 | -0/+3 |
| | |||||
* | Removing print-out message. | Alan Mishchenko | 2012-07-09 | 1 | -1/+1 |
| | |||||
* | Adding several command-line arguments to 'dsat'. | Alan Mishchenko | 2012-07-09 | 2 | -6/+15 |
| | |||||
* | Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, ↵ | Alan Mishchenko | 2012-07-09 | 7 | -262/+706 |
| | | | | dsat, etc). | ||||
* | Updating memory print-out of &vta and &gla. | Alan Mishchenko | 2012-07-08 | 2 | -4/+5 |
| |