infix 2 ==>
infix 3 OR ||
infix 4 AND &&
infix 5 == <>;
infix 3 OR
infix 4 AND;
infix 2 IMPLIES IFF;
infix 2 INTERSECTS;
infix 2 IMP;
nonfix --;

signature LOGICSIG =
sig
  include PROPOSITIONSIG
  eqtype Bdd
  eqtype Var
  type Assoc
  type Subst
  datatype Method = SIFT |  STABLE_WINDOW | NONE
  datatype 'a Option = Some of 'a |None
  exception Error of string
  val bdd_start    : unit -> unit
  val bdd_restart : unit -> unit

  val lit2var : Lit -> Var
  val var2lit : Var -> Lit
  val rmLit   : Lit -> unit
  val rmVar   : Var -> unit

  val Assoc : Var list -> Assoc
  val Subst : (Var * Bdd) list -> Subst

  val V : Var -> Bdd
  val I : Var -> int

  val NEW : unit -> Var
  val nVars   : unit -> int
  val noVars  : unit -> Bdd
  val allVars : unit -> Bdd
  val TRUE    : unit -> Bdd 
  val FALSE   : unit -> Bdd 

  val eval :  Name TypedList ->
     Term TypedList -> (Lit -> Bdd) -> Formula -> Bdd
  val symb : Bdd -> Formula

  val ++ : Bdd -> Bdd
  val -- : Bdd -> unit

  val SUPPORT : Bdd -> (Var list)
  val SATISFY : Bdd -> Bdd
  val SAT : Bdd -> (Var list) Option

  val OR  : Bdd * Bdd -> Bdd
  val AND : Bdd * Bdd -> Bdd
  val IMP : Bdd * Bdd -> Bdd
  val INTERSECTS : Bdd * Bdd -> bool
  val IMPLIES : Bdd * Bdd -> bool
  val IFF : Bdd * Bdd -> Bdd
  val ITE : Bdd -> Bdd -> Bdd -> Bdd
  val NOT : Bdd -> Bdd

  val ORL  : Bdd list -> Bdd
  val ANDL : Bdd list -> Bdd

  val EXISTS : Assoc -> Bdd -> Bdd
  val PROD   : Assoc -> Bdd -> Bdd -> Bdd
  val SUBST  : Subst -> Bdd -> Bdd

  val REDUCE : Bdd -> Bdd -> Bdd

  val GC : unit -> unit  
  val REORDER : unit -> unit
  val REORDERING : Method -> unit
  val TOTALSIZE : unit -> int
  val SIZE : Bdd -> int
  val SIZEMULTIPLE : Bdd list -> int
  val FRACTION : Bdd -> real
  val STATES : Bdd -> int

  val LITWITHINDEX : int -> Lit
  val CACHERATIO : int -> int
  val VO : unit -> unit
end;