Documentation

Lean.Meta.Tactic.Grind.BVDecide.Types

This module installs a no-op solver extension to grind. The sole job of this extension is to carry persistent, backtrackable state in grind's goals for bv_decide. This state is used for incremental pre-processing by bv_decide_push.

source
structure Lean.Meta.Grind.BVDecide.Caches :
Type

The caches of all bv_normalize passes that maintain one. bv_decide_push hands these from one invocation of the pre-processor to the next.

  • reduction : Sym.DSimp.Cache

    Cache for the DSimp component of the reduction pass.

  • rewriteSimp : Sym.Simp.Cache

    Cache for the Simp component of the rewriter.

  • rewriteDSimp : Sym.DSimp.Cache

    Cache for the DSimp component of the rewriter.

  • ac : Sym.Simp.Cache

    Cache for the Simp component of the AC pass.

Instances For
    source
    opaque Lean.Meta.Grind.BVDecide.bvExt :
    SolverExtension Caches
    source
    def Lean.Meta.Grind.BVDecide.getCaches :
    GoalM Caches
    Equations
    Instances For
      source
      @[inline]
      def Lean.Meta.Grind.BVDecide.setCaches (caches : Caches) :
      GoalM Unit
      Equations
      Instances For