def Int.Internal.Linear.Poly.isZero : Poly → Bool

Equations

• (Int.Internal.Linear.Poly.num 0).isZero = true
• x✝.isZero = false

def Int.Internal.Linear.Poly.isSorted (p : Poly) : Bool

Returns true if the variables in the given polynomial are sorted in decreasing order.

Equations

• p.isSorted = Int.Internal.Linear.Poly.isSorted.go✝ none p

def Lean.Meta.Grind.Arith.Cutsat.get' : GoalM State

Equations

• Lean.Meta.Grind.Arith.Cutsat.get' = Lean.Meta.Grind.Arith.Cutsat.cutsatExt.getState

@[inline]

def Lean.Meta.Grind.Arith.Cutsat.modify' (f : State → State) : GoalM Unit

Equations

• Lean.Meta.Grind.Arith.Cutsat.modify' f = Lean.Meta.Grind.Arith.Cutsat.cutsatExt.modifyState f

def Lean.Meta.Grind.Arith.Cutsat.isSupportedType (type : Expr) : GoalM Bool

Returns true if cutsat natively supports type.

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.canBeEvaluated (α : Expr) : GoalM Bool

Returns true if numerals of the embedded type α can be evaluated, i.e., their embedded (Fin.val/toNat/toInt) value can be computed directly. Such numerals are not given embedding-accessor applications. Currently this means the modulus of α is known, but future embedded types may be evaluable without one.

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.inconsistent : GoalM Bool

Returns true if the cutsat state is inconsistent.

Equations

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

@[extern lean_grind_cutsat_mk_var]

opaque Lean.Meta.Grind.Arith.Cutsat.mkVar (e : Expr) : GoalM Var

Creates a new variable in the cutsat module.

def Lean.Meta.Grind.Arith.Cutsat.getVars : GoalM (PArray Expr)

Equations

• Lean.Meta.Grind.Arith.Cutsat.getVars = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.vars

def Lean.Meta.Grind.Arith.Cutsat.getVar (x : Var) : GoalM Expr

Equations

• Lean.Meta.Grind.Arith.Cutsat.getVar x = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.vars[x]!

def Lean.Meta.Grind.Arith.Cutsat.hasVar (e : Expr) : GoalM Bool

Returns true if e is already associated with a cutsat variable.

Equations

• Lean.Meta.Grind.Arith.Cutsat.hasVar e = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure (Lean.PersistentHashMap.contains __do_lift.varMap { expr := e })

def Lean.Meta.Grind.Arith.Cutsat.isIntTerm (e : Expr) : GoalM Bool

Equations

• Lean.Meta.Grind.Arith.Cutsat.isIntTerm e = Lean.Meta.Grind.Arith.Cutsat.hasVar e

def Lean.Meta.Grind.Arith.Cutsat.eliminated (x : Var) : GoalM Bool

Returns true if x has been eliminated using an equality constraint.

Equations

• Lean.Meta.Grind.Arith.Cutsat.eliminated x = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.elimEqs[x]!.isSome

@[extern lean_grind_cutsat_assert_eq]

opaque Lean.Meta.Grind.Arith.Cutsat.EqCnstr.assert (c : EqCnstr) : GoalM Unit

def Lean.Meta.Grind.Arith.Cutsat.resetAssignmentFrom (x : Var) : GoalM Unit

Resets the assignment of any variable bigger or equal to x.

Equations

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

def Int.Internal.Linear.Poly.pp (p : Poly) : Lean.Meta.Grind.GoalM Lean.MessageData

Equations

• One or more equations did not get rendered due to their size.
• (Int.Internal.Linear.Poly.num k).pp = pure (Lean.toMessageData k)
• (Int.Internal.Linear.Poly.add 1 x p_2).pp = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.getVar x Int.Internal.Linear.Poly.pp.go✝ (Lean.Meta.Grind.Arith.quoteIfArithTerm __do_lift) p_2

def Int.Internal.Linear.Poly.denoteExpr' (p : Poly) : Lean.Meta.Grind.GoalM Lean.Expr

Equations

• p.denoteExpr' = do let vars ← Lean.Meta.Grind.Arith.Cutsat.getVars liftM (Int.Internal.Linear.Poly.denoteExpr (fun (x : Nat) => vars[x]!) p)

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.isTrivial (c : DvdCnstr) : Bool

Equations

• c.isTrivial = match c.p with | Int.Internal.Linear.Poly.num k' => k' % c.d == 0 | x => c.d == 1

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.pp (c : DvdCnstr) : GoalM MessageData

Equations

• c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData c.d ++ Lean.toMessageData " ∣ " ++ Lean.toMessageData __do_lift)

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.denoteExpr (c : DvdCnstr) : GoalM Expr

Equations

• c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkIntDvd (Lean.toExpr c.d) __do_lift)

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.throwUnexpected {α : Type} (c : DvdCnstr) : GoalM α

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.isTrivial (c : DiseqCnstr) : Bool

Equations

• c.isTrivial = match c.p with | Int.Internal.Linear.Poly.num k => k != 0 | x => c.p.getConst % ↑c.p.gcdCoeffs' != 0

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.pp (c : DiseqCnstr) : GoalM MessageData

Equations

• c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData __do_lift ++ Lean.toMessageData " ≠ 0")

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.throwUnexpected {α : Type} (c : DiseqCnstr) : GoalM α

Equations

• c.throwUnexpected = do let __do_lift ← c.pp Lean.throwError (Lean.toMessageData "`grind` internal error, unexpected" ++ Lean.toMessageData (Lean.indentD __do_lift))

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.denoteExpr (c : DiseqCnstr) : GoalM Expr

