def Blaster.Optimize.propExprToBoolExpr? (op1 op2 : Lean.Expr) (isBoolAnd? : Bool := true) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.optimizeBoolPropAnd (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Call optimizeAnd f args and apply the following simplification/normalization rules on the resulting And expression (if any):

• B1 = e1 ∧ B2 = e2 ==> true = (NOP(B1, e1) && NOP(B2, e2)) (if B1 ∨ B2)
• B1 = e1 ∧ B2 = e2 ==> false = (e1 || e2) (if ¬ B1 ∧ ¬ B2) with NOP(B, e) := e if B := !e otherwise

Assume that f = Expr.const ``And.

TODO: consider simplification rule:

• B = e ∧ (a = b) | (a = b) ∧ B = e ===> true = (NOP(B, e) && a == b) if isCompatibleBeqType Type(a)
• (a = b) ∧ (c = d) ===> true = (a == b && c == d) if isCompatibleBeqType Type(a) ∧ isCompatibleBeqType Type(c)`
• ¬ (a = b) ∧ (c = d) | (c = d) ∧ ¬ (a = b) ===> true = (c == d && !(a == b)) if isCompatibleBeqType Type(a) ∧ isCompatibleBeqType Type(c)`
• ¬ (a = b) ∧ ¬ (c = d) ===> true = (!(a == b) && !(c == d)) if isCompatibleBeqType Type(a) ∧ isCompatibleBeqType Type(c)` We need extra simplification rules on boolean operators to avoid hanlding the last case, i.e., either normalize to CNF or push negation outside, i.e., ¬ ((a = b) ∨ (c = d)).

TODO: reordering on list of ∧ must be performed to regroup all B = e together and all prop expression together. The reordering must be deterministic to produce the same sequence.

Equations

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

def Blaster.Optimize.optimizeBoolPropOr (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Call optimizeOr f args and apply the following simplification/normalization rules on the resulting Or expression (if any):

• B1 = e1 ∨ B2 = e2 ==> true = (NOP(B1, e1) || NOP(B2, e2)) (if B1 ∨ B2)
• B1 = e1 ∨ B2 = e2 ==> false = (e1 && e2) (if ¬ B1 ∧ ¬ B2) with NOP(B, e) := e if B := !e otherwise

Assume that f = Expr.const ``Or.

TODO: consider simplification rule:

• B = e ∨ (a = b) | (a = b) ∨ B = e ===> true = (NOP(B, e) || a == b) if isCompatibleBeqType Type(a)
• (a = b) ∨ (c = d) ===> true = (a == b || c == d) if isCompatibleBeqType Type(a) ∧ isCompatibleBeqType Type(c)`
• ¬ (a = b) ∨ (c = d) | (c = d) ∨ ¬ (a = b) ===> true = (c == d || !(a == b)) if isCompatibleBeqType Type(a) ∧ isCompatibleBeqType Type(c)`
• ¬ (a = b) ∨ ¬ (c = d) ===> true = (!(a == b) | !(c == d)) if isCompatibleBeqType Type(a) ∧ isCompatibleBeqType Type(c)` We need extra simplification rules on boolean operators to avoid hanlding the last case, i.e., either normalize to CNF or push negation outside, i.e., ¬ ((a = b) ∧ (c = d)).

TODO: reordering on list of ∨ must be performed to regroup all B = e together and all prop expression together. The reordering must be deterministic to produce the same sequence.

Equations

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

def Blaster.Optimize.optimizePropBinary? (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Apply simplification and normalization rules on proposition binary formulae.

Equations

• Blaster.Optimize.optimizePropBinary? (Lean.Expr.const `And us) args = do let a ← Blaster.Optimize.optimizeBoolPropAnd (Lean.Expr.const `And us) args pure (some a)
• Blaster.Optimize.optimizePropBinary? (Lean.Expr.const `Or us) args = do let a ← Blaster.Optimize.optimizeBoolPropOr (Lean.Expr.const `Or us) args pure (some a)
• Blaster.Optimize.optimizePropBinary? (Lean.Expr.const `Iff us) args = do let a ← Blaster.Optimize.optimizeIff args pure (some a)
• Blaster.Optimize.optimizePropBinary? (Lean.Expr.const n us) args = pure none
• Blaster.Optimize.optimizePropBinary? f args = pure none