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

Show file tree
Hide file tree
Changes from 37 commits
Commits
Show all changes
60 commits
Select commit Hold shift + click to select a range
c6d19a9
initial components for coefficients added
DrMichaelPetter May 15, 2024
d2ce175
adaptation of forget_variable to coefficients
DrMichaelPetter May 15, 2024
8891619
more accurate representation and canonicalization
DrMichaelPetter May 15, 2024
19c43f6
conversion to lincons
DrMichaelPetter May 15, 2024
5c2e741
[skip ci] generate coefficient-carrying monomials from texp
DrMichaelPetter May 16, 2024
e97e26e
[skip ci] migrated meet_with_one_conj
DrMichaelPetter May 17, 2024
a9248db
[skip ci] tiny migration steps, low hanging fruit
DrMichaelPetter May 17, 2024
1257b68
[skip ci] dealt with simplifying linear expressions to lin2vars with …
DrMichaelPetter May 19, 2024
034492e
[skip ci] replaced overspecialized subtract_with_constant by affine_t…
DrMichaelPetter May 20, 2024
4d26681
[skip ci] bounds
DrMichaelPetter May 21, 2024
fa58e2e
[skip ci] leq/implies now also for coefficients
DrMichaelPetter May 21, 2024
ba48580
[skip ci] migrated meet_tcons
DrMichaelPetter May 21, 2024
80ef4bd
[skip ci] formulated new join sorting criterium
DrMichaelPetter May 21, 2024
0fb3741
Merge branch 'master' into lin2var-coefficients
DrMichaelPetter May 21, 2024
7e5b727
[skip ci] satisfy semgrep
DrMichaelPetter May 21, 2024
ad01be4
[skip ci] finally affine transform the reference variables in join
DrMichaelPetter May 22, 2024
f88f22a
Merge branch 'master' into lin2var-coefficients
DrMichaelPetter May 22, 2024
9923eaf
cosmetics
DrMichaelPetter May 22, 2024
dfeb715
sign errors corrected
DrMichaelPetter May 22, 2024
c6928c5
do not enforce pattern on variable names
DrMichaelPetter May 22, 2024
ada7065
migration to appendix A - join (part 1)
DrMichaelPetter May 22, 2024
5edfbca
Merge branch 'master' into lin2var-coefficients
DrMichaelPetter May 22, 2024
b458827
Merge branch 'master' into lin2var-coefficients
DrMichaelPetter May 23, 2024
366b04c
error in tracing
DrMichaelPetter May 22, 2024
cb3b486
join of two different constants still remains in one equivalence class
DrMichaelPetter May 23, 2024
58c4e7d
made join criteria much more legible
DrMichaelPetter May 23, 2024
b5fed08
added case distinction for equivalence classes
DrMichaelPetter May 23, 2024
083d1ea
satisfy semgrep
DrMichaelPetter May 23, 2024
c633651
join carried out for const cases
DrMichaelPetter May 23, 2024
9e4cd58
migration to appendix A - join (part 2)
DrMichaelPetter May 24, 2024
e290d3c
added regression test for coefficient-heavy transactions
DrMichaelPetter May 24, 2024
9de6f85
make coefficents in regression coprime, and flex with propagation of …
DrMichaelPetter May 24, 2024
3291633
wave through var-var equivalences if var1=var2
DrMichaelPetter May 24, 2024
83d7fb8
removed warning 8
DrMichaelPetter May 24, 2024
16c8e65
got rid of unnecessarily largearray
DrMichaelPetter May 24, 2024
aded7d5
rm redundancies
DrMichaelPetter May 24, 2024
26419aa
Update src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
DrMichaelPetter May 24, 2024
49895fe
replace = with more specialized Rhs.equal
DrMichaelPetter May 24, 2024
7e2a741
gotten rid of silly record deconstruction
DrMichaelPetter May 24, 2024
62e569b
make indentation happy again
DrMichaelPetter May 24, 2024
4810b5d
make gcd more compact
DrMichaelPetter May 24, 2024
98ae9a4
explain canonicalization
DrMichaelPetter May 24, 2024
55c15f7
printf tuning
DrMichaelPetter May 24, 2024
9078c2a
oversight of %+, so lets do it the affeq way
DrMichaelPetter May 25, 2024
e0e9c34
point out IMap has nothing directly to do with EConj
DrMichaelPetter May 25, 2024
c6ec44b
more concise subst
DrMichaelPetter May 25, 2024
6f02c2a
rm faulty eval_int answer
DrMichaelPetter May 25, 2024
31bb802
rm Z.t->int conv issues
DrMichaelPetter May 27, 2024
ec3deed
wrong brackets
DrMichaelPetter May 28, 2024
075f2e8
fix unmatched monom in forget_variable
DrMichaelPetter May 28, 2024
94ebf86
fixed broken is_top
DrMichaelPetter May 29, 2024
9663b1c
make combine tracing in relational analysis more specific
DrMichaelPetter May 29, 2024
caa8437
forget did not forget about the actual head-variable of the new cluster
DrMichaelPetter May 29, 2024
e1462b3
fixed forget_variable by a) sorting vars in cluster and b) rehauling …
DrMichaelPetter May 29, 2024
d510fc7
Merge branch 'master' into lin2var-coefficients
DrMichaelPetter Jun 1, 2024
aed4cec
added treatment of speculative computations in relational analyses
DrMichaelPetter Jun 10, 2024
f2f8189
Merge branch 'master' into lin2var-coefficients
DrMichaelPetter Jun 10, 2024
3df5980
tweaks from MS' PR comments
DrMichaelPetter Jun 11, 2024
ca31b6e
added explanation
DrMichaelPetter Jun 11, 2024
d340284
Merge branch 'master' into lin2var-coefficients
DrMichaelPetter Jun 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading