Module AltErgoLib.Expr

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