Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Transforming the solver to use different clause representation. | Alan Mishchenko | 2011-12-22 | 1 | -143/+143 |
| | |||||
* | Computing interpolants as truth tables. | Alan Mishchenko | 2011-12-22 | 8 | -0/+825 |
| | |||||
* | Undoing temporary change to the solver. | Alan Mishchenko | 2011-12-15 | 1 | -1/+1 |
| | |||||
* | Temporary change to the solver. | Alan Mishchenko | 2011-12-15 | 1 | -1/+1 |
| | |||||
* | Started SAT-based reparameterization. | Alan Mishchenko | 2011-12-13 | 3 | -149/+73 |
| | |||||
* | Implementing rollback in the updated solver. | Alan Mishchenko | 2011-12-10 | 1 | -5/+6 |
| | |||||
* | Implementing rollback in the updated solver. | Alan Mishchenko | 2011-12-10 | 3 | -14/+46 |
| | |||||
* | Implemented rollback in the main SAT solver and updated PDR to use it (saves ↵ | Alan Mishchenko | 2011-12-10 | 4 | -8/+89 |
| | | | | about 5% of runtime). | ||||
* | Implementing rollback in the updated solver. | Alan Mishchenko | 2011-12-10 | 3 | -81/+218 |
| | |||||
* | Removing unused files. | Alan Mishchenko | 2011-12-10 | 6 | -6483/+0 |
| | |||||
* | Changes to the main SAT solver: fixing performance bug (resetting decay ↵ | Alan Mishchenko | 2011-12-09 | 4 | -315/+330 |
| | | | | params after each restart), making the SAT solver platform- and runtime-independent (by using interger-based activity). | ||||
* | Integrated new proof-logging into proof-based gate-level abstraction. | Alan Mishchenko | 2011-12-08 | 3 | -228/+187 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-08 | 3 | -133/+334 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-08 | 5 | -120/+211 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-07 | 3 | -176/+124 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-06 | 3 | -65/+163 |
| | |||||
* | g++ portability changes. | Alan Mishchenko | 2011-12-06 | 1 | -2/+2 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-05 | 2 | -32/+34 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-05 | 4 | -391/+524 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-05 | 3 | -18/+34 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-04 | 2 | -32/+41 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-04 | 3 | -283/+352 |
| | |||||
* | Proof-logging in the updated solver. | Alan Mishchenko | 2011-12-04 | 5 | -216/+481 |
| | |||||
* | Removing redundant function declarations. | Alan Mishchenko | 2011-12-02 | 1 | -4/+0 |
| | |||||
* | Started proof transformations. | Alan Mishchenko | 2011-12-01 | 2 | -0/+477 |
| | |||||
* | Started experiments with a new solver. | Alan Mishchenko | 2011-11-27 | 2 | -645/+265 |
| | |||||
* | Started experiments with a new solver. | Alan Mishchenko | 2011-11-26 | 4 | -555/+466 |
| | |||||
* | Started experiments with a new solver. | Alan Mishchenko | 2011-11-26 | 1 | -3/+10 |
| | |||||
* | Started experiments with a new solver. | Alan Mishchenko | 2011-11-26 | 3 | -4/+6 |
| | |||||
* | Started experiments with a new solver. | Alan Mishchenko | 2011-11-26 | 3 | -72/+371 |
| | |||||
* | Started experiments with a new solver. | Alan Mishchenko | 2011-11-25 | 4 | -7/+1732 |
| | |||||
* | Commented out the default call to UNSAT core verification. | Alan Mishchenko | 2011-11-25 | 1 | -1/+1 |
| | |||||
* | Improvement to the SAT solver (skipping binary clauses). | Alan Mishchenko | 2011-11-25 | 3 | -5/+57 |
| | |||||
* | Enabled skipping random decisions in PBA, which are performed by default. | Alan Mishchenko | 2011-11-12 | 2 | -1/+9 |
| | |||||
* | Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc. | Alan Mishchenko | 2011-10-31 | 1 | -3/+4 |
| | |||||
* | New abstraction code. | Alan Mishchenko | 2011-10-15 | 1 | -0/+2 |
| | |||||
* | Reduced default growth rate of vectors in the SAT solver. | Alan Mishchenko | 2011-07-13 | 1 | -2/+4 |
| | |||||
* | Adding SAT-solver-level timeouts to the BMC engines. | Alan Mishchenko | 2011-04-08 | 2 | -1/+9 |
| | |||||
* | Added test package (new files). | Alan Mishchenko | 2011-03-29 | 1 | -0/+5 |
| | |||||
* | Cumulative changes in the last few weeks. | Alan Mishchenko | 2011-01-13 | 2 | -39/+152 |
| | |||||
* | Initial implementation of AnalyseFinal | Alan Mishchenko | 2010-12-03 | 2 | -1/+9 |
| | |||||
* | Adding missing license agreements | Alan Mishchenko | 2010-11-29 | 1 | -0/+21 |
| | |||||
* | initial commit of public abc | Alan Mishchenko | 2010-11-01 | 20 | -113/+3653 |
| | |||||
* | Version abc90310 | Alan Mishchenko | 2009-03-10 | 1 | -0/+1 |
| | |||||
* | Version abc90215 | Alan Mishchenko | 2009-02-15 | 13 | -237/+223 |
| | |||||
* | Version abc90118 | Alan Mishchenko | 2009-01-18 | 2 | -12/+140 |
| | |||||
* | Version abc81029 | Alan Mishchenko | 2008-10-29 | 1 | -0/+8 |
| | |||||
* | Version abc81013 | Alan Mishchenko | 2008-10-13 | 1 | -2/+57 |
| | |||||
* | Version abc81004 | Alan Mishchenko | 2008-10-04 | 5 | -27/+2424 |
| | |||||
* | Version abc80927 | Alan Mishchenko | 2008-09-27 | 2 | -1/+1049 |
| |