source
@[reducible, inline]
abbrev Lean.Meta.Grind.Arith.Linear.LinExpr :
Type
Equations

- Lean.Meta.Grind.Arith.Linear.LinExpr = Lean.Grind.Linarith.Expr

Instances For

source
def Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean.hash :
Poly → UInt64
Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean.hash Lean.Grind.Linarith.Poly.nil = 0

Instances For

source
instance Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean :
Hashable Poly
Equations

- Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean = { hash := Lean.Meta.Grind.Arith.Linear.instHashablePoly_lean.hash }

source
instance Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean :
Hashable Grind.Linarith.Expr
Equations

- Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean = { hash := Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash }

source
def Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash :
Grind.Linarith.Expr → UInt64
Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash Lean.Grind.Linarith.Expr.zero = 0
- Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash (Lean.Grind.Linarith.Expr.var a) = mixHash 1 (hash a)
- Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a.neg = mixHash 4 (Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a)
- Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash (Lean.Grind.Linarith.Expr.natMul a a_1) = mixHash (mixHash 5 (hash a)) (Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a_1)
- Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash (Lean.Grind.Linarith.Expr.intMul a a_1) = mixHash (mixHash 6 (hash a)) (Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean.hash a_1)

Instances For

source
structure Lean.Meta.Grind.Arith.Linear.EqCnstr :
Type

An equality constraint and its justification/proof.

- p : Poly
- h : EqCnstrProof

Instances For

source
inductive Lean.Meta.Grind.Arith.Linear.EqCnstrProof :
Type

