summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver2.h
Commit message (Collapse)AuthorAgeFilesLines
* C++ portability changes.Alan Mishchenko2012-10-031-1/+0
|
* Bug fix in &gla.Alan Mishchenko2012-08-271-2/+3
|
* Saving variable activity during rollback.Alan Mishchenko2012-07-301-0/+4
|
* Saving variable activity during rollback.Alan Mishchenko2012-07-301-1/+4
|
* Reducing memory usage in proof-based abstraction.Alan Mishchenko2012-07-291-2/+6
|
* Changes to clause mapping.Alan Mishchenko2012-07-111-22/+23
|
* Changes to clause mapping.Alan Mishchenko2012-07-111-1/+1
|
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-111-55/+21
|
* Improving print-outs of &vta and &gla.Alan Mishchenko2012-07-101-0/+5
|
* Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, ↵Alan Mishchenko2012-07-091-15/+16
| | | | dsat, etc).
* Updating memory print-out of &vta and &gla.Alan Mishchenko2012-07-081-1/+1
|
* Updating project settings to have simpler include paths.Alan Mishchenko2012-07-071-1/+1
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-3/+3
|
* Added memory reporting to &vta.Alan Mishchenko2012-06-221-0/+2
|
* Moving Vec_Set_t to the vector directory.Alan Mishchenko2012-03-281-1/+1
|
* Improved memory management of proof-logging and propagated changes.Alan Mishchenko2012-02-161-11/+17
|
* Variable timeframe abstraction.Alan Mishchenko2012-02-131-7/+1
|
* Variable timeframe abstraction.Alan Mishchenko2012-02-121-4/+14
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-271-4/+4
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-241-8/+2
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-211-6/+1
|
* Major restructuring of the code.Alan Mishchenko2012-01-211-2/+2
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-201-3/+3
|
* Bug fix related to not properly resizing SAT solver's model array.Alan Mishchenko2012-01-061-5/+5
|
* APIs to represent simple gates in CNF.Alan Mishchenko2012-01-051-0/+112
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-231-2/+2
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-231-0/+2
|
* Computing interpolants as truth tables.Alan Mishchenko2011-12-221-0/+1
|
* Started SAT-based reparameterization.Alan Mishchenko2011-12-131-0/+5
|
* Implementing rollback in the updated solver.Alan Mishchenko2011-12-101-1/+1
|
* Implementing rollback in the updated solver.Alan Mishchenko2011-12-101-1/+12
|
* Changes to the main SAT solver: fixing performance bug (resetting decay ↵Alan Mishchenko2011-12-091-13/+14
| | | | 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-081-10/+5
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-081-1/+1
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-081-4/+6
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-071-6/+3
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-061-5/+8
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-051-76/+110
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-051-0/+8
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-041-0/+1
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-041-5/+6
|
* Proof-logging in the updated solver.Alan Mishchenko2011-12-041-10/+21
|
* Removing redundant function declarations.Alan Mishchenko2011-12-021-4/+0
|
* Started experiments with a new solver.Alan Mishchenko2011-11-271-8/+24
|
* Started experiments with a new solver.Alan Mishchenko2011-11-261-55/+45
|
* Started experiments with a new solver.Alan Mishchenko2011-11-261-2/+2
|
* Started experiments with a new solver.Alan Mishchenko2011-11-261-0/+1
|
* Started experiments with a new solver.Alan Mishchenko2011-11-251-0/+194