aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Bounds
Commit message (Expand)AuthorAge
* remove old pipelineGravatar Andres Erbsen2019-01-09
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Try out stronger land, lor boundsGravatar Jason Gross2018-06-27
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* Remove dead code for renaming bindersGravatar Jason Gross2017-11-13
* Make pipeline options more easily extensibleGravatar Jason Gross2017-11-13
* Reflow commentGravatar Jason Gross2017-11-13
* Remove slow "intros [a b]"Gravatar Jason Gross2017-11-13
* More granularity in src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.vGravatar Jason Gross2017-11-13
* Split up reflective side condition tacticsGravatar Jason Gross2017-11-13
* Extract rexpr_sig from the recordGravatar Jason Gross2017-10-18
* Extract evars from reflective pipelineGravatar Jason Gross2017-10-18
* Package reflective pipeline side-conditions into a recordGravatar Jason Gross2017-10-18
* Make use of faster interp rewritingGravatar Jason Gross2017-10-17
* Fix a spelling errorGravatar Jason Gross2017-10-13
* Factor out truncation_boundsGravatar Jason Gross2017-10-13
* Add comment to Compilers/Z/Bounds/Interpretation.vGravatar Jason Gross2017-10-13
* Add reflective compose, notation for Z.Syntax.{Expr,Interp}Gravatar Jason Gross2017-10-12
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
* Add nonzero synthesisGravatar Jason Gross2017-06-26
* Allow disabling adc-fusionGravatar Jason Gross2017-06-25
* Work around bug #5615 (constr not being updated)Gravatar Jason Gross2017-06-22
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
* Use solve_wf_side_condition to synch the depth of auto with wfGravatar Jason Gross2017-06-20
* Add convenience for supporting uint8Gravatar 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
* Add more simplification to pipelineGravatar Jason Gross2017-06-17
* Add linearization to inline pairs in post-bounds pipelineGravatar Jason Gross2017-06-17
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* Add bool into P256Gravatar Jason Gross2017-06-17
* Reify Z.mul_with_split_at_bitwidthGravatar Jason Gross2017-06-13
* Handle IdWithAlt in the simplifierGravatar Jason Gross2017-06-12
* Push bounds side conditions through the pipelineGravatar Jason Gross2017-06-12
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
* Be more forceful about clearing before abstract in glue codeGravatar Jason Gross2017-06-11
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Only use bool in freezeGravatar Jason Gross2017-05-21
* Fix extra opp in freezeGravatar Jason Gross2017-05-20
* Get sbb conversion working in the pipelineGravatar Jason Gross2017-05-20
* Add adc -> sbb to arithmetic simpliferGravatar Jason Gross2017-05-20
* Add SubWithGetBorrow to reflective machineryGravatar Jason Gross2017-05-20
* Add compiler optimization for add-with-carryGravatar Jason Gross2017-05-17
* Allow 'bool' in outputGravatar Jason Gross2017-05-17
* Add reflective machinery for adc, zselectGravatar Jason Gross2017-05-17
* Ltac scope interprets some notations as errors, so we make anf a definitionGravatar Jason Gross2017-05-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 11:01:45 +0000