summaryrefslogtreecommitdiffstats
path: root/src/sat
Commit message (Expand)AuthorAgeFilesLines
* 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-107-21/+106
* 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 param...Alan Mishchenko2011-12-094-315/+330
* 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 19:16:04 +0000