dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type

Smtlib logics

type theory = [
| `Core
| `Arrays
| `Bitvectors
| `Floats
| `String
| `Ints
| `Reals
| `Reals_Ints
]

Smtlib theories.

type features = {
free_sorts : bool;
free_functions : bool;
datatypes : bool;
quantifiers : bool;
arithmetic : Arith.Smtlib2.arith;
arrays : Arrays.Smtlib2.arrays;
}

Smtlib features.

type t = {
theories : theory list;
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