structure Lean.Meta.Grind.MBTC.Context : Type

Model-based theory combination context.

• isInterpreted : Expr → GoalM Bool

  isInterpreted e returns true if e is an interpreted symbol in the target theory. Example: + for cutsat

• hasTheoryVar : Expr → GoalM Bool

  hasTheoryVar e returns true if e has a theory variable in the target theory. For example, suppose we have the constraint x + y ≤ 0, then x and y have theory vars in the cutsat procedure.

• eqAssignment : Expr → Expr → GoalM Bool

  eqAssignment x y returns true it the theory variables for x and y have the same interpretation/assignment in the target theory. For example, suppose we have the constraint x + y ≤ 0, and cutsat satified it by assignining both x and y to 0. Then, eqAssignment x y must return true.

def Lean.Meta.Grind.mbtc (ctx : MBTC.Context) : GoalM Bool

Model-based theory combination.

Equations

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

def Lean.Meta.Grind.mbtcTac (ctx : MBTC.Context) : GrindTactic

Equations

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