theory DebugNitpick
  imports Main "HOL-Library.FSet"
begin

datatype 'a boolean_circuit =
  Var 'a
  | Not "'a boolean_circuit"
  | And "'a boolean_circuit fset"
  | Or "'a boolean_circuit fset"

typedef 'a var_interpretation = "{var :: ('a ⇒ bool). finite {v. var v}}"
  using not_finite_existsD by auto

(* the number of variables that are assigned to True *)
definition weight :: "'a var_interpretation ⇒ nat" where
  "weight var = card {v. Rep_var_interpretation var v}"

function eval :: "'a var_interpretation ⇒ 'a boolean_circuit ⇒ bool" where
  "eval var (Var v) = Rep_var_interpretation var v"
| "eval var (Not circuit) = (¬eval var circuit)"
| "eval var (And circuits) = fBall circuits (eval var)"
| "eval var (Or circuits) = fBex circuits (eval var)"
  by pat_completeness auto
termination sorry (* this is provable, omitted here for simplicity *)

(* weighted circuit sat = is there a satisfying interpretation with weight k? *)
definition wcs :: "'a boolean_circuit ⇒ nat ⇒ bool" where
  "wcs circuit k = (∃ var. weight var = k ∧ eval var circuit)"

datatype debug_type = debug_el

declare[[show_types]]

(* "And {Or {}}" does not have a satisfying interpretation with weight 0,
    i.e. the empty interpretation *)
lemma "¬wcs (And {| Or (fempty :: debug_type boolean_circuit fset)|}) 0"
  nitpick
  (* here, nitpick finds a counterexample with an empty variable interpretation
     in wcs, which should however have "eval var circuit" evaluate to False;
     so this counterexample is invalid *)
  unfolding wcs_def
  apply (simp)
  done

end