sig
  type t
  val equal : Symbol.t -> Symbol.t -> bool
  val hash : Symbol.t -> int
  val compare : Symbol.t -> Symbol.t -> int
  val name_declared : string -> bool
  val declare : string -> int -> Symbol.t
  val declare_uninterpreted : string -> int -> Symbol.t
  val find : string -> Symbol.t
  val arity : Symbol.t -> int
  val interpreted : Symbol.t -> bool
  val string_of_symbol : Symbol.t -> string
  val pp_print : Format.formatter -> Symbol.t -> unit
  module Primitive :
    sig
      val truth : Symbol.t
      val falsity : Symbol.t
      val equality : Symbol.t
      val negation : Symbol.t
      val disjunction : Symbol.t
      val conjunction : Symbol.t
      val difference : Symbol.t
      val equivalence : Symbol.t
      val implication : Symbol.t
      val conditional : Symbol.t
      val ite : Symbol.t
      val k : Symbol.t
      val update : Symbol.t
      val mk_array : Symbol.t
      val select : Symbol.t
      val store : Symbol.t
      val less : Symbol.t
      val less_or_equal : Symbol.t
      val greater : Symbol.t
      val greater_or_equal : Symbol.t
      val unary_minus : Symbol.t
      val plus : Symbol.t
      val minus : Symbol.t
      val times : Symbol.t
      val divide : Symbol.t
    end
end

---

Hosted by the ^* web site.
^*Other names and brands may be claimed as the property of others.