summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
Commit message (Expand)AuthorAgeFilesLines
* 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 disabling...Alan Mishchenko2016-04-301-0/+7
* 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 con...Alan Mishchenko2016-04-123-33/+2
* 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
* Compiler warnings.Alan Mishchenko2014-10-281-2/+2
* Adding command to dump UNSAT core of BMC instance.Alan Mishchenko2014-04-075-16/+76
* Adding switch to handle only single faults.Alan Mishchenko2014-04-011-4/+4
* Changes to LUT mappers.Alan Mishchenko2014-03-041-0/+64
* Changes to LUT mappers.Alan Mishchenko2014-02-271-0/+46
* Specialized induction check.Alan Mishchenko2013-10-311-0/+39
* Specialized induction check.Alan Mishchenko2013-10-311-0/+19
* Compiler warning about unused variable.Alan Mishchenko2013-09-171-2/+2
* Changing dynamic CNF loading code to perform loading before propagate() as op...Alan Mishchenko2013-09-161-0/+31
* Corrected variable naming in clause2_proofid().Alan Mishchenko2013-09-111-1/+1
* Unifying parameters for the &ps command.Alan Mishchenko2013-09-051-1/+1
* Adding interpolant computation sat_solver2.Alan Mishchenko2013-09-021-0/+242
* Adding interpolant computation sat_solver2.Alan Mishchenko2013-09-023-1/+28
* Bug fix in 'int'.Alan Mishchenko2013-08-051-2/+2
* Bug fix in 'int'.Alan Mishchenko2013-08-051-42/+35
* SAT solver with dynamic CNF loading.Alan Mishchenko2013-08-012-4/+34
* Bug fix in the timeout for 'int'.Alan Mishchenko2013-07-011-1/+1
* Adding timeout to the interpolant computation procedure.Alan Mishchenko2013-06-282-2/+19
* Limiting runtime limit checks in 'pdr'.Alan Mishchenko2013-06-212-2/+2
* Adding a wrapper around clock() for more accurate time counting in ABC.Alan Mishchenko2013-05-279-86/+86
* Changing how often timeout is checked in the SAT solver and several applicati...Alan Mishchenko2013-05-272-2/+2
* SAT variable profiling.Alan Mishchenko2013-05-182-4/+4
* SAT variable profiling.Alan Mishchenko2013-05-183-3/+27
* SAT variable profiling (undo).Alan Mishchenko2013-05-182-16/+0
* SAT variable profiling.Alan Mishchenko2013-05-182-0/+16
* SAT variable profiling (undo).Alan Mishchenko2013-05-182-16/+0