package dolmen_type

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package dolmen_type

dolmen_type
- Dolmen_type
  - Arith
    
    Ae
    
    Tff
    
    T
    
    Int
    
    Real
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Smtlib2
    
    Int
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Real
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Real_Int
    
    Tff
    
    T
    
    Int
    
    Real
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Tptp
    
    Tff
    
    T
    
    Int
    
    Rat
    
    Real
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Zf
    
    Thf
    
    T
    
    Int
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Arrays
    
    Ae
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Smtlib2
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Base
  - Bitv
    
    Ae
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Smtlib2
    
    Bvconv
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Core
    
    Ae
    
    Tff
    
    T
    
    Tag
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Dimacs
    
    Tff
    
    T
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Smtlib2
    
    Tff
    
    T
    
    Tag
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Tptp
    
    Tff
    
    T
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Thf
    
    T
    
    Const
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Zf
    
    Tff
    
    T
    
    Tag
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Def
    
    Declare
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Subst
    
    T
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Subst_arg
  - Float
    
    Smtlib2
    
    Tff
    
    T
    
    Bitv
    
    Float
    
    Real
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Intf
    
    Formulas
  - Logic
    
    Smtlib2
  - Misc
    
    Bitv
    
    Lists
    
    Options
    
    Strings
  - Strings
    
    Smtlib2
    
    Tff
    
    T
    
    String
    
    RegLan
    
    Ty
    
    Type
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Tff
    
    Make
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Tff_intf
    
    S
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Thf
    
    Make
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
  - Thf_intf
    
    S
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Type : Tff_intf.S

module Ty : Dolmen.Intf.Ty.Smtlib_Bitv with type t := Type.Ty.t

module T : Dolmen.Intf.Term.Smtlib_Bitv with type t := Type.T.t

Signature

type Type.err +=

| Non_positive_bitvector_size : int -> Dolmen.Std.Term.t Type.err
| Invalid_extract : int * int * int -> Dolmen.Std.Term.t Type.err
| Invalid_bin_char : char -> Dolmen.Std.Term.t Type.err
| Invalid_hex_char : char -> Dolmen.Std.Term.t Type.err
| Invalid_dec_char : char -> Dolmen.Std.Term.t Type.err

val parse : Dolmen.Smtlib2.version -> Type.builtin_symbols