Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Bug fix in QBF solver. | Alan Mishchenko | 2015-05-04 | 1 | -0/+4 |
| | |||||
* | Experiments with SAT-based cube enumeration. | Alan Mishchenko | 2015-03-05 | 1 | -19/+19 |
| | |||||
* | Compiler warnings. | Alan Mishchenko | 2015-02-19 | 1 | -1/+1 |
| | |||||
* | Compiler warnings. | Alan Mishchenko | 2014-10-28 | 1 | -2/+2 |
| | |||||
* | Adding command to dump UNSAT core of BMC instance. | Alan Mishchenko | 2014-04-07 | 5 | -16/+76 |
| | |||||
* | Adding switch to handle only single faults. | Alan Mishchenko | 2014-04-01 | 1 | -4/+4 |
| | |||||
* | Changes to LUT mappers. | Alan Mishchenko | 2014-03-04 | 1 | -0/+64 |
| | |||||
* | Changes to LUT mappers. | Alan Mishchenko | 2014-02-27 | 1 | -0/+46 |
| | |||||
* | Specialized induction check. | Alan Mishchenko | 2013-10-31 | 1 | -0/+39 |
| | |||||
* | Specialized induction check. | Alan Mishchenko | 2013-10-31 | 1 | -0/+19 |
| | |||||
* | Compiler warning about unused variable. | Alan Mishchenko | 2013-09-17 | 1 | -2/+2 |
| | |||||
* | Changing dynamic CNF loading code to perform loading before propagate() as ↵ | Alan Mishchenko | 2013-09-16 | 1 | -0/+31 |
| | | | | opposed to when the literal first implied in enqueue(). | ||||
* | Corrected variable naming in clause2_proofid(). | Alan Mishchenko | 2013-09-11 | 1 | -1/+1 |
| | |||||
* | Unifying parameters for the &ps command. | Alan Mishchenko | 2013-09-05 | 1 | -1/+1 |
| | |||||
* | Adding interpolant computation sat_solver2. | Alan Mishchenko | 2013-09-02 | 1 | -0/+242 |
| | |||||
* | Adding interpolant computation sat_solver2. | Alan Mishchenko | 2013-09-02 | 3 | -1/+28 |
| | |||||
* | Bug fix in 'int'. | Alan Mishchenko | 2013-08-05 | 1 | -2/+2 |
| | |||||
* | Bug fix in 'int'. | Alan Mishchenko | 2013-08-05 | 1 | -42/+35 |
| | |||||
* | SAT solver with dynamic CNF loading. | Alan Mishchenko | 2013-08-01 | 2 | -4/+34 |
| | |||||
* | Bug fix in the timeout for 'int'. | Alan Mishchenko | 2013-07-01 | 1 | -1/+1 |
| | |||||
* | Adding timeout to the interpolant computation procedure. | Alan Mishchenko | 2013-06-28 | 2 | -2/+19 |
| | |||||
* | Limiting runtime limit checks in 'pdr'. | Alan Mishchenko | 2013-06-21 | 2 | -2/+2 |
| | |||||
* | Adding a wrapper around clock() for more accurate time counting in ABC. | Alan Mishchenko | 2013-05-27 | 9 | -86/+86 |
| | |||||
* | Changing how often timeout is checked in the SAT solver and several ↵ | Alan Mishchenko | 2013-05-27 | 2 | -2/+2 |
| | | | | application packages. | ||||
* | SAT variable profiling. | Alan Mishchenko | 2013-05-18 | 2 | -4/+4 |
| | |||||
* | SAT variable profiling. | Alan Mishchenko | 2013-05-18 | 3 | -3/+27 |
| | |||||
* | SAT variable profiling (undo). | Alan Mishchenko | 2013-05-18 | 2 | -16/+0 |
| | |||||
* | SAT variable profiling. | Alan Mishchenko | 2013-05-18 | 2 | -0/+16 |
| | |||||
* | SAT variable profiling (undo). | Alan Mishchenko | 2013-05-18 | 2 | -16/+0 |
| | |||||
* | 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 |
| |