Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | 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 | |
| | ||||||
* | 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 | |
| |