summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
Commit message (Collapse)AuthorAgeFilesLines
* Experiments with pattern generation.Alan Mishchenko2021-10-101-0/+18
|
* Experiments with simulation-based engines.Alan Mishchenko2020-03-251-1/+2
|
* Changes to several APIs.Alan Mishchenko2019-11-011-6/+22
|
* An improvement to 'twoexact' and 'lutexact'.Alan Mishchenko2017-12-062-15/+19
|
* Changes to 'pdr' to run with updated Satoko.Alan Mishchenko2017-09-061-0/+8
|
* Several changes to various packages.Alan Mishchenko2017-09-041-1/+2
|
* Improvements to minimize_assumptions.Alan Mishchenko2017-09-031-7/+22
|
* Adding an option to bmc3 to use Satoko intead of the default SAT solver.Alan Mishchenko2017-08-132-2/+2
|
* Compiler warnings.Alan Mishchenko2017-04-281-3/+3
|
* Compiler warnings.Alan Mishchenko2017-04-281-3/+3
|
* Compiler warnings.Alan Mishchenko2017-04-281-3/+3
|
* Experiments with hashing.Alan Mishchenko2017-04-112-0/+6
|
* Experiments with don't-cares.Alan Mishchenko2017-04-042-0/+15
|
* Experiments with don't-cares.Alan Mishchenko2017-04-021-2/+2
|
* added callbacks to bmc3 and sat solverYen-Sheng Ho2017-03-202-0/+6
|
* Clone of the main SAT solver to eneable independent work.Alan Mishchenko2017-03-031-0/+1
|
* Clone of the main SAT solver to eneable independent work.Alan Mishchenko2017-03-032-0/+2921
|
* Adding alternative generalization procedure.Alan Mishchenko2017-03-022-3/+92
|
* Adding efficient procedure to minimize the set of assumptions (improved ↵Alan Mishchenko2017-03-021-1/+8
| | | | literal reordering).
* Adding alternative generalization procedure.Alan Mishchenko2017-03-011-1/+1
|
* Adding efficient procedure to minimize the set of assumptions.Alan Mishchenko2017-03-012-0/+53
|
* Fixing missing sat_solver APIs in 'iprove'.Alan Mishchenko2017-02-161-6/+24
|
* Fixing missing sat_solver APIs in 'iprove'.Alan Mishchenko2017-02-151-3/+40
|
* Commenting out uncommented message.Alan Mishchenko2017-02-111-1/+1
|
* Updates to variable activity in the SAT solver.Alan Mishchenko2017-02-112-342/+224
|
* Movinng custom floating-point implementations, etc.Alan Mishchenko2017-02-111-1/+2
|
* Re-introducing floating-point activity in the SAT solver.Alan Mishchenko2017-02-071-2/+18
|
* Re-introducing floating-point activity in the SAT solver.Alan Mishchenko2017-02-062-39/+171
|
* Improvements to inductive generalization in IC3/PDR by Zyad Hassan.Alan Mishchenko2017-02-022-0/+122
|
* Updates to delay optimization project.Alan Mishchenko2016-12-291-1/+6
|
* Fixes and adjustments for the edge computation flow.Alan Mishchenko2016-07-151-1/+1
|
* Experiments with edge-based mapping.Alan Mishchenko2016-06-151-2/+3
|
* Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.Alan Mishchenko2016-05-192-1/+2
|
* This code was accidentally deleted from the SAT solver (effectively ↵Alan Mishchenko2016-04-301-0/+7
| | | | disabling restarts!)
* Improved algo for edge computation.Alan Mishchenko2016-04-232-1/+14
|
* Adding new implementation of LEXSAT.Alan Mishchenko2016-04-122-0/+69
|
* Restructing sat_solver_solve() method for pushing/popping assumptions.Alan Mishchenko2016-04-123-151/+153
|
* Removing unused feature of the SAT solver (user-guided variable ordering).Alan Mishchenko2016-04-122-53/+1
|
* Removing unused feature of the SAT solver (native support for cardinality ↵Alan Mishchenko2016-04-123-33/+2
| | | | constraint).
* Improvements to delay-optimization in &satlut.Alan Mishchenko2016-04-041-1/+8
|
* Experiments with SAT-based mapping.Alan Mishchenko2016-02-071-0/+23
|
* Experiments with SAT-based mapping.Alan Mishchenko2016-01-101-0/+9
|
* Adding support of candinality clause to the SAT solver.Alan Mishchenko2016-01-103-3/+35
|
* Added comment how to print binary clauses in procedure Sat_SolverWriteDimacs().Alan Mishchenko2015-10-161-1/+4
|
* Tuning SAT solver for QBF instances.Alan Mishchenko2015-09-181-4/+6
|
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-042-1/+8
|
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-032-8/+51
|
* Bug fix in QBF solver.Alan Mishchenko2015-05-041-0/+4
|
* Experiments with SAT-based cube enumeration.Alan Mishchenko2015-03-051-19/+19
|
* Compiler warnings.Alan Mishchenko2015-02-191-1/+1
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-28 19:28:20 +0000