Module Arith.Shostak

Parameters

module X : Sig.X
module P : Polynome.EXTENDED_Polynome with type r = X.r

Signature

type t = P.t

Type of terms of the theory

type r = X.r

Type of representants of terms of the theory

val name : string

Name of the theory

val is_mine_symb : Symbols.t -> Ty.t -> bool

return true if the symbol and the type are owned by the theory

val make : Expr.t -> r * Expr.t list

Give a representant of a term of the theory

val term_extract : r -> Expr.t option * bool
val color : r Sig.ac -> r
val type_info : t -> Ty.t
val embed : r -> t
val is_mine : t -> r
val leaves : t -> r list

Give the leaves of a term of the theory

val subst : r -> r -> t -> r
val compare : r -> r -> int
val equal : t -> t -> bool
val hash : t -> int

solve r1 r2, solve the equality r1=r2 and return the substitution

val solve : r -> r -> r Sig.solve_pb -> r Sig.solve_pb
val print : Format.formatter -> t -> unit
val fully_interpreted : Symbols.t -> bool
val abstract_selectors : t -> (r * r) list -> r * (r * r) list
val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string