You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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 aninfer_logic
function that figures out the appropriate type.The text was updated successfully, but these errors were encountered: