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

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

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

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

@[inline]

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

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

Returns true if cutsat natively supports type.

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

Returns true if cutsat is enabled and natively supports type, i.e., cutsat handles it.

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.

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

Returns true if the cutsat state is inconsistent.

@[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)

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

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

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

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

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

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

@[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.

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

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

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

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

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

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

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

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

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

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

@[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

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

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

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

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

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

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

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

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

Returns occurrences of 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].

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.

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.

@[reducible, inline]

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

@[reducible, inline]

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

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.

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

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.

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.

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.

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.

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

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

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