aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Add RTLParFU to top-levelYann Herklotz2021-11-141-0/+2
|
* Replace HTLPargen by HTLParFUgenYann Herklotz2021-11-142-896/+19
|
* Improve simplification of predicatesYann Herklotz2021-11-141-2/+10
|
* 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
|
generated by cgit (git 2.34.1) at 2024-07-07 21:11:39 +0000