Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | SAT variable profiling. | Alan Mishchenko | 2013-05-18 | 2 | -0/+16 | |
| | ||||||
* | 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 | |
| |