Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof

source
def Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean.hash :
Int.Internal.Linear.Expr → UInt64
Equations
Instances For
    source
    @[instance_reducible]
    instance Lean.Meta.Grind.Arith.Cutsat.instHashableExpr_lean :
    Hashable Int.Internal.Linear.Expr
    Equations

    State for the cutsat proof construction monad.

    The final proof may reference only a small subset of the cutsat variables. Thus, we normalize the variables and remove any that are unused from the context. The variable order must be preserved, as the cutsat auxiliary theorems assume the polynomials are ordered.

    Another complication is that cutsat may reorder variables during the search, possibly several times. Each reordering starts a new epoch (see State.varsHistory), and a .reorder c justification is the delimiter into the previous epoch: c and its dependencies use the variable order of the epoch before the reordering. Every epoch has its own variable context and declarations.

    We create auxiliary free variables for variables, polynomials, and expressions. Cutsat also uses the ring solver to normalize nonlinear polynomials.

    Remark: after normalization variable declarations are expanded. We do not create let-declarations for them since they are just a numeral.

    source
    def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.toExprProof (h : UnsatProof) :
    GoalM Expr
    Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.Cutsat.setInconsistent (h : UnsatProof) :
      GoalM Unit
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        A cutsat proof may depend on decision variables. We collect them and perform non chronological backtracking.

        source
        partial def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.collectDecVars (c' : EqCnstr) :
        CollectDecVarsM Unit
        source
        partial def Lean.Meta.Grind.Arith.Cutsat.CooperSplit.collectDecVars (s : CooperSplit) :
        CollectDecVarsM Unit
        source
        partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.collectDecVars (c' : DvdCnstr) :
        CollectDecVarsM Unit
        source
        partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.collectDecVars (c' : LeCnstr) :
        CollectDecVarsM Unit
        source
        partial def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.collectDecVars (c' : DiseqCnstr) :
        CollectDecVarsM Unit
        source
        def Lean.Meta.Grind.Arith.Cutsat.UnsatProof.collectDecVars (h : UnsatProof) :
        CollectDecVarsM Unit
        Equations
        Instances For