Effective lookup of the preceding input copy

The field evaluator scans the already supplied gate/value pairs. A read of input i uses the last value attached to an earlier input gate for i, or the external input value if there is no such gate. Binary indices are compared directly; malformed large indices never cause unary expansion.

noncomputable def MIPRE.SAT.Circuit.matchesInputProg : Cost.PolyTimeFun (ℕ × Gate) Bool

Test whether a gate reads the specified external input.

Equations

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

@[simp]

theorem MIPRE.SAT.Circuit.matchesInputProg_apply (p : ℕ × Gate) : matchesInputProg.toFun p = decide (p.2 = Gate.input p.1)

def MIPRE.SAT.Circuit.lastInputValue {α : Type u_1} (l : List (Gate × α)) (i : ℕ) (initial : α) : α

Last supplied value of an input gate for i, with a supplied initial value.

Equations

• MIPRE.SAT.Circuit.lastInputValue l i initial = List.foldl (fun (acc : α) (p : MIPRE.SAT.Gate × α) => if p.1 = MIPRE.SAT.Gate.input i then p.2 else acc) initial l

@[simp]

theorem MIPRE.SAT.Circuit.lastInputValue_append {α : Type u_1} [Cost.SizedEncoding α] (l r : List (Gate × α)) (i : ℕ) (a : α) : lastInputValue (l ++ r) i a = lastInputValue r i (lastInputValue l i a)

theorem MIPRE.SAT.Circuit.lastInputValue_range {α : Type u_1} [Cost.SizedEncoding α] (C : Circuit) (k i : ℕ) (x w : ℕ → α) : lastInputValue (List.map (fun (j : ℕ) => (C.gates.getD j (Gate.const false), w j)) (List.range k)) i (x i) = Sum.elim x w (C.inputRef k i)

The executable scan reads exactly the variable selected by input-copy routing.

def MIPRE.SAT.Circuit.inputStep {α : Type u_1} (s : ℕ × α) (p : Gate × α) : ℕ × α

Equations

• MIPRE.SAT.Circuit.inputStep s p = (s.1, if p.1 = MIPRE.SAT.Gate.input s.1 then p.2 else s.2)

noncomputable def MIPRE.SAT.Circuit.inputStepProg {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun ((ℕ × α) × Gate × α) (ℕ × α)

Equations

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

theorem MIPRE.SAT.Circuit.fold_inputStep {α : Type u_1} [Cost.SizedEncoding α] (l : List (Gate × α)) (i : ℕ) (initial : α) : List.foldl inputStep (i, initial) l = (i, lastInputValue l i initial)

noncomputable def MIPRE.SAT.Circuit.lastInputValueProg {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun ((ℕ × α) × List (Gate × α)) α

The last-input-value scan, with an ambient polynomial running-time proof.

Equations

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

@[simp]

theorem MIPRE.SAT.Circuit.lastInputValueProg_apply {α : Type u_1} [Cost.SizedEncoding α] (p : (ℕ × α) × List (Gate × α)) : lastInputValueProg.toFun p = lastInputValue p.2 p.1.1 p.1.2