package dolmen_type

  1. Overview
  2. Docs
On This Page
  1. Smtlib logics
Legend:
Library
Module
Module type
Parameter
Class
Class type

Smtlib logics

type theory = [
  1. | `Core
  2. | `Arrays
  3. | `Bitvectors
  4. | `Floats
  5. | `String
  6. | `Ints
  7. | `Reals
  8. | `Reals_Ints
]

Smtlib theories.

type features = {
  1. free_sorts : bool;
  2. free_functions : bool;
  3. datatypes : bool;
  4. quantifiers : bool;
  5. arithmetic : Arith.Smtlib2.arith;
  6. arrays : Arrays.Smtlib2.arrays;
}

Smtlib features.

type t = {
  1. theories : theory list;
  2. features : features;
}

Structured representation of an smtlib logic.

val parse : string -> t option

Parses an smtlib logic string and returns its structured version.

val all : t

All the smtlib2 logic parsable