summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver2.c
Commit message (Collapse)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 ↵Alan Mishchenko2013-05-271-1/+1
| | | | application packages.
* 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 ↵Alan Mishchenko2012-09-121-2/+2
| | | | it works with rollback and it is not used in &gla -pn -L 0.
* 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 ↵Alan Mishchenko2012-07-301-1/+1
| | | | (tends to generate smaller abstarctions).
* 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 ↵Alan Mishchenko2012-07-101-10/+0
| | | | rollback).
* Performance bug fix in the SAT solver (clearing variable activity after ↵Alan Mishchenko2012-07-091-0/+7
| | | | rollback).
* Performance bug fix in the SAT solver (clearing variable activity after ↵Alan Mishchenko2012-07-091-0/+3
| | | | rollback).
* 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, ↵Alan Mishchenko2012-07-091-49/+49
| | | | dsat, etc).
* 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
|