structure Lean.Meta.Linear.Var : Type

• id : Nat

instance Lean.Meta.Linear.instInhabitedVar : Inhabited Lean.Meta.Linear.Var

instance Lean.Meta.Linear.instOrdVar : Ord Lean.Meta.Linear.Var

instance Lean.Meta.Linear.instDecidableEqVar : DecidableEq Lean.Meta.Linear.Var

instance Lean.Meta.Linear.instReprVar : Repr Lean.Meta.Linear.Var

instance Lean.Meta.Linear.instLTVar : LT Lean.Meta.Linear.Var

instance Lean.Meta.Linear.instDecidableLtVarInstLTVar (a : Lean.Meta.Linear.Var) (b : Lean.Meta.Linear.Var) : Decidable (a < b)

structure Lean.Meta.Linear.Assignment : Type

• val : Array Lean.Rat

instance Lean.Meta.Linear.instInhabitedAssignment : Inhabited Lean.Meta.Linear.Assignment

@[inline, reducible]

abbrev Lean.Meta.Linear.Assignment.size (a : Lean.Meta.Linear.Assignment) : Nat

@[inline, reducible]

abbrev Lean.Meta.Linear.Assignment.get? (a : Lean.Meta.Linear.Assignment) (x : Lean.Meta.Linear.Var) : Option Lean.Rat

@[inline, reducible]

abbrev Lean.Meta.Linear.Assignment.push (a : Lean.Meta.Linear.Assignment) (v : Lean.Rat) : Lean.Meta.Linear.Assignment

@[inline, reducible]

abbrev Lean.Meta.Linear.Assignment.shrink (a : Lean.Meta.Linear.Assignment) (newSize : Nat) : Lean.Meta.Linear.Assignment

structure Lean.Meta.Linear.Poly : Type

• val : Array (Int × Lean.Meta.Linear.Var)

instance Lean.Meta.Linear.instInhabitedPoly : Inhabited Lean.Meta.Linear.Poly

instance Lean.Meta.Linear.instReprPoly : Repr Lean.Meta.Linear.Poly

instance Lean.Meta.Linear.instDecidableEqPoly : DecidableEq Lean.Meta.Linear.Poly

@[inline, reducible]

abbrev Lean.Meta.Linear.Poly.size (e : Lean.Meta.Linear.Poly) : Nat

@[inline, reducible]

abbrev Lean.Meta.Linear.Poly.getMaxVarCoeff (e : Lean.Meta.Linear.Poly) : Int

@[inline, reducible]

abbrev Lean.Meta.Linear.Poly.getMaxVar (e : Lean.Meta.Linear.Poly) : Lean.Meta.Linear.Var

@[inline, reducible]

abbrev Lean.Meta.Linear.Poly.get (e : Lean.Meta.Linear.Poly) (i : Fin (Lean.Meta.Linear.Poly.size e)) : Int × Lean.Meta.Linear.Var

def Lean.Meta.Linear.Poly.scale (d : Int) (e : Lean.Meta.Linear.Poly) : Lean.Meta.Linear.Poly

def Lean.Meta.Linear.Poly.add (e₁ : Lean.Meta.Linear.Poly) (e₂ : Lean.Meta.Linear.Poly) : Lean.Meta.Linear.Poly

def Lean.Meta.Linear.Poly.add.go (e₁ : Lean.Meta.Linear.Poly) (e₂ : Lean.Meta.Linear.Poly) (i₁ : Nat) (i₂ : Nat) (r : Array (Int × Lean.Meta.Linear.Var)) : Lean.Meta.Linear.Poly

Equations

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

def Lean.Meta.Linear.Poly.combine (d₁ : Int) (e₁ : Lean.Meta.Linear.Poly) (d₂ : Int) (e₂ : Lean.Meta.Linear.Poly) : Lean.Meta.Linear.Poly

def Lean.Meta.Linear.Poly.combine.go (d₁ : Int) (e₁ : Lean.Meta.Linear.Poly) (d₂ : Int) (e₂ : Lean.Meta.Linear.Poly) (i₁ : Nat) (i₂ : Nat) (r : Array (Int × Lean.Meta.Linear.Var)) : Lean.Meta.Linear.Poly

Equations

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

def Lean.Meta.Linear.Poly.eval? (e : Lean.Meta.Linear.Poly) (a : Lean.Meta.Linear.Assignment) : Option Lean.Rat

structure Lean.Meta.Linear.AssumptionId : Type

• id : Nat

instance Lean.Meta.Linear.instInhabitedAssumptionId : Inhabited Lean.Meta.Linear.AssumptionId

instance Lean.Meta.Linear.instDecidableEqAssumptionId : DecidableEq Lean.Meta.Linear.AssumptionId

instance Lean.Meta.Linear.instReprAssumptionId : Repr Lean.Meta.Linear.AssumptionId

inductive Lean.Meta.Linear.Justification : Type

• combine: Int → Lean.Meta.Linear.Justification → Int → Lean.Meta.Linear.Justification → Lean.Meta.Linear.Justification
• assumption: Lean.Meta.Linear.AssumptionId → Lean.Meta.Linear.Justification