Equations

• c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkNot (Lean.mkIntEq __do_lift (Lean.mkIntLit 0)))

@[extern lean_grind_cutsat_assert_le]

opaque Lean.Meta.Grind.Arith.Cutsat.LeCnstr.assert (c : LeCnstr) : GoalM Unit

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.isTrivial (c : LeCnstr) : Bool

Equations

• c.isTrivial = match c.p with | Int.Internal.Linear.Poly.num k => decide (k ≤ 0) | x => false

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.pp (c : LeCnstr) : GoalM MessageData

Equations

• c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData __do_lift ++ Lean.toMessageData " ≤ 0")

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.denoteExpr (c : LeCnstr) : GoalM Expr

Equations

• c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkIntLE __do_lift (Lean.mkIntLit 0))

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.throwUnexpected {α : Type} (c : LeCnstr) : GoalM α

Equations

• c.throwUnexpected = do let __do_lift ← c.pp Lean.throwError (Lean.toMessageData "`grind` internal error, unexpected" ++ Lean.toMessageData (Lean.indentD __do_lift))

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.isTrivial (c : EqCnstr) : Bool

Equations

• c.isTrivial = match c.p with | Int.Internal.Linear.Poly.num k => k == 0 | x => false

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.pp (c : EqCnstr) : GoalM MessageData

Equations

• c.pp = do let __do_lift ← c.p.pp pure (Lean.toMessageData __do_lift ++ Lean.toMessageData " = 0")

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.denoteExpr (c : EqCnstr) : GoalM Expr

Equations

• c.denoteExpr = do let __do_lift ← c.p.denoteExpr' pure (Lean.mkIntEq __do_lift (Lean.mkIntLit 0))

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.throwUnexpected {α : Type} (c : EqCnstr) : GoalM α

Equations

• c.throwUnexpected = do let __do_lift ← c.pp Lean.throwError (Lean.toMessageData "`grind` internal error, unexpected" ++ Lean.toMessageData (Lean.indentD __do_lift))

def Lean.Meta.Grind.Arith.Cutsat.getOccursOf (x : Var) : GoalM VarSet

Returns occurrences of x.

Equations

• Lean.Meta.Grind.Arith.Cutsat.getOccursOf x = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure __do_lift.occurs[x]!

def Lean.Meta.Grind.Arith.Cutsat.addOcc (x y : Var) : GoalM Unit

Adds y as an occurrence of x. That is, x occurs in lowers[y], uppers[y], or dvdCnstrs[y].

Equations

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

def Int.Internal.Linear.Poly.updateOccs (p : Poly) : Lean.Meta.Grind.GoalM Unit

Given p a polynomial being inserted into lowers, uppers, or dvdCnstrs, get its leading variable y, and adds y as an occurrence for the remaining variables in p.

Equations

• (Int.Internal.Linear.Poly.add k x p_2).updateOccs = Int.Internal.Linear.Poly.updateOccs.go✝ x p_2
• p.updateOccs = Lean.throwError (Lean.toMessageData "`grind` internal error, unexpected constant polynomial")

def Int.Internal.Linear.Poly.eval? (p : Poly) : Lean.Meta.Grind.GoalM (Option Rat)

Tries to evaluate the polynomial p using the partial model/assignment built so far. The result is none if the polynomial contains variables that have not been assigned.

Equations

• p.eval? = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' have a : Lean.PArray Rat := __do_lift.assignment pure (Int.Internal.Linear.Poly.eval?.go✝ a 0 p)

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.LeCnstr.isUnsat (c : LeCnstr) : Bool

Equations

• c.isUnsat = c.p.isUnsatLe

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.isUnsat (c : DvdCnstr) : Bool

Equations

• c.isUnsat = Int.Internal.Linear.Poly.isUnsatDvd c.d c.p

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.satisfied (c : DvdCnstr) : GoalM LBool

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

Equations

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

def Int.Internal.Linear.Poly.satisfiedLe (p : Poly) : Lean.Meta.Grind.GoalM Lean.LBool

Equations

• p.satisfiedLe = do let __x ← p.eval? match __x with | some v => pure (Lean.Bool.toLBool (decide (v ≤ 0))) | x => pure Lean.LBool.undef

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.satisfied (c : LeCnstr) : GoalM LBool

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

Equations

• c.satisfied = c.p.satisfiedLe

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.satisfied (c : DiseqCnstr) : GoalM LBool

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

Equations

• c.satisfied = do let __x ← c.p.eval? match __x with | some v => pure (Lean.Bool.toLBool (v != 0)) | x => pure Lean.LBool.undef

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.satisfied (c : EqCnstr) : GoalM LBool

Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

Equations

• c.satisfied = do let __x ← c.p.eval? match __x with | some v => pure (Lean.Bool.toLBool (v == 0)) | x => pure Lean.LBool.undef

def Int.Internal.Linear.Poly.findVarToSubst (p : Poly) : Lean.Meta.Grind.GoalM (Option (Int × Var × Lean.Meta.Grind.Arith.Cutsat.EqCnstr))

Given a polynomial p, returns some (x, k, c) if p contains the monomial k*x, and x has been eliminated using the equality c.

Equations

• One or more equations did not get rendered due to their size.
• (Int.Internal.Linear.Poly.num k).findVarToSubst = pure none

def Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.numCases (pred : CooperSplitPred) : Nat

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.pp (pred : CooperSplitPred) : GoalM MessageData

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.pp (h : UnsatProof) : GoalM MessageData

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c).pp = c.pp
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c).pp = c.pp
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c).pp = c.pp
• (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c).pp = c.pp