aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Predicate.v
Commit message (Collapse)AuthorAgeFilesLines
* Rearrange definitions and create IfConversion templateYann Herklotz2022-06-061-0/+12
|
* Fix many more lemmasYann Herklotz2022-06-051-0/+9
|
* Work on CondElim proofYann Herklotz2022-06-031-3/+3
|
* Abstract useful function into Predicate.vYann Herklotz2022-05-311-0/+7
|
* Improve simplification of predicatesYann Herklotz2021-11-141-2/+10
|
* Add the tseytin transformation insteadYann Herklotz2021-11-141-210/+359
|
* Improve simplification of predicatesYann Herklotz2021-11-131-57/+80
|
* Add simplify operation and simplify IfConversionYann Herklotz2021-11-111-0/+58
|
* Add intermediate step in proof of sem presYann Herklotz2021-10-271-0/+26
|
* Work more on equivalence of SATYann Herklotz2021-10-261-0/+15
|
* Add type-class proofs to Predicate.vYann Herklotz2021-10-241-4/+207
|
* Add work towards decidability of SAT solverYann Herklotz2021-10-211-0/+201