@[inline]

def Blaster.Optimize.isZeroNat (e : Lean.Expr) : Bool

Return true when e corresponds to the zero nat literal.

Equations

• Blaster.Optimize.isZeroNat e = match Blaster.Optimize.isNatValue? e with | some 0 => true | x => false

def Blaster.Optimize.notEqSimp? (ne : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given ne the operand for Not apply the following normalization rules:

• When ne := false = e
  • return some (true = e)
• When ne := true = e
  • return some (false = e)
• Otherwise:
  • return none.

Equations

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

def Blaster.Optimize.notLTNumNorm? (ne : Lean.Expr) (restart : Bool := true) : TranslateEnvT (Option Lean.Expr)

Given ne the operand for Not, apply the following normalization rule:

• When ne := 0 < e ∧ Type(a) = Nat:
  • return some (0 = e)
• Otherwise:
  • return none

Equations

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

def Blaster.Optimize.optimizeNot (f : Lean.Expr) (args : Array Lean.Expr) (cacheResult : Bool := true) : TranslateEnvT Lean.Expr

Apply the following simplification/normalization rules on Not :

• ¬ False ==> True
• ¬ True ==> False
• ¬ (¬ e) ==> e (classical)
• ¬ (false = e) ==> true = e
• ¬ (true = e) ==> false = e
• ¬ (0 < e) ==> (0 = e) (if Type(e) = Nat) Assume that f = Expr.const ``Not. An error is triggered if args.size ≠ 1 (i.e., only fully applied Not expected at this stage) TODO: consider additional simplification rules

Equations

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

def Blaster.Optimize.notLogicalSimp? (ne : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given ne the operand for Not apply the following normalization rules:

• When ne := ¬ e1 ∧ ¬ e2
  • return e1 ∨ e2
• When ne := ¬ e1 ∨ ¬ e2
  • return e1 ∧ e2
• Otherwise:
  • return none.

Equations

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

def Blaster.Optimize.notLogicalSimp?.notPropagation? (ne1 ne2 op : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

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

Call optimizeNot f args and apply the following simplification/normalization rules on Not :

• ¬ (¬ e1 ∧ ¬ e2) ==> (e1 ∨ e2)
• ¬ (¬ e1 ∨ ¬ e2) ==> (e1 ∧ e2) Assume that f = Expr.const ``Not. An error is triggered if args.size ≠ 1 (i.e., only fully applied Not expected at this stage)

Equations

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

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

Apply simplification and normalization rules on proposition Not formulae.

Equations

• Blaster.Optimize.optimizePropNot? (Lean.Expr.const `Not us) args = do let a ← Blaster.Optimize.optimizeAdvancedNot (Lean.Expr.const `Not us) args pure (some a)
• Blaster.Optimize.optimizePropNot? f args = pure none