package alt-ergo-lib

  1. Overview
  2. Docs
include Sig.X
type r
val make : Expr.t -> r * Expr.t list
val type_info : r -> Ty.t
val str_cmp : r -> r -> int
val hash_cmp : r -> r -> int
val equal : r -> r -> bool
val hash : r -> int
val leaves : r -> r list
val subst : r -> r -> r -> r
val solve : r -> r -> (r * r) list
val term_embed : Expr.t -> r
val term_extract : r -> Expr.t option * bool
val ac_embed : r Sig.ac -> r
val ac_extract : r -> r Sig.ac option
val color : r Sig.ac -> r
val fully_interpreted : Symbols.t -> Ty.t -> bool
val is_a_leaf : r -> bool
val print : Format.formatter -> r -> unit
val abstract_selectors : r -> (r * r) list -> r * (r * r) list
val top : unit -> r
val bot : unit -> r
val is_solvable_theory_symbol : Symbols.t -> Ty.t -> bool
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
val embed : r abstract -> r
val extract : r -> r abstract option
OCaml

Innovation. Community. Security.