Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extending Linear Two-Variable Equalities with Coefficients #1466

Merged
merged 60 commits into from
Jun 12, 2024
Merged

Extending Linear Two-Variable Equalities with Coefficients #1466

merged 60 commits into from
Jun 12, 2024

Commits on May 15, 2024

  1. initial components for coefficients added

    @DrMichaelPetter
    DrMichaelPetter committed May 15, 2024
    Configuration menu
    Copy the full SHA
    c6d19a9 View commit details
    Browse the repository at this point in the history

  2. adaptation of forget_variable to coefficients

    @DrMichaelPetter
    DrMichaelPetter committed May 15, 2024
    Configuration menu
    Copy the full SHA
    d2ce175 View commit details
    Browse the repository at this point in the history

  3. more accurate representation and canonicalization

    @DrMichaelPetter
    DrMichaelPetter committed May 15, 2024
    Configuration menu
    Copy the full SHA
    8891619 View commit details
    Browse the repository at this point in the history

  4. conversion to lincons

    @DrMichaelPetter
    DrMichaelPetter committed May 15, 2024
    Configuration menu
    Copy the full SHA
    19c43f6 View commit details
    Browse the repository at this point in the history

Commits on May 16, 2024

  1. [skip ci] generate coefficient-carrying monomials from texp

    @DrMichaelPetter
    DrMichaelPetter committed May 16, 2024
    Configuration menu
    Copy the full SHA
    5c2e741 View commit details
    Browse the repository at this point in the history

Commits on May 17, 2024

  1. [skip ci] migrated meet_with_one_conj

    @DrMichaelPetter
    DrMichaelPetter committed May 17, 2024
    Configuration menu
    Copy the full SHA
    e97e26e View commit details
    Browse the repository at this point in the history

  2. [skip ci] tiny migration steps, low hanging fruit

    @DrMichaelPetter
    DrMichaelPetter committed May 17, 2024
    Configuration menu
    Copy the full SHA
    a9248db View commit details
    Browse the repository at this point in the history

Commits on May 19, 2024

  1. [skip ci] dealt with simplifying linear expressions to lin2vars with … 

    …coeffs
    @DrMichaelPetter
    DrMichaelPetter committed May 19, 2024
    Configuration menu
    Copy the full SHA
    1257b68 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2024

  1. [skip ci] replaced overspecialized subtract_with_constant by affine_t… 

    …ransform
    @DrMichaelPetter
    DrMichaelPetter committed May 20, 2024
    Configuration menu
    Copy the full SHA
    034492e View commit details
    Browse the repository at this point in the history

Commits on May 21, 2024

  1. [skip ci] bounds

    @DrMichaelPetter
    DrMichaelPetter committed May 21, 2024
    Configuration menu
    Copy the full SHA
    4d26681 View commit details
    Browse the repository at this point in the history

  2. [skip ci] leq/implies now also for coefficients

    @DrMichaelPetter
    DrMichaelPetter committed May 21, 2024
    Configuration menu
    Copy the full SHA
    fa58e2e View commit details
    Browse the repository at this point in the history

  3. [skip ci] migrated meet_tcons

    @DrMichaelPetter
    DrMichaelPetter committed May 21, 2024
    Configuration menu
    Copy the full SHA
    ba48580 View commit details
    Browse the repository at this point in the history

  4. [skip ci] formulated new join sorting criterium

    @DrMichaelPetter
    DrMichaelPetter committed May 21, 2024
    Configuration menu
    Copy the full SHA
    80ef4bd View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into lin2var-coefficients

    @DrMichaelPetter
    DrMichaelPetter authored May 21, 2024
    Configuration menu
    Copy the full SHA
    0fb3741 View commit details
    Browse the repository at this point in the history

  6. [skip ci] satisfy semgrep

    @DrMichaelPetter
    DrMichaelPetter committed May 21, 2024
    Configuration menu
    Copy the full SHA
    7e5b727 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2024

  1. [skip ci] finally affine transform the reference variables in join

    @DrMichaelPetter
    DrMichaelPetter committed May 22, 2024
    Configuration menu
    Copy the full SHA
    ad01be4 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into lin2var-coefficients

    @DrMichaelPetter
    DrMichaelPetter authored May 22, 2024
    Configuration menu
    Copy the full SHA
    f88f22a View commit details
    Browse the repository at this point in the history

  3. cosmetics

    @DrMichaelPetter
    DrMichaelPetter committed May 22, 2024
    Configuration menu
    Copy the full SHA
    9923eaf View commit details
    Browse the repository at this point in the history

  4. sign errors corrected

    @DrMichaelPetter
    DrMichaelPetter committed May 22, 2024
    Configuration menu
    Copy the full SHA
    dfeb715 View commit details
    Browse the repository at this point in the history

  5. do not enforce pattern on variable names

    @DrMichaelPetter
    DrMichaelPetter committed May 22, 2024
    Configuration menu
    Copy the full SHA
    c6928c5 View commit details
    Browse the repository at this point in the history

  6. migration to appendix A - join (part 1)

    @DrMichaelPetter
    DrMichaelPetter committed May 22, 2024
    Configuration menu
    Copy the full SHA
    ada7065 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into lin2var-coefficients

    @DrMichaelPetter
    DrMichaelPetter authored May 22, 2024
    Configuration menu
    Copy the full SHA
    5edfbca View commit details
    Browse the repository at this point in the history

