package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

Data structures

type binders = (Ty.t * int) Symbols.Map.t
type t
type decl_kind =
  1. | Dtheory
  2. | Daxiom
  3. | Dgoal
  4. | Dpredicate of t
  5. | Dfunction of t
type term_view = private {
  1. f : Symbols.t;
  2. xs : t list;
  3. ty : Ty.t;
  4. bind : bind_kind;
  5. tag : int;
  6. vars : (Ty.t * int) Symbols.Map.t;
  7. vty : AltErgoLib.Ty.Svty.t;
  8. depth : int;
  9. nb_nodes : int;
  10. pure : bool;
  11. mutable neg : t option;
}
and bind_kind =
  1. | B_none
  2. | B_lemma of quantified
  3. | B_skolem of quantified
  4. | B_let of letin
and quantified = private {
  1. name : string;
  2. main : t;
  3. toplevel : bool;
  4. user_trs : trigger list;
  5. binders : binders;
  6. sko_v : t list;
  7. sko_vty : Ty.t list;
  8. loc : Loc.t;
  9. kind : decl_kind;
}
and letin = private {
  1. let_v : Symbols.t;
  2. let_e : t;
  3. in_e : t;
  4. let_sko : t;
  5. is_bool : bool;
}
and semantic_trigger =
  1. | Interval of t * Symbols.bound * Symbols.bound
  2. | MapsTo of Var.t * t
  3. | NotTheoryConst of t
  4. | IsTheoryConst of t
  5. | LinearDependency of t * t
and trigger = {
  1. content : t list;
  2. semantic : semantic_trigger list;
  3. hyp : t list;
  4. t_depth : int;
  5. from_user : bool;
  6. guard : t option;
}
module Set : Stdlib.Set.S with type elt = t
module Map : Stdlib.Map.S with type key = t
type subst = t Symbols.Map.t * Ty.subst
type lit_view = private
  1. | Eq of t * t
  2. | Eql of t list
  3. | Distinct of t list
  4. | Builtin of bool * Symbols.builtin * t list
  5. | Pred of t * bool
type form_view = private
  1. | Unit of t * t
  2. | Clause of t * t * bool
  3. | Iff of t * t
  4. | Xor of t * t
  5. | Literal of t
  6. | Lemma of quantified
  7. | Skolem of quantified
  8. | Let of letin

different views of an expression

val term_view : t -> term_view
val lit_view : t -> lit_view
val form_view : t -> form_view

constant casts

val int_view : t -> int

Extracts the integer value of the expression, if there is one.

The returned value may be negative or null.

  • raises Failure

    if the expression is not a constant integer.

val rounding_mode_view : t -> Fpa_rounding.rounding_mode

Extracts the rounding mode value of the expression, if there is one.

  • raises Failure

    if the expression is not a constant rounding mode.

pretty printing

val print : Stdlib.Format.formatter -> t -> unit
val print_list : Stdlib.Format.formatter -> t list -> unit
val print_list_sep : string -> Stdlib.Format.formatter -> t list -> unit
val print_triggers : Stdlib.Format.formatter -> trigger list -> unit

Comparison and hashing functions

val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val uid : t -> int
val compare_subst : subst -> subst -> int
val equal_subst : subst -> subst -> bool
val compare_quant : quantified -> quantified -> int
val compare_let : letin -> letin -> int

Some auxiliary functions

val mk_binders : Set.t -> binders
val free_vars : t -> (Ty.t * int) Symbols.Map.t -> (Ty.t * int) Symbols.Map.t
val free_type_vars : t -> AltErgoLib.Ty.Svty.t
val is_ground : t -> bool
val size : t -> int
val depth : t -> int
val is_positive : t -> bool
val neg : t -> t
val is_fresh : t -> bool
val is_fresh_skolem : t -> bool
val is_int : t -> bool
val is_real : t -> bool
val type_info : t -> Ty.t
val symbol_info : t -> Symbols.t

Labeling and models

