Lean.Meta.Tactic.LinearArith.Solver

source

structure Lean.Meta.Linear.Var :

Type

id : Nat

Instances For

source

instance Lean.Meta.Linear.instInhabitedVar :

Inhabited Var

Equations

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

source

instance Lean.Meta.Linear.instOrdVar :

Ord Var

Equations

Lean.Meta.Linear.instOrdVar = { compare := Lean.Meta.Linear.ordVar✝ }

source

instance Lean.Meta.Linear.instDecidableEqVar :

DecidableEq Var

Equations

Lean.Meta.Linear.instDecidableEqVar = Lean.Meta.Linear.decEqVar✝

source

instance Lean.Meta.Linear.instReprVar :

Repr Var

Equations

Lean.Meta.Linear.instReprVar = { reprPrec := Lean.Meta.Linear.reprVar✝ }

source

instance Lean.Meta.Linear.instLTVar :

LT Var

Equations

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

source

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

Decidable (a < b)

Equations

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

source

structure Lean.Meta.Linear.Assignment :

Type

val : Array Std.Internal.Rat

Instances For

Lean.Meta.Linear.instInhabitedAssignment

source

instance Lean.Meta.Linear.instInhabitedAssignment :

Inhabited Assignment

Equations

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

source

@[reducible, inline]

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

Nat

Equations

a.size = a.val.size

source

@[reducible, inline]

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

Option Std.Internal.Rat

Equations

a.get? x = if h : x.id < a.size then some a.val[x.id] else none

source

@[reducible, inline]

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

Assignment

Equations

a.push v = { val := a.val.push v }

source

@[reducible, inline]

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

Assignment

Equations

a.take newSize = { val := a.val.take newSize }

source

structure Lean.Meta.Linear.Poly :

Type

val : Array (Int × Var)

Instances For

source

instance Lean.Meta.Linear.instInhabitedPoly :

Inhabited Poly

Equations

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

source

instance Lean.Meta.Linear.instReprPoly :

Repr Poly

Equations

Lean.Meta.Linear.instReprPoly = { reprPrec := Lean.Meta.Linear.reprPoly✝ }

source

instance Lean.Meta.Linear.instDecidableEqPoly :

DecidableEq Poly

Equations

Lean.Meta.Linear.instDecidableEqPoly = Lean.Meta.Linear.decEqPoly✝

source

@[reducible, inline]

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

Nat

Equations

e.size = e.val.size

source

@[reducible, inline]

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

Int

Equations

e.getMaxVarCoeff = e.val.back!.fst

source

@[reducible, inline]

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

Var

Equations

e.getMaxVar = e.val.back!.snd

source

@[reducible, inline]

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

Int × Var

Equations

e.get i = e.val[i]

source

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

Poly

Equations

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

source

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

Poly

Equations

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

source

@[irreducible]

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

Poly

Equations

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

source

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

Poly

Equations

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

source

@[irreducible]

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

Poly

Equations

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

source

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

Option Std.Internal.Rat

Equations

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

source

structure Lean.Meta.Linear.AssumptionId :

Type

id : Nat

Instances For

source

instance Lean.Meta.Linear.instInhabitedAssumptionId :

Inhabited AssumptionId

Equations

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

source

instance Lean.Meta.Linear.instDecidableEqAssumptionId :

DecidableEq AssumptionId

Equations

Lean.Meta.Linear.instDecidableEqAssumptionId = Lean.Meta.Linear.decEqAssumptionId✝

source

instance Lean.Meta.Linear.instReprAssumptionId :

Repr AssumptionId

Equations

Lean.Meta.Linear.instReprAssumptionId = { reprPrec := Lean.Meta.Linear.reprAssumptionId✝ }

source

inductive Lean.Meta.Linear.Justification :

Type

combine (c₁ : Int) (j₁ : Justification) (c₂ : Int) (j₂ : Justification) : Justification
assumption (id : AssumptionId) : Justification

Instances For

source

instance Lean.Meta.Linear.instInhabitedJustification :

Inhabited Justification

Equations

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

source

instance Lean.Meta.Linear.instDecidableEqJustification :

DecidableEq Justification

Equations

