{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DeriveGeneric #-} module Language.Fixpoint.Types.Config ( Config (..) , defConfig , withPragmas , getOpts -- * SMT Solver options , SMTSolver (..) -- * Eliminate options , Eliminate (..) , useElim -- * parallel solving options , defaultMinPartSize , defaultMaxPartSize , multicore , queryFile ) where import Data.Serialize (Serialize (..)) import Control.Monad import GHC.Generics import System.Console.CmdArgs import System.Console.CmdArgs.Explicit import System.Environment import Language.Fixpoint.Utils.Files -------------------------------------------------------------------------------- withPragmas :: Config -> [String] -> IO Config -------------------------------------------------------------------------------- withPragmas = foldM withPragma withPragma :: Config -> String -> IO Config withPragma c s = withArgs [s] $ cmdArgsRun config { modeValue = (modeValue config) { cmdArgsValue = c } } -------------------------------------------------------------------------------- -- | Configuration Options ----------------------------------------------------- -------------------------------------------------------------------------------- defaultMinPartSize :: Int defaultMinPartSize = 500 defaultMaxPartSize :: Int defaultMaxPartSize = 700 data Config = Config { srcFile :: FilePath -- ^ src file (*.hs, *.ts, *.c, or even *.fq or *.bfq) , cores :: Maybe Int -- ^ number of cores used to solve constraints , minPartSize :: Int -- ^ Minimum size of a partition , maxPartSize :: Int -- ^ Maximum size of a partition. Overrides minPartSize , solver :: SMTSolver -- ^ which SMT solver to use , linear :: Bool -- ^ not interpret div and mul in SMT , stringTheory :: Bool -- ^ interpretation of string theory by SMT , defunction :: Bool -- ^ defunctionalize (use 'apply' for all uninterpreted applications) , allowHO :: Bool -- ^ allow higher order binders in the logic environment , allowHOqs :: Bool -- ^ allow higher order qualifiers , eliminate :: Eliminate -- ^ eliminate non-cut KVars , elimBound :: Maybe Int -- ^ maximum length of KVar chain to eliminate , elimStats :: Bool -- ^ print eliminate stats , solverStats :: Bool -- ^ print solver stats , metadata :: Bool -- ^ print meta-data associated with constraints , stats :: Bool -- ^ compute constraint statistics , parts :: Bool -- ^ partition FInfo into separate fq files , save :: Bool -- ^ save FInfo as .bfq and .fq file , minimize :: Bool -- ^ min .fq by delta debug (unsat with min constraints) , minimizeQs :: Bool -- ^ min .fq by delta debug (sat with min qualifiers) , minimizeKs :: Bool -- ^ min .fq by delta debug (sat with min kvars) , minimalSol :: Bool -- ^ shrink final solution by pruning redundant qualfiers from fixpoint , gradual :: Bool -- ^ solve "gradual" constraints , ginteractive :: Bool -- ^ interactive gradual solving , extensionality :: Bool -- ^ allow function extensionality , alphaEquivalence :: Bool -- ^ allow lambda alpha equivalence axioms , betaEquivalence :: Bool -- ^ allow lambda beta equivalence axioms , normalForm :: Bool -- ^ allow lambda normal-form equivalence axioms , autoKuts :: Bool -- ^ ignore given kut variables , nonLinCuts :: Bool -- ^ Treat non-linear vars as cuts , noslice :: Bool -- ^ Disable non-concrete KVar slicing , rewriteAxioms :: Bool -- ^ allow axiom instantiation via rewriting , arithmeticAxioms :: Bool -- ^ allow axiom instantiation on arithmetic expressions } deriving (Eq,Data,Typeable,Show,Generic) instance Default Config where def = defConfig --------------------------------------------------------------------------------------- data SMTSolver = Z3 | Cvc4 | Mathsat deriving (Eq, Data, Typeable, Generic) instance Default SMTSolver where def = Z3 instance Show SMTSolver where show Z3 = "z3" show Cvc4 = "cvc4" show Mathsat = "mathsat" --------------------------------------------------------------------------------------- -- | Eliminate describes the number of KVars to eliminate: -- None = use PA/Quals for ALL k-vars, i.e. no eliminate -- Some = use PA/Quals for CUT k-vars, i.e. eliminate non-cuts -- All = eliminate ALL k-vars, solve cut-vars to TRUE --------------------------------------------------------------------------------------- data Eliminate = None | Some | All deriving (Eq, Data, Typeable, Generic) instance Serialize Eliminate instance Default Eliminate where def = None instance Show Eliminate where show None = "none" show Some = "some" show All = "all" useElim :: Config -> Bool useElim cfg = eliminate cfg /= None --------------------------------------------------------------------------------------- defConfig :: Config defConfig = Config { srcFile = "out" &= args &= typFile , defunction = False &= help "Allow higher order binders into fixpoint environment" , solver = def &= help "Name of SMT Solver" , linear = False &= help "Use uninterpreted integer multiplication and division" , stringTheory = False &= help "Interpretation of String Theory by SMT" , allowHO = False &= help "Allow higher order binders into fixpoint environment" , allowHOqs = False &= help "Allow higher order qualifiers" , eliminate = None &= help "Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]" , elimBound = Nothing &= name "elimBound" &= help "(alpha) Maximum eliminate-chain depth" , elimStats = False &= help "(alpha) Print eliminate stats" , solverStats = False &= help "Print solver stats" , save = False &= help "Save Query as .fq and .bfq files" , metadata = False &= help "Print meta-data associated with constraints" , stats = False &= help "Compute constraint statistics" , parts = False &= help "Partition constraints into indepdendent .fq files" , cores = def &= help "(numeric) Number of threads to use" , minPartSize = defaultMinPartSize &= help "(numeric) Minimum partition size when solving in parallel" , maxPartSize = defaultMaxPartSize &= help "(numeric) Maximum partiton size when solving in parallel." , minimize = False &= help "Delta debug to minimize fq file (unsat with min constraints)" , minimizeQs = False &= help "Delta debug to minimize fq file (sat with min qualifiers)" , minimizeKs = False &= help "Delta debug to minimize fq file (sat with max kvars replaced by True)" , minimalSol = False &= help "Shrink fixpoint by removing implied qualifiers" , gradual = False &= help "Solve gradual-refinement typing constraints" , ginteractive = False &= help "Interactive Gradual Solving" , extensionality = False &= help "Allow function extensionality axioms" , alphaEquivalence = False &= help "Allow lambda alpha equivalence axioms" , betaEquivalence = False &= help "Allow lambda alpha equivalence axioms" , normalForm = False &= help "Allow lambda normal-form equivalence axioms" , autoKuts = False &= help "Ignore given Kut vars, compute from scratch" , nonLinCuts = False &= help "Treat non-linear kvars as cuts" , noslice = False &= help "Disable non-concrete KVar slicing" , rewriteAxioms = False &= help "allow axiom instantiation via rewriting" , arithmeticAxioms = False &= help "Disable non-concrete KVar slicing" } &= verbosity &= program "fixpoint" &= help "Predicate Abstraction Based Horn-Clause Solver" &= summary "fixpoint Copyright 2009-15 Regents of the University of California." &= details [ "Predicate Abstraction Based Horn-Clause Solver" , "" , "To check a file foo.fq type:" , " fixpoint foo.fq" ] config :: Mode (CmdArgs Config) config = cmdArgsMode defConfig getOpts :: IO Config getOpts = do md <- cmdArgs defConfig putStrLn banner return md banner :: String banner = "\n\nLiquid-Fixpoint Copyright 2013-15 Regents of the University of California.\n" ++ "All Rights Reserved.\n" multicore :: Config -> Bool multicore cfg = cores cfg /= Just 1 queryFile :: Ext -> Config -> FilePath queryFile e = extFileName e . srcFile