SMT-LIB Logics. This module defines the set of SMT-LIB logics, which specify the theories and operations that a solver may handle. Each logic represents a combination of supported theories, such as arithmetic, arrays, bitvectors, and uninterpreted functions.
type t = | ALLThe logic that encompasses all theories.
*)| AUFLIAArrays, uninterpreted functions, and linear integer arithmetic.
*)| AUFLIRAArrays, uninterpreted functions, linear integer and real arithmetic.
*)| AUFNIRAArrays, uninterpreted functions, and non-linear integer and real arithmetic.
*)| LIALinear integer arithmetic.
*)| LRALinear real arithmetic.
*)| QF_ABVQuantifier-free arrays and bitvectors.
*)| QF_AUFBVQuantifier-free arrays, uninterpreted functions, and bitvectors.
*)| QF_AUFLIAQuantifier-free arrays, uninterpreted functions, and linear integer arithmetic.
*)| QF_AXQuantifier-free array theory.
*)| QF_BVQuantifier-free bitvector theory.
*)| QF_BVFPQuantifier-free bitvectors and floating-point arithmetic.
*)| QF_IDLQuantifier-free integer difference logic.
*)| QF_LIAQuantifier-free linear integer arithmetic.
*)| QF_LRAQuantifier-free linear real arithmetic.
*)| QF_NIAQuantifier-free non-linear integer arithmetic.
*)| QF_NRAQuantifier-free non-linear real arithmetic.
*)| QF_RDLQuantifier-free real difference logic.
*)| QF_SQuantifier-free string theory.
*)| QF_UFQuantifier-free uninterpreted functions.
*)| QF_UFBVQuantifier-free uninterpreted functions with bitvectors.
*)| QF_UFIDLQuantifier-free uninterpreted functions with integer difference logic.
*)| QF_UFLIAQuantifier-free uninterpreted functions with linear integer arithmetic.
*)| QF_UFLRAQuantifier-free uninterpreted functions with linear real arithmetic.
*)| QF_UFNRAQuantifier-free uninterpreted functions with non-linear real arithmetic.
*)| UFLRAUninterpreted functions with linear real arithmetic.
*)| UFNIAUninterpreted functions with non-linear integer arithmetic.
*)A type representing various SMT-LIB logics.
val of_string : string -> (t, [> `Msg of string ]) Smtml_prelude.resultof_string s parses an SMT-LIB logic from a string. Returns `Ok t if parsing is successful, or `Error `Msg if the string does not match a known logic.