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

100% Lean 4, pre-DCP rewrites and more #5

Merged
merged 593 commits into from
Nov 22, 2023
Merged

100% Lean 4, pre-DCP rewrites and more #5

merged 593 commits into from
Nov 22, 2023

Conversation

ramonfmir
Copy link
Contributor

Summary of changes:

  • Removal of mathlib3port dependencies.
  • Several new atoms.
  • Condition inference for dcp.
  • Support for non-trivial atoms.
  • The equivalence command.
  • The convexify tactic.
  • Support for changes of variables.
  • More tests and examples (some are WIP).
  • General re-structuring and clean-up.

This is a very large PR and not to be taken as an example.

Note: rebase issues with #4.

@ramonfmir
wip: evaluation with aesop
734a255
@ramonfmir
test: main example
b0bb8e5
@ramonfmir
chore: remove Test.lean
f139ddb
@ramonfmir
chore: main example consistent with paper
12444f8
@ramonfmir
feat: convexify unfolds if necessary
86a9172
@ramonfmir
chore: remove rewriteWrapperApplyExprEquivalence
e4d6734
@ramonfmir
feat: add many aesop rules
9491f63
@ramonfmir
chore: print result from main example
761c52c
@ramonfmir
feat: aesop working for simple examples
0d1c642
@ramonfmir
feat: norm_num_clean_up as a tactic
9d56c88
@ramonfmir
feat: simp_or_rw
463acea
@ramonfmir
feat: punctuation to register rewrite
abb58d3
@ramonfmir
test: another position test
9895bd5
@ramonfmir
wip: more aesop work
d8cc383
@ramonfmir
chore: rename rewrite_or_simp_only
60ca69a
@ramonfmir
chore: remove aesop test
3e5e906
@ramonfmir
feat: assertions in tests
900f7c8
@ramonfmir
feat: increase e-graph limits for some GPs
3c72e8b
@ramonfmir
fix: first try simp then rw in rewrite map
62686c5
@ramonfmir
chore: CleanEgg -> EggClean
f0cac00
@ramonfmir
fix: handle objective mapping in equivalence mode
ecf1098
@ramonfmir
fix: almost DGP tests
b1a5d0a
@ramonfmir
feat: map_domain in equivalence
7257d69
@ramonfmir
feat: add domain to parameters
7deca04
@ramonfmir
fix: all rule tests work
471000d
@ramonfmir
fix: backward rewrites flip correctly
2d4db87
@ramonfmir
fix: domain added to gp6 test
4abd118
@ramonfmir
feat: is_ge_zero
b1acd04
@ramonfmir
feat: add squaring rewrite to handle gp3
6ef7edb
@ramonfmir
feat: all tests in DGP work
9518642
@ramonfmir
feat: deep atom such as KL-div works!
92c9f16
@ramonfmir
wip: bringing back some tests
a3dff84
@ramonfmir
fix: convexify dependencies
6c8fb8a
@ramonfmir
fix: equality in flat_term_check_rewrite_no_failure
879c0a1
@ramonfmir
fix: repeat () is different from {}
531dcb7
@ramonfmir
fix: gp6 test works
8547216
@ramonfmir
feat: domain pre-processing, intersecting
8754678
@ramonfmir
chore: no error comments in unit tests
57ebcd6
@ramonfmir
feat: prepare_positivity and positivity_ext
37f2b96
@ramonfmir
wip: debug hypersonic shape design DQCP with convexify
f6e820a
@ramonfmir
fix: make equivalence handle meta-variables like reduction
1060d0b
@ramonfmir
feat: convexify returns unsolved goals on failure
80ada47
@ramonfmir
feat: more positivity extensions
ec791c0
@ramonfmir
feat: convexify works on hypersonic shape design
17b0746
@ramonfmir
wip: relaxation command
8402dfd
@ramonfmir
wip: close equivalence in command
2fea541
@ramonfmir
style: spaces
1003b71
@ramonfmir
fix: name conflict in DQCP
9d0e787
@ramonfmir
feat: soCone_add_sub_two_mul_of_nonneg
4916d71
@ramonfmir
feat: powers (-1 and -2)
9dd6391
@ramonfmir
chore: add power to atom library
1662e02
@ramonfmir
chore: factor out positivity_ext
f68ce74
@ramonfmir
feat: use positivity_ext in DCP
fedc31f
@ramonfmir
feat: hypersonic shape design reducing
5809164
@ramonfmir
chore: use cache in build.sh
79efdb6
@ramonfmir
chore: install Rust and Cargo in CI
09a4b61
@ramonfmir
fix: Rust installation command
c1d3839
@ramonfmir
chore: remove failing DCP tests
edade52
@ramonfmir ramonfmir merged commit 138f294 into main Nov 22, 2023
2 checks passed
@ramonfmir ramonfmir deleted the pre-dcp-rewrites-fix branch November 24, 2023 15:12
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