Infer logic type from expression

[elsoroka]

If we implement the SMT-LIB logic definitions, this would allow Satisfiability.jl to infer the best logic type for a given SAT problem. Some SAT solvers will do this themselves (Z3), but others (CVC5) want to receive an explicit (set-logic _) command. Currently, users must provide this command explicitly when solvers require it, so it would be nice to have an infer_logic function that figures out the appropriate type.

[Fe-r-oz]

Thank you for your insights regarding the use of promote_rule and its use to encode the logic types. I think the first step maybe be to identify the logic_types currently supported, and to determine the type promotion rules based on the logic_type hierarchy. This can be aligned with the available logics as outlined in the figure on SMT-LIB.

Please let me know whether the following logic types are currently supported for Reals, Ints, and FixedSizeBitVectors? I have compiled the list of logics that exclude FloatingPoint, ArrayEx, and Strings.

Additionally, I think there may be some logics not implemented in the schematic shown below:

mindmap
  Logics
    LIA
    LRA
    QF_BV
    QF_IDL
    QF_LIA
    QF_NIA
    QF_RDL
    QF_UF
    QF_UFBV
    QF_UFIDL
    QF_UFLIA
    QF_UFLRA
    QF_LRA

Loading

Regarding the encoding of the promotion rules, maybe we can prepare a list of promotion rules. An initial attempt that needs further refinement is shown below:

QF-IDL -> {QF-LIA, QF_UFLIA} -> {QF-NIA, LIA}
QF-RDL -> {QF-RIA, QF_ULRA} -> {Q-LRA, LRA}
QF-BV -> {QF-UFBV}

Please let me know your thoughts and feedback. Thank you!