- core (a b : Expr) (lhs rhs : LinExpr) : EqCnstrProof
- coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : EqCnstrProof
- coreOfNat (a b : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : EqCnstrProof
- neg (c : EqCnstr) : EqCnstrProof
- coeff (k : Nat) (c : EqCnstr) : EqCnstrProof
- subst (x : Var) (c₁ c₂ : EqCnstr) : EqCnstrProof

Instances For

source
structure Lean.Meta.Grind.Arith.Linear.IneqCnstr :
Type

An inequality constraint and its justification/proof.

- p : Poly
- strict : Bool
- h : IneqCnstrProof

Instances For

source
inductive Lean.Meta.Grind.Arith.Linear.IneqCnstrProof :
Type

- core (e : Expr) (lhs rhs : LinExpr) : IneqCnstrProof
- notCore (e : Expr) (lhs rhs : LinExpr) : IneqCnstrProof
- coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : IneqCnstrProof
- notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : IneqCnstrProof
- coreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : IneqCnstrProof
- notCoreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : IneqCnstrProof
- combine (c₁ c₂ : IneqCnstr) : IneqCnstrProof
- norm (c₁ : IneqCnstr) (k : Nat) : IneqCnstrProof
- dec (h : FVarId) : IneqCnstrProof
- ofDiseqSplit (c₁ : DiseqCnstr) (decVar : FVarId) (h : UnsatProof) (decVars : Array FVarId) : IneqCnstrProof
- oneGtZero : IneqCnstrProof
- ofEq (a b : Expr) (la lb : LinExpr) : IneqCnstrProof

  `a ≤ b` from an equality `a = b` coming from the core.

- ofEqOfNat (a b : Expr) (natStructId : Nat) (la lb : LinExpr) : IneqCnstrProof

  `a ≤ b` from an equality `a = b` coming from the core.

- ofCommRingEq (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : IneqCnstrProof

  `a ≤ b` from an equality `a = b` coming from the core.

- subst (x : Var) (c₁ : EqCnstr) (c₂ : IneqCnstr) : IneqCnstrProof

Instances For

source
structure Lean.Meta.Grind.Arith.Linear.DiseqCnstr :
Type

- p : Poly
- h : DiseqCnstrProof

Instances For

source
inductive Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof :
Type

- core (a b : Expr) (lhs rhs : LinExpr) : DiseqCnstrProof
- coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : CommRing.Poly) (lhs' : LinExpr) : DiseqCnstrProof
- coreOfNat (a b : Expr) (natStructId : Nat) (lhs rhs : LinExpr) : DiseqCnstrProof
- neg (c : DiseqCnstr) : DiseqCnstrProof
- subst (k₁ k₂ : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
- subst1 (k : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
- oneNeZero : DiseqCnstrProof

Instances For

source
inductive Lean.Meta.Grind.Arith.Linear.UnsatProof :
Type

- diseq (c : DiseqCnstr) : UnsatProof
- lt (c : IneqCnstr) : UnsatProof

Instances For

source
instance Lean.Meta.Grind.Arith.Linear.instInhabitedDiseqCnstr :
Inhabited DiseqCnstr
Equations

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

source
instance Lean.Meta.Grind.Arith.Linear.instInhabitedEqCnstr :
Inhabited EqCnstr
Equations

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

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Arith.Linear.VarSet :
Type
Equations

- Lean.Meta.Grind.Arith.Linear.VarSet = Std.TreeSet Lean.Grind.Linarith.Var compare

Instances For

source
structure Lean.Meta.Grind.Arith.Linear.Struct :
Type

State for each algebraic structure by this module. Each type must at least implement the instance `IntModule`. For being able to process inequalities, it must at least implement `Preorder`, and `OrderedAdd`

- id : Nat
- ringId? : Option Nat

  If the structure is a ring, we store its id in the `CommRing` module at `ringId?`

- type : Expr
- u : Level

  Cached `getDecLevel type`

- intModuleInst : Expr

  `IntModule` instance

- leInst? : Option Expr

  `LE` instance if available

- ltInst? : Option Expr

  `LT` instance if available

- lawfulOrderLTInst? : Option Expr

  `LawfulOrderLT` instance if available

- isPreorderInst? : Option Expr

  `IsPreorder` instance if available

- orderedAddInst? : Option Expr

  `OrderedAdd` instance with `IsPreorder` if available

- isLinearInst? : Option Expr

  `IsLinearOrder` instance if available

- noNatDivInst? : Option Expr

  `NoNatZeroDivisors`

- ringInst? : Option Expr

  `Ring` instance

- commRingInst? : Option Expr

  `CommRing` instance

- orderedRingInst? : Option Expr

  `OrderedRing` instance with `Preorder`

- fieldInst? : Option Expr

  `Field` instance

- charInst? : Option (Expr × Nat)

  `IsCharP` instance for `type` if available.

- zero : Expr
- ofNatZero : Expr
- one? : Option Expr
- leFn? : Option Expr
- ltFn? : Option Expr
- addFn : Expr
- zsmulFn : Expr
- nsmulFn : Expr
- zsmulFn? : Option Expr
- nsmulFn? : Option Expr
- homomulFn? : Option Expr
- subFn : Expr
- negFn : Expr
- vars : PArray Expr

  Mapping from variables to their denotations. Remark each variable can be in only one ring.

- varMap : PHashMap ExprPtr Var

  Mapping from `Expr` to a variable representing it.

- lowers : PArray (PArray IneqCnstr)

  Mapping from variables to their "lower" bounds. We say a relational constraint `c` is a lower bound for a variable `x` if `x` is the maximal variable in `c`, and `x` coefficient in `c` is negative.

- uppers : PArray (PArray IneqCnstr)

  Mapping from variables to their "upper" bounds. We say a relational constraint `c` is a upper bound for a variable `x` if `x` is the maximal variable in `c`, and `x` coefficient in `c` is positive.

- diseqs : PArray (PArray DiseqCnstr)

  Mapping from variables to their disequalities. We say a disequality constraint `c` is a disequality for a variable `x` if `x` is the maximal variable in `c`.

- assignment : PArray Rat

  Partial assignment being constructed by linarith.

- caseSplits : Bool

  `caseSplits` is `true` if linarith is searching for model and already performed case splits. This information is used to decide whether a conflict should immediately close the current `grind` goal or not.

- conflict? : Option UnsatProof

  `conflict?` is `some ..` if a contradictory constraint was derived. This field is only set when `caseSplits` is `true`. Otherwise, we can convert `UnsatProof` into a Lean term and close the current `grind` goal.

- diseqSplits : PHashMap Poly FVarId

  Cache decision variables used when splitting on disequalities. This is necessary because the same disequality may be in different conflicts.

- elimEqs : PArray (Option EqCnstr)

  Mapping from variable to equation constraint used to eliminate it. `solved` variables should not occur in `diseqs`, `lowers`, or `uppers`.

- elimStack : List Var

  Elimination stack. For every variable in `elimStack`. If `x` in `elimStack`, then `elimEqs[x]` is not `none`.

- occurs : PArray VarSet

  Mapping from variable to occurrences. For example, an entry `x ↦ {y, z}` means that `x` may occur in `lowers`, or `uppers`, or `diseqs` of variables `y` and `z`. If `x` occurs in `diseqs[y]`, `lowers[y]`, or `uppers[y]`, then `y` is in `occurs[x]`, but the reverse is not true. If `x` is in `elimStack`, then `occurs[x]` is the empty set.

- ignored : PArray Expr

  Linear constraints that are not supported. We use this information for diagnostics. TODO: store constraints instead.

Instances For

source
def Lean.Meta.Grind.Arith.Linear.instInhabitedStruct.default :
Struct
Equations

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

Instances For

source
instance Lean.Meta.Grind.Arith.Linear.instInhabitedStruct :
Inhabited Struct
Equations

- Lean.Meta.Grind.Arith.Linear.instInhabitedStruct = { default := Lean.Meta.Grind.Arith.Linear.instInhabitedStruct.default }

source
structure Lean.Meta.Grind.Arith.Linear.NatStruct :
Type

- id : Nat
- structId : Nat

  Id for `OfNatModule.Q`

- type : Expr
- u : Level

  Cached `getDecLevel type`

- natModuleInst : Expr

  `NatModule` instance for `type`

- leInst? : Option Expr

  `LE` instance if available

- ltInst? : Option Expr

  `LT` instance if available

- lawfulOrderLTInst? : Option Expr

  `LawfulOrderLT` instance if available

- isPreorderInst? : Option Expr

  `IsPreorder` instance if available

- orderedAddInst? : Option Expr

  `OrderedAdd` instance with `IsPreorder` if available

- isLinearInst? : Option Expr

  `IsLinearOrder` instance if available

- addRightCancelInst? : Option Expr
- rfl_q : Expr
- zero : Expr
- toQFn : Expr
- addFn : Expr
- smulFn : Expr
- termMap : PHashMap ExprPtr (Expr × Expr)

Instances For

source
structure Lean.Meta.Grind.Arith.Linear.State :
Type

State for all `IntModule` types detected by `grind`.

- structs : Array Struct

  Structures detected. We expect to find a small number of `IntModule`s in a given goal. Thus, using `Array` is fine here.

- typeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "structure id". We cache failures using `none`. `typeIdOf[type]` is `some id`, then `id < structs.size`.

- exprToStructId : PHashMap ExprPtr Nat
- forbiddenNatModules : PHashSet ExprPtr

  Some types are unordered rings, so we do not process them in `linarith`. When such types are detected in `getStructId?`, we add them to the set `forbiddenNatModules` to avoid reprocessing them in `getNatStructId?`.

- natStructs : Array NatStruct

  `NatModule`. We support them using the envelope `OfNatModule.Q`

- natTypeIdOf : PHashMap ExprPtr (Option Nat)

  Mapping from types to its "nat module id". We cache failures using `none`. `natTypeIdOf[type]` is `some id`, then `id < natStructs.size`. If a type is in this map, it is not in `typeIdOf`.

- exprToNatStructId : PHashMap ExprPtr Nat

Instances For

source
def Lean.Meta.Grind.Arith.Linear.instInhabitedState.default :
State
Equations

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

Instances For

source
instance Lean.Meta.Grind.Arith.Linear.instInhabitedState :
Inhabited State
Equations

- Lean.Meta.Grind.Arith.Linear.instInhabitedState = { default := Lean.Meta.Grind.Arith.Linear.instInhabitedState.default }

source
opaque Lean.Meta.Grind.Arith.Linear.linearExt :
SolverExtension State