package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. O
    OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.3.tar.gz
sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388
md5=3b060044767d16d1de3416944abd2dd5

doc/alt-ergo-lib/AltErgoLib/Typed/index.html

Module AltErgoLib.TypedSource

Typed AST

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

Annotations

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

An annoted structure. Usually used to annotate terms.

Sourceval new_id : unit -> int

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

Sourceval 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

Sourcetype tconstant =
  1. | Tint of string
    (*

    An integer constant.

    *)
  2. | Treal of Num.num
    (*

    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.

Sourcetype 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.

Sourcetype pattern =
  1. | Constr of {
    1. name : Hstring.t;
    2. args : (Var.t * Hstring.t * Ty.t) list;
    }
  2. | Var of Var.t
Sourcetype '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.

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

type alias for annoted typed terms.

Sourceand '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.why

    *)
  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 * 'a atterm * 'a atterm
    (*

    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 bool * 'a atterm * Hstring.t
    (*

    Field (conditional) access on ADTs. The boolean is true when the projection is 'guarded' and cannot be simplified (because functions are total)

    *)
  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.

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

Type alias for annoted typed atoms.

Sourceand '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 tterm, 'a) annoted * Hstring.t
    (*

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

    *)

Typed atoms.

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

    Variables that are quantified by this formula.

    *)
  2. qf_upvars : (Symbols.t * Ty.t) list;
    (*

    Free variables that occur in the formula.

    *)
  3. 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).

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

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

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

    The quantified formula.

    *)
}

Quantified formulas.

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

Type alias for typed annoted formulas.

Sourceand '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 (Symbols.t * Ty.t) list * (Symbols.t * 'a tlet_kind) list * 'a atform
    (*

    Let binding. TODO: what is in the first list ?

    *)
  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.

Sourceand '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

Sourcetype '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.

Sourcetype goal_sort =
  1. | Cut
    (*

    Introduce a cut in a goal. Once the cut proved, it's added as a hypothesis.

    *)
  2. | Check
    (*

    Check if some intermediate assertion is prouvable

    *)
  3. | Thm
    (*

    The goal to be proved

    *)

Goal sort. Used in typed declarations.

Sourceval fresh_hypothesis_name : goal_sort -> string

create a fresh hypothesis name given a goal sort.

Sourceval is_local_hyp : string -> bool

Assuming a name generated by fresh_hypothesis_name, answers whether the name design a local hypothesis ?

Sourceval is_global_hyp : string -> bool

Assuming a name generated by fresh_hypothesis_name, does the name design a global hypothesis ?

Sourcetype 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).

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

Type alias for annoted typed declarations.

Sourceand '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 * 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.

    *)

Typed declarations.

Printing
Sourceval print_term : Format.formatter -> _ atterm -> unit

Print annoted typed terms. Ignore the annotations.

Sourceval print_formula : Format.formatter -> _ atform -> unit

Print annoted typed formulas; Ignores the annotations.

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

Print a list of bound typed variables.

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

Print a list of triggers.

Sourceval print_goal_sort : Format.formatter -> goal_sort -> unit

Print a goal sort

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

Print a rewrite rule