Documentation

MIPRE.Foundations.SAT.Rename

Renaming formula inputs in polynomial time #

The padding construction changes the offsets of the five index blocks and their sign bits. Renaming scans the post-order serialization, applying an ambient program only at input nodes. renameBy uses a finite table and the binary-indexed lookup program, so its cost does not assume that all input indices are small.

source
def MIPRE.SAT.Fml.rename (ρ : ℕ → ℕ) :
Fml → Fml

Rename the input bits without changing the formula's tree.

Equations
Instances For
    source
    @[simp]
    theorem MIPRE.SAT.Fml.eval_rename (ρ : ℕ → ℕ) (f : Fml) (x : ℕ → Bool) :
    eval x (rename ρ f) = eval (x ∘ ρ) f
    source
    @[simp]
    theorem MIPRE.SAT.Fml.size_rename (ρ : ℕ → ℕ) (f : Fml) :
    (rename ρ f).size = f.size
    source
    theorem MIPRE.SAT.Fml.eval_congr_of_inputsLt {n : ℕ} {f : Fml} (hf : InputsLt n f) (x y : ℕ → Bool) (hxy : ∀ i < n, x i = y i) :
    eval x f = eval y f

    Only the input positions used by a bounded formula affect its value.

    source
    theorem MIPRE.SAT.Fml.InputsLt.rename {n m : ℕ} {f : Fml} (hf : InputsLt n f) (ρ : ℕ → ℕ) (hρ : ∀ i < n, ρ i < m) :
    InputsLt m (Fml.rename ρ f)
    source
    def MIPRE.SAT.Fml.Node.rename (ρ : ℕ → ℕ) :
    Node → Node

    The serialization-level action of a renaming.

    Equations
    Instances For
      source
      theorem MIPRE.SAT.Fml.rpn_rename (ρ : ℕ → ℕ) (f : Fml) :
      (rename ρ f).rpn = List.map (Node.rename ρ) f.rpn
      source
      noncomputable def MIPRE.SAT.Fml.renameNodeProg {α : Type u_1} [Cost.SizedEncoding α] (R : Cost.PolyTimeFun (α × ℕ) ℕ) :
      Cost.PolyTimeFun (α × Node) Node
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.SAT.Fml.renameNodeProg_apply {α : Type u_1} [Cost.SizedEncoding α] (R : Cost.PolyTimeFun (α × ℕ) ℕ) (a : α) (nd : Node) :
        (renameNodeProg R).toFun (a, nd) = Node.rename (fun (i : ℕ) => R.toFun (a, i)) nd
        source
        noncomputable def MIPRE.SAT.Fml.renameProg {α : Type u_1} [Cost.SizedEncoding α] (R : Cost.PolyTimeFun (α × ℕ) ℕ) :
        Cost.PolyTimeFun (α × Fml) Fml

        Any polynomial-time index transformation gives a polynomial-time formula renaming.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.SAT.Fml.renameProg_apply {α : Type u_1} [Cost.SizedEncoding α] (R : Cost.PolyTimeFun (α × ℕ) ℕ) (p : α × Fml) :
          (renameProg R).toFun p = rename (fun (i : ℕ) => R.toFun (p.1, i)) p.2
          source
          noncomputable def MIPRE.SAT.Fml.renameBy :
          Cost.PolyTimeFun (List ℕ × Fml) Fml

          Rename inputs using the supplied table; an out-of-range index maps to zero.

          Equations
          Instances For
            source
            @[simp]
            theorem MIPRE.SAT.Fml.renameBy_apply (ρ : List ℕ) (f : Fml) :
            renameBy.toFun (ρ, f) = rename (fun (i : ℕ) => ρ.getD i 0) f