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 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;
}
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 : Set.S with type elt = t
module Map : Map.S with type key = t
type subst = t Symbols.Map.t * Ty.subst
type term_view = private
  1. | Term of view
  2. | Not_a_term of {
    1. is_lit : bool;
    }
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
  6. | Not_a_lit of {
    1. is_form : 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
  9. | Not_a_form

different views of an expression

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

pretty printing

val print : Format.formatter -> t -> unit
val print_list : Format.formatter -> t list -> unit
val print_list_sep : string -> Format.formatter -> t list -> unit
val print_triggers : 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 -> Ty.Svty.t
val is_ground : t -> bool
val id : t -> int
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

Labeling and models

val add_label : Hstring.t -> t -> unit
val label : t -> Hstring.t
val is_in_model : t -> bool
val name_of_lemma : t -> string
val name_of_lemma_opt : t option -> string
val print_tagged_classes : 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 -> int -> t
val mk_and : t -> t -> bool -> int -> t
val mk_imp : t -> t -> int -> t
val mk_iff : t -> t -> int -> t
val mk_if : t -> t -> t -> int -> t
val mk_xor : t -> t -> int -> t
val mk_ite : t -> t -> t -> int -> 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 resolution_triggers : is_back:bool -> quantified -> trigger list
val mk_forall : string -> Loc.t -> binders -> trigger list -> t -> int -> toplevel:bool -> decl_kind:decl_kind -> t
val mk_exists : string -> Loc.t -> binders -> trigger list -> t -> int -> toplevel:bool -> decl_kind:decl_kind -> t
val mk_let : Symbols.t -> t -> t -> int -> 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 -> int -> 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 : 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

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