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

Non-trivial atoms and convexify improvements #6

Merged
merged 189 commits into from
Dec 15, 2023
Merged

Non-trivial atoms and convexify improvements #6

merged 189 commits into from
Dec 15, 2023

Conversation

ramonfmir
Copy link
Contributor

Non-trivial atoms are atoms defined using previously defined atoms. The atom library has been extended to make these work.

The convexify tactic has been extended to handle more atoms, and a number of examples have been formalized.

@ramonfmir
feat: make cones irreducible
0b2ba4d
@ramonfmir
wip: ensure cones are not unfolded
5edb3ac
@ramonfmir
fix: sets with irreducible cones
7d0a944
@ramonfmir
fix: atom declarations with irreducible cones
61e3cb7
@ramonfmir
wip: reducing all constraints?
de8c402
@ramonfmir
fix: extra constraints in Huber
e851e6c
@ramonfmir
wip: optimality for eq needs an intros
37a1cd2
@ramonfmir
wip: adjust optimality condition for non-trivial atoms
79f1a9b
@ramonfmir
fix: use atom range to build inequality
87899da
@ramonfmir
wip: issue with replaceProjections
b4b1913
@ramonfmir
test: recovered most of the old DCP tests
69764b8
@ramonfmir
fix: make atoms reducible for adjusted optimality
c4b6355
@ramonfmir
test: DCP exercises from course
e94ae63
@ramonfmir
wip: geo_mean and quad_over_lin in cost check
e3a5a28
@ramonfmir
test: geo_mean and quad_over_lin
f54b864
@ramonfmir
wip: add norm2 to handle example 3.33
f8b0ab5
@ramonfmir
feat: extend egg language with xexp, entr, qol and norm2
f71b4af
@ramonfmir
fix: extra space in rule
c357af3
@ramonfmir
wip: remove ad-hoc cost for composed atoms
79805c2
@ramonfmir
fix: conditions in atom folding rules
2543f0a
@ramonfmir
feat: all composition rules and joining curvatures
b2e1160
@ramonfmir
feat: cost calculation for new atoms
625bf98
@ramonfmir
feat: add domain calculation for new atoms
606b136
@ramonfmir
feat: cost and rule for geo_mean
78fef5c
@ramonfmir
feat: get_steps_from_string
ca82529
@ramonfmir
fix: missing variable in extractor
fd72a6a
@ramonfmir
wip: restricted constant folding
2af01a0
@ramonfmir
feat: tests outside of optimization problems
8fc1b07
@ramonfmir
chore: remove unused tag
40dba18
@ramonfmir
chore: increase node limit
a4a4574
@ramonfmir
chroe: problem goal not needed for solve
ef3daca
@ramonfmir
chore: disable trace.Meta.debugs
93ec0fb
@ramonfmir
fix: logSumExp₂ in translation
4efe582
@ramonfmir
feat: more robust simp_or_rw
280b4e7
@ramonfmir
test: formalize DCP quiz tests
93bd6d9
@ramonfmir
test: add quiz tests to test suite
f4c68e4
@ramonfmir
chore: print term JSON
d863d8a
@ramonfmir
chore: print problem names for convexify evaluation
f31e4a6
@ramonfmir
test: start checker tests
f94b6fc
@ramonfmir
feat: more refined even powers
545aa1f
@ramonfmir
feat: rpow_eq_mul_rpow_pred
ec577ee
@ramonfmir
wip: Stanford tests
580f866
@ramonfmir
test: benchmarking 3.67
4946b02
@ramonfmir
feat: extend test util
0fd76c9
@ramonfmir
feat: allow user-specified node limits
d8147bb
@ramonfmir
feat: sqrt_mul
2625448
@ramonfmir
test: some statistics for 3.67
44a8d94
@ramonfmir
chore: ignore plots
d690d45
@ramonfmir
fix: issue with empty solver directory
fc8c080
@ramonfmir
fix: create MOSEK files in build.sh
0be8102
@ramonfmir
test: add gp8 to egg tests
6b70358
@ramonfmir
chore: clean egg directory in build.sh
4682a76
@ramonfmir
fix: remove power rule
eef8b27
@ramonfmir
chore: increase node limit
00e19e0
@ramonfmir
chore: bump to v4.4.0-rc1
700c909
@ramonfmir
fix: broken proofs from version update
aa20593
@ramonfmir
fix: tests passing with new Lean version
2507d04
@ramonfmir
feat: random names for solver files to avoid race conditions
35e6bb8
@ramonfmir
fix: SO test power type
b829b51
@ramonfmir ramonfmir merged commit e9593f6 into main Dec 15, 2023
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
1 participant
@ramonfmir