Dolmen_type.LogicSome languages define a notion of logics to distinguish different fragments at type-checking and during solving. This file is here to help with handling such logics.
module Smtlib2 : sig ... endtype t = | Auto | (* Default case when no logic is specified or for languages which do not have a notion of different logics (i.e. the language only has one logic). *) |
| Smtlib2 of Smtlib2.t | (* Smtlib2 logic. *) |
Wrapper type to represent the different logics.