instance Lean.Meta.Linear.instInhabitedJustification : Inhabited Lean.Meta.Linear.Justification

instance Lean.Meta.Linear.instDecidableEqJustification : DecidableEq Lean.Meta.Linear.Justification

instance Lean.Meta.Linear.instBEqJustification : BEq Lean.Meta.Linear.Justification

instance Lean.Meta.Linear.instReprJustification : Repr Lean.Meta.Linear.Justification

inductive Lean.Meta.Linear.CnstrKind : Type

• eq: Lean.Meta.Linear.CnstrKind
• div: Lean.Meta.Linear.CnstrKind
• lt: Lean.Meta.Linear.CnstrKind
• le: Lean.Meta.Linear.CnstrKind

instance Lean.Meta.Linear.instInhabitedCnstrKind : Inhabited Lean.Meta.Linear.CnstrKind

instance Lean.Meta.Linear.instDecidableEqCnstrKind : DecidableEq Lean.Meta.Linear.CnstrKind

instance Lean.Meta.Linear.instBEqCnstrKind : BEq Lean.Meta.Linear.CnstrKind

instance Lean.Meta.Linear.instReprCnstrKind : Repr Lean.Meta.Linear.CnstrKind

structure Lean.Meta.Linear.Cnstr : Type

• kind : Lean.Meta.Linear.CnstrKind
• lhs : Lean.Meta.Linear.Poly
• rhs : Int
• jst : Lean.Meta.Linear.Justification

instance Lean.Meta.Linear.instInhabitedCnstr : Inhabited Lean.Meta.Linear.Cnstr

instance Lean.Meta.Linear.instDecidableEqCnstr : DecidableEq Lean.Meta.Linear.Cnstr

instance Lean.Meta.Linear.instBEqCnstr : BEq Lean.Meta.Linear.Cnstr

instance Lean.Meta.Linear.instReprCnstr : Repr Lean.Meta.Linear.Cnstr

@[inline, reducible]

abbrev Lean.Meta.Linear.Cnstr.isStrict (c : Lean.Meta.Linear.Cnstr) : Bool

def Lean.Meta.Linear.Cnstr.getBound (c : Lean.Meta.Linear.Cnstr) (a : Lean.Meta.Linear.Assignment) : Lean.Rat

def Lean.Meta.Linear.Cnstr.isUnsat (c : Lean.Meta.Linear.Cnstr) (a : Lean.Meta.Linear.Assignment) : Bool

def Lean.Meta.Linear.getBestBound? (cs : Array Lean.Meta.Linear.Cnstr) (a : Lean.Meta.Linear.Assignment) (isLower : Bool) (isInt : Bool) : Option (Lean.Rat × Lean.Meta.Linear.Cnstr)

inductive Lean.Meta.Linear.Result : Type

• unsat: Lean.Meta.Linear.Justification → Lean.Meta.Linear.Result
• unsupported: Lean.Meta.Linear.Result
• timeout: Lean.Meta.Linear.Result
• sat: Lean.Meta.Linear.Assignment → Lean.Meta.Linear.Result

structure Lean.Meta.Linear.Context : Type

• int : Array Bool

structure Lean.Meta.Linear.State : Type

• lowers : Array (Array Lean.Meta.Linear.Cnstr)
• uppers : Array (Array Lean.Meta.Linear.Cnstr)
• int : Array Bool
• assignment : Lean.Meta.Linear.Assignment

instance Lean.Meta.Linear.instInhabitedState : Inhabited Lean.Meta.Linear.State

@[inline, reducible]

abbrev Lean.Meta.Linear.State.getNumVars (s : Lean.Meta.Linear.State) : Nat

@[inline, reducible]

abbrev Lean.Meta.Linear.State.currVar (s : Lean.Meta.Linear.State) : Nat

@[inline, reducible]

abbrev Lean.Meta.Linear.State.getBestLowerBound? (s : Lean.Meta.Linear.State) : Option (Lean.Rat × Lean.Meta.Linear.Cnstr)

@[inline, reducible]

abbrev Lean.Meta.Linear.State.getBestUpperBound? (s : Lean.Meta.Linear.State) : Option (Lean.Rat × Lean.Meta.Linear.Cnstr)

@[inline, reducible]

abbrev Lean.Meta.Linear.State.assignCurr (s : Lean.Meta.Linear.State) (v : Lean.Rat) : Lean.Meta.Linear.State

def Lean.Meta.Linear.pickAssignment? (lower : Lean.Rat) (lowerIsStrict : Bool) (upper : Lean.Rat) (upperIsStrict : Bool) : Option Lean.Rat

def Lean.Meta.Linear.resolve (s : Lean.Meta.Linear.State) (cl : Lean.Meta.Linear.Cnstr) (cu : Lean.Meta.Linear.Cnstr) : Lean.Meta.Linear.Result ⊕ Lean.Meta.Linear.State

def Lean.Meta.Linear.solve (n : Nat) (s : Lean.Meta.Linear.State) : Lean.Meta.Linear.Result

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Linear.solve 0 s = Lean.Meta.Linear.Result.timeout