package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
module LX : Xliteral.S with type elt = r
val empty : unit -> t
val add : t -> Expr.t -> t * Expr.t list
val mem : t -> Expr.t -> bool
val find : t -> Expr.t -> r * Explanation.t
val find_r : t -> r -> r * Explanation.t
val union : t -> r -> r -> Explanation.t -> t * (r * (r * r * Explanation.t) list * r) list
val distinct : t -> r list -> Explanation.t -> t
val are_equal : t -> Expr.t -> Expr.t -> added_terms:bool -> Th_util.answer
val are_distinct : t -> Expr.t -> Expr.t -> Th_util.answer
val already_distinct : t -> r list -> bool
val class_of : t -> Expr.t -> Expr.t list
val rclass_of : t -> r -> Expr.Set.t
val cl_extract : t -> Expr.Set.t list
val model : t -> (r * Expr.t list * (Expr.t * r) list) list * Expr.t list list
val print : t -> unit
val term_repr : t -> Expr.t -> Expr.t
val make : t -> Expr.t -> r
val is_normalized : t -> r -> bool
val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t
val output_concrete_model : t -> unit