Lean.Meta.Linear.instDecidableEqJustification = Lean.Meta.Linear.decEqJustification✝

source

instance Lean.Meta.Linear.instBEqJustification :

BEq Justification

Equations

Lean.Meta.Linear.instBEqJustification = { beq := Lean.Meta.Linear.beqJustification✝ }

source

instance Lean.Meta.Linear.instReprJustification :

Repr Justification

Equations

Lean.Meta.Linear.instReprJustification = { reprPrec := Lean.Meta.Linear.reprJustification✝ }

source

inductive Lean.Meta.Linear.CnstrKind :

Type

eq : CnstrKind
div : CnstrKind
lt : CnstrKind
le : CnstrKind

Instances For

source

instance Lean.Meta.Linear.instInhabitedCnstrKind :

Inhabited CnstrKind

Equations

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

source

instance Lean.Meta.Linear.instDecidableEqCnstrKind :

DecidableEq CnstrKind

Equations

Lean.Meta.Linear.instDecidableEqCnstrKind x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

source

instance Lean.Meta.Linear.instBEqCnstrKind :

BEq CnstrKind

Equations

Lean.Meta.Linear.instBEqCnstrKind = { beq := Lean.Meta.Linear.beqCnstrKind✝ }

source

instance Lean.Meta.Linear.instReprCnstrKind :

Repr CnstrKind

Equations

Lean.Meta.Linear.instReprCnstrKind = { reprPrec := Lean.Meta.Linear.reprCnstrKind✝ }

source

structure Lean.Meta.Linear.Cnstr :

Type

kind : CnstrKind
lhs : Poly
rhs : Int
jst : Justification

Instances For

source

instance Lean.Meta.Linear.instInhabitedCnstr :

Inhabited Cnstr

Equations

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

source

instance Lean.Meta.Linear.instDecidableEqCnstr :

DecidableEq Cnstr

Equations

Lean.Meta.Linear.instDecidableEqCnstr = Lean.Meta.Linear.decEqCnstr✝

source

instance Lean.Meta.Linear.instBEqCnstr :

BEq Cnstr

Equations

Lean.Meta.Linear.instBEqCnstr = { beq := Lean.Meta.Linear.beqCnstr✝ }

source

instance Lean.Meta.Linear.instReprCnstr :

Repr Cnstr

Equations

Lean.Meta.Linear.instReprCnstr = { reprPrec := Lean.Meta.Linear.reprCnstr✝ }

source

@[reducible, inline]

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

Bool

Equations

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

source

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

Std.Internal.Rat

Equations

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

source

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

Bool

Equations

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

source

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

Option (Std.Internal.Rat × Cnstr)

Equations

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

source

inductive Lean.Meta.Linear.Result :

Type

unsat (j : Justification) : Result
unsupported : Result
timeout : Result
sat (a : Assignment) : Result

source

structure Lean.Meta.Linear.Context :

Type

int : Array Bool

source

structure Lean.Meta.Linear.State :

Type

lowers : Array (Array Cnstr)
uppers : Array (Array Cnstr)
int : Array Bool
assignment : Assignment

Instances For

Lean.Meta.Linear.instInhabitedState

source

instance Lean.Meta.Linear.instInhabitedState :

Inhabited State

Equations

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

source

@[reducible, inline]

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

Nat

Equations

s.getNumVars = s.lowers.size

source

@[reducible, inline]

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

Nat

Equations

s.currVar = s.assignment.size

source

@[reducible, inline]

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

Option (Std.Internal.Rat × Cnstr)

Equations

s.getBestLowerBound? = Lean.Meta.Linear.getBestBound? s.lowers[s.currVar]! s.assignment true s.int[s.currVar]!

source

@[reducible, inline]

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

Option (Std.Internal.Rat × Cnstr)

Equations

s.getBestUpperBound? = Lean.Meta.Linear.getBestBound? s.uppers[s.currVar]! s.assignment false s.int[s.currVar]!

source

@[reducible, inline]

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

State

Equations

s.assignCurr v = { lowers := s.lowers, uppers := s.uppers, int := s.int, assignment := s.assignment.push v }

source

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

Option Std.Internal.Rat

Equations

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

source

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

Result ⊕ State

Equations

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

source

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

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