Lean.Meta.Tactic.LinearArith.Solver

source

structure Lean.Meta.Linear.Var:

Type

id : Nat

source

instance Lean.Meta.Linear.instInhabitedVar:

Inhabited Lean.Meta.Linear.Var

Equations

Lean.Meta.Linear.instInhabitedVar = { default := { id := default } }

source

instance Lean.Meta.Linear.instOrdVar:

Ord Lean.Meta.Linear.Var

Equations

Lean.Meta.Linear.instOrdVar = { compare := [anonymous] }

source

instance Lean.Meta.Linear.instDecidableEqVar:

DecidableEq Lean.Meta.Linear.Var

Equations

Lean.Meta.Linear.instDecidableEqVar = [anonymous]

source

instance Lean.Meta.Linear.instReprVar:

Repr Lean.Meta.Linear.Var

Equations

Lean.Meta.Linear.instReprVar = { reprPrec := [anonymous] }

source

instance Lean.Meta.Linear.instLTVar:

LT Lean.Meta.Linear.Var

Equations

Lean.Meta.Linear.instLTVar = { lt := fun a b => a.id < b.id }

source

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

Decidable (a < b)

Equations

Lean.Meta.Linear.instDecidableLtVarInstLTVar a b = inferInstanceAs (Decidable (a.id < b.id))

source

structure Lean.Meta.Linear.Assignment:

Type

val : Array Lean.Rat

source

instance Lean.Meta.Linear.instInhabitedAssignment:

Inhabited Lean.Meta.Linear.Assignment

Equations

Lean.Meta.Linear.instInhabitedAssignment = { default := { val := default } }

source

@[inline]

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

Nat

Equations

Lean.Meta.Linear.Assignment.size a = Array.size a.val

source

@[inline]

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

Option Lean.Rat

Equations

Lean.Meta.Linear.Assignment.get? a x = if h : x.id < Lean.Meta.Linear.Assignment.size a then some (Array.get a.val { val := x.id, isLt := h }) else none

source

@[inline]

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

Lean.Meta.Linear.Assignment

Equations

Lean.Meta.Linear.Assignment.push a v = { val := Array.push a.val v }

source

@[inline]

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

Lean.Meta.Linear.Assignment

Equations

Lean.Meta.Linear.Assignment.shrink a newSize = { val := Array.shrink a.val newSize }

source

structure Lean.Meta.Linear.Poly:

Type

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

source

instance Lean.Meta.Linear.instInhabitedPoly:

Inhabited Lean.Meta.Linear.Poly

Equations

Lean.Meta.Linear.instInhabitedPoly = { default := { val := default } }

source

instance Lean.Meta.Linear.instReprPoly:

Repr Lean.Meta.Linear.Poly

Equations

Lean.Meta.Linear.instReprPoly = { reprPrec := [anonymous] }

source

instance Lean.Meta.Linear.instDecidableEqPoly:

DecidableEq Lean.Meta.Linear.Poly

Equations

Lean.Meta.Linear.instDecidableEqPoly = [anonymous]

source

@[inline]

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

Nat

Equations

Lean.Meta.Linear.Poly.size e = Array.size e.val

source

@[inline]

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

Int

Equations

Lean.Meta.Linear.Poly.getMaxVarCoeff e = (Array.back e.val).fst

source

@[inline]

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

Lean.Meta.Linear.Var

Equations

Lean.Meta.Linear.Poly.getMaxVar e = (Array.back e.val).snd

source

@[inline]

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

Int × Lean.Meta.Linear.Var

Equations

Lean.Meta.Linear.Poly.get e i = Array.get e.val i

source

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

Lean.Meta.Linear.Poly

Equations

Lean.Meta.Linear.Poly.scale d e = { val := Array.map (fun x => match x with | (c, x) => (c * d, x)) e.val }

source

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

Lean.Meta.Linear.Poly

Equations

Lean.Meta.Linear.Poly.add e₁ e₂ = Lean.Meta.Linear.Poly.add.go e₁ e₂ 0 0 #[]

source

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.

source

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

Lean.Meta.Linear.Poly

Equations

Lean.Meta.Linear.Poly.combine d₁ e₁ d₂ e₂ = Lean.Meta.Linear.Poly.combine.go d₁ e₁ d₂ e₂ 0 0 #[]

source

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.

source

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

Option Lean.Rat

Equations

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

source

structure Lean.Meta.Linear.AssumptionId:

Type

id : Nat

source

instance Lean.Meta.Linear.instInhabitedAssumptionId:

Inhabited Lean.Meta.Linear.AssumptionId

Equations

Lean.Meta.Linear.instInhabitedAssumptionId = { default := { id := default } }

source

instance Lean.Meta.Linear.instDecidableEqAssumptionId:

DecidableEq Lean.Meta.Linear.AssumptionId

Equations

Lean.Meta.Linear.instDecidableEqAssumptionId = [anonymous]

source

