AltErgoLib.Expr
Data structures
type binders = (Ty.t * int) Symbols.Map.t
and semantic_trigger =
| Interval of t * Symbols.bound * Symbols.bound |
| MapsTo of Var.t * t |
| NotTheoryConst of t |
| IsTheoryConst of t |
| LinearDependency of t * t |
and trigger = {
content : t list; |
semantic : semantic_trigger list; |
hyp : t list; |
t_depth : int; |
from_user : bool; |
guard : t option; |
}
type subst = t Symbols.Map.t * Ty.subst
different views of an expression
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 hash : t -> int
val uid : t -> int
val compare_quant : quantified -> quantified -> 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 id : t -> int
val size : t -> int
val depth : t -> int
val is_positive : t -> bool
val is_fresh : t -> bool
val is_fresh_skolem : t -> bool
val is_int : t -> bool
val is_real : t -> bool
Labeling and models
val is_in_model : t -> bool
val name_of_lemma : t -> string
val name_of_lemma_opt : t option -> string
smart constructors for terms
val vrai : t
val faux : t
val void : t
val int : string -> t
val real : string -> t
smart constructors for literals
val mk_builtin : is_pos:bool -> Symbols.builtin -> t list -> t
simple smart constructors for formulas
Substitutions
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_match : t -> (Typed.pattern * t) list -> t
val skolemize : quantified -> t
type th_elt = {
th_name : string; |
ax_name : string; |
ax_form : t; |
extends : Util.theories_extensions; |
axiom_kind : Util.axiom_kind; |
}
val print_th_elt : Stdlib.Format.formatter -> th_elt -> unit
val is_pure : t -> bool