Commits on May 23, 2024

  1. Merge branch 'master' into lin2var-coefficients

    @DrMichaelPetter
    DrMichaelPetter authored May 23, 2024
    Configuration menu
    Copy the full SHA
    b458827 View commit details
    Browse the repository at this point in the history

  2. error in tracing

    @DrMichaelPetter
    DrMichaelPetter committed May 23, 2024
    Configuration menu
    Copy the full SHA
    366b04c View commit details
    Browse the repository at this point in the history

  3. join of two different constants still remains in one equivalence class

    @DrMichaelPetter
    DrMichaelPetter committed May 23, 2024
    Configuration menu
    Copy the full SHA
    cb3b486 View commit details
    Browse the repository at this point in the history

  4. made join criteria much more legible

    @DrMichaelPetter
    DrMichaelPetter committed May 23, 2024
    Configuration menu
    Copy the full SHA
    58c4e7d View commit details
    Browse the repository at this point in the history

  5. added case distinction for equivalence classes

    @DrMichaelPetter
    DrMichaelPetter committed May 23, 2024
    Configuration menu
    Copy the full SHA
    b5fed08 View commit details
    Browse the repository at this point in the history

  6. satisfy semgrep

    @DrMichaelPetter
    DrMichaelPetter committed May 23, 2024
    Configuration menu
    Copy the full SHA
    083d1ea View commit details
    Browse the repository at this point in the history

  7. join carried out for const cases

    @DrMichaelPetter
    DrMichaelPetter committed May 23, 2024
    Configuration menu
    Copy the full SHA
    c633651 View commit details
    Browse the repository at this point in the history

Commits on May 24, 2024

  1. migration to appendix A - join (part 2)

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    9e4cd58 View commit details
    Browse the repository at this point in the history

  2. added regression test for coefficient-heavy transactions

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    e290d3c View commit details
    Browse the repository at this point in the history

  3. make coefficents in regression coprime, and flex with propagation of … 

    …2var relations
    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    9de6f85 View commit details
    Browse the repository at this point in the history

  4. wave through var-var equivalences if var1=var2

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    3291633 View commit details
    Browse the repository at this point in the history

  5. removed warning 8

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    83d7fb8 View commit details
    Browse the repository at this point in the history

  6. got rid of unnecessarily largearray

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    16c8e65 View commit details
    Browse the repository at this point in the history

  7. rm redundancies

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    aded7d5 View commit details
    Browse the repository at this point in the history

  8. Update src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml 

    make repopulation of the sparse conjunction more concise

Co-authored-by: Michael Schwarz <[email protected]>
    @DrMichaelPetter @michael-schwarz
    DrMichaelPetter and michael-schwarz authored May 24, 2024
    Configuration menu
    Copy the full SHA
    26419aa View commit details
    Browse the repository at this point in the history

  9. replace = with more specialized Rhs.equal

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    49895fe View commit details
    Browse the repository at this point in the history

  10. gotten rid of silly record deconstruction

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    7e2a741 View commit details
    Browse the repository at this point in the history

  11. make indentation happy again

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    62e569b View commit details
    Browse the repository at this point in the history

  12. make gcd more compact

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    4810b5d View commit details
    Browse the repository at this point in the history

  13. explain canonicalization

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    98ae9a4 View commit details
    Browse the repository at this point in the history

  14. printf tuning

    @DrMichaelPetter
    DrMichaelPetter committed May 24, 2024
    Configuration menu
    Copy the full SHA
    55c15f7 View commit details
    Browse the repository at this point in the history