instance Lean.Meta.Linear.instReprAssumptionId:

Repr Lean.Meta.Linear.AssumptionId

Equations

Lean.Meta.Linear.instReprAssumptionId = { reprPrec := [anonymous] }

source

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

source

instance Lean.Meta.Linear.instInhabitedJustification:

Inhabited Lean.Meta.Linear.Justification

Equations

Lean.Meta.Linear.instInhabitedJustification = { default := Lean.Meta.Linear.Justification.assumption default }

source

instance Lean.Meta.Linear.instDecidableEqJustification:

DecidableEq Lean.Meta.Linear.Justification

Equations

Lean.Meta.Linear.instDecidableEqJustification = [anonymous]

source

instance Lean.Meta.Linear.instBEqJustification:

BEq Lean.Meta.Linear.Justification

Equations

Lean.Meta.Linear.instBEqJustification = { beq := [anonymous] }

source

instance Lean.Meta.Linear.instReprJustification:

Repr Lean.Meta.Linear.Justification

Equations

Lean.Meta.Linear.instReprJustification = { reprPrec := [anonymous] }

source

inductive Lean.Meta.Linear.CnstrKind:

Type

source

instance Lean.Meta.Linear.instInhabitedCnstrKind:

Inhabited Lean.Meta.Linear.CnstrKind

Equations

Lean.Meta.Linear.instInhabitedCnstrKind = { default := Lean.Meta.Linear.CnstrKind.eq }

source

instance Lean.Meta.Linear.instDecidableEqCnstrKind:

DecidableEq Lean.Meta.Linear.CnstrKind

Equations

Lean.Meta.Linear.instDecidableEqCnstrKind x y = if h : Lean.Meta.Linear.CnstrKind.toCtorIdx x = Lean.Meta.Linear.CnstrKind.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

source

instance Lean.Meta.Linear.instBEqCnstrKind:

BEq Lean.Meta.Linear.CnstrKind

Equations

Lean.Meta.Linear.instBEqCnstrKind = { beq := [anonymous] }

source

instance Lean.Meta.Linear.instReprCnstrKind:

Repr Lean.Meta.Linear.CnstrKind

Equations

Lean.Meta.Linear.instReprCnstrKind = { reprPrec := [anonymous] }

source

structure Lean.Meta.Linear.Cnstr:

Type

source

instance Lean.Meta.Linear.instInhabitedCnstr:

Inhabited Lean.Meta.Linear.Cnstr

Equations

Lean.Meta.Linear.instInhabitedCnstr = { default := { kind := default, lhs := default, rhs := default, jst := default } }

source

instance Lean.Meta.Linear.instDecidableEqCnstr:

DecidableEq Lean.Meta.Linear.Cnstr

Equations

Lean.Meta.Linear.instDecidableEqCnstr = [anonymous]

source

instance Lean.Meta.Linear.instBEqCnstr:

BEq Lean.Meta.Linear.Cnstr

Equations

Lean.Meta.Linear.instBEqCnstr = { beq := [anonymous] }

source

instance Lean.Meta.Linear.instReprCnstr:

Repr Lean.Meta.Linear.Cnstr

Equations

Lean.Meta.Linear.instReprCnstr = { reprPrec := [anonymous] }

source

@[inline]

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

Bool

Equations

Lean.Meta.Linear.Cnstr.isStrict c = match c.kind with | Lean.Meta.Linear.CnstrKind.lt => true | x => false

source

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

Lean.Rat

Equations

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

source

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

Bool

Equations

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

source

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)

Equations

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

source

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

source

structure Lean.Meta.Linear.Context:

Type

int : Array Bool

source

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

source

instance Lean.Meta.Linear.instInhabitedState:

Inhabited Lean.Meta.Linear.State

Equations

Lean.Meta.Linear.instInhabitedState = { default := { lowers := default, uppers := default, int := default, assignment := default } }

source

@[inline]

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

Nat

Equations

Lean.Meta.Linear.State.getNumVars s = Array.size s.lowers

source

@[inline]

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

Nat

Equations

Lean.Meta.Linear.State.currVar s = Lean.Meta.Linear.Assignment.size s.assignment

source

@[inline]

abbrev Lean.Meta.Linear.State.getBestLowerBound? (s : Lean.Meta.Linear.State) :

Option (Lean.Rat × Lean.Meta.Linear.Cnstr)

Equations

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

source

@[inline]

abbrev Lean.Meta.Linear.State.getBestUpperBound? (s : Lean.Meta.Linear.State) :

Option (Lean.Rat × Lean.Meta.Linear.Cnstr)

Equations

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

source

@[inline]

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

Lean.Meta.Linear.State

Equations

Lean.Meta.Linear.State.assignCurr s v = { lowers := s.lowers, uppers := s.uppers, int := s.int, assignment := Lean.Meta.Linear.Assignment.push s.assignment v }

source

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

Option Lean.Rat

Equations

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

source

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

Equations

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

source

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