package alt-ergo-lib

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

Module AltErgoLib.ExprSource

Data structures

Sourcetype binders = (Ty.t * int) Symbols.Map.t
Sourcetype decl_kind =
  1. | Dtheory
  2. | Daxiom
  3. | Dgoal
  4. | Dpredicate of string
  5. | Dfunction of string
Sourcetype t
Sourcetype 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 : Ty.Svty.t;
  8. depth : int;
  9. nb_nodes : int;
  10. pure : bool;
  11. mutable neg : t option;
}
Sourceand bind_kind =
  1. | B_none
  2. | B_lemma of quantified
  3. | B_skolem of quantified
  4. | B_let of letin
Sourceand 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;
}
Sourceand letin = private {
  1. let_v : Symbols.t;
  2. let_e : t;
  3. in_e : t;
  4. let_sko : t;
  5. is_bool : bool;
}
Sourceand 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
Sourceand 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;
}
Sourcemodule Set : Set.S with type elt = t
Sourcemodule Map : Map.S with type key = t
Sourcetype term_view = private
  1. | Term of view
  2. | Not_a_term of {
    1. is_lit : bool;
    }
Sourcetype 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
  6. | Not_a_lit of {
    1. is_form : bool;
    }
Sourcetype 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
  9. | Not_a_form

different views of an expression

Sourceval term_view : t -> term_view
Sourceval lit_view : t -> lit_view
Sourceval form_view : t -> form_view

pretty printing

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

Comparison and hashing functions

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

Some auxiliary functions

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

Labeling and models

Sourceval add_label : Hstring.t -> t -> unit
Sourceval label : t -> Hstring.t
Sourceval is_in_model : t -> bool
Sourceval name_of_lemma : t -> string
Sourceval name_of_lemma_opt : t option -> string
Sourceval print_tagged_classes : Format.formatter -> Set.t list -> unit

smart constructors for terms

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

smart constructors for literals

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

simple smart constructors for formulas

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

Substitutions

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

Subterms, and related stuff

Sourceval 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

Sourceval max_pure_subterms : t -> Set.t

max_pure_subterms e returns the maximal pure terms of the given expression

Sourceval 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) *

Sourceval max_ground_terms_of_lit : t -> Set.t

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

Sourceval 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

Sourceval 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 *

Sourceval make_triggers : t -> binders -> decl_kind -> Util.matching_env -> trigger list
Sourceval resolution_triggers : is_back:bool -> quantified -> trigger list
Sourceval mk_forall : string -> Loc.t -> binders -> trigger list -> t -> int -> toplevel:bool -> decl_kind:decl_kind -> t
Sourceval mk_exists : string -> Loc.t -> binders -> trigger list -> t -> int -> toplevel:bool -> decl_kind:decl_kind -> t
Sourceval mk_let : Symbols.t -> t -> t -> int -> t
Sourceval mk_match : t -> (Typed.pattern * t) list -> t
Sourceval skolemize : quantified -> t
Sourceval elim_let : letin -> t
Sourceval elim_iff : t -> t -> int -> with_conj:bool -> t
Sourceval purify_form : t -> t
Sourcetype 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;
}
Sourcetype 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;
}
Sourceval print_th_elt : Format.formatter -> th_elt -> unit
Sourceval is_pure : t -> bool
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