Revision 163b81570ce2e07a5466ac0b578b0b95419f1117 authored by mkolosick on 16 November 2019, 17:37:16 UTC, committed by mkolosick on 16 November 2019, 17:37:16 UTC
1 parent d4c6f6f
Fixpoint.hs
import Language.Fixpoint.Solver (solveFQ)
import Language.Fixpoint.Horn.Solve (solveHorn)
import qualified Language.Fixpoint.Misc as Misc
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Types.Config as F
import qualified Language.Fixpoint.Utils.Files as F
import System.Exit
import qualified Control.Exception as Ex
main :: IO ()
main = do
cfg <- F.getOpts
Misc.writeLoud ("Options: " ++ show cfg)
e <- solveQuery cfg
exitWith e
---------------------------------------------------------------------------
solveQuery :: F.Config -> IO ExitCode
solveQuery cfg = solver cfg `Ex.catch` errorExit
where
solver
| isHorn cfg = solveHorn
| otherwise = solveFQ
isHorn :: F.Config -> Bool
isHorn = F.isExtFile F.Smt2 . F.srcFile
errorExit :: F.Error -> IO ExitCode
errorExit e = do
Misc.colorStrLn Misc.Sad ("Oops, unexpected error: " ++ F.showpp e)
return (ExitFailure 2)
Computing file changes ...