aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
Commit message (Expand)AuthorAge
* 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
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* Add some more display constantsGravatar Jason Gross2017-06-17
* Add bool into P256Gravatar Jason Gross2017-06-17
* Remove fails; if we fail too strongly, we miss debugging informationGravatar Jason Gross2017-06-17
* Try to fail a bit faster in bad reificationGravatar Jason Gross2017-06-17
* Add back failure at level 100Gravatar Jason Gross2017-06-17
* Better error messages in reificationGravatar Jason Gross2017-06-17
* Better reification tactic debuggingGravatar Jason Gross2017-06-17
* Revert PR #203Gravatar Jason Gross2017-06-16
* Fix CArrayNotationsGravatar Jason Gross2017-06-16
* Revert "Revert "Add CArrayNotations""Gravatar Jason Gross2017-06-16
* Revert "Add CArrayNotations"Gravatar Jason Gross2017-06-15
* Add CArrayNotationsGravatar Jason Gross2017-06-15
* Display Z operations with ℤ attachedGravatar Jason Gross2017-06-15
* Eliminate well-bounded IdWithAlt from final outputGravatar Jason Gross2017-06-15
* Fix debugging codeGravatar Jason Gross2017-06-15
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
* Add constant-pushing IdWithAlt optimizationGravatar Jason Gross2017-06-14
* Rework and speed up arithmetic simplifier proofsGravatar Jason Gross2017-06-14
* Make rewrite_eta_match_base_type_impl a bit fasterGravatar Jason Gross2017-06-13
* Fix a typoGravatar Jason Gross2017-06-13
* Add rewrite_eta_match_base_type_implGravatar Jason Gross2017-06-13
* Add eta_match_base_type_implGravatar Jason Gross2017-06-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 13:47:34 +0000