Minimization problem to Egg minimization (S-expressions)

Using CvxLean/Tactic/PreDCP/Egg/UncheckedDCP.lean, we build an atom tree from a given problem, ignoring the curvature checks. This file does all the processing needed after that point to turn it into a problem that can be sent to egg. This includes:

• Adjusting the name of the constructors.
• Building the domain for each variable in normalized linear constraint to initialize the e-class analyses.
• Flattening the trees to strings.

def CvxLean.EggTree.opMap : Lean.HashMap String (String × Array CvxLean.EggTreeOpArgTag)

Mapping between atom names that come from the unchecked tree construction and their egg counterparts. prob, objFun, constr and constrs are special cases. The rest of names come from the atom library. It also returns the extra arguments, which sometimes may be pre-determined, for example, the atom powNegOne corresponds to the constructor pow in the egg language with the second argumetn set to -1.

Equations

• One or more equations did not get rendered due to their size.

partial def CvxLean.EggTree.adjustOps (t : CvxLean.EggTree) : Lean.MetaM CvxLean.EggTree

Traverse the tree and use opMap to align the names of the constructors.

partial def CvxLean.EggTree.getNumericalValue? : CvxLean.EggTree → Option Float

Extract the numerical value from the egg tree, if any. This is used to construct the domain information needed in the e-class analyses. NOTE: This is a source of inaccuracy as some operations are approximate, however, it does not compromise the soundness of the procedure. If the domains sent to egg are incorrect, which may lead to an incorrect sequence of steps to, transform the problem, Lean will reject the proof.

def CvxLean.EggTree.getIdentifier? (vars : List String) : CvxLean.EggTree → Option String

If the tree corresponds to a variable or parameter, return its name.

Equations

• One or more equations did not get rendered due to their size.

partial def CvxLean.EggTree.toEggString : CvxLean.EggTree → String

Flatten an EggTree to a string to send to egg.

partial def CvxLean.EggTree.size : CvxLean.EggTree → ℕ

Size of the expresison's AST that an EggTree encodes..

def CvxLean.EggTree.ofEggOCTree (ocTree : CvxLean.EggOCTree) : CvxLean.EggTree

Compose the components of an EggOCTree into a single EggTree.

Equations

• One or more equations did not get rendered due to their size.

def CvxLean.EggOCTreeExtended.processDomainExprTree (h : String) (c : CvxLean.Tree String String) (vars : List String) : Option CvxLean.EggDomainIdentified

Helper function for fromComponents that processes a single domain-defining expression.

Equations

• One or more equations did not get rendered due to their size.

def CvxLean.EggOCTreeExtended.fromComponents (objFun : String × CvxLean.EggTree) (constr : Array (String × CvxLean.EggTree)) (vars : List String) : Lean.MetaM CvxLean.EggOCTreeExtended

Given an expression representing a minimization problem, turn it into a tree of strings, also extract all the domain information from simple constraints. Adjust operations to match the names of the constructors in the egg language.

Equations

• One or more equations did not get rendered due to their size.

def CvxLean.EggOCTreeExtended.fromMinimization (e : CvxLean.Meta.MinimizationExpr) (vars : List String) : Lean.MetaM CvxLean.EggOCTreeExtended

Get the atom tree form a minimization problem. Then call fromComponents, which takes care of adjusting all nodes and extracting the domain information from the constraints.

Equations

• One or more equations did not get rendered due to their size.

def CvxLean.EggMinimization.ofEggOCTree (oc : CvxLean.EggOCTree) : CvxLean.EggMinimization

Convert EggOCTree EggMinimization` by flattening all trees.

Equations

• One or more equations did not get rendered due to their size.