summaryrefslogtreecommitdiffstats
path: root/src/proof
Commit message (Collapse)AuthorAgeFilesLines
* Compiler warnings.Alan Mishchenko2012-08-261-1/+1
|
* Compiler warnings.Alan Mishchenko2012-08-241-1/+1
|
* Added simulation of comb circuits with user-specified patterns in command 'sim'.Alan Mishchenko2012-08-245-11/+159
|
* Fixing interpolation to run without resource limits by default.Alan Mishchenko2012-07-251-1/+1
|
* Removed unused files from the project.Alan Mishchenko2012-07-254-5/+2
|
* Fixing compiler warning.Alan Mishchenko2012-07-131-0/+1
|
* Upgraded &equiv3 to periodically restart simulation from the init state.Alan Mishchenko2012-07-121-7/+24
|
* Improvements in the proof-logging SAT solver.Alan Mishchenko2012-07-112-8/+8
|
* Replacing Mb/Gb to be MB/GB.Alan Mishchenko2012-07-095-6/+6
|
* Adding several command-line arguments to 'dsat'.Alan Mishchenko2012-07-093-9/+16
|
* Adding restart to rarity simulation in sim3 and &sim3.Alan Mishchenko2012-07-082-18/+39
|
* Adding flushing stdout after printing verbose stats.Alan Mishchenko2012-07-072-0/+2
|
* Updating project settings to have simpler include paths.Alan Mishchenko2012-07-0740-86/+86
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-071-1/+1
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-073-6/+9
|
* Fixing time primtouts throughout the code.Alan Mishchenko2012-07-0782-311/+409
|
* Making 'pdr', &gla, &vta print correctly in batch mode.Alan Mishchenko2012-07-072-3/+6
|
* Fixing time printouts in 'pdr'.Alan Mishchenko2012-07-072-2/+2
|
* Fixing time printouts in 'pdr'.Alan Mishchenko2012-07-076-22/+21
|
* Fixing time printouts in 'pdr'.Alan Mishchenko2012-07-072-13/+13
|
* Setting infinite default conflict limits in 'bmc', 'int', 'pdr'.Alan Mishchenko2012-07-062-4/+4
|
* Various changes to enable sensitization-based refinement in &gla.Alan Mishchenko2012-07-042-3/+3
|
* Added min-cut-based refinement of gate-level abstraction (command &gla_refine).Alan Mishchenko2012-06-241-0/+3
|
* Disallow the circiut-based solver in &scorr to run with more than 1000 ↵Alan Mishchenko2012-04-241-0/+3
| | | | conflicts.
* Misc changes.Alan Mishchenko2012-04-221-3/+3
|
* Renamed Aig_ObjPioNum to be Aig_ObjCioId.Alan Mishchenko2012-03-0914-33/+33
|
* Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)...Alan Mishchenko2012-03-0972-409/+409
|
* Renamed Aig_ManForEachPi/Po to be ...Ci/Co and Aig_ObjCreatePi/Po to be ↵Alan Mishchenko2012-03-0950-263/+263
| | | | ...Ci/Co.
* Silencing remaining gcc warnings.Alan Mishchenko2012-03-091-19/+19
|
* Silencing remaining gcc warnings.Alan Mishchenko2012-03-092-13/+13
|
* Redirecting printf messages.Alan Mishchenko2012-03-021-2/+2
|
* Redirecting printf messages.Alan Mishchenko2012-03-026-55/+50
|
* Bug fix in 'in' (look at the OR of the interpolants, rather than the last ↵Alan Mishchenko2012-02-281-0/+4
| | | | frontier, when K > 1).
* Disabled verbose print-out in the SAT solvers.Alan Mishchenko2012-02-261-2/+2
|
* Isomorphism checking code.Alan Mishchenko2012-02-191-1/+1
|
* Added printout of BMC tents in &ps.Alan Mishchenko2012-02-191-1/+1
|
* Silencing some of the gcc warnings.Alan Mishchenko2012-02-173-4/+4
|
* Silencing some of the gcc warnings.Alan Mishchenko2012-02-1622-38/+37
|
* Improved memory management of proof-logging and propagated changes.Alan Mishchenko2012-02-161-2/+2
|
* Isomorphism checking code.Alan Mishchenko2012-02-141-18/+0
|
* Added restarts to PDR.Alan Mishchenko2012-02-141-1/+1
|
* Added restarts to PDR.Alan Mishchenko2012-02-135-15/+35
|
* Timeout crash fix in 'reachy'.Alan Mishchenko2012-02-131-5/+16
|
* Bug fixes in &cec command.Alan Mishchenko2012-02-101-29/+83
|
* Trying to fix a false-positive due to incorrect inductive termination check ↵Alan Mishchenko2012-02-011-3/+9
| | | | in 'int' when K is more than 1 (not fixed yet).
* Bug fix for incorrect memory allocation in main SAT solver, leading to ↵Alan Mishchenko2012-01-231-1/+1
| | | | crashes in 'dsec' (correction to the previous fix).
* Bug fix for incorrect memory allocation in main SAT solver, leading to ↵Alan Mishchenko2012-01-222-2/+2
| | | | crashes in 'dsec'.
* Major restructuring of the code.Alan Mishchenko2012-01-21156-0/+67230