Module AltErgoLib.Typed

Typed AST

This module defines a typed AST, used to represent typed terms before they are hashconsed.

Annotations

type ('a, 'b) annoted = {
  1. c : 'a;
  2. annot : 'b;
}

An annoted structure. Usually used to annotate terms.

val new_id : unit -> int

Generate a new, fresh integer (useful for annotations).

val mk : ?annot:int -> 'a -> ('a, int) annoted

Create an annoted value with the given annotation. If no annotation is given, a fresh annotation is generated using new_id.

Terms and formulas

type tconstant =
  1. | Tint of string
    (*

    An integer constant.

    *)
  2. | Treal of Numbers.Q.t
    (*

    Real constant.

    *)
  3. | Tbitv of string
    (*

    Bitvector constant.

    *)
  4. | Ttrue
    (*

    The true boolean (or proposition ?)

    *)
  5. | Tfalse
    (*

    The false boolean

    *)
  6. | Tvoid
    (*

    The only value of type unit

    *)

Typed constants.

type oplogic =
  1. | OPand
    (*

    conjunction

    *)
  2. | OPor
    (*

    disjunction

    *)
  3. | OPxor
    (*

    exclusive disjunction

    *)
  4. | OPimp
    (*

    implication

    *)
  5. | OPnot
    (*

    negation

    *)
  6. | OPiff
    (*

    equivalence

    *)
  7. | OPif
    (*

    conditional branching

    *)

Logic operators.

type pattern =
  1. | Constr of {
    1. name : Uid.term_cst;
    2. args : (Var.t * Uid.term_cst * Ty.t) list;
    }
  2. | Var of Var.t
type 'a tterm = {
  1. tt_ty : Ty.t;
    (*

    type of the term

    *)
  2. tt_desc : 'a tt_desc;
    (*

    term descriptor

    *)
}

Typed terms. Polymorphic in the annotation: an 'a tterm is a term annoted with values of type 'a.

and 'a atterm = ('a tterm, 'a) annoted

type alias for annoted typed terms.

and 'a tt_desc =
  1. | TTconst of tconstant
    (*

    Term constant

    *)
  2. | TTvar of Symbols.t
    (*

    Term variables

    *)
  3. | TTinfix of 'a atterm * Symbols.t * 'a atterm
    (*

    Infix symbol application

    *)
  4. | TTprefix of Symbols.t * 'a atterm
    (*

    Prefix symbol application

    *)
  5. | TTapp of Symbols.t * 'a atterm list
    (*

    Arbitrary symbol application

    *)
  6. | TTmapsTo of Var.t * 'a atterm
    (*

    Used in semantic triggers for floating point arithmetic. See sources/preludes/fpa-theory-2017-01-04-16h00.ae

    *)
  7. | TTinInterval of 'a atterm * Symbols.bound * Symbols.bound
    (*

    Represent floating point intervals (used for triggers in Floating point arithmetic theory). TTinInterval (lower, l_strict, t, upper, u_strict) is a constraint stating that term t is in the interval lower, upper, and that the lower (resp. upper) bound is strict iff l_strict (resp. u_strict) is true.

    *)
  8. | TTget of 'a atterm * 'a atterm
    (*

    Get operation on arrays

    *)
  9. | TTset of 'a atterm * 'a atterm * 'a atterm
    (*

    Set operation on arrays

    *)
  10. | TTextract of 'a atterm * int * int
    (*

    Extract a sub-bitvector

    *)
  11. | TTconcat of 'a atterm * 'a atterm
  12. | TTdot of 'a atterm * Hstring.t
    (*

    Field access on structs/records

    *)
  13. | TTrecord of (Hstring.t * 'a atterm) list
    (*

    Record creation.

    *)
  14. | TTlet of (Symbols.t * 'a atterm) list * 'a atterm
    (*

    Let-bindings. Accept a list of mutually recursive le-bindings.

    *)
  15. | TTnamed of Hstring.t * 'a atterm
    (*

    Attach a label to a term.

    *)
  16. | TTite of 'a atform * 'a atterm * 'a atterm
    (*

    Conditional branching, of the form TTite (condition, then_branch, else_branch).

    *)
  17. | TTproject of 'a atterm * Hstring.t
    (*

    Field (conditional) access on ADTs.

    *)
  18. | TTmatch of 'a atterm * (pattern * 'a atterm) list
    (*

    pattern matching on ADTs

    *)
  19. | TTform of 'a atform
    (*

    formulas inside terms: simple way to add them without making a lot of changes

    *)

Typed terms descriptors.

and 'a atatom = ('a tatom, 'a) annoted

Type alias for annoted typed atoms.

and 'a tatom =
  1. | TAtrue
    (*

    The true atom

    *)
  2. | TAfalse
    (*

    The false atom

    *)
  3. | TAeq of 'a atterm list
    (*

    Equality of a set of typed terms.

    *)
  4. | TAdistinct of 'a atterm list
    (*

    Disequality. All terms in the set are pairwise distinct.

    *)
  5. | TAneq of 'a atterm list
    (*

    Equality negation: at least two elements in the list are not equal.

    *)
  6. | TAle of 'a atterm list
    (*

    Arithmetic ordering: lesser or equal. Chained on lists of terms.

    *)
  7. | TAlt of 'a atterm list
    (*

    Strict arithmetic ordering: less than. Chained on lists of terms.

    *)
  8. | TApred of 'a atterm * bool
    (*

    Term predicate, negated if the boolean is true. TApred (t, negated) is satisfied iff t <=> not negated

    *)
  9. | TTisConstr of 'a atterm * Hstring.t
    (*

    Test if the given term's head symbol is identitical to the provided ADT consturctor

    *)

Typed atoms.

and 'a quant_form = {
  1. qf_bvars : (Symbols.t * Ty.t) list;
    (*

    Variables that are quantified by this formula.

    *)
  2. qf_triggers : ('a atterm list * bool) list;
    (*

    Triggers associated wiht the formula. For each trigger, the boolean specifies whether the trigger was given in the input file (compared to inferred).

    *)
  3. qf_hyp : 'a atform list;
    (*

    Hypotheses of axioms with semantic triggers in FPA theory. Typically, these hypotheses reduce to TRUE after instantiation

    *)
  4. qf_form : 'a atform;
    (*

    The quantified formula.

    *)
}

Quantified formulas.

and 'a atform = ('a tform, 'a) annoted

Type alias for typed annoted formulas.

and 'a tform =
  1. | TFatom of 'a atatom
    (*

    Atomic formula.

    *)
  2. | TFop of oplogic * 'a atform list
    (*

    Application of logical operators.

    *)
  3. | TFforall of 'a quant_form
    (*

    Universal quantification.

    *)
  4. | TFexists of 'a quant_form
    (*

    Existencial quantification.

    *)
  5. | TFlet of (Var.t * 'a tlet_kind) list * 'a atform
    (*

    Let binding.

    *)
  6. | TFnamed of Hstring.t * 'a atform
    (*

    Attach a name to a formula.

    *)
  7. | TFmatch of 'a atterm * (pattern * 'a atform) list
    (*

    pattern matching on ADTs

    *)

Typed formulas.

and 'a tlet_kind =
  1. | TletTerm of 'a atterm
    (*

    Term let-binding

    *)
  2. | TletForm of 'a atform
    (*

    Formula let-binding

    *)

The different kinds of let-bindings, whether they bind terms or formulas.

Declarations

type 'a rwt_rule = {
  1. rwt_vars : (Symbols.t * Ty.t) list;
    (*

    Variables of the rewrite rule

    *)
  2. rwt_left : 'a;
    (*

    Left side of the rewrite rule (aka pattern).

    *)
  3. rwt_right : 'a;
    (*

    Right side of the rewrite rule.

    *)
}

