summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
Commit message (Collapse)AuthorAgeFilesLines
* 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 ↵Alan Mishchenko2013-09-161-0/+31
| | | | opposed to when the literal first implied in enqueue().
* 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 ↵Alan Mishchenko2013-05-272-2/+2
| | | | application packages.
* 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
|
* SAT variable profiling.Alan Mishchenko2013-05-182-0/+16
|
* Adding rollback for the other solver.Alan Mishchenko2013-04-253-3/+141
|
* Fixing the dump of SAT solver into a CNF file.Alan Mishchenko2013-03-263-17/+18
|
* Compiler warnings.Alan Mishchenko2013-02-232-0/+5
|
* Fixing compilation problems on Linux-32 related to constants of type ↵Alan Mishchenko2013-01-301-6/+6
| | | | unsigned long long.
* Increasing memory page limit in the main SAT solver.Alan Mishchenko2012-10-311-1/+1
|
* C++ portability changes.Alan Mishchenko2012-10-032-2/+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-273-5/+16
|
* Scalable gate-level abstraction.Alan Mishchenko2012-08-021-0/+12
|
* Scalable gate-level abstraction.Alan Mishchenko2012-07-311-1/+1
|
* Saving variable activity during rollback.Alan Mishchenko2012-07-302-0/+7
|
* Saving variable activity during rollback.Alan Mishchenko2012-07-302-1/+10
|
* Disabling learned clause removal when incremental proof-logging is running ↵Alan Mishchenko2012-07-301-1/+1
| | | | (tends to generate smaller abstarctions).
* Fixing performance bug with old proof-logging (adding clauses multiple times).Alan Mishchenko2012-07-301-0/+1
|
* Fixed compiler warnings.Alan Mishchenko2012-07-291-2/+2
|
* Reducing memory usage in proof-based abstraction.Alan Mishchenko2012-07-293-30/+393
|
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-281-37/+49
|
* Fixed the problem with 'write_cnf' after recent changes to the SAT solver.Alan Mishchenko2012-07-282-65/+89
|
* 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-222-1/+19
|
* Debugging a proof error.Alan Mishchenko2012-07-132-12/+7
|
* Debugging a proof error.Alan Mishchenko2012-07-131-2/+2
|
* Debugging a proof error.Alan Mishchenko2012-07-131-0/+2
|
* Debugging a proof error.Alan Mishchenko2012-07-131-25/+9
|