package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val empty : unit -> t
val assume : ?ordered:bool -> (Expr.t * Explanation.t * int * int) list -> t -> t * Expr.Set.t * int
val query : Expr.t -> t -> Th_util.answer
val print_model : Format.formatter -> t -> unit
val cl_extract : t -> Expr.Set.t list
val extract_ground_terms : t -> Expr.Set.t
val get_real_env : t -> Ccx.Main.t
val get_case_split_env : t -> Ccx.Main.t
val do_case_split : t -> t * Expr.Set.t
val add_term : t -> Expr.t -> add_in_cs:bool -> t
val compute_concrete_model : t -> t
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
val theories_instances : do_syntactic_matching:bool -> (Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t) -> t -> (Expr.t -> Expr.t -> bool) -> int -> int -> t * Sig_rel.instances
val get_assumed : t -> Expr.Set.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct