Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.SearchM

source
inductive Lean.Meta.Grind.Arith.Cutsat.CaseKind :
Type

In principle, we only need to support two kinds of case split.

  • Disequalities.
  • Cooper-Left, but we have 4 different variants of this one.
Instances For
    source
    @[instance_reducible]
    instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedCaseKind :
    Inhabited CaseKind
    source
    structure Lean.Meta.Grind.Arith.Cutsat.Case :
    Type
    • kind : CaseKind
    • fvarId : FVarId

      Decision variable used to represent the case-split. For example, suppose we are splitting on p ≠ 0. Then, we create a decision variable h : p + 1 ≤ 0

    • saved : State

      Snapshot of the cutsat state for backtracking purposes. We do not use a trail stack.

    Instances For
      source
      @[instance_reducible]
      instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedCase :
      Inhabited Case
      source
      inductive Lean.Meta.Grind.Arith.Cutsat.Search.Kind :
      Type
      • rat : Kind

        Allow variables to be assigned to rational numbers during model construction.

      • int : Kind

        Variables must be assigned to integer numbers. Cooper case splits are required in this mode.

      Instances For
        source
        @[instance_reducible]
        instance Lean.Meta.Grind.Arith.Cutsat.Search.instInhabitedKind :
        Inhabited Kind
        source
        @[instance_reducible]
        instance Lean.Meta.Grind.Arith.Cutsat.Search.instBEqKind :
        BEq Kind
        source
        def Lean.Meta.Grind.Arith.Cutsat.Search.instBEqKind.beq :
        Kind → Kind → Bool
        Instances For
          source
          structure Lean.Meta.Grind.Arith.Cutsat.Search.State :
          Type

          State of the model search procedure.

          • cases : PArray Case

            Decision stack (aka case-split stack)

          • precise : Bool

            precise := false if not all constraints were satisfied during the search.

          • decVars : FVarIdSet

            Set of decision variables in cases.

          • steps : Nat

            Number of steps performed by the current search. Remark: we cannot use the steps counter in the cutsat state because it is rolled back when backtracking case splits.

          Instances For
            source
            @[reducible, inline]
            abbrev Lean.Meta.Grind.Arith.Cutsat.SearchM (α : Type) :
            Type
            Instances For
              source
              def Lean.Meta.Grind.Arith.Cutsat.isApprox :
              SearchM Bool

              Returns true if approximations are allowed.

              Instances For
                source
                def Lean.Meta.Grind.Arith.Cutsat.setImprecise :
                SearchM Unit

                Sets precise to false to indicate that some constraint was not satisfied.

                Instances For
                  source
                  def Lean.Meta.Grind.Arith.Cutsat.checkMaxSteps :
                  SearchM Bool

                  Increments the search steps counter, and returns true if the cumulative number of steps reached the liaSteps configuration threshold.

                  Instances For
                    source
                    def Lean.Meta.Grind.Arith.Cutsat.saveSteps :
                    SearchM Unit

                    Adds the number of steps performed by the current search to the cumulative counter in the cutsat state. It must be invoked after resetDecisionStack because backtracking rolls back the cutsat state.

                    Instances For
                      source
                      def Lean.Meta.Grind.Arith.Cutsat.mkCase (kind : CaseKind) :
                      SearchM FVarId
                      Instances For