summaryrefslogtreecommitdiffstats
path: root/src/proof
Commit message (Collapse)AuthorAgeFilesLines
* Experiments with simulation.Alan Mishchenko2017-02-141-0/+194
|
* Adding PDR with abstraction.Alan Mishchenko2017-02-131-5/+5
|
* Adding PDR with abstraction.Alan Mishchenko2017-02-111-1/+10
|
* Adding PDR with abstraction.Alan Mishchenko2017-02-113-41/+11
|
* Adding PDR with abstraction.Alan Mishchenko2017-02-105-13/+39
|
* Compiler warnings.Alan Mishchenko2017-02-101-1/+1
|
* Adding PDR with abstraction.Alan Mishchenko2017-02-105-71/+221
|
* Re-introducing floating-point activity in the SAT solver.Alan Mishchenko2017-02-103-0/+5
|
* Standardizing the use of new CNF generator. Adding CNF variable connectivity ↵Alan Mishchenko2017-02-102-7/+4
| | | | information.
* Making sure 'inv_out' can match flops by name.Alan Mishchenko2017-02-091-0/+2
|
* Adding specialized flop ordering before generalization in 'pdr'.Alan Mishchenko2017-02-062-1/+32
|
* Improving new X-valued simulation in 'pdr'.Alan Mishchenko2017-02-063-13/+176
|
* Compiler warnings.Alan Mishchenko2017-02-051-18/+22
|
* Adding structural flop priority heuristics in 'pdr' (bug fix).Alan Mishchenko2017-02-031-9/+126
|
* Adding structural flop priority heuristics in 'pdr'.Alan Mishchenko2017-02-037-120/+208
|
* Removing dead code in 'pdr'.Alan Mishchenko2017-02-034-81/+0
|
* Enabling new X-valued simulation in 'pdr'.Alan Mishchenko2017-02-038-3/+414
|
* Improvements to inductive generalization in IC3/PDR by Zyad Hassan.Alan Mishchenko2017-02-026-9/+342
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-304-5/+400
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-294-143/+152
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-285-10/+422
|
* Adding features for invariant minimization.Alan Mishchenko2017-01-251-2/+2
|
* Adding features for invariant minimization.Alan Mishchenko2017-01-251-3/+13
|
* Adding features for invariant minimization.Alan Mishchenko2017-01-251-0/+2
|
* Adding features for invariant minimization.Alan Mishchenko2017-01-251-29/+73
|
* Adding features for invariant minimization.Alan Mishchenko2017-01-241-16/+27
|
* Adding features for invariant minimization.Alan Mishchenko2017-01-241-10/+71
|
* Adding features for invariant minimization.Alan Mishchenko2017-01-243-4/+230
|
* Fix mismatch in output formatting.Alan Mishchenko2017-01-213-8/+8
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-193-24/+90
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-165-30/+55
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-157-23/+359
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-145-28/+157
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-146-94/+171
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-133-268/+298
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-132-2/+63
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-124-9/+452
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-116-214/+297
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-114-31/+257
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-103-4/+283
|
* Updates to arithmetic verification.Alan Mishchenko2017-01-108-47/+71
|
* Updated to arithmetic verification.Alan Mishchenko2017-01-094-11/+421
|
* Compiler warnings.Alan Mishchenko2017-01-071-1/+1
|
* Creating file name from design name for PDR invariant.Alan Mishchenko2017-01-061-1/+2
|
* C++ compatibility fix.Alan Mishchenko2016-12-281-0/+2
|
* Several changes in arithmetic circuit manipulation.Alan Mishchenko2016-12-223-1/+311
|
* Bug fix in 'dsat <file.cnf>' when the number of classes in listed incorrectly.Alan Mishchenko2016-12-131-0/+204
|
* Compiler warnings.Alan Mishchenko2016-12-051-1/+1
|
* Analysis of arithmetic logic cones.Alan Mishchenko2016-12-044-18/+351
|
* Changes to arithmetic logic detection.Alan Mishchenko2016-12-026-59/+724
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-02 02:42:36 +0000