module type T = sig endth is specified by means of amap f a for replacing uninterpreted
subterms of a with f a and canonizing the result, andsolve. map f a for replacing uninterpreted
positions x of a with f b followed by canonization in the
given theory, anddisjunction. If disjunction always returns Not_found,
then th is also said to be a convex Shostak theory.val th : Th.tval map : (Term.t -> Term.t) -> Term.t -> Term.t
val solve : Fact.Equal.t -> Fact.Equal.t list| Parameters: |
|
val disjunction : Fact.Equal.t -> Clause.t| Parameters: |
|