aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
* Add proper functional unit generationYann Herklotz2021-11-142-23/+98
* Add helper functions to FunctionalUnitsYann Herklotz2021-11-141-0/+74
* Add the tseytin transformation insteadYann Herklotz2021-11-142-219/+359
* Add RTLPar with functional unitsYann Herklotz2021-11-133-0/+1302
* Add commented out pretty printing for AbstrYann Herklotz2021-11-131-0/+39
* Move lp_solve to the /temp directoryYann Herklotz2021-11-131-4/+6
* Small progress on the proof of correctnessYann Herklotz2021-11-131-1/+5
* Simplify the RTLPargen update functionYann Herklotz2021-11-131-11/+21
* Fix pretty printing of predicatesYann Herklotz2021-11-131-3/+3
* Improve simplification of predicatesYann Herklotz2021-11-131-57/+80
* Prove some of the theorems furtherYann Herklotz2021-11-111-14/+17
* Add documentation to RTLPargenYann Herklotz2021-11-111-18/+72
* Add documentation to RTLBlockInstrYann Herklotz2021-11-111-11/+62
* Add simplify operation and simplify IfConversionYann Herklotz2021-11-112-4/+60
* Fix the scheduler to not remove dead codeYann Herklotz2021-11-111-1/+1
* Uncomment many more proofsYann Herklotz2021-11-022-917/+752
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2021-11-021-8/+6
|\
| * Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2021-11-014-170/+335
| |\
| * | [sched] Simplify some of the Lemma statementsYann Herklotz2021-11-011-8/+6
* | | No admitted theorems in RTLPargenproof.vYann Herklotz2021-11-022-13/+14
| |/ |/|
* | Add work on RTLPargenproof.vYann Herklotz2021-11-012-140/+165
* | Add RTLBlockInstr proofsYann Herklotz2021-11-011-0/+23
* | Add Admitted theorems for existence proofsYann Herklotz2021-11-011-9/+2
* | Add construction of state in semYann Herklotz2021-10-311-23/+147
|/
* Fix compilation issues with new typesYann Herklotz2021-10-304-46/+37
* Make Abstr pass with admitted to check top-levelYann Herklotz2021-10-301-45/+110
* Add a predicate to RBsetpredYann Herklotz2021-10-303-6/+6
* Remove admitted from subproofYann Herklotz2021-10-291-6/+57
* Add intermediate step in proof of sem presYann Herklotz2021-10-272-24/+108
* Work more on equivalence of SATYann Herklotz2021-10-263-34/+137
* Continue on semantics preservation proofYann Herklotz2021-10-241-198/+178
* Fix if-conversion and translation with PlitYann Herklotz2021-10-242-5/+5
* Add type-class proofs to Predicate.vYann Herklotz2021-10-242-12/+217
* Add setoid typeclassYann Herklotz2021-10-211-15/+21
* Add work towards decidability of SAT solverYann Herklotz2021-10-216-279/+377
* Start to prove termination of SATYann Herklotz2021-10-203-244/+266
* Continuations on proof of predicatesYann Herklotz2021-10-192-127/+151
* [sched] Fix passes with new predicatesYann Herklotz2021-10-142-1/+3
* [sched] Add combination of equivalent expressionsYann Herklotz2021-10-141-10/+40
* [sched] Add true and false predicates to typeYann Herklotz2021-10-141-1/+23
* [sched] Finish det proofs of basic Abstr semanticsYann Herklotz2021-10-131-27/+44
* [sched] Add more proof to sem_pred_detYann Herklotz2021-10-131-1/+6
* [sched] Add proofs of sem_pred_detYann Herklotz2021-10-131-8/+44
* [sched] Add start to proof of sem_value_detYann Herklotz2021-10-121-0/+12
* [sched] Remove unnecessary importsYann Herklotz2021-10-121-11/+0
* [sched] Add more lemmas into HashTreeYann Herklotz2021-10-122-10/+37
* [sched] Update Abstr.v to use HashTreeYann Herklotz2021-10-121-29/+97
* [sched] Add HashTree.v for hashing arbitrary valuesYann Herklotz2021-10-121-0/+413
* Merge branch 'dev/scheduling' of git.ymhg.org:vericert into dev/schedulingYann Herklotz2021-10-129-70/+84
|\
| * Fix warnings for Coq 8.13.2Yann Herklotz2021-10-099-70/+84
generated by cgit (git 2.34.1) at 2024-07-02 20:40:59 +0000