Module AltErgoLib.Expr

Data structures

type t
include Container_types.S_plus_stdlib with type t := t
module T : Container_types_intf.Thing with type t = t
include Container_types_intf.Thing with type t := T.t
include Stdlib.Hashtbl.HashedType with type t := T.t
val equal : T.t -> T.t -> bool
val hash : T.t -> int
include Stdlib.Map.OrderedType with type t := T.t
val compare : T.t -> T.t -> int
val print : T.t Fmt.t
module Map : Container_types_intf.Map_plus_stdlib with type key = t and module Set = Set
module Table = Tbl
type binders = Ty.t Var.Map.t
type decl_kind =
  1. | Dtheory
  2. | Daxiom
  3. | Dgoal
  4. | Dpredicate of t
  5. | Dfunction of t
  6. | Dobjective
type term_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) Var.Map.t;
    (*

    Map of free term variables in the term to their type and number of occurrences.

    *)
  7. vty : AltErgoLib.Ty.TvSet.t;
    (*

    Map of free type variables in the term.

    *)
  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;
    (*

    Name of the lemma. This field is used by printers.

    *)
  2. main : t;
    (*

    The underlying formula.

    *)
  3. prenex : bool;
    (*

    Determine if the quantified formula is in prenex position, i.e. if it is the root of a formula introduced by an assertion, a goal or a function definition (possibly under quantifiers over type variables only).

    For instance, ∀y:int. G(y) is in prenex position in the asserted formula ∀y:int. G(y), but neither in ¬(∀y:int. G(y)) nor in P ∧ ∀y:int. G(y).

    Notice that quantifiers of the same kind are packed as much as possible. For instance, if we assert the formula: ∀α. ∀x:list α. ∃y:α. F(x, y) Then the two universal quantifiers are packed in a same prenex formula but the subformula ∃y:α. F(x, y) is not in prenex position.

    This flag is important for the prenex polymorphism.

    • If this flag is true, all the free type variables of main are implicitely considered as quantified.
    • Otherwise, the free type variables of the lemma are the same as the underlying formula main and are stored in the field sko_vty.
    *)
  4. user_trs : trigger list;
    (*

    List of the triggers defined by the user.

    The solver doesn't generate multi-triggers if the user has defined some multi-triggers.

    *)
  5. binders : binders;
    (*

    The ordered list of quantified term variables of main.

    This list has to be ordered for the skolemization.

    *)
  6. sko_v : t list;
    (*

    Set of all the free variables of the quantified formula. In other words, this set is always the complementary of binders in the set of free variables of main.

    The purpose of this field is to retrieve these variables quickly while performing the lazy skolemization in the SAT solver (see skolemize).

    *)
  7. sko_vty : Ty.t list;
    (*

    The set of free type variables. In particular this set is always empty if we are the top level.

    *)
  8. loc : Loc.t;
    (*

    Location of the "GLOBAL" axiom containing this quantified formula. It forms with name a unique identifier.

    *)
  9. kind : decl_kind;
    (*

    Kind of declaration.

    *)
}
and letin = private {
  1. let_v : Var.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 = private {
  1. content : t list;
    (*

    List of terms that must be present for this trigger to match.

    Sorted using matching heuristics; the first term is estimated as the least likely to match.

    *)
  2. semantic : semantic_trigger list;
  3. hyp : t list;
  4. t_depth : int;
  5. from_user : bool;
}
type subst = t Var.Map.t * Ty.subst
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
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
module Labeled : sig ... end

different views of an expression

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

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.

  • raises Failure

    if the expression is not a constant integer.

val rounding_mode_view : t -> Fpa_rounding.rounding_mode option

Extracts the rounding mode value of the expression, if there is one. Return None if the expression is not a constant rounding mode.

pretty printing

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
val pp_smtlib : t Fmt.t

pp_smtlib ppf e prints the expression e on the formatter ppf using the SMT-LIB standard.

Comparison and hashing functions

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
val free_vars : t -> (Ty.t * int) Var.Map.t -> (Ty.t * int) Var.Map.t

Some auxiliary functions

val free_type_vars : t -> AltErgoLib.Ty.TvSet.t
val is_ground : t -> bool
val size : t -> int
val depth : t -> int
val is_positive : t -> bool
val neg : t -> t
val is_int : t -> bool
val is_real : t -> bool
val type_info : t -> Ty.t
val symbol_info : t -> Symbols.t

Labeling and models

val add_label : Hstring.t -> t -> unit
val label : t -> Hstring.t
val name_of_lemma : t -> string
val name_of_lemma_opt : t option -> string
val print_tagged_classes : Stdlib.Format.formatter -> Set.t list -> unit

smart constructors for terms

val mk_trigger : ?user:bool -> ?depth:int -> ?hyp:t list -> t list -> trigger
val mk_term : Symbols.t -> t list -> Ty.t -> t
val mk_uninterpreted_term : string -> t list -> Ty.t -> t

mk_uninterpreted_term name args ret_ty builds an application of the uninterpreted symbol name to args, of type ret_ty.

val vrai : t

The boolean constant true with neg vrai == faux.

val faux : t

The boolean constant false with neg faux == vrai.

val void : t

The unit value, i.e. the only constructor of the unit type Ty.tunit.

val int : string -> t
val real : string -> t
val bitv : string -> Ty.t -> t
val float : Fp_value.t -> int -> int -> t
val fresh_name : Ty.t -> t

Special names used for AC(X) abstraction. These corresponds to the K sort in the AC(X) paper.

val fresh_ac_name : Ty.t -> t
val is_fresh_ac_name : t -> bool
val mk_abstract : Ty.t -> t

mk_abstract ty creates an abstract model term of type ty. This function is intended to be used only in models.

val pred : t -> t

smart constructors for literals

val mk_eq : iff:bool -> t -> t -> t
val mk_distinct : iff:bool -> t list -> t

mk_distinct ~iff l builds distinct l, where l has at least two elements. With at least three non-boolean arguments, it is a single n-ary literal.

The negation of this literal means that at least two of its arguments are equal. The theories ignore it, as this is a disjunction, instead, the SAT solvers add the disjunction of the equalities between the arguments when the literal is false.

val mk_builtin : is_pos:bool -> Symbols.builtin -> t list -> t

simple smart constructors for formulas

val mk_or : t -> t -> bool -> t
val mk_and : t -> t -> bool -> t
val mk_imp : t -> t -> t
val mk_iff : t -> t -> t
val mk_if : t -> t -> t -> t
val mk_xor : t -> t -> t
val mk_ite : t -> t -> t -> t

smart constructor for datatypes.

val mk_constr : Dolmen.Std.Expr.term_cst -> t list -> Ty.t -> t

mk_constr c args ty converts the Dolmen constructor c into an expression with arguments args.

  • raises Invalid_argument

    if c is not a Dolmen constructor.

  • raises Invalid_argument

    if no order have been attached to c with Nest.attach_orders.

val mk_tester : Dolmen.Std.Expr.term_cst -> t -> 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 : name:string -> loc:Loc.t -> t -> binders -> decl_kind -> Util.triggers_env -> trigger list

make_triggers ~name ~loc f binders decl menv generate multi-triggers for the formula f and binders binders. name and loc are the name and location of the quantified formula, used in warnings.

An escaped variable of a pattern is a variable that is not in binders (but the variable is bound by an inner quantified formula). We can replace escaped variables by the underscore variable Var.underscore.

For instance, if binders is the set {x, y} and g(x, y, z) is a pattern where {(x, y, z)} are free term variables, we can replace z by _.

Our strategy for multi-trigger generations depends on the matching environment menv as follows:

If menv.greedy is false, we try to generate in order:

  • Mono-triggers;
  • Multi-triggers without escaped variables.

If menv.greedy is true, we try to generate in order:

  • Mono and multi-triggers with escaped variables.
  • Mono and multi-triggers without escaped variables;

If menv.triggers_var is true, we allow variables as valid triggers.

Note: Mono-trigger with `Sy.Plus` or `Sy.Minus` top symbols are ignored if other mono-triggers have been generated.

The matching environment env is used to limit the number of multi-triggers generated per axiom.

val clean_trigger : in_theory:bool -> string -> trigger -> trigger

clean trigger: remove useless terms in multi-triggers after inlining of lets

val resolution_triggers : is_back:bool -> quantified -> trigger list
val mk_forall : string -> Loc.t -> binders -> trigger list -> t -> prenex:bool -> decl_kind:decl_kind -> t
val mk_exists : string -> Loc.t -> binders -> trigger list -> t -> prenex:bool -> decl_kind:decl_kind -> t
val mk_let : Var.t -> t -> t -> t
val skolemize : quantified -> t
val elim_let : recursive:bool -> letin -> t
val elim_iff : t -> t -> 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 : Stdlib.Format.formatter -> th_elt -> unit
val is_pure : t -> bool
val is_model_term : t -> bool

is_model_term e checks if the expression e is a model terms. A model term can be:

  • A constructor application involving only model terms,
  • A literal of a basic type (integer, real, boolean, unit or bitvector),
  • An abstract name, representing an abstract value (following SMT-LIB terminology).

The definition of model term maps to value terms in the SMT-LIB standard.

val save_cache : unit -> unit

Saves the modules cache

val reinit_cache : unit -> unit

Reinitializes the module's cache

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 Reals : sig ... end

Constructors from the smtlib theory of reals. https://smtlib.cs.uiowa.edu/theories-Reals.shtml

module BV : sig ... end

Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV logic.

module FP : sig ... end

Constructors from the smtlib theory of floating-point numbers.

module ArraysEx : sig ... end

Constructors from the smtlib theory of functional arrays with extensionality logic.