summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
Commit message (Collapse)AuthorAgeFilesLines
* Variable timeframe abstraction.Alan Mishchenko2012-02-131-0/+6
|
* Variable timeframe abstraction.Alan Mishchenko2012-02-133-27/+85
|
* Variable timeframe abstraction.Alan Mishchenko2012-02-132-9/+7
|
* Variable timeframe abstraction.Alan Mishchenko2012-02-131-16/+19
|
* Variable timeframe abstraction.Alan Mishchenko2012-02-122-71/+62
|
* Variable timeframe abstraction.Alan Mishchenko2012-02-111-9/+28
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-281-13/+17
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-273-210/+127
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-242-23/+42
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-241-10/+80
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-211-6/+1
|
* Major restructuring of the code.Alan Mishchenko2012-01-2113-26/+26
|
* Variable timeframe abstraction.Alan Mishchenko2012-01-204-30/+39
|
* Improving printout in the SAT solver.Alan Mishchenko2012-01-132-2/+4
|
* Bug fix related to not properly resizing SAT solver's model array.Alan Mishchenko2012-01-122-0/+2
|
* Bug fix related to not properly resizing SAT solver's model array.Alan Mishchenko2012-01-065-31/+25
|
* APIs to represent simple gates in CNF.Alan Mishchenko2012-01-051-0/+112
|
* APIs to represent simple gates in CNF.Alan Mishchenko2012-01-051-0/+100
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-233-38/+83
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-233-91/+45
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-232-4/+4
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-238-542/+2484
|
* Transforming the solver to use different clause representation.Alan Mishchenko2011-12-221-143/+143
|
* Computing interpolants as truth tables.Alan Mishchenko2011-12-228-0/+825
|
* Undoing temporary change to the solver.Alan Mishchenko2011-12-151-1/+1
|
* Temporary change to the solver.Alan Mishchenko2011-12-151-1/+1
|
* Started SAT-based reparameterization.Alan Mishchenko2011-12-133-149/+73
|
* Implementing rollback in the updated solver.Alan Mishchenko2011-12-101-5/+6
|
* Implementing rollback in the updated solver.Alan Mishchenko2011-12-103-14/+46
|
* Implemented rollback in the main SAT solver and updated PDR to use it (saves ↵Alan Mishchenko2011-12-104-8/+89
| | | | 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
|