summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver2.c
Commit message (Expand)AuthorAgeFilesLines
* Adding an option to bmc3 to use Satoko intead of the default SAT solver.Alan Mishchenko2017-08-131-1/+1
* Compiler warnings.Alan Mishchenko2015-02-191-1/+1
* Adding interpolant computation sat_solver2.Alan Mishchenko2013-09-021-1/+16
* 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-11/+11
* Changing how often timeout is checked in the SAT solver and several applicati...Alan Mishchenko2013-05-271-1/+1
* Adding rollback for the other solver.Alan Mishchenko2013-04-251-2/+2
* C++ portability changes.Alan Mishchenko2012-10-031-1/+3
* Reversed to a buggy version of reduceDB in complete proof-logging, because it...Alan Mishchenko2012-09-121-2/+2
* Changes to allow &gla to run with fSimple = 1 (useful for debugging).Alan Mishchenko2012-08-311-0/+1
* Bug fix in &gla.Alan Mishchenko2012-08-271-3/+12
* Scalable gate-level abstraction.Alan Mishchenko2012-08-021-0/+12
* Saving variable activity during rollback.Alan Mishchenko2012-07-301-0/+3
* Saving variable activity during rollback.Alan Mishchenko2012-07-301-0/+6
* Disabling learned clause removal when incremental proof-logging is running (t...Alan Mishchenko2012-07-301-1/+1
* Reducing memory usage in proof-based abstraction.Alan Mishchenko2012-07-291-28/+61
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+4
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+2
* Several small changes and fixes.Alan Mishchenko2012-07-131-3/+7
* Added procedure for checking satisfied clauses.Alan Mishchenko2012-07-121-0/+37
* Silencing warnings.Alan Mishchenko2012-07-111-1/+1
* Silencing warnings.Alan Mishchenko2012-07-111-3/+1
* Changes to clause mapping.Alan Mishchenko2012-07-111-1/+6
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-111-307/+302
* Improving print-outs of &vta and &gla.Alan Mishchenko2012-07-101-0/+1
* Performance bug fix in the SAT solver (clearing variable activity after rollb...Alan Mishchenko2012-07-101-10/+0
* Performance bug fix in the SAT solver (clearing variable activity after rollb...Alan Mishchenko2012-07-091-0/+7
* Performance bug fix in the SAT solver (clearing variable activity after rollb...Alan Mishchenko2012-07-091-0/+3
* Replacing Mb/Gb to be MB/GB.Alan Mishchenko2012-07-091-1/+1
* Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat...Alan Mishchenko2012-07-091-49/+49
* Updating memory print-out of &vta and &gla.Alan Mishchenko2012-07-081-3/+4
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-1/+2
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-3/+4
* Added memory reporting to &vta.Alan Mishchenko2012-06-221-1/+51
* Switching to a variable-page-size memory manager for clauses and proofs.Alan Mishchenko2012-03-211-1/+1
* Some fixes for VTA under Bridge.Niklas Een2012-03-031-81/+80
* Added QuickSort based on 3-way partitioning.Alan Mishchenko2012-02-191-1/+1
* Silencing some of the gcc warnings.Alan Mishchenko2012-02-171-1/+1
* Silencing some of the gcc warnings.Alan Mishchenko2012-02-171-2/+2
* 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-6/+7
* Improved memory management of proof-logging and propagated changes.Alan Mishchenko2012-02-161-64/+72
* Variable timeframe abstraction.Alan Mishchenko2012-02-131-23/+23
* Variable timeframe abstraction.Alan Mishchenko2012-02-131-2/+6
* Variable timeframe abstraction.Alan Mishchenko2012-02-131-16/+19
* Variable timeframe abstraction.Alan Mishchenko2012-02-121-67/+48
* Variable timeframe abstraction.Alan Mishchenko2012-02-111-9/+28
* Variable timeframe abstraction.Alan Mishchenko2012-01-281-13/+17
* Variable timeframe abstraction.Alan Mishchenko2012-01-271-196/+98
* Variable timeframe abstraction.Alan Mishchenko2012-01-241-15/+40