val add_label : Hstring.t -> t -> unit
val label : t -> Hstring.t
val name_of_lemma : t -> string
val name_of_lemma_opt : t option -> string
val print_tagged_classes : Stdlib.Format.formatter -> Set.t list -> unit

smart constructors for terms

val mk_term : Symbols.t -> t list -> Ty.t -> t
val vrai : t
val faux : t
val void : t
val int : string -> t
val real : string -> t
val bitv : string -> Ty.t -> t
val fresh_name : Ty.t -> t
val pred : t -> t

smart constructors for literals

val mk_eq : iff:bool -> t -> t -> t
val mk_distinct : iff:bool -> t list -> t
val mk_builtin : is_pos:bool -> Symbols.builtin -> t list -> t

simple smart constructors for formulas

val mk_or : t -> t -> bool -> t
val mk_and : t -> t -> bool -> t
val mk_imp : t -> t -> t
val mk_iff : t -> t -> t
val mk_if : t -> t -> t -> t
val mk_xor : t -> t -> t
val mk_ite : t -> t -> t -> t

Substitutions

val apply_subst : subst -> t -> t
val apply_subst_trigger : subst -> trigger -> trigger

Subterms, and related stuff

val sub_terms : Set.t -> t -> Set.t

sub_term acc e returns the acc augmented with the term and all its sub-terms. Returns the acc if e is not a term. Does not go through literals (except positive uninterpreted predicates application) and formulas

val max_pure_subterms : t -> Set.t

max_pure_subterms e returns the maximal pure terms of the given expression

val max_terms_of_lit : t -> Set.t

returns the maximal terms of the given literal. Assertion failure if not a literal (should replace the assertion failure with a better error) *

val max_ground_terms_of_lit : t -> Set.t

returns the maximal ground terms of the given literal. Assertion failure if not a literal *

val atoms_rec_of_form : only_ground:bool -> t -> Set.t -> Set.t

traverses a formula recursively and collects its atoms. Only ground atoms are kept if ~only_ground is true

val max_ground_terms_rec_of_form : t -> Set.t

traverses a formula recursively and collects its maximal ground terms

skolemization and other smart constructors for formulas *

val make_triggers : t -> binders -> decl_kind -> Util.matching_env -> trigger list
val clean_trigger : in_theory:bool -> string -> trigger -> trigger

clean trigger: remove useless terms in multi-triggers after inlining of lets

val resolution_triggers : is_back:bool -> quantified -> trigger list
val mk_forall : string -> Loc.t -> binders -> trigger list -> t -> toplevel:bool -> decl_kind:decl_kind -> t
val mk_exists : string -> Loc.t -> binders -> trigger list -> t -> toplevel:bool -> decl_kind:decl_kind -> t
val mk_let : Symbols.t -> t -> t -> t
val mk_match : t -> (Typed.pattern * t) list -> t
val skolemize : quantified -> t
val elim_let : recursive:bool -> letin -> t
val elim_iff : t -> t -> with_conj:bool -> t
val purify_form : t -> t
type gformula = {
  1. ff : t;
  2. nb_reductions : int;
  3. trigger_depth : int;
  4. age : int;
  5. lem : t option;
  6. origin_name : string;
  7. from_terms : t list;
  8. mf : bool;
  9. gf : bool;
  10. gdist : int;
  11. hdist : int;
  12. theory_elim : bool;
}
type th_elt = {
  1. th_name : string;
  2. ax_name : string;
  3. ax_form : t;
  4. extends : Util.theories_extensions;
  5. axiom_kind : Util.axiom_kind;
}
val print_th_elt : Stdlib.Format.formatter -> th_elt -> unit
val is_pure : t -> bool
val const_term : t -> bool

return true iff the given argument is a term without arguments

val save_cache : unit -> unit

Saves the modules cache

val reinit_cache : unit -> unit

Reinitializes the module's cache

module Core : sig ... end

Constructors from the smtlib core theory. https://smtlib.cs.uiowa.edu/theories-Core.shtml

module Ints : sig ... end

Constructors from the smtlib theory of integers. https://smtlib.cs.uiowa.edu/theories-Ints.shtml

module BV : sig ... end

Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV logic.

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