Rewrite rules. Polymorphic to allow for different representation of terms.

type tlogic_type =
  1. | TPredicate of Ty.t list
    (*

    Predicate type declarations

    *)
  2. | TFunction of Ty.t list * Ty.t
    (*

    Function type declarations

    *)

Type declarations. Specifies the list of argument types, as well as the return type for functions (predicate implicitly returns a proposition, so there is no need for an explicit return type).

type 'a atdecl = ('a tdecl, 'a) annoted

Type alias for annoted typed declarations.

and 'a tdecl =
  1. | TTheory of Loc.t * string * Util.theories_extensions * 'a atdecl list
    (*

    Theory declarations. The list of declarations in a Theory may only contain Axioms.

    *)
  2. | TAxiom of Loc.t * string * Util.axiom_kind * 'a atform
    (*

    New axiom that can be used in proofs.

    *)
  3. | TRewriting of Loc.t * string * 'a atterm rwt_rule list
    (*

    New rewrite rule that can be used.

    *)
  4. | TGoal of Loc.t * Ty.goal_sort * string * 'a atform
    (*

    New goal to prove.

    *)
  5. | TLogic of Loc.t * string list * tlogic_type
    (*

    Function (or predicate) type declaration.

    *)
  6. | TPredicate_def of Loc.t * string * (string * Ty.t) list * 'a atform
    (*

    Predicate definition. TPredicate_def (loc, name, vars, body) defines a predicate fun vars => body.

    *)
  7. | TFunction_def of Loc.t * string * (string * Ty.t) list * Ty.t * 'a atform
    (*

    Predicate definition. TPredicate_def (loc, name, vars, ret, body) defines a function fun vars => body, where body has type ret.

    *)
  8. | TTypeDecl of Loc.t * Ty.t
    (*

    New type declaration. TTypeDecl (loc, vars, t, body) declares a type t, with parameters vars, and with contents body. This new type may either be abstract, a record type, or an enumeration.

    *)
  9. | TPush of Loc.t * int
    (*

    push (loc,n) pushs n new assertions levels onto the assertion stack

    *)
  10. | TPop of Loc.t * int
    (*

    pop (loc,n) pops n assertions levels from the assertion stack

    *)
  11. | TReset of Loc.t
    (*

    Resets all the context.

    *)
  12. | TExit of Loc.t
    (*

    Exits the solver.

    *)
  13. | TOptimize of Loc.t * 'a atterm * bool
    (*

    Optimization declaration. TOptimize (loc, obj, is_max) declares an objective function obj. The flag is_max determines if we try to maximize of minimize obj.

    *)

Typed declarations.

Printing
val print_term : Stdlib.Format.formatter -> _ atterm -> unit

Print annoted typed terms. Ignore the annotations.

val print_formula : Stdlib.Format.formatter -> _ atform -> unit

Print annoted typed formulas; Ignores the annotations.

val print_binders : Stdlib.Format.formatter -> (Symbols.t * Ty.t) list -> unit

Print a list of bound typed variables.

val print_triggers : Stdlib.Format.formatter -> ('a atterm list * bool) list -> unit

Print a list of triggers.

val print_rwt : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a rwt_rule -> unit

Print a rewrite rule

val print_atdecl : Stdlib.Format.formatter -> _ atdecl -> unit

Print an annoted term decl.