setVar_same

formal source

  17def setVar {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) : PartialAssignment n :=
  18  fun w => if w = v then some b else σ w
  19
  20@[simp] lemma setVar_same {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) :
  21    setVar σ v b v = some b := by
  22  unfold setVar; simp
  23
  24lemma setVar_ne {n} (σ : PartialAssignment n) (v w : Var n) (b : Bool) (hvw : w ≠ v) :
  25    setVar σ v b w = σ w := by
  26  unfold setVar
  27  simp only [ite_eq_right_iff]
  28  intro heq
  29  exact absurd heq hvw
  30
  31/-- Evaluate a literal under a partial assignment. -/
  32def valueOfLit {n} (σ : PartialAssignment n) : Lit n → Option Bool
  33  | .pos v => σ v
  34  | .neg v => Option.map not (σ v)
  35
  36/-- Evaluate a clause under a partial assignment: returns `some b` if all literals
  37    are known, otherwise none. -/
  38def valueOfClause {n} (σ : PartialAssignment n) (C : Clause n) : Option Bool :=
  39  let vals := C.map (valueOfLit σ)
  40  if vals.all Option.isSome then
  41    some (vals.any fun o => o.getD false)
  42  else
  43    none
  44
  45/-- Evaluate an XOR constraint under a partial assignment: returns `some b` if all
  46    vars are known, else none. -/
  47def valueOfXOR {n} (σ : PartialAssignment n) (X : XORConstraint n) : Option Bool :=
  48  if X.vars.all (fun v => (σ v).isSome) then
  49    some (X.vars.foldl (fun acc v => Bool.xor acc ((σ v).getD false)) false)
  50  else