Module SL.Term

type t
val nil : t
val is_nil : t -> bool
val is_heap_term : t -> bool
val as_heap_term : t -> MemoryModel.Field.t * t
val is_smt_term : t -> bool
val mk_var : string -> Sort.t -> t
val mk_fresh_var : string -> Sort.t -> t
val mk_heap_term : MemoryModel.Field.t -> t -> t
val mk_smt : SMT.t -> t
val mk_if_equal : t list -> t -> t -> t
val mk_block_begin : t -> t
val mk_block_end : t -> t
val of_var : Variable.t -> t
val get_subterm : t -> t

Assumes that the term is not a variable.

val mem_var : Variable.t -> t -> bool
val free_vars : t -> Variable.t list
val is_ground : ground:Variable.t list -> t -> bool
val is_ground' : forbidden:Variable.t list -> t -> bool

True if the term does not contatin any of provided variables.

TODO: logic_sig?

include Logic_sig.SORTED with type t := t and module Sort = Sort
module Sort = Sort
val get_sort : t -> Sort.t
val has_sort : Sort.t -> t -> bool
val show_with_sort : t -> string
include Datatype_sig.COMPARABLE with type t := t
include Datatype_sig.COMPARISON with type t := t
val compare : t -> t -> int
val equal : t -> t -> bool
include Datatype_sig.PRINTABLE with type t := t
include Datatype_sig.SHOW with type t := t
val show : t -> string

String representation of type t

val pp : Stdlib.Format.formatter -> t -> unit

Output to formatter

val print : ?prefix:string -> t -> unit

Output to stdout.

val show_option : t option -> string
val print_option : ?prefix:string -> t option -> unit
val dump : string -> t -> unit

Dump to file given by filename

Lists of printable values

val show_list : ?separator:string -> t list -> string
val pp_list : Stdlib.Format.formatter -> t list -> unit
val print_list : ?separator:string -> ?prefix:string -> t list -> unit
include Datatype_sig.COLLECTIONS with type t := t
module Set : Datatype_sig.SET with type elt = t

Set over type t

module MonoList : Datatype_sig.MONO_LIST with type key = t and type t = t list

Monomorphic list over type t

module Map : Datatype_sig.MAP with type key = t

Polymorphic map from t to 'a

module MonoMap (Data : Datatype_sig.SHOW) : Datatype_sig.MONO_MAP with type key = t and type data = Data.t

Monomorphic map from t to Data.t

val hash : t -> int
type view =
  1. | Var of Variable.t
  2. | HeapTerm of MemoryModel.Field.t * t
  3. | SmtTerm of SMT.t
  4. | IfEqual of t list * t * t
  5. | BlockBegin of t
  6. | BlockEnd of t
val view : t -> view
val as_var : t -> Variable.t