aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
Commit message (Expand)AuthorAge
* Coq 8.5 can't handle symbol-free notationsGravatar Jason Gross2017-10-06
* Clean up TestCase a bitGravatar Jason Gross2017-10-06
* Add another constantGravatar Jason Gross2017-10-06
* Make some typeclasses opaqueGravatar Jason Gross2017-10-02
* Speed up reification a little bitGravatar Jason Gross2017-10-02
* Update constants filesGravatar Jason Gross2017-09-21
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
* Fix CSE_sym denoteGravatar Jason Gross2017-07-07
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
* Stronger contextsGravatar Jason Gross2017-07-07
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
* Fix a mis-aligned comment marker in CNotations scriptGravatar Jason Gross2017-07-03
* change notation `_ == _ ? _ : _ ` to `cmovznz(_, _, _)`Gravatar Jason Gross2017-06-29
* Fix comment-in-string issuesGravatar Jason Gross2017-06-29
* More C Notations for uin8_t-valued addcarryxGravatar Jason Gross2017-06-29
* Remove a [Check]Gravatar Jason Gross2017-06-29
* Add nonzero synthesisGravatar Jason Gross2017-06-26
* Allow disabling adc-fusionGravatar Jason Gross2017-06-25
* Convert adc to sbb when doing [0 - x]Gravatar Jason Gross2017-06-25
* Revert "Convert adc to sbb when doing [0 - x]"Gravatar Jason Gross2017-06-25
* Convert adc to sbb when doing [0 - x]Gravatar Jason Gross2017-06-24
* Propogate neg through constant multiplicationGravatar Jason Gross2017-06-24
* Add notation for logical orGravatar Jason Gross2017-06-22
* Work around bug #5615 (constr not being updated)Gravatar Jason Gross2017-06-22
* Also key adc->sbb on the carry-bit being negativeGravatar Jason Gross2017-06-20
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
* Add more Z-notationsGravatar Jason Gross2017-06-20
* Add another fusion to adc-fusionGravatar Jason Gross2017-06-20
* Use solve_wf_side_condition to synch the depth of auto with wfGravatar Jason Gross2017-06-20
* Add more constant notationsGravatar Jason Gross2017-06-20
* Add more constantsGravatar Jason Gross2017-06-18
* Better simplification of mulsplitGravatar Jason Gross2017-06-18
* Fix typo in formatGravatar Jason Gross2017-06-18
* Add fake notation for addcarryx_u128 and similarGravatar Jason Gross2017-06-18
* Add some notations for mulxGravatar Jason Gross2017-06-18
* Better test for simplifierGravatar Jason Gross2017-06-18
* Stronger simplification of adc too add when we can prove the carry is 0Gravatar Jason Gross2017-06-18
* Add cnotations for addcarryx with uint8_tGravatar Jason Gross2017-06-18
* Add convenience for supporting uint8Gravatar Jason Gross2017-06-18
* Add notationsGravatar Jason Gross2017-06-18
* Adding more (possibly unneeded) simplificationGravatar Jason Gross2017-06-18
* Try more simplificationGravatar Jason Gross2017-06-17
* Drop the 0-carry bit before bounds analysisGravatar Jason Gross2017-06-17
* Be a bit more forceful in eliminating zeros in arith simplGravatar Jason Gross2017-06-17
* More arithmetic simplification for adc, mulGravatar Jason Gross2017-06-17
* Add more simplification to pipelineGravatar Jason Gross2017-06-17
* Add linearization to inline pairs in post-bounds pipelineGravatar Jason Gross2017-06-17
* Add extra simplification to simplifier for adcGravatar Jason Gross2017-06-17
* Add more constantsGravatar Jason Gross2017-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 17:12:11 +0000