Commits on May 25, 2024

  1. oversight of %+, so lets do it the affeq way

    @DrMichaelPetter
    DrMichaelPetter committed May 25, 2024
    Configuration menu
    Copy the full SHA
    9078c2a View commit details
    Browse the repository at this point in the history

  2. point out IMap has nothing directly to do with EConj

    @DrMichaelPetter
    DrMichaelPetter committed May 25, 2024
    Configuration menu
    Copy the full SHA
    e0e9c34 View commit details
    Browse the repository at this point in the history

  3. more concise subst

    @DrMichaelPetter
    DrMichaelPetter committed May 25, 2024
    Configuration menu
    Copy the full SHA
    c6ec44b View commit details
    Browse the repository at this point in the history

  4. rm faulty eval_int answer

    @DrMichaelPetter
    DrMichaelPetter committed May 25, 2024
    Configuration menu
    Copy the full SHA
    6f02c2a View commit details
    Browse the repository at this point in the history

Commits on May 27, 2024

  1. rm Z.t->int conv issues

    @DrMichaelPetter
    DrMichaelPetter committed May 27, 2024
    Configuration menu
    Copy the full SHA
    31bb802 View commit details
    Browse the repository at this point in the history

Commits on May 28, 2024

  1. wrong brackets

    @DrMichaelPetter
    DrMichaelPetter committed May 28, 2024
    Configuration menu
    Copy the full SHA
    ec3deed View commit details
    Browse the repository at this point in the history

  2. fix unmatched monom in forget_variable

    @DrMichaelPetter
    DrMichaelPetter committed May 28, 2024
    Configuration menu
    Copy the full SHA
    075f2e8 View commit details
    Browse the repository at this point in the history

Commits on May 29, 2024

  1. fixed broken is_top

    @DrMichaelPetter
    DrMichaelPetter committed May 29, 2024
    Configuration menu
    Copy the full SHA
    94ebf86 View commit details
    Browse the repository at this point in the history

  2. make combine tracing in relational analysis more specific

    @DrMichaelPetter
    DrMichaelPetter committed May 29, 2024
    Configuration menu
    Copy the full SHA
    9663b1c View commit details
    Browse the repository at this point in the history

  3. forget did not forget about the actual head-variable of the new cluster

    @DrMichaelPetter
    DrMichaelPetter committed May 29, 2024
    Configuration menu
    Copy the full SHA
    caa8437 View commit details
    Browse the repository at this point in the history

  4. fixed forget_variable by a) sorting vars in cluster and b) rehauling … 

    …cluster transformation with subst/inverse convenience functions
    @DrMichaelPetter
    DrMichaelPetter committed May 29, 2024
    Configuration menu
    Copy the full SHA
    e1462b3 View commit details
    Browse the repository at this point in the history

Commits on Jun 1, 2024

  1. Merge branch 'master' into lin2var-coefficients

    @DrMichaelPetter
    DrMichaelPetter authored Jun 1, 2024
    Configuration menu
    Copy the full SHA
    d510fc7 View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2024

  1. added treatment of speculative computations in relational analyses

    @DrMichaelPetter
    DrMichaelPetter committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    aed4cec View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into lin2var-coefficients

    @DrMichaelPetter
    DrMichaelPetter authored Jun 10, 2024
    Configuration menu
    Copy the full SHA
    f2f8189 View commit details
    Browse the repository at this point in the history

Commits on Jun 11, 2024

  1. tweaks from MS' PR comments

    @DrMichaelPetter
    DrMichaelPetter committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    3df5980 View commit details
    Browse the repository at this point in the history

  2. added explanation

    @DrMichaelPetter
    DrMichaelPetter committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    ca31b6e View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into lin2var-coefficients

    @DrMichaelPetter
    DrMichaelPetter authored Jun 11, 2024
    Configuration menu
    Copy the full SHA
    d340284 View commit details
    Browse the repository at this point in the history