summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver.c
Commit message (Expand)AuthorAgeFilesLines
* Updates to variable activity in the SAT solver.Alan Mishchenko2017-02-111-286/+193
* 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-061-39/+135
* Improvements to inductive generalization in IC3/PDR by Zyad Hassan.Alan Mishchenko2017-02-021-0/+120
* 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-191-1/+1
* 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-231-0/+13
* Adding new implementation of LEXSAT.Alan Mishchenko2016-04-121-0/+68
* Restructing sat_solver_solve() method for pushing/popping assumptions.Alan Mishchenko2016-04-121-142/+134
* Removing unused feature of the SAT solver (user-guided variable ordering).Alan Mishchenko2016-04-121-41/+1
* Removing unused feature of the SAT solver (native support for cardinality con...Alan Mishchenko2016-04-121-21/+2
* Improvements to delay-optimization in &satlut.Alan Mishchenko2016-04-041-1/+8
* Adding support of candinality clause to the SAT solver.Alan Mishchenko2016-01-101-2/+23
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-041-1/+1
* Experiments with SAT-based collapsing.Alan Mishchenko2015-09-031-8/+40
* Adding command to dump UNSAT core of BMC instance.Alan Mishchenko2014-04-071-0/+8
* 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
* SAT solver with dynamic CNF loading.Alan Mishchenko2013-08-011-4/+28
* Limiting runtime limit checks in 'pdr'.Alan Mishchenko2013-06-211-1/+1
* Adding a wrapper around clock() for more accurate time counting in ABC.Alan Mishchenko2013-05-271-12/+12
* Changing how often timeout is checked in the SAT solver and several applicati...Alan Mishchenko2013-05-271-1/+1
* SAT variable profiling.Alan Mishchenko2013-05-181-2/+2
* SAT variable profiling.Alan Mishchenko2013-05-181-1/+11
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-14/+0
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+14
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-14/+0
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+14
* Adding rollback for the other solver.Alan Mishchenko2013-04-251-1/+118
* Fixing the dump of SAT solver into a CNF file.Alan Mishchenko2013-03-261-1/+2
* Compiler warnings.Alan Mishchenko2013-02-231-0/+4
* Increasing memory page limit in the main SAT solver.Alan Mishchenko2012-10-311-1/+1
* Recording and reusing learned util clauses in bmc2.Alan Mishchenko2012-07-221-0/+1
* Recording and reusing learned util clauses in bmc3.Alan Mishchenko2012-07-221-0/+16
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-111-10/+4
* Improving print-outs of &vta and &gla.Alan Mishchenko2012-07-101-1/+3
* Bug fix in the recent changes to the SAT solver.Alan Mishchenko2012-07-091-0/+3
* Removing print-out message.Alan Mishchenko2012-07-091-1/+1
* Adding several command-line arguments to 'dsat'.Alan Mishchenko2012-07-091-6/+12
* Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat...Alan Mishchenko2012-07-091-190/+217
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-1/+2
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-2/+2
* Added memory reporting to &vta.Alan Mishchenko2012-06-221-2/+3
* Reporing memory usage by the SAT solver in 'bmc3'.Alan Mishchenko2012-06-151-0/+35
* Switching to a variable-page-size memory manager for clauses and proofs.Alan Mishchenko2012-03-211-1/+1
* Silencing some of the gcc warnings.Alan Mishchenko2012-02-161-4/+4
* Improved memory management of proof-logging and propagated changes.Alan Mishchenko2012-02-161-34/+19
* Improving printout in the SAT solver.Alan Mishchenko2012-01-131-1/+2