package dolmen_type

  1. Overview
  2. Docs
On This Page
  1. Smtlib logics
package dolmen_type
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.config;
  6. arrays : Arrays.Smtlib2.config;
}

Smtlib features.

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

Structured representation of an smtlib logic.

val print : Stdlib.Format.formatter -> t -> unit
val print_theory : Stdlib.Format.formatter -> theory -> unit
val print_theories : Stdlib.Format.formatter -> theory list -> unit
val print_features : Stdlib.Format.formatter -> features -> unit

Printing functions

val parse : string -> t option

Parses an smtlib logic string and returns its structured version.

val all : t

All the smtlib2 logic parsable