Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449145014511452145314541455145614571458145914601461146214631464146514661467146814691470147114721473147414751476147714781479148014811482148314841485148614871488148914901491149214931494149514961497149814991500150115021503150415051506150715081509151015111512151315141515151615171518151915201521152215231524152515261527152815291530153115321533153415351536153715381539154015411542154315441545154615471548154915501551155215531554155515561557155815591560156115621563156415651566156715681569157015711572157315741575157615771578157915801581158215831584158515861587158815891590159115921593159415951596159715981599160016011602160316041605160616071608160916101611161216131614161516161617161816191620162116221623162416251626162716281629163016311632163316341635163616371638163916401641164216431644164516461647164816491650165116521653165416551656165716581659166016611662166316641665166616671668166916701671167216731674167516761677167816791680168116821683168416851686168716881689169016911692169316941695169616971698169917001701170217031704170517061707170817091710171117121713171417151716171717181719172017211722172317241725172617271728172917301731173217331734173517361737173817391740174117421743174417451746174717481749175017511752175317541755175617571758175917601761176217631764176517661767176817691770177117721773177417751776177717781779178017811782178317841785178617871788178917901791179217931794179517961797179817991800180118021803180418051806180718081809181018111812181318141815181618171818181918201821182218231824182518261827182818291830183118321833183418351836183718381839184018411842184318441845184618471848184918501851185218531854185518561857185818591860186118621863186418651866186718681869187018711872187318741875187618771878187918801881188218831884188518861887188818891890189118921893189418951896189718981899190019011902190319041905190619071908190919101911191219131914191519161917191819191920192119221923192419251926192719281929193019311932193319341935193619371938193919401941194219431944194519461947194819491950195119521953195419551956195719581959196019611962196319641965196619671968196919701971197219731974197519761977197819791980198119821983198419851986198719881989199019911992199319941995199619971998199920002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202320242025202620272028202920302031203220332034203520362037203820392040204120422043204420452046204720482049205020512052205320542055205620572058205920602061206220632064
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
(** Interfaces for Terms. This module defines Interfaces that implementation of terms must respect in order to be used to instantiated the corresponding language classes. *)
(** {2 Signature for Parsing Logic languages} *)
module type Logic = sig
(** Signature used by the Logic class, which parses languages such as tptp, smtlib, etc... Mainly used to parse first-order terms, it is also used to parse tptp's THF language, which uses higher order terms, so some first-order constructs such as conjunction, equality, etc... also need to be represented by standalone terms. *)
type t (** The type of terms. *)
type id (** The type of identifiers used for constants. *)
type location (** The type of locations attached to terms. *)
(** {3 Predefined terms} *)
val eq_t : ?loc:location -> unit -> t val neq_t : ?loc:location -> unit -> t (** The terms representing equality and disequality, respectively. *)
val wildcard : ?loc:location -> unit -> t (** The wildcard term, usually used in place of type arguments to explicit polymorphic functions to not explicit types that can be inferred by the type-checker. *)
val tType : ?loc:location -> unit -> t (** The type of types, defined as specific token by the Zipperposition format; in other languages, will be represented as a constant (the "$tType" constant in tptp for instance). Used to define new types, or quantify type variables in languages that support polymorphism. *)
val prop : ?loc:location -> unit -> t (** The type of propositions. Also defined as a lexical token by the Zipperposition format. Will be defined as a constant in most other languages (for instance, "$o" in tptp). *)
val bool : ?loc:location -> unit -> t (** The type of boolean, defined as a specific token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name. *)
val ty_unit : ?loc:location -> unit -> t (** The type unit, defined as a specific token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name. *)
val ty_int : ?loc:location -> unit -> t (** The type of integers, defined as a specific token by the Zipperposition and Alt-ergo formats; in other languages, it might be represented as a constant with a specific name (for isntance, tptp's "$int") .*)
val ty_real : ?loc:location -> unit -> t (** The type of integers, defined as a specific token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name (for isntance, tptp's "$int") .*)
val ty_bitv : ?loc:location -> int -> t (** The type of bitvectors of the given constant length, defined as a specifi token by the Alt-ergo format; in other languages, it might be represented as a constant with a specific name (for isntance, smtlib(s "bitv") .*)
val void : ?loc:location -> unit -> t (** The only value of type unit, defined as a specific token by the Alt-ergo format. *)
val true_ : ?loc:location -> unit -> t val false_ : ?loc:location -> unit -> t (** The constants for the true and false propositional constants. Again defined as lexical token in the Zipperposition format, while treated as a constant in other languages ("$true" in tptp). *)
val not_t : ?loc:location -> unit -> t val or_t : ?loc:location -> unit -> t val and_t : ?loc:location -> unit -> t val xor_t : ?loc:location -> unit -> t val nor_t : ?loc:location -> unit -> t val nand_t : ?loc:location -> unit -> t val equiv_t : ?loc:location -> unit -> t val implied_t : ?loc:location -> unit -> t val implies_t : ?loc:location -> unit -> t val pi_t : ?loc:location -> unit -> t val sigma_t : ?loc:location -> unit -> t (** Standard logical connectives viewed as terms. [implies_t] is usual right implication, i.e [apply implies_t \[p; q\] ] is "p implies q", while [apply implied_t \[p; q \]] means "p is implied by q" or "q implies p". *)
val data_t : ?loc:location -> unit -> t (** Term without semantic meaning, used for creating "data" terms. Used in tptp's annotations, and with similar meaning as smtlib's s-expressions (as used in the [sexpr] function defined later). *)
(** {3 Terms leaf constructors} *)
val var : ?loc:location -> id -> t val const : ?loc:location -> id -> t (** Variable and constant constructors. While in some languages they can distinguished at the lexical level (in tptp for instance), in most languages, it is an issue dependant on scoping rules, so terms parsed from an smtlib file will have all variables parsed as constants. *)
val atom : ?loc:location -> int -> t (** Atoms are used for dimacs cnf parsing. Positive integers denotes variables, and negative integers denote the negation of the variable corresponding to their absolute value. *)
val distinct : ?loc:location -> id -> t (** Used in tptp to specify constants different from other constants, for instance the 'distinct' "Apple" should be syntactically different from the "Apple" constant. Can be safely aliased to the [const] function as the [distinct] function is always given strings already enclosed with quotes, so in the example above, [const] would be called with ["Apple"] as string argument, while [distinct] would be called with the string ["\"Apple\""] *)
val str : ?loc:location -> string -> t val int : ?loc:location -> string -> t val rat : ?loc:location -> string -> t val real : ?loc:location -> string -> t val hexa : ?loc:location -> string -> t val binary : ?loc:location -> string -> t (** Constructors for words defined as numeric or string formats by the languages specifications. These also can be safely aliased to [const], but then the provenance information is lost, which might complicate the task of a type-checker. *)
val bitv : ?loc:location -> string -> t (** Bitvetor literal, defined as a specific token in Alt-ergo; Expects a decimal integer in the string to be extended as a bitvector. *)
(** {3 Term constructors} *)
val colon : ?loc:location -> t -> t -> t (** Represents juxtaposition of two terms, usually denoted "t : t'" in most languages, and mainly used to annotated terms with their supposed, or defined, type. *)
val eq : ?loc:location -> t -> t -> t val neq : ?loc:location -> t list -> t (** Equality and dis-equality of terms. *)
val not_ : ?loc:location -> t -> t val or_ : ?loc:location -> t list -> t val and_ : ?loc:location -> t list -> t val xor : ?loc:location -> t -> t -> t val imply : ?loc:location -> t -> t -> t val equiv : ?loc:location -> t -> t -> t (** Proposition construction functions. The conjunction and disjunction are n-ary instead of binary mostly because they are in smtlib (and that is subsumes the binary case). *)
val apply : ?loc:location -> t -> t list -> t (** Application constructor, seen as higher order application rather than first-order application for the following reasons: being able to parse tptp's THF, having location attached to function symbols. *)
val fake_apply : ?loc:location -> t -> t list -> t (** "Fake" application: this looks like an application, but different enough semantics that treating it as an application would be problematic. This is useful for languages that try and overload the application syntax to mean different things, so that it can be treated specifically later during typechecking. *)
val ite : ?loc:location -> t -> t -> t -> t (** Conditional constructor, both for first-order terms and propositions. Used in the following schema: [ite condition then_branch else_branch]. *)
val match_ : ?loc:location -> t -> (t * t) list -> t (** Pattern matching. The first term is the term to match, and each tuple in the list is a match case, which is a pair of a pattern and a match branch. *)
val pi : ?loc:location -> t list -> t -> t val par : ?loc:location -> t list -> t -> t val letin : ?loc:location -> t list -> t -> t val letand : ?loc:location -> t list -> t -> t val forall : ?loc:location -> t list -> t -> t val exists : ?loc:location -> t list -> t -> t val lambda : ?loc:location -> t list -> t -> t val choice : ?loc:location -> t list -> t -> t val description : ?loc:location -> t list -> t -> t (** Binders for variables. Takes a list of terms as first argument for simplicity, the lists will almost always be a list of variables, optionally typed using the [colon] term constructor. - Pi is the polymorphic type quantification, for instance the polymorphic identity function has type: "Pi alpha. alpha -> alpha" - Letin is local binding, takes a list of equality of equivalences whose left hand-side is a variable. Letand is the parrallel version of Letin. - Forall is universal quantification - Par is universal quantification over type variables specifically (i.e. the same as forall, but only for a list of type variables, which thus may omit the [colon] annotations in the arguments). - Exists is existential quantification - Lambda is used for function construction - Choice is the choice operator, also called indefinite description, or also epsilon terms, i.e "Choice x. p(x)" is one "x" such that "p(x)" is true. - Description is the definite description, i.e "Description x. p(x)" is the {b only} "x" that satisfies p. *)
(** {3 Type constructors} *)
val arrow : ?loc:location -> t -> t -> t (** Function type constructor, for curryfied functions. Functions that takes multiple arguments in first-order terms might take a product as only argument (see the following [product] function) in some languages (e.g. tptp), or be curryfied using this constructor in other languages (e.g. alt-ergo). *)
val product : ?loc:location -> t -> t -> t (** Product type constructor, used for instance in the types of functions that takes multiple arguments in a non-curry way. *)
val union : ?loc:location -> t -> t -> t (** Union type constructor, currently used in tptp's THF format. *)
val subtype : ?loc:location -> t -> t -> t (** Subtype relation for types. *)
(** {3 Record constructors} *)
val record : ?loc:location -> t list -> t (** Create a record expression. *)
val record_with : ?loc:location -> t -> t list -> t (** Record "with" update (e.g. "{ r with ....}"). *)
val record_access : ?loc:location -> t -> id -> t (** Field record access. *)
(** {3 Algebraic datatypes} *)
val adt_check : ?loc:location -> t -> id -> t (** Check whether some expression matches a given adt constructor (in head position). *)
val adt_project : ?loc:location -> t -> id -> t (** Project a field of an adt constructor (usually unsafe except when guarded by an adt_check function). *)
(** {3 Array constructors} *)
val array_get : ?loc:location -> t -> t -> t (** Array getter. *)
val array_set : ?loc:location -> t -> t -> t -> t (** Array setter. *)
(** {3 Bitvector constructors} *)
val bitv_extract : ?loc:location -> t -> int -> int -> t (** Bitvector extraction. *)
val bitv_concat : ?loc:location -> t -> t -> t (** Bitvector concatenation. *)
(** {3 Arithmetic constructors} *)
val uminus : ?loc:location -> t -> t (** Arithmetic unary minus. *)
val add : ?loc:location -> t -> t -> t (** Arithmetic addition. *)
val sub : ?loc:location -> t -> t -> t (** Arithmetic substraction. *)
val mult : ?loc:location -> t -> t -> t (** Arithmetic multiplication. *)
val div : ?loc:location -> t -> t -> t (** Arithmetic division quotient. *)
val mod_ : ?loc:location -> t -> t -> t (** Arithmetic modulo (aka division reminder). *)
val int_pow : ?loc:location -> t -> t -> t (** Integer power. *)
val real_pow : ?loc:location -> t -> t -> t (** Real power. *)
val lt : ?loc:location -> t -> t -> t (** Arithmetic "lesser than" comparison (strict). *)
val leq : ?loc:location -> t -> t -> t (** Arithmetic "lesser or equal" comparison. *)
val gt : ?loc:location -> t -> t -> t (** Arithmetic "greater than" comparison (strict). *)
val geq : ?loc:location -> t -> t -> t (** Arithmetic "greater or equal" comparison. *)
(** {3 Triggers} *)
val in_interval : ?loc:location -> t -> (t * bool) -> (t * bool) -> t (** Create a predicate for whether a term is within the given bounds (each bound is represented by a term which is tis value and a boolean which specifies whether it is strict or not). *)
val maps_to : ?loc:location -> id -> t -> t (** Id mapping (see alt-ergo). *)
val trigger : ?loc:location -> t list -> t (** Create a multi-trigger (i.e. all terms in the lsit must match to trigger). *)
val triggers : ?loc:location -> t -> t list -> t (** [triggers ~loc f l] annotates formula/term [f] with a list of triggers. *)
val filters : ?loc:location -> t -> t list -> t (** [filters ~loc f l] annotates formula/term [f] with a list of filters. *)
(** {3 Special constructions} *)
val tracked : ?loc:location -> id -> t -> t (** Name a term for tracking purposes. *)
val quoted : ?loc:location -> string -> t (** Create an attribute from a quoted string (in Zf). *)
val sequent : ?loc:location -> t list -> t list -> t (** Sequents as terms *)
val check : ?loc:location -> t -> t (** Check a term (see alt-ergo). *)
val cut : ?loc:location -> t -> t (** Create a cut (see alt-ergo). *)
val annot : ?loc:location -> t -> t list -> t (** Attach a list of attributes (also called annotations) to a term. Attributes have no logical meaning (they can be safely ignored), but may serve to give hints or meta-information. *)
val as_ : ?loc:location -> t -> t -> t list -> t (** SMT-LIB's `as` """type annotation""" (big quotes). *)
val sexpr : ?loc:location -> t list -> t (** S-expressions (for smtlib attributes), should probably be related to the [data_t] term. *)
val map_lambda : ?loc:location -> t list -> t -> t (** "Fake" lambdas, i.e. encodings of higher-order functions in first-order, as used by SMT-LIB2.7. *)
end
(** {2 Signature for Response terms} *)
module type Response = Logic(** Simply an alias to the Logic signature. *)
(** {2 Signature for Typechecked terms} *)
module type Tff = sig (** Signature required by terms for typing first-order polymorphic terms. *)
type t (** The type of terms and term variables. *)
type path (** The type of patsh to constants. *)
type ty type ty_var type ty_const type ty_def (** The representation of term types, type variables, and type constants, and lastly type definitions. *)
type 'a tag (** The type of tags used to annotate arbitrary terms. *)
val ty : t -> ty (** Returns the type of a term. *)
val print : Format.formatter -> t -> unit (** Printing function for terms. *)
(** A module for variables that occur in terms. *) module Var : sig
type t (** The type of variables the can occur in terms *)
val print : Format.formatter -> t -> unit (** Printing function for term variables. *)
val compare : t -> t -> int (** Comparison function on variables. *)
val mk : string -> ty -> t (** Create a new typed variable. *)
val ty : t -> ty (** Return the type of the variable. *)
val get_tag : t -> 'a tag -> 'a option (** Return the value bound to a tag (if any). *)
val set_tag : t -> 'a tag -> 'a -> unit (** Set the value bound to the tag. *)
val unset_tag : t -> _ tag -> unit (** Remove the binding to the given tag. *)
end
(** A module for constant symbols that occur in terms. *) module Const : sig
type t (** The type of constant symbols that can occur in terms *)
val print : Format.formatter -> t -> unit (** Printing function for term constants. *)
val compare : t -> t -> int (** Comparison function on constant symbols. *)
val ty : t -> ty (** Return the type of the constant. *)
val mk : path -> ty -> t (** Create a constant symbol. *)
val set_tag : t -> 'a tag -> 'a -> unit (** Tag a constant. *)
val add_tag : t -> 'a list tag -> 'a -> unit (** Add a value to the list of values bound to a tag. *)
end
(** A module for Algebraic datatype constructors. *) module Cstr : sig
type t (** An algebraic type constructor. Note that such constructors are used to build terms, and not types, e.g. consider the following: [type 'a list = Nil | Cons of 'a * 'a t], then [Nil] and [Cons] are the constructors, while [list] would be a type constant of arity 1 used to name the type. *)
val ty : t -> ty (** Return the type of the constant. *)
val compare : t -> t -> int (** Comparison function on constant symbols. *)
val pattern_arity : t -> ty -> ty list -> ty list (** Used in the type-checking of pattern matching. [pattern_arity cstr ret ty_args] should return the types of the expected arguments [args] such that [apply_cstr cstr ty_args args] has type [ret]. *)
end
module Field : sig
type t (** A field of a record. *)
val compare : t -> t -> int (** Comparison function on constant symbols. *)
end
val define_adt : ty_const -> ty_var list -> (path * (ty * path option) list) list -> ty_def * (Cstr.t * (ty * Const.t option) list) list (** [define_aft t vars cstrs] defines the type constant [t], parametrised over the type variables [ty_vars] as defining an algebraic datatypes with constructors [cstrs]. [cstrs] is a list where each elements of the form [(name, l)] defines a new constructor for the algebraic datatype, with the given name. The list [l] defines the arguments to said constructor, each element of the list giving the type [ty] of the argument expected by the constructor (which may contain any of the type variables in [vars]), as well as an optional destructor name. If the construcotr name is [Some s], then the ADT definition also defines a function that acts as destructor for that particular field. This polymorphic function is expected to takes as arguments as many types as there are variables in [vars], an element of the algebraic datatype being defined, and returns a value for the given field. For instance, consider the following definition for polymorphic lists: [define_adt list \[ty_var_a\] \[ "nil", \[\]; "const", \[ (Ty.of_var ty_var_a , Some "hd"); (ty_list_a , Some "tl"); \]; \] ] This definition defines the usual type of polymorphic linked lists, as well as two destructors "hd" and "tl". "hd" would have type [forall alpha. alpha list -> a], and be the partial function returning the head of the list. *)
val define_record : ty_const -> ty_var list -> (path * ty) list -> ty_def * Field.t list (** Define a (previously abstract) type to be a record type, with the given fields. *)
exception Wrong_type of t * ty (** Exception raised in case of typing error during term construction. [Wrong_type (t, ty)] should be raised by term constructor functions when some term [t] is expected to have type [ty], but does not have that type. *)
exception Wrong_sum_type of Cstr.t * ty (** Raised when some constructor was expected to belong to some type but does not belong to the given type. *)
exception Wrong_record_type of Field.t * ty_const (** Exception raised in case of typing error during term construction. This should be raised when the returned field was expected to be a field for the returned record type constant, but it was of another record type. *)
exception Field_repeated of Field.t (** Field repeated in a record expression. *)
exception Field_missing of Field.t (** Field missing in a record expression. *)
exception Pattern_expected of t (** Raised when trying to create a pattern matching, but a non-pattern term was provided where a pattern was expected. *)
exception Empty_pattern_matching (** Raise when creating a pattern matching but an empty list of branches was provided *)
exception Partial_pattern_match of t list (** Raised when a partial pattern matching was created. A list of terms not covered by the patterns is provided. *)
exception Over_application of t list (** Raised when an application was provided too many term arguments. The extraneous arguments are returned by the exception. *)
exception Bad_poly_arity of ty_var list * ty list (** Raised when a polymorphic application does not have an adequate number of arguments. *)
val ensure : t -> ty -> t (** Ensure that a given term has the given type. *)
val of_var : Var.t -> t (** Create a term from a variable *)
val apply_cst : Const.t -> ty list -> t list -> t (** Polymorphic application of a constant. *)
val apply_cstr : Cstr.t -> ty list -> t list -> t (** Polymorphic application of a constructor. *)
val apply_field : Field.t -> t -> t (** Apply a field to a record. *)
val record : (Field.t * t) list -> t (** Create a record. *)
val record_with : t -> (Field.t * t) list -> t (** Create an updated record *)
val cstr_tester : Cstr.t -> t -> t (** Given a constructor [c] and a term [t], returns a terms that evaluates to [true] iff [t] has [c] as head constructor. *)
val _true : t (** The `true` literal. *)
val _and : t list -> t (** Conjunction of formulas *)
val lam : ty_var list * Var.t list -> t -> t (** Create a local function. *)
val all : ty_var list * Var.t list -> t -> t (** Universally quantify the given formula over the type and terms variables. *)
val ex : ty_var list * Var.t list -> t -> t (** Existencially quantify the given formula over the type and terms variables. *)
val bind : Var.t -> t -> t (** Bind a variable to an expressions. This function is called when typing a let-binding, before the body of the let-binding is typed. The returned expressions is used to replace the variable everywhere in the body of the let-binding being typed. *)
val letin : (Var.t * t) list -> t -> t (** Create a sequential let-binding. *)
val letand : (Var.t * t) list -> t -> t (** Create a parrallel let-binding. *)
val pattern_match : ?redundant:(t -> unit) -> t -> (t * t) list -> t (** [pattern_match scrutinee branches] creates a pattern match expression on the scrutinee with the given branches, each of the form [(pattern, body)] *)
val set_tag : t -> 'a tag -> 'a -> unit (** Annotate the given formula wiht the tag and value. *)
val add_tag : t -> 'a list tag -> 'a -> unit (** Add a value to the list of values bound to a tag. *)
val fv : t -> ty_var list * Var.t list (** Returns the list of free variables in the formula. *)
end
module type Thf = sig
include Tff
val apply : t -> ty list -> t list -> t (** Polymorphic application. *)
end
(** Minimum required to type dimacs *)module type Dimacs = sig
type t (** The type of terms *)
val neg : t -> t (** Logical negation. *)
end
(** Minimum required to type ae's tff *)module type Ae_Base = sig
type t (** The type of terms *)
type term_var (** The type of term variables *)
val void : t (** The only value of type unit. *)
val eq : t -> t -> t (** Build the equality of two terms. *)
val _true : t (** The smybol for [true] *)
val _false : t (** The symbol for [false] *)
val neg : t -> t (** Negation. *)
val _or : t list -> t (** Disjunction of formulas *)
val _and : t list -> t (** Conjunction of formulas *)
val imply : t -> t -> t (** Implication *)
val equiv : t -> t -> t (** Equivalence *)
val xor : t -> t -> t (** Exclusive disjunction. *)
val ite : t -> t -> t -> t (** [ite condition then_t else_t] creates a conditional branch. *)
val distinct : t list -> t (** Distinct constraints on terms. *)
val multi_trigger : t list -> t (** Create a multi trigger from a list of arbtirary terms. *)
val semantic_trigger : t -> t (** Semantic triggers for alt-ergo. *)
val maps_to : term_var -> t -> t (** Semantic trigger: maps to. *)
end
module type Ae_Arith_Common = sig
type t (** The type of terms *)
val minus : t -> t (** Arithmetic unary minus/negation. *)
val add : t -> t -> t (** Arithmetic addition. *)
val sub : t -> t -> t (** Arithmetic substraction *)
val mul : t -> t -> t (** Arithmetic multiplication *)
val pow : t -> t -> t (** Arithmetic exponentiation *)
val lt : t -> t -> t (** Arithmetic "less than" comparison. *)
val le : t -> t -> t (** Arithmetic "less or equal" comparison. *)
val gt : t -> t -> t (** Arithmetic "greater than" comparison. *)
val ge : t -> t -> t (** Arithmetic "greater or equal" comparison. *)
end
(** Minimum required to type ae's arith *)module type Ae_Arith = sig
type t (** The type of terms. *)
type ty (** The type of types. *)
val ty : t -> ty (** Get the type of a term. *)
val int : string -> t (** Integer literals *)
val real : string -> t (** Real literals *)
val semantic_trigger : t -> t (** Semantic triggers for alt-ergo. *)
module Int : sig include Ae_Arith_Common with type t := t
val div_e : t -> t -> t (** Euclidian division quotient *)
val rem_e : t -> t -> t (** Euclidian division remainder *)
val to_real : t -> t (** Conversion from an integer term to a real term. *)
val abs : t -> t (** Arithmetic absolute value. *)
end
module Real : sig include Ae_Arith_Common with type t := t
val div : t -> t -> t (** Exact division on reals. *)
val is_int : t -> t (** Integer testing *)
val floor_to_int : t -> t (** Greatest integer smaller than the given real *)
end
end
module type Ae_Array = sig
type t (** The type of terms *)
val select : t -> t -> t (** [select arr idx] creates the get operation on functionnal array [arr] for index [idx]. *)
val store : t -> t -> t -> t (** [store arr idx value] creates the set operation on functional array [arr] for value [value] at index [idx]. *)
end
(** Minimum required to type ae's bitvectors *)module type Ae_Bitv = sig
type t (** The type of terms *)
val mk : string -> t (** Create a bitvector litteral from a string representation. The string should only contain characters '0' or '1'. *)
val concat : t -> t -> t (** Bitvector concatenation. *)
val extract : int -> int -> t -> t (** Bitvector extraction, using in that order, the start and then end positions of the bitvector to extract. *)
val repeat : int -> t -> t (** Repetition of a bitvector. *)
val zero_extend : int -> t -> t (** Extend the given bitvector with the given number of 0s. *)
val sign_extend : int -> t -> t (** Extend the given bitvector with its most significant bit repeated the given number of times. *)
val rotate_right : int -> t -> t (** [rotate_right i x] means rotate bits of x to the right i times. *)
val rotate_left : int -> t -> t (** [rotate_left i x] means rotate bits of x to the left i times. *)
val not : t -> t (** Bitwise negation. *)
val and_ : t -> t -> t (** Bitwise conjunction. *)
val or_ : t -> t -> t (** Bitwise disjunction. *)
val nand : t -> t -> t (** [nand s t] abbreviates [not (and_ s t)]. *)
val nor : t -> t -> t (** [nor s t] abbreviates [not (or_ s t)]. *)
val xor : t -> t -> t (** [xor s t] abbreviates [or_ (and_ s (not t)) (and_ (not s) t)]. *)
val xnor : t -> t -> t (** [xnor s t] abbreviates [or_ (and_ s t) (and_ (not s) (not t))]. *)
val comp : t -> t -> t (** Bitwise comparison. [comp s t] equals [#b1] iff [s] and [t] are bitwise equal. *)
val neg : t -> t (** Arithmetic complement on bitvectors. Supposing an input bitvector of size [m] representing an integer [k], the resulting term should represent the integer [2^m - k]. *)
val add : t -> t -> t (** Arithmetic addition on bitvectors, modulo the size of the bitvectors (overflows wrap around [2^m] where [m] is the size of the two input bitvectors). *)
val sub : t -> t -> t (** Arithmetic substraction on bitvectors, modulo the size of the bitvectors (2's complement subtraction modulo). [sub s t] should be equal to [add s (neg t)]. *)
val mul : t -> t -> t (** Arithmetic multiplication on bitvectors, modulo the size of the bitvectors (see {!add}). *)
val udiv : t -> t -> t (** Arithmetic euclidian integer division on bitvectors. *)
val urem : t -> t -> t (** Arithmetic euclidian integer remainder on bitvectors. *)
val sdiv : t -> t -> t (** Arithmetic 2's complement signed division. (see smtlib's specification for more information). *)
val srem : t -> t -> t (** Arithmetic 2's complement signed remainder (sign follows dividend). (see smtlib's specification for more information). *)
val smod : t -> t -> t (** Arithmetic 2's complement signed remainder (sign follows divisor). (see smtlib's specification for more information). *)
val shl : t -> t -> t (** Logical shift left. [shl t k] return the result of shifting [t] to the left [k] times. In other words, this should return the bitvector representing [t * 2^k] (since bitvectors represent integers using the least significatn bit in cell 0). *)
val lshr : t -> t -> t (** Logical shift right. [lshr t k] return the result of shifting [t] to the right [k] times. In other words, this should return the bitvector representing [t / (2^k)]. *)
val ashr : t -> t -> t (** Arithmetic shift right, like logical shift right except that the most significant bits of the result always copy the most significant bit of the first argument*)
val ult : t -> t -> t (** Boolean arithmetic comparison (less than). [ult s t] should return the [true] term iff [s < t]. *)
val ule : t -> t -> t (** Boolean arithmetic comparison (less or equal than). *)
val ugt : t -> t -> t (** Boolean arithmetic comparison (greater than). *)
val uge : t -> t -> t (** Boolean arithmetic comparison (greater or equal than). *)
val slt : t -> t -> t (** Boolean signed arithmetic comparison (less than). (See smtlib's specification for more information) *)
val sle : t -> t -> t (** Boolean signed arithmetic comparison (less or equal than). *)
val sgt : t -> t -> t (** Boolean signed arithmetic comparison (greater than). *)
val sge : t -> t -> t (** Boolean signed arithmetic comparison (greater or equal than). *)
end
module type Ae_Float_Float = sig
type t (** the type of terms *)
val roundNearestTiesToEven: t (** constant for rounding mode RNE *)
val roundNearestTiesToAway: t (** constant for rounding mode RNA *)
val roundTowardPositive: t (** constant for rounding mode RTP *)
val roundTowardNegative: t (** constant for rounding mode RTN *)
val roundTowardZero: t (** constant for rounding mode RTZ *)
end
(* Minimum required to type Ae floats *)module type Ae_Float = sig
type t (** The type of terms *)
type ty (** The type of types. *)
val ty : t -> ty (** Type of a term. *)
module Float : Ae_Float_Float with type t := t (** Sub-module used for namespacing the floating number part of the theory requirements *)
end
(** Minimum required to type tptp's tff *)module type Tptp_Tff_Core = sig
type t (** The type of terms *)
val _true : t (** The smybol for [true] *)
val _false : t (** The symbol for [false] *)
val neg : t -> t (** Negation. *)
val _or : t list -> t (** Disjunction of formulas *)
val _and : t list -> t (** Conjunction of formulas *)
val nand : t -> t -> t (** Not-and *)
val nor : t -> t -> t (** Not-or *)
val imply : t -> t -> t (** Implication *)
val implied : t -> t -> t (** Implication *)
val equiv : t -> t -> t (** Equivalence *)
val xor : t -> t -> t (** Exclusive disjunction. *)
val ite : t -> t -> t -> t (** [ite condition then_t else_t] creates a conditional branch. *)
val eq : t -> t -> t (** Build the equality of two terms. *)
val neq : t -> t -> t (** Disequality. *)
val distinct : t list -> t (** Distinct constraints on terms. *)
end
module type Tptp_Thf_Core_Const = sig
type t (** Type for term constans *)
val _true : t (** The smybol for [true] *)
val _false : t (** The symbol for [false] *)
val neg : t (** Negation. *)
val or_ : t (** Binary disjunction of formulas *)
val and_ : t (** Binary conjunction of formulas *)
val nand : t (** Not-and *)
val nor : t (** Not-or *)
val imply : t (** Implication *)
val implied : t (** Reverse implication *)
val equiv : t (** Equivalence *)
val xor : t (** Exclusive disjunction. *)
val ite : t (** [ite condition then_t else_t] creates a conditional branch. *)
val eq : t (** Build the equality of two terms. *)
val neq : t (** Binary disequality. *)
val pi : t (** Higher-order encoding of universla quantification. *)
val sigma : t (** Higher-order encoding of existancial quantification. *)
end
(** Minimum required to type tptp's thf *)module type Tptp_Thf_Core = sig
type t (** The type of terms *)
type ty (** The type of types *)
module Const : Tptp_Thf_Core_Const (** Constants *)
val of_cst : Const.t -> t (** Create a term out of aconstant. *)
val distinct : t list -> t (** Distinct constraints on terms. *)
end
(** Common signature for tptp arithmetics *)module type Tptp_Tff_Arith_Common = sig
type t (** The type of terms *)
val minus : t -> t (** Arithmetic unary minus/negation. *)
val add : t -> t -> t (** Arithmetic addition. *)
val sub : t -> t -> t (** Arithmetic substraction *)
val mul : t -> t -> t (** Arithmetic multiplication *)
val div_e : t -> t -> t (** Euclidian division quotient *)
val div_t : t -> t -> t (** Truncation of the rational/real division. *)
val div_f : t -> t -> t (** Floor of the ration/real division. *)
val rem_e : t -> t -> t (** Euclidian division remainder *)
val rem_t : t -> t -> t (** Remainder for the truncation of the rational/real division. *)
val rem_f : t -> t -> t (** Remaidner for the floor of the ration/real division. *)
val lt : t -> t -> t (** Arithmetic "less than" comparison. *)
val le : t -> t -> t (** Arithmetic "less or equal" comparison. *)
val gt : t -> t -> t (** Arithmetic "greater than" comparison. *)
val ge : t -> t -> t (** Arithmetic "greater or equal" comparison. *)
val floor : t -> t (** Floor function. *)
val ceiling : t -> t (** Ceiling *)
val truncate : t -> t (** Truncation. *)
val round : t -> t (** Rounding to the nearest integer. *)
val is_int : t -> t (** Integer testing *)
val is_rat : t -> t (** Rationality testing. *)
val to_int : t -> t (** Convesion to an integer. *)
val to_rat : t -> t (** Conversion to a rational. *)
val to_real : t -> t (** Conversion to a real. *)
end
(** Signature required by terms for typing tptp arithmetic. *)module type Tptp_Tff_Arith = sig
type t (** The type of terms. *)
type ty (** The type of types. *)
val ty : t -> ty (** Get the type of a term. *)
val int : string -> t (** Integer literals *)
val rat : string -> t (** Rational literals *)
val real : string -> t (** Real literals *)
module Int : sig include Tptp_Tff_Arith_Common with type t := t end
module Rat : sig include Tptp_Tff_Arith_Common with type t := t
val div : t -> t -> t (** Exact division on rationals. *) end
module Real : sig include Tptp_Tff_Arith_Common with type t := t
val div : t -> t -> t (** Exact division on reals. *) end
end
(** Minimum required to type smtlib's core theory. *)module type Smtlib_Base = sig
type t (** The type of terms. *)
type cstr (** The type of ADT constructor *)
val _true : t (** The smybol for [true] *)
val _false : t (** The symbol for [false] *)
val neg : t -> t (** Negation. *)
val _or : t list -> t (** Disjunction of formulas *)
val _and : t list -> t (** Disjunction of formulas *)
val nand : t -> t -> t (** Not-and *)
val nor : t -> t -> t (** Not-or *)
val imply : t -> t -> t (** Implication *)
val equiv : t -> t -> t (** Equivalence *)
val xor : t -> t -> t (** Exclusive disjunction. *)
val ite : t -> t -> t -> t (** [ite condition then_t else_t] creates a conditional branch. *)
val eq : t -> t -> t (** Create a chain of equalities. *)
val distinct : t list -> t (** Distinct constraints on terms. *)
val multi_trigger : t list -> t (** Create a multi trigger from a list of arbtirary terms. *)
end
module type Smtlib_Ho = sig
type t (** The type of terms. *)
type var (** The type of term variables *)
val map_app : t -> t -> t (** Application operation for the encoding of higher-order terms into first-order. *)
val map_lambda : var list -> t -> t (** Shallow embedding of lambdas/actual functions into the higher-order encoding. *)
end
(** Common signature for first-order arithmetic *)module type Smtlib_Arith_Common = sig
type t (** The type of terms *)
type cst (** The type of term constants. *)
val mk : string -> t (** Build a constant. The literal is passed as a string to avoid overflow caused by the limited precision of native number formats. *)
val minus : t -> t (** Arithmetic unary minus/negation. *)
val add : t -> t -> t (** Arithmetic addition. *)
val sub : t -> t -> t (** Arithmetic substraction *)
val mul : t -> t -> t (** Arithmetic multiplication *)
val lt : t -> t -> t (** Arithmetic "less than" comparison. *)
val le : t -> t -> t (** Arithmetic "less or equal" comparison. *)
val gt : t -> t -> t (** Arithmetic "greater than" comparison. *)
val ge : t -> t -> t (** Arithmetic "greater or equal" comparison. *)
end
(** Signature required by terms for typing smtlib int arithmetic. *)module type Smtlib_Int = sig
include Smtlib_Arith_Common
val div' : cst (** Constant for the division. *)
val div : t -> t -> t (** Euclidian division. See Smtlib theory for a full description. *)
val rem' : cst (** Constant for the remainder. *)
val rem : t -> t -> t (** Euclidian integer remainder See Smtlib theory for a full description. *)
val abs : t -> t (** Arithmetic absolute value. *)
val pow : t -> t -> t (** Exponentiation / power operation. *)
val divisible : string -> t -> t (** Arithmetic divisibility predicate. Indexed over constant integers (represented as strings, see {!int}). *)
end
(** Signature required by terms for typing smtlib real arithmetic. *)module type Smtlib_Real = sig
include Smtlib_Arith_Common
val div' : cst (** Constant for the division. *)
val div : t -> t -> t (** Real division. See Smtlib theory for a full description. *)
end
(** Signature required by terms for typing smtlib real_int arithmetic. *)module type Smtlib_Real_Int = sig
type t (** The type of terms. *)
type ty (** The type of types. *)
val ty : t -> ty (** Get the type of a term. *)
module Int : sig
include Smtlib_Int with type t := t
val to_real : t -> t (** Conversion from an integer term to a real term. *)
end
module Real : sig
include Smtlib_Real with type t := t
val is_int : t -> t (** Arithmetic predicate, true on reals that are also integers. *)
val floor_to_int : t -> t (** Greatest integer smaller than the given real *)
end
end
module type Smtlib_Array = sig
type t (** The type of terms *)
type ty (** Type of of types. *)
val const : ty -> t -> t (** [const ty base] creates a constant array that maps any value of type [ty] to [base]. *)
val select : t -> t -> t (** [select arr idx] creates the get operation on functionnal array [arr] for index [idx]. *)
val store : t -> t -> t -> t (** [store arr idx value] creates the set operation on functional array [arr] for value [value] at index [idx]. *)
end
module type Smtlib_Bvconv = sig
type t (** The type of terms *)
val to_int : signed:bool -> t -> t (** Application of the bv2nat conversion function. *)
val of_int : int -> t -> t (** Application of the int2bv conversion function. *)
end
module type Smtlib_Bitv = sig
type t (** The type of terms *)
val mk : string -> t (** Create a bitvector litteral from a string representation. The string should only contain characters '0' or '1'. *)
val concat : t -> t -> t (** Bitvector concatenation. *)
val extract : int -> int -> t -> t (** Bitvector extraction, using in that order, the end (exclusive) and then the start (inclusive) position of the bitvector to extract. *)
val repeat : int -> t -> t (** Repetition of a bitvector. *)
val zero_extend : int -> t -> t (** Extend the given bitvector with the given number of 0s. *)
val sign_extend : int -> t -> t (** Extend the given bitvector with its most significant bit repeated the given number of times. *)
val rotate_right : int -> t -> t (** [rotate_right i x] means rotate bits of x to the right i times. *)
val rotate_left : int -> t -> t (** [rotate_left i x] means rotate bits of x to the left i times. *)
val not : t -> t (** Bitwise negation. *)
val and_ : t -> t -> t (** Bitwise conjunction. *)
val or_ : t -> t -> t (** Bitwise disjunction. *)
val nand : t -> t -> t (** [nand s t] abbreviates [not (and_ s t)]. *)
val nor : t -> t -> t (** [nor s t] abbreviates [not (or_ s t)]. *)
val xor : t -> t -> t (** [xor s t] abbreviates [or_ (and_ s (not t)) (and_ (not s) t)]. *)
val xnor : t -> t -> t (** [xnor s t] abbreviates [or_ (and_ s t) (and_ (not s) (not t))]. *)
val comp : t -> t -> t (** Bitwise comparison. [comp s t] equals [#b1] iff [s] and [t] are bitwise equal. *)
val neg : t -> t (** Arithmetic complement on bitvectors. Supposing an input bitvector of size [m] representing an integer [k], the resulting term should represent the integer [2^m - k]. *)
val add : t -> t -> t (** Arithmetic addition on bitvectors, modulo the size of the bitvectors (overflows wrap around [2^m] where [m] is the size of the two input bitvectors). *)
val sub : t -> t -> t (** Arithmetic substraction on bitvectors, modulo the size of the bitvectors (2's complement subtraction modulo). [sub s t] should be equal to [add s (neg t)]. *)
val mul : t -> t -> t (** Arithmetic multiplication on bitvectors, modulo the size of the bitvectors (see {!add}). *)
val udiv : t -> t -> t (** Arithmetic euclidian integer division on bitvectors. *)
val urem : t -> t -> t (** Arithmetic euclidian integer remainder on bitvectors. *)
val sdiv : t -> t -> t (** Arithmetic 2's complement signed division. (see smtlib's specification for more information). *)
val srem : t -> t -> t (** Arithmetic 2's complement signed remainder (sign follows dividend). (see smtlib's specification for more information). *)
val smod : t -> t -> t (** Arithmetic 2's complement signed remainder (sign follows divisor). (see smtlib's specification for more information). *)
val shl : t -> t -> t (** Logical shift left. [shl t k] return the result of shifting [t] to the left [k] times. In other words, this should return the bitvector representing [t * 2^k] (since bitvectors represent integers using the least significatn bit in cell 0). *)
val lshr : t -> t -> t (** Logical shift right. [lshr t k] return the result of shifting [t] to the right [k] times. In other words, this should return the bitvector representing [t / (2^k)]. *)
val ashr : t -> t -> t (** Arithmetic shift right, like logical shift right except that the most significant bits of the result always copy the most significant bit of the first argument*)
val ult : t -> t -> t (** Boolean arithmetic comparison (less than). [ult s t] should return the [true] term iff [s < t]. *)
val ule : t -> t -> t (** Boolean arithmetic comparison (less or equal than). *)
val ugt : t -> t -> t (** Boolean arithmetic comparison (greater than). *)
val uge : t -> t -> t (** Boolean arithmetic comparison (greater or equal than). *)
val slt : t -> t -> t (** Boolean signed arithmetic comparison (less than). (See smtlib's specification for more information) *)
val sle : t -> t -> t (** Boolean signed arithmetic comparison (less or equal than). *)
val sgt : t -> t -> t (** Boolean signed arithmetic comparison (greater than). *)
val sge : t -> t -> t (** Boolean signed arithmetic comparison (greater or equal than). *)
val nego : t -> t (** Boolean unary overflow predicate for unary minus. *)
val addo : signed:bool -> t -> t -> t (** Boolean unary binary overflow predicate for signed/unsigned addition *)
val subo : signed:bool -> t -> t -> t (** Boolean unary binary overflow predicate for signed/unsigned subtraction *)
val mulo : signed:bool -> t -> t -> t (** Boolean unary binary overflow predicate for signed/unsigned multiplication *)
val divo : t -> t -> t (** Boolean unary binary overflow predicate for signed division *)
val to_int : signed:bool -> t -> t (** Application of the bv2nat conversion function. *)
val of_int : int -> t -> t (** Application of the int2bv conversion function. *)
end
(** Bitvector part of the smtlib float requirements *)module type Smtlib_Float_Bitv = sig
type t (** the type of terms *)
val mk : string -> t (** Bitvector litteral. *)
end
(** Real part of the smtlib float requirements *)module type Smtlib_Float_Real = sig
type t (** the type of terms *)
val mk : string -> t (** Bitvector litteral. *)
end
(** Float part of the smtlib float requirements *)module type Smtlib_Float_Float = sig
type t (** the type of terms *)
type cst (** The type of term constants. *)
val fp : t -> t -> t -> t (** Construct a floating point from bitvector literals (sign, exponent, significand). The sign should be of size 1. *)
val roundNearestTiesToEven: t (** constant for rounding mode RNE *)
val roundNearestTiesToAway: t (** constant for rounding mode RNA *)
val roundTowardPositive: t (** constant for rounding mode RTP *)
val roundTowardNegative: t (** constant for rounding mode RTN *)
val roundTowardZero: t (** constant for rounding mode RTZ *)
val plus_infinity: int -> int -> t (** The constant plus infinity, it is also equivalent to a literal *)
val minus_infinity: int -> int -> t (** The constant minus infinity, it is also equivalent to a literal *)
val plus_zero: int -> int -> t (** The constant plus zero, it is also equivalent to a literal *)
val minus_zero: int -> int -> t (** The constant minus zero, it is also equivalent to a literal *)
val nan: int -> int -> t (** The constant Non-numbers, it is also equivalent to many literals which are equivalent together *)
val abs : t -> t (** absolute value *)
val neg : t -> t (** negation *)
val add : t -> t -> t -> t (** [add rm f1 f2] addition *)
val sub : t -> t -> t -> t (** [sub rm f1 f2] subtraction *)
val mul : t -> t -> t -> t (** [mul rm f1 f2] multiplication *)
val div : t -> t -> t -> t (** [mul rm f1 f2] division *)
val fma : t -> t -> t -> t -> t (** [mul rm f1 f2] fused multiplication and addition *)
val sqrt : t -> t -> t (** [sqrt rm f] square root *)
val rem : t -> t -> t (** [rem f1 f2] remainder *)
val roundToIntegral : t -> t -> t (** [roundToIntegral rm f] rounding to integral *)
val min : t -> t -> t (** [min f1 f2] minimum *)
val min' : int * int -> cst (** Constant for float min. *)
val max : t -> t -> t (** [max f1 f2] maximum *)
val max' : int * int -> cst (** Constant for float max. *)
val leq : t -> t -> t (** [leq f1 f2] less or equal floating point comparison *)
val lt : t -> t -> t (** [lt f1 f2] less than floating point comparison *)
val geq : t -> t -> t (** [geq f1 f2] greater or equal floating point comparison *)
val gt : t -> t -> t (** [lt f1 f2] greater than floating point comparison *)
val eq : t -> t -> t (** [eq f1 f2] floating point equality *)
val isNormal : t -> t (** [isNormal f] test if it is a normal floating point *)
val isSubnormal : t -> t (** [isSubnormal f] test if it is a subnormal floating point *)
val isZero : t -> t (** [isZero f] test if it is a zero *)
val isInfinite : t -> t (** [isInfinite f] test if it is an infinite *)
val isNaN : t -> t (** [isNaN f] test if it is NaN *)
val isNegative : t -> t (** [isNegative f] test if it is a negative floating point *)
val isPositive : t -> t (** [isPositive f] test if it is a positive floating point *)
val ieee_format_to_fp: int -> int -> t -> t (** [ieee_format_to_fp e s bv] Convert a bitvector into a floating point using IEEE 754-2008 interchange format. (reinterpret the bitvector into floating-point) *)
val to_fp: int -> int -> t -> t -> t (** [to_fp e s rm f] convert from one floating point format to another *)
val real_to_fp: int -> int -> t -> t -> t (** [real_to_fp e s rm r] convert from a real *)
val sbv_to_fp: int -> int -> t -> t -> t (** [sbv_to_fp e s rm bv] convert from a signed integer *)
val ubv_to_fp: int -> int -> t -> t -> t (** [ubv_to_fp e s rm bv] convert from an unsigned integer *)
val to_ubv: int -> t -> t -> t (** [to_ubv m rm f] convert to an unsigned integer (bitvector of size m) *)
val to_ubv' : int -> int * int -> cst (** constant for [to_ubv] *)
val to_sbv: int -> t -> t -> t (** [to_ubv m rm f] convert to a signed integer (bitvector of size m) *)
val to_sbv' : int -> int * int -> cst (** constant for [to_sbv] *)
val to_real: t -> t (** [to_real f] convert to a real *)
end
(* Requirement for the Floats SMTLIB theory *)module type Smtlib_Float = sig
(** Floating points are complicated so this documentation is not in anyway sufficient. A detailed description of the theory together with the rationale of several models decisions as well as a formal semantics of the theory can be found in
[BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic Technical Report, 2015. (http://smt-lib.org/papers/BTRW15.pdf) *)
type t (** The type of terms *)
type ty (** The type of types. *)
type cst (** The type of term constants *)
val ty : t -> ty (** Type of a term. *)
module Real : Smtlib_Float_Real with type t := t (** Sub-module used for namespacing the real part of the theory requirements *)
module Bitv : Smtlib_Float_Bitv with type t := t (** Sub-module used for namespacing the bitvector part of the theory requirements *)
module Float : Smtlib_Float_Float with type t := t and type cst := cst (** Sub-module used for namespacing the floating number part of the theory requirements *)
end
module type Smtlib_String_RegLan = sig
type t (** The type of terms *)
val empty : t (** The empty regular language. *)
val all : t (** The language that contains all strings *)
val allchar : t (** The language that contains all strings of length 1 *)
val of_string : t -> t (** Singleton language containing a single string. *)
val range : t -> t -> t (** [range s1 s2] is the language containing all singleton strings (i.e. string of length 1) that are lexicographically beetween [s1] and [s2], **assuming [s1] and [s2] are singleton strings**. Else it is the empty language. *)
val concat : t -> t -> t (** Language concatenation. *)
val union : t -> t -> t (** Language union. *)
val inter : t -> t -> t (** language intersection. *)
val star : t -> t (** Kleene closure. *)
val cross : t -> t (** Kleene cross. [cross e] abbreviates [concat e (star e)] *)
val complement : t -> t (** Complement. *)
val diff : t -> t -> t (** Difference *)
val option : t -> t (** Option. [option e] abbreviates [union e (of_string "")] *)
val power : int -> t -> t (** [power n e] is [n]-th power of [e]. *)
val loop : int -> int -> t -> t (** Loop. See SMTLIb documentation. *)
end
module type Smtlib_String_String = sig
type t (** The type of terms *)
val of_ustring : string -> t (** Create a string from a unicode UTF-8 encoded string (with escape sequences already interpreted as unicode characters). *)
val length : t -> t (** Length of a string expression. *)
val at : t -> t -> t (** Get the char at the given position. *)
val is_digit : t -> t (** Is the string a singleton string with a single digit character ? *)
val to_code : t -> t (** Returns the code point of the single character of the string, or [(-1)] is the string is not a singleton. *)
val of_code : t -> t (** Returns the singleton string whose only character is the given code point. *)
val to_int : t -> t (** Evaluates the string as a decimal natural number, or [(-1)] if it's not possible. *)
val of_int : t -> t (** Convert an int expression to a string in decimal representation. *)
val concat : t -> t -> t (** String concatenation. *)
val sub : t -> t -> t -> t (** Substring extraction. *)
val index_of : t -> t -> t -> t (** Index of the first occurrence of the second string in first one, starting at the position of the third argument. *)
val replace : t -> t -> t -> t (** Replace the first occurrence. *)
val replace_all : t -> t -> t -> t (** Replace all occurrences. *)
val replace_re : t -> t -> t -> t (** Replace the leftmost, shortest re ocurrence. *)
val replace_re_all : t -> t -> t -> t (** Replace left-to-right, each shortest non empty re occurrence. *)
val is_prefix : t -> t -> t (** First string is a prefix of the second one. *)
val is_suffix : t -> t -> t (** First string is a suffix of the second one. *)
val contains : t -> t -> t (** First string contains the second one. *)
val lt : t -> t -> t (** Lexicographic strict ordering. *)
val leq : t -> t -> t (** Lexicographic large ordering. *)
val in_re : t -> t -> t (** String Regular languager membership *)
module RegLan : Smtlib_String_RegLan with type t := t (** Sub-module used for namespacing for the regular language part of the theory requirements. *)
end
module type Smtlib_String = sig
type t (** The type of terms *)
module String : Smtlib_String_String with type t := t (** Sub-module used for namespacing for the string part of the theory requirements. *)
end
module type Zf_Base = sig
type t (** The type of terms *)
val _true : t (** The smybol for [true] *)
val _false : t (** The symbol for [false] *)
val neg : t -> t (** Negation. *)
val _or : t list -> t (** Disjunction of formulas *)
val _and : t list -> t (** Conjunction of formulas *)
val imply : t -> t -> t (** Logical Implication. *)
val equiv : t -> t -> t (** Logical Equivalence. *)
val eq : t -> t -> t (** Build the equality of two terms. *)
val neq : t -> t -> t (** Disequality. *)
val ite : t -> t -> t -> t (** If-then-else *)
end
module type Zf_Arith = sig
type t (** The type of terms *)
val int : string -> t (** Integer literals *)
module Int : sig val minus : t -> t (** Arithmetic unary minus/negation. *)
val add : t -> t -> t (** Arithmetic addition. *)
val sub : t -> t -> t (** Arithmetic substraction *)
val mul : t -> t -> t (** Arithmetic multiplication *)
val lt : t -> t -> t (** Arithmetic "less than" comparison. *)
val le : t -> t -> t (** Arithmetic "less or equal" comparison. *)
val gt : t -> t -> t (** Arithmetic "greater than" comparison. *)
val ge : t -> t -> t (** Arithmetic "greater or equal" comparison. *) end
end