Infer logic type from expression
Opened this issue · 0 comments
elsoroka commented
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.