module Language.Fixpoint.Config (
Config (..)
, getOpts
, Command (..)
, SMTSolver (..)
, GenQualifierSort (..)
, UeqAllSorts (..)
, withTarget
, withUEqAllSorts
) where
import System.Console.CmdArgs
import System.Console.CmdArgs.Verbosity (whenLoud)
import Data.Generics (Data)
import Data.Typeable (Typeable)
import Language.Fixpoint.Files
import System.Console.CmdArgs.Default
import System.FilePath
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
, srcFile :: FilePath
, solver :: SMTSolver
, genSorts :: GenQualifierSort
, ueqAllSorts :: UeqAllSorts
, native :: Bool
, real :: Bool
, eliminate :: Bool
} deriving (Eq,Data,Typeable,Show)
instance Default Config where
def = Config "" def def def def def def def def
instance Command Config where
command c = command (genSorts c)
++ command (ueqAllSorts 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"
newtype UeqAllSorts = UAS Bool
deriving (Eq, Data,Typeable,Show)
instance Default UeqAllSorts where
def = UAS False
instance Command UeqAllSorts where
command (UAS True) = " -ueq-all-sorts "
command (UAS False) = ""
withUEqAllSorts c b = c { ueqAllSorts = UAS b }
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
config = Config {
inFile = def &= typ "TARGET" &= args &= typFile
, outFile = "out" &= help "Output file"
, srcFile = def &= help "Source File from which FQ is generated"
, solver = def &= help "Name of SMT Solver"
, genSorts = def &= help "Generalize qualifier sorts"
, ueqAllSorts = def &= help "use UEq on all sorts"
, native = False &= help "(alpha) Haskell Solver"
, real = False &= help "(alpha) Theory of real numbers"
, eliminate = False &= help "(alpha) Eliminate non-cut KVars"
}
&= verbosity
&= program "fixpoint"
&= help "Predicate Abstraction Based Horn-Clause Solver"
&= summary "fixpoint Copyright 2009-13 Regents of the University of California."
&= details [ "Predicate Abstraction Based Horn-Clause Solver"
, ""
, "To check a file foo.fq type:"
, " fixpoint foo.fq"
]
getOpts :: IO Config
getOpts = do md <- cmdArgs config
putStrLn $ banner md
return md
banner args = "Liquid-Fixpoint Copyright 2009-13 Regents of the University of California.\n"
++ "All Rights Reserved.\n"