summaryrefslogtreecommitdiffstats
path: root/src/sat
Commit message (Collapse)AuthorAgeFilesLines
* Changing per-output runtime limit to be in miliseconds.Alan Mishchenko2013-05-091-2/+2
|
* Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>).Alan Mishchenko2013-05-031-1/+3
|
* Adding runtime limit per output to multi-output BMC (bmc3 -H <num_sec>).Alan Mishchenko2013-05-032-10/+45
|
* Adding rollback for the other solver.Alan Mishchenko2013-04-253-3/+141
|
* Adding callback to bmc3, sim3, pdr in the multi-output mode.Alan Mishchenko2013-04-172-8/+14
|
* Added switch '-x' to save CEXes in 'bmc3' and 'pdr' in multi-output mode.Alan Mishchenko2013-04-092-13/+34
|
* Updating bmc3 printout to show the number of failed outputs.Alan Mishchenko2013-03-301-14/+12
|
* Updating bmc3 printout to show the number of failed outputs.Alan Mishchenko2013-03-301-5/+11
|
* Compiler warnings.Alan Mishchenko2013-03-301-3/+3
|
* Updating bmc3 printout to show the number of failed outputs.Alan Mishchenko2013-03-301-4/+6
|
* Added dumping QDIMACS files in command 'qbf'.Alan Mishchenko2013-03-272-6/+34
|
* Fixing the dump of SAT solver into a CNF file.Alan Mishchenko2013-03-263-17/+18
|
* Fixing gap timeout in 'bmc3'.Alan Mishchenko2013-03-131-6/+40
|
* Making 'bmc3' with switch '-a' not save CEXes.Alan Mishchenko2013-03-071-13/+13
|
* User-controlable SAT sweeper and other small changes.Alan Mishchenko2013-02-271-2/+1
|
* Compiler warnings.Alan Mishchenko2013-02-232-0/+5
|
* Compiler warnings.Alan Mishchenko2013-02-211-3/+3
|
* Added 'gap timeout' to bmc3 and sim3.Alan Mishchenko2013-02-161-0/+1
|
* Added 'gap timeout' to bmc3 and sim3.Alan Mishchenko2013-02-152-0/+12
|
* Fixing compilation problems on Linux-32 related to constants of type ↵Alan Mishchenko2013-01-302-12/+12
| | | | unsigned long long.
* Enabled detecting CEXes in multiple POs without stopping (sim3 -a).Alan Mishchenko2013-01-232-4/+8
|
* New unrolling manager.Alan Mishchenko2012-12-242-1/+457
|
* Unifification of custom extensions.Alan Mishchenko2012-12-102-4/+4
|
* Counter-example analysis and optimization.Alan Mishchenko2012-12-011-64/+258
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-301-3/+1
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-301-17/+21
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-301-12/+78
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-291-0/+590
|
* Counter-example analysis and optimization.Alan Mishchenko2012-11-281-1/+2
|
* Added switch 'cexcut -m' to generate bad states for all frames after G.Alan Mishchenko2012-11-152-10/+139
|
* Added switch 'cexcut -n' to generate only one bad state.Alan Mishchenko2012-11-152-24/+238
|
* Added command 'cexcut' and 'cexmerge'.Alan Mishchenko2012-11-142-12/+15
|
* Added command 'cexcut' and 'cexmerge'.Alan Mishchenko2012-11-142-16/+52
|
* Added command 'cexcut' and 'cexmerge'.Alan Mishchenko2012-11-141-2/+102
|
* Added command 'cexsave' and 'cexload'.Alan Mishchenko2012-11-146-8/+12
|
* Isolating BMC code into a separate package.Alan Mishchenko2012-11-149-0/+3941
|
* Increasing memory page limit in the main SAT solver.Alan Mishchenko2012-10-311-1/+1
|
* Making explicit cast to 64-bit unsigned in a few places.Alan Mishchenko2012-10-091-2/+2
|
* C++ portability changes.Alan Mishchenko2012-10-032-2/+3
|
* Added delay multipliers to 'map'.Alan Mishchenko2012-09-161-1/+1
|
* Prepared &gla to try abstracting and proving concurrently.Alan Mishchenko2012-09-142-51/+47
|
* 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
|