sig
  type formula =
      True
    | False
    | Not of Prop_logic.formula
    | Var of string
    | And of Prop_logic.formula * Prop_logic.formula
    | Or of Prop_logic.formula * Prop_logic.formula
    | Implicates of Prop_logic.formula * Prop_logic.formula
    | Equals of Prop_logic.formula * Prop_logic.formula
  type model
  val empty : Prop_logic.model
  type assignment = Prop_logic.model -> Prop_logic.model
  exception Var_unbound
  val lookup : var:string -> Prop_logic.model -> bool
  val assign : var:string -> bool -> Prop_logic.assignment
  val combine :
    Prop_logic.assignment -> Prop_logic.assignment -> Prop_logic.assignment
  val create : Prop_logic.assignment list -> Prop_logic.model
  val solve : Prop_logic.formula -> Prop_logic.model -> bool
  val find_vars : Prop_logic.formula -> string list
  val print_bool : bool -> unit
  val print_model : Prop_logic.model -> unit
  val is_solvable : Prop_logic.formula -> Prop_logic.model option
  val find_models : Prop_logic.formula -> Prop_logic.model list
end