Ersatz.Solver.Z3

Documentation

z3 :: MonadIO m => Solver SAT m

Solver for SAT problems that tries to invoke the z3 executable from the PATH

z3Path :: MonadIO m => FilePath -> Solver SAT m

Solver for SAT problems that tries to invoke a program that takes z3 compatible arguments.

The FilePath refers to the path to the executable.