package alt-ergo-lib

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

Install

Dune Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Maintainers

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.1.tbz
sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba
sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb

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

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 : Format.formatter -> _ atterm -> unit

Print annoted typed terms. Ignore the annotations.

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

Print annoted typed formulas; Ignores the annotations.

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

Print a list of bound typed variables.

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

Print a list of triggers.

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

Print a rewrite rule

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

Print an annoted term decl.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct