Module Th
module Th: sig end
Classification of function symbols.
Classification of function symbols.
type t = int
val eq : 'a -> 'a -> bool
val of_int : 'a -> 'a
val to_int : 'a -> 'a
val names : string list
val num_of_theories : t
val u : int
val la : int
val p : int
val bv : int
val cop : int
val pprod : int
val app : int
val arr : int
val bvarith : int
val to_string : t -> string
val all : int list
val interp : int list
exception Found of t
val of_string : string -> t
val pp : Format.formatter -> t -> unit
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
th |
: |
t
|
|
val is_fully_uninterp : int -> bool
val is_fully_interp : int -> bool
val of_sym : Sym.t -> int
module Array: sig end
Theory-specific normalization.
val maps : ((Term.t -> Term.t) -> Term.t -> Term.t) array
val map : int -> (Term.t -> Term.t) -> Term.t -> Term.t
sigma-normal forms.
val sigma : Sym.t -> Term.t list -> Term.t
Theory-specific solver
val solvers : (Fact.equal -> Fact.equal list) array
val solve : int -> Fact.equal -> Fact.equal list