mentionsVarClause

formal source

  19  | .neg u => decide (u = v)
  20
  21/-- Whether a variable is mentioned in a clause. -/
  22def mentionsVarClause {n} (C : Clause n) (v : Var n) : Bool :=
  23  C.any (fun l => mentionsVarLit l v)
  24
  25/-- Whether a variable is mentioned in an XOR constraint. -/
  26def mentionsVarXOR {n} (X : XORConstraint n) (v : Var n) : Bool :=
  27  X.vars.any (fun u => decide (u = v))
  28
  29/-- Whether a variable is mentioned in a mixed constraint. -/
  30def mentionsVar {n} (K : Constraint n) (v : Var n) : Bool :=
  31  match K with
  32  | .cnf C => mentionsVarClause C v
  33  | .xor X => mentionsVarXOR X v
  34
  35/-- Satisfaction semantics for mixed constraints. -/
  36def satisfiesConstraint {n} (a : Assignment n) (K : Constraint n) : Prop :=
  37  match K with
  38  | .cnf C => evalClause a C = true
  39  | .xor X => parityOf a X.vars = X.parity
  40
  41/-- The constraint K determines variable v w.r.t. reference assignment `aRef`:
  42    fixing all non-v variables to `aRef` and requiring `K` forces `v = aRef v`. -/
  43def determinesVar {n}
  44  (aRef : Assignment n) (K : Constraint n) (v : Var n) : Prop :=
  45  ∀ (a' : Assignment n),
  46    (∀ w : Var n, w ≠ v → a' w = aRef w) →
  47    satisfiesConstraint a' K →
  48    a' v = aRef v
  49
  50/-- Collect all constraints arising from a CNF+XOR instance. -/
  51def constraintsOf {n} (φ : CNF n) (H : XORSystem n) : List (Constraint n) :=
  52  (φ.clauses.map Constraint.cnf) ++ (H.map Constraint.xor)