def Blaster.Optimize.decideOpDecide? (op1 op2 : Lean.Expr) (mkOpExpr : Lean.Expr → Lean.Expr → Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given op1 and op2 corresponding to the operands for a Boolean binary operator:

• return some (decide' (mkOpExpr #[e1, e2])) when op1 := decide' e1 ∧ op2 := decide' e2
• return some (decide' (mkOpExpr #[e1, true = e2])) when op1 := decide' e1 ∧ op2 := e2
• return some (decide' (mkOpExpr #[e1, true = e2])) when op1 := e2 ∧ op2 := decide' e1 Otherwise none.

Equations

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

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

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

• decide' e1 && decide' e2 ==> decide' (e1 ∧ e2)
• decide' e1 && e2 | e2 && decide' e1 ==> decide' (e1 ∧ true = e2)

Assume that f = Expr.const ``and.

TODO: reordering on list of && must be performed to regroup all decide e together and all boolean 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.optimizeDecideBoolOr (f : Lean.Expr) (args : Array Lean.Expr) : TranslateEnvT Lean.Expr

Call optimizeBoolOr f args and apply the following decide simplification/normalization rules on the resulting or expression (if any):

• decide' e1 || decide' e2 ==> decide' (e1 ∨ e2)
• decide' e1 || e2 | e2 || decide' e1 ==> decide' (e1 ∨ true = e2)

Assume that f = Expr.const ``or.

Do nothing if operator is partially applied (i.e., args.size < 2) TODO: reordering on list of || must be performed to regroup all decide' e together and all boolean expression together. The reordering must be deterministic to produce the same sequence. TODO: consider additional simplification rules

Equations

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

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

Apply simplification/normalization rules on Boolean binary operators.

Equations

• Blaster.Optimize.optimizeBoolBinary? (Lean.Expr.const `Bool.and us) args = do let a ← Blaster.Optimize.optimizeDecideBoolAnd (Lean.Expr.const `Bool.and us) args pure (some a)
• Blaster.Optimize.optimizeBoolBinary? (Lean.Expr.const `Bool.or us) args = do let a ← Blaster.Optimize.optimizeDecideBoolOr (Lean.Expr.const `Bool.or us) args pure (some a)
• Blaster.Optimize.optimizeBoolBinary? (Lean.Expr.const n us) args = pure none
• Blaster.Optimize.optimizeBoolBinary? f args = pure none