summaryrefslogtreecommitdiffstats
path: root/src/sat
Commit message (Collapse)AuthorAgeFilesLines
...
* Implemented rollback in the main SAT solver and updated PDR to use it (saves ↵Alan Mishchenko2011-12-107-21/+106
| | | | about 5% of runtime).
* Implementing rollback in the updated solver.Alan Mishchenko2011-12-103-81/+218
|
* Removing unused files.Alan Mishchenko2011-12-106-6483/+0
|
* Changes to the main SAT solver: fixing performance bug (resetting decay ↵Alan Mishchenko2011-12-094-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 Mishchenko2011-12-083-228/+187
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-083-133/+334
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-085-120/+211
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-073-176/+124
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-063-65/+163
|
* g++ portability changes.Alan Mishchenko2011-12-061-2/+2
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-052-32/+34
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-054-391/+524
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-053-18/+34
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-042-32/+41
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-043-283/+352
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-045-216/+481
|
* Removing redundant function declarations.Alan Mishchenko2011-12-021-4/+0
|
* Started proof transformations.Alan Mishchenko2011-12-012-0/+477
|
* Started experiments with a new solver.Alan Mishchenko2011-11-272-645/+265
|
* Started experiments with a new solver.Alan Mishchenko2011-11-264-555/+466
|
* Started experiments with a new solver.Alan Mishchenko2011-11-261-3/+10
|
* Started experiments with a new solver.Alan Mishchenko2011-11-263-4/+6
|
* Started experiments with a new solver.Alan Mishchenko2011-11-263-72/+371
|
* Started experiments with a new solver.Alan Mishchenko2011-11-254-7/+1732
|
* Commented out the default call to UNSAT core verification.Alan Mishchenko2011-11-251-1/+1
|
* Improvement to the SAT solver (skipping binary clauses).Alan Mishchenko2011-11-253-5/+57
|
* Enabled skipping random decisions in PBA, which are performed by default.Alan Mishchenko2011-11-122-1/+9
|
* Dump last frame clauses with 'pdr -d' even if the problem is SAT or undecided.Alan Mishchenko2011-11-123-7/+17
|
* Corner-case bug in PDR.Alan Mishchenko2011-11-112-2/+9
|
* Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.Alan Mishchenko2011-10-312-6/+7
|
* New abstraction code.Alan Mishchenko2011-10-151-0/+2
|
* Added handling of exceeding conflict limit in PushClasses.Alan Mishchenko2011-10-011-3/+15
|
* Changing the ordering of arguments in two iterators.Alan Mishchenko2011-08-012-15/+15
|
* Removed useless typecasts related to changes in Vec_VecEntry().Alan Mishchenko2011-08-011-2/+2
|
* Reduced default growth rate of vectors in the SAT solver.Alan Mishchenko2011-07-131-2/+4
|
* Added switch to PDR to disable expensive generalization step.Alan Mishchenko2011-07-132-66/+71
|
* Modified the PDR print-out to be compatible with Niklas.Alan Mishchenko2011-07-121-3/+3
|
* Added printout of flop names in the PLA file representing the invariant.Alan Mishchenko2011-07-111-0/+16
|
* The cube in PDR can have more than 2^15 literals.Alan Mishchenko2011-06-272-4/+4
|
* Improvements to timeout.Alan Mishchenko2011-05-111-0/+2
|
* Adding SAT-solver-level timeouts to the BMC engines.Alan Mishchenko2011-04-082-1/+9
|
* Unsuccessful attempt to improve PDR and a few minor changes.Alan Mishchenko2011-04-0710-37/+243
|
* Added test package (new files).Alan Mishchenko2011-03-291-0/+5
|
* Improvements in Vec_Vec_t.Alan Mishchenko2011-03-272-3/+3
|
* Made abc.h independent of CUDD and Extra.Alan Mishchenko2011-03-031-13/+13
|
* Unified the use of counter-examples in three packages.Alan Mishchenko2011-02-131-2/+1
|
* Changes to enable C++ compilation after recent modifications.Alan Mishchenko2011-02-132-3/+3
|
* Make PDR return the number of completed frames.Alan Mishchenko2011-02-032-0/+8
|
* New code since Dec 2010.Alan Mishchenko2011-01-1312-0/+3483
|
* Cumulative changes in the last few weeks.Alan Mishchenko2011-01-132-39/+152
|