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
constant casts
val int_view : t -> int
Extracts the integer value of the expression, if there is one.
The returned value may be negative or null.
val rounding_mode_view : t -> Fpa_rounding.rounding_mode
Extracts the rounding mode value of the expression, if there is one.
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 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 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
clean trigger: remove useless terms in multi-triggers after inlining of lets
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
val const_term : t -> bool
return true iff the given argument is a term without arguments
module Core : sig ... end
Constructors from the smtlib core theory. https://smtlib.cs.uiowa.edu/theories-Core.shtml
module Ints : sig ... end
Constructors from the smtlib theory of integers. https://smtlib.cs.uiowa.edu/theories-Ints.shtml
module BV : sig ... end
Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV logic.