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 -> (Shostak.Literal.t * Th_util.lit_origin * Explanation.t * int * int) list -> t -> t * AltErgoLib.Expr.Set.t * int
val add_objective : t -> Objective.Function.t -> Objective.Value.t -> t

add_objective env fn value indicates that the objective fn has been optimized to value.

val query : Expr.t -> t -> Th_util.answer
val cl_extract : t -> AltErgoLib.Expr.Set.t list
val extract_ground_terms : t -> AltErgoLib.Expr.Set.t
val get_real_env : t -> Ccx.Main.t
val get_case_split_env : t -> Ccx.Main.t
val do_optimize : acts:Shostak.Literal.t Th_util.acts -> t -> unit
val do_case_split : ?acts:Shostak.Literal.t Th_util.acts -> t -> Util.case_split_policy -> t * AltErgoLib.Expr.Set.t
val add_term : t -> Expr.t -> add_in_cs:bool -> t
val compute_concrete_model : acts:Shostak.Literal.t Th_util.acts -> t -> unit
val extract_concrete_model : declared_ids:Id.typed list -> t -> Models.t Stdlib.Lazy.t * Objective.Model.t
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
val theories_instances : do_syntactic_matching:bool -> (Matching_types.info AltErgoLib.Expr.Map.t * Expr.t list AltErgoLib.Expr.Map.t AltErgoLib.Symbols.Map.t) -> t -> (Expr.t -> Expr.t -> bool) -> int -> int -> t * Sig_rel.instances
val get_assumed : t -> AltErgoLib.Expr.Set.t
val reinit_cpt : unit -> unit

Reinitializes the internal counter.

val get_objectives : t -> Objective.Model.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