Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding rollback for the other solver. | Alan Mishchenko | 2013-04-25 | 3 | -3/+141 |
| | |||||
* | Fixing the dump of SAT solver into a CNF file. | Alan Mishchenko | 2013-03-26 | 3 | -17/+18 |
| | |||||
* | Compiler warnings. | Alan Mishchenko | 2013-02-23 | 2 | -0/+5 |
| | |||||
* | Fixing compilation problems on Linux-32 related to constants of type ↵ | Alan Mishchenko | 2013-01-30 | 1 | -6/+6 |
| | | | | unsigned long long. | ||||
* | Increasing memory page limit in the main SAT solver. | Alan Mishchenko | 2012-10-31 | 1 | -1/+1 |
| | |||||
* | C++ portability changes. | Alan Mishchenko | 2012-10-03 | 2 | -2/+3 |
| | |||||
* | 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 | 3 | -24/+30 |
| | |||||
* | 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 | 8 | -10/+10 |
| | |||||
* | 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 |
| |