Typed AST
This module defines a typed AST, used to represent typed terms before they are hashconsed.
val mk : ?annot:int -> 'a -> ('a, int) annotedCreate an annoted value with the given annotation. If no annotation is given, a fresh annotation is generated using new_id.
type tconstant = | Tint of stringAn integer constant.
*)| Treal of Numbers.Q.tReal constant.
*)| Tbitv of stringBitvector constant.
*)| TtrueThe true boolean (or proposition ?)
*)| TfalseThe false boolean
*)| TvoidThe only value of type unit
*)Typed constants.
type pattern = | Constr of {name : Uid.term_cst;args : (Var.t * Uid.term_cst * Ty.t) list;}| Var of Var.tTyped terms. Polymorphic in the annotation: an 'a tterm is a term annoted with values of type 'a.
and 'a tt_desc = | TTconst of tconstantTerm constant
*)| TTvar of Symbols.tTerm variables
*)| TTinfix of 'a atterm * Symbols.t * 'a attermInfix symbol application
*)| TTprefix of Symbols.t * 'a attermPrefix symbol application
*)| TTapp of Symbols.t * 'a atterm listArbitrary symbol application
*)| TTmapsTo of Var.t * 'a attermUsed in semantic triggers for floating point arithmetic. See sources/preludes/fpa-theory-2017-01-04-16h00.ae
*)| TTinInterval of 'a atterm * Symbols.bound * Symbols.boundRepresent 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.
| TTget of 'a atterm * 'a attermGet operation on arrays
*)| TTset of 'a atterm * 'a atterm * 'a attermSet operation on arrays
*)| TTextract of 'a atterm * int * intExtract a sub-bitvector
*)| TTconcat of 'a atterm * 'a atterm| TTdot of 'a atterm * Hstring.tField access on structs/records
*)| TTrecord of (Hstring.t * 'a atterm) listRecord creation.
*)| TTlet of (Symbols.t * 'a atterm) list * 'a attermLet-bindings. Accept a list of mutually recursive le-bindings.
*)| TTnamed of Hstring.t * 'a attermAttach a label to a term.
*)| TTite of 'a atform * 'a atterm * 'a attermConditional branching, of the form TTite (condition, then_branch, else_branch).
| TTproject of 'a atterm * Hstring.tField (conditional) access on ADTs.
*)| TTmatch of 'a atterm * (pattern * 'a atterm) listpattern matching on ADTs
*)| TTform of 'a atformformulas inside terms: simple way to add them without making a lot of changes
*)Typed terms descriptors.
and 'a tatom = | TAtrueThe true atom
| TAfalseThe false atom
| TAeq of 'a atterm listEquality of a set of typed terms.
*)| TAdistinct of 'a atterm listDisequality. All terms in the set are pairwise distinct.
*)| TAneq of 'a atterm listEquality negation: at least two elements in the list are not equal.
*)| TAle of 'a atterm listArithmetic ordering: lesser or equal. Chained on lists of terms.
*)| TAlt of 'a atterm listStrict arithmetic ordering: less than. Chained on lists of terms.
*)| TApred of 'a atterm * boolTerm predicate, negated if the boolean is true. TApred (t, negated) is satisfied iff t <=> not negated
| TTisConstr of 'a atterm * Hstring.tTest if the given term's head symbol is identitical to the provided ADT consturctor
*)Typed atoms.
and 'a quant_form = {qf_bvars : (Symbols.t * Ty.t) list;Variables that are quantified by this formula.
*)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).
*)qf_hyp : 'a atform list;Hypotheses of axioms with semantic triggers in FPA theory. Typically, these hypotheses reduce to TRUE after instantiation
*)qf_form : 'a atform;The quantified formula.
*)}Quantified formulas.
and 'a tform = | TFatom of 'a atatomAtomic formula.
*)| TFop of oplogic * 'a atform listApplication of logical operators.
*)| TFforall of 'a quant_formUniversal quantification.
*)| TFexists of 'a quant_formExistencial quantification.
*)| TFlet of (Var.t * 'a tlet_kind) list * 'a atformLet binding.
*)| TFnamed of Hstring.t * 'a atformAttach a name to a formula.
*)| TFmatch of 'a atterm * (pattern * 'a atform) listpattern matching on ADTs
*)Typed formulas.
type 'a rwt_rule = {rwt_vars : (Symbols.t * Ty.t) list;Variables of the rewrite rule
*)rwt_left : 'a;Left side of the rewrite rule (aka pattern).
*)rwt_right : 'a;Right side of the rewrite rule.
*)}Rewrite rules. Polymorphic to allow for different representation of terms.
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).
and 'a tdecl = | TTheory of Loc.t * string * Util.theories_extensions * 'a atdecl listTheory declarations. The list of declarations in a Theory may only contain Axioms.
*)| TAxiom of Loc.t * string * Util.axiom_kind * 'a atformNew axiom that can be used in proofs.
*)| TRewriting of Loc.t * string * 'a atterm rwt_rule listNew rewrite rule that can be used.
*)| TGoal of Loc.t * Ty.goal_sort * string * 'a atformNew goal to prove.
*)| TLogic of Loc.t * string list * tlogic_typeFunction (or predicate) type declaration.
*)| TPredicate_def of Loc.t * string * (string * Ty.t) list * 'a atformPredicate definition. TPredicate_def (loc, name, vars, body) defines a predicate fun vars => body.
| TFunction_def of Loc.t * string * (string * Ty.t) list * Ty.t * 'a atformPredicate definition. TPredicate_def (loc, name, vars, ret, body) defines a function fun vars => body, where body has type ret.
| TTypeDecl of Loc.t * Ty.tNew 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.
| TPush of Loc.t * intpush (loc,n) pushs n new assertions levels onto the assertion stack
| TPop of Loc.t * intpop (loc,n) pops n assertions levels from the assertion stack
| TReset of Loc.tResets all the context.
*)| TExit of Loc.tExits the solver.
*)| TOptimize of Loc.t * 'a atterm * boolOptimization 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.
val print_term : Format.formatter -> _ atterm -> unitPrint annoted typed terms. Ignore the annotations.
val print_formula : Format.formatter -> _ atform -> unitPrint annoted typed formulas; Ignores the annotations.
val print_binders : Format.formatter -> (Symbols.t * Ty.t) list -> unitPrint a list of bound typed variables.
val print_triggers : Format.formatter -> ('a atterm list * bool) list -> unitPrint a list of triggers.
val print_rwt :
(Format.formatter -> 'a -> unit) ->
Format.formatter ->
'a rwt_rule ->
unitPrint a rewrite rule
val print_atdecl : Format.formatter -> _ atdecl -> unitPrint an annoted term decl.