Module AltErgoLib.ExprSource

Data structures

Sourcetype binders = (Ty.t * int) Symbols.Map.t
Sourcetype t
Sourcetype decl_kind =
  1. | Dtheory
  2. | Daxiom
  3. | Dgoal
  4. | Dpredicate of t
  5. | Dfunction of 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
Sourceval const_term : t -> bool

return true iff the given argument is a term without arguments