Module Smtml.LogicSource

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.

Logic Types

Sourcetype t =
  1. | ALL
    (*

    The logic that encompasses all theories.

    *)
  2. | AUFLIA
    (*

    Arrays, uninterpreted functions, and linear integer arithmetic.

    *)
  3. | AUFLIRA
    (*

    Arrays, uninterpreted functions, linear integer and real arithmetic.

    *)
  4. | AUFNIRA
    (*

    Arrays, uninterpreted functions, and non-linear integer and real arithmetic.

    *)
  5. | LIA
    (*

    Linear integer arithmetic.

    *)
  6. | LRA
    (*

    Linear real arithmetic.

    *)
  7. | QF_ABV
    (*

    Quantifier-free arrays and bitvectors.

    *)
  8. | QF_AUFBV
    (*

    Quantifier-free arrays, uninterpreted functions, and bitvectors.

    *)
  9. | QF_AUFLIA
    (*

    Quantifier-free arrays, uninterpreted functions, and linear integer arithmetic.

    *)
  10. | QF_AX
    (*

    Quantifier-free array theory.

    *)
  11. | QF_BV
    (*

    Quantifier-free bitvector theory.

    *)
  12. | QF_BVFP
    (*

    Quantifier-free bitvectors and floating-point arithmetic.

    *)
  13. | QF_FP
    (*

    Quantifier-free floating-point arithmetic.

    *)
  14. | QF_IDL
    (*

    Quantifier-free integer difference logic.

    *)
  15. | QF_LIA
    (*

    Quantifier-free linear integer arithmetic.

    *)
  16. | QF_LRA
    (*

    Quantifier-free linear real arithmetic.

    *)
  17. | QF_NIA
    (*

    Quantifier-free non-linear integer arithmetic.

    *)
  18. | QF_NRA
    (*

    Quantifier-free non-linear real arithmetic.

    *)
  19. | QF_RDL
    (*

    Quantifier-free real difference logic.

    *)
  20. | QF_S
    (*

    Quantifier-free string theory.

    *)
  21. | QF_UF
    (*

    Quantifier-free uninterpreted functions.

    *)
  22. | QF_UFBV
    (*

    Quantifier-free uninterpreted functions with bitvectors.

    *)
  23. | QF_UFIDL
    (*

    Quantifier-free uninterpreted functions with integer difference logic.

    *)
  24. | QF_UFLIA
    (*

    Quantifier-free uninterpreted functions with linear integer arithmetic.

    *)
  25. | QF_UFLRA
    (*

    Quantifier-free uninterpreted functions with linear real arithmetic.

    *)
  26. | QF_UFNRA
    (*

    Quantifier-free uninterpreted functions with non-linear real arithmetic.

    *)
  27. | UFLRA
    (*

    Uninterpreted functions with linear real arithmetic.

    *)
  28. | UFNIA
    (*

    Uninterpreted functions with non-linear integer arithmetic.

    *)

A type representing various SMT-LIB logics.

Sourceval pp : t Fmt.t

pp fmt logic pretty-prints an SMT-LIB logic using the formatter fmt.

Sourceval of_string : string -> (t, [> `Msg of string ]) Smtml_prelude.result

of_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.