Module type Acsym.TERM


module type TERM = sig  end
Canonizer and iterators for AC theories.

val d_interp : Term.t -> Term.t * Term.t
If a is of the form b*c, then d_interp a returns (b, c).
Parameters:
? : Term.t
val is_interp : Term.t -> bool
is_interp a holds iff a is of the form b*c.
Parameters:
? : Term.t
val make : Term.t -> Term.t -> Term.t
For canonical a, b, make a b returns a canonical term c with AC |= c = a * b.
Parameters:
? : Term.t
? : Term.t
val iterate : Term.t -> int -> Term.t
For n>=1, iterate a n iterates make a n-1 times. We sometimes write a^n to denote this term.
Parameters:
? : Term.t
? : int
val multiplicity : Term.t -> Term.t -> int
multiplicity x a counts the number of interpreted occurrences of x in a.
Parameters:
? : Term.t
? : Term.t
val decompose : Term.t -> (Term.t * int) * Term.t option
Decompose x*x*...*x*y*.... into (x, n) with n the multiplicity of x in a and y*....
Parameters:
? : Term.t
val fold : (Term.t -> int -> 'a -> 'a) -> Term.t -> 'a -> 'a
If a is of the form x1^m1*(x2^m2*...*xn^mn), then fold f a e is f x1 m1 (f x2 m2 (... (f xn mn e)...)).
Parameters:
? : Term.t -> int -> 'a -> 'a
? : Term.t
? : 'a
val iter : (Term.t -> int -> unit) -> Term.t -> unit
If a is of the form x1^m1*(x2^m2*...*xn^mn), then iter f a is f x1 m1; f x2 m2; ...; f xn mn.
Parameters:
? : Term.t -> int -> unit
? : Term.t
val sigma : Sym.t -> Term.t list -> Term.t
If f equals *, then sigma f [a1; a2] reduces to make a1 a2; otherwise the uninterpreted application f(a1, a2) is built.
Parameters:
? : Sym.t
? : Term.t list
val map : (Term.t -> Term.t) -> Term.t -> Term.t
map f a applies f at uninterpreted positions and recanonizes the result.
Parameters:
? : Term.t -> Term.t
? : Term.t