module Language.Fixpoint.Config (
Config (..)
, Command (..)
, SMTSolver (..)
, GenQualifierSort (..)
, withTarget
) where
import Language.Fixpoint.Files
import System.FilePath
import System.Console.CmdArgs.Default
import Data.Typeable (Typeable)
import Data.Generics (Data)
class Command a where
command :: a -> String
withTarget :: Config -> FilePath -> Config
withTarget cfg fq = cfg { inFile = fq } { outFile = fq `withExt` Out }
data Config
= Config {
inFile :: FilePath
, outFile :: FilePath
, solver :: SMTSolver
, genSorts :: GenQualifierSort
} deriving (Eq,Data,Typeable,Show)
instance Default Config where
def = Config "" def def def
instance Command Config where
command c = command (genSorts c)
++ command (solver c)
++ " -out "
++ (outFile c) ++ " " ++ (inFile c)
newtype GenQualifierSort = GQS Bool
deriving (Eq, Data,Typeable,Show)
instance Default GenQualifierSort where
def = GQS False
instance Command GenQualifierSort where
command (GQS True) = ""
command (GQS False) = "-no-gen-qual-sorts"
data SMTSolver = Z3 | Cvc4 | Mathsat | Z3mem
deriving (Eq,Data,Typeable)
instance Command SMTSolver where
command s = " -smtsolver " ++ show s
instance Default SMTSolver where
def = Z3
instance Show SMTSolver where
show Z3 = "z3"
show Cvc4 = "cvc4"
show Mathsat = "mathsat"
show Z3mem = "z3mem"
smtSolver "z3" = Z3
smtSolver "cvc4" = Cvc4
smtSolver "mathsat" = Mathsat
smtSolver "z3mem" = Z3mem
smtSolver other = error $ "ERROR: unsupported SMT Solver = " ++ other