| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Config
- data Config = Config {
- srcFile :: FilePath
- cores :: Maybe Int
- minPartSize :: Int
- maxPartSize :: Int
- solver :: SMTSolver
- linear :: Bool
- stringTheory :: Bool
- defunction :: Bool
- allowHO :: Bool
- allowHOqs :: Bool
- eliminate :: Eliminate
- elimBound :: Maybe Int
- elimStats :: Bool
- solverStats :: Bool
- metadata :: Bool
- stats :: Bool
- parts :: Bool
- save :: Bool
- minimize :: Bool
- minimizeQs :: Bool
- minimizeKs :: Bool
- minimalSol :: Bool
- gradual :: Bool
- ginteractive :: Bool
- extensionality :: Bool
- alphaEquivalence :: Bool
- betaEquivalence :: Bool
- normalForm :: Bool
- autoKuts :: Bool
- nonLinCuts :: Bool
- noslice :: Bool
- rewriteAxioms :: Bool
- arithmeticAxioms :: Bool
- defConfig :: Config
- withPragmas :: Config -> [String] -> IO Config
- getOpts :: IO Config
- data SMTSolver
- data Eliminate
- useElim :: Config -> Bool
- defaultMinPartSize :: Int
- defaultMaxPartSize :: Int
- multicore :: Config -> Bool
- queryFile :: Ext -> Config -> FilePath
Documentation
Constructors
| Config | |
Fields
| |
SMT Solver options
Eliminate options
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
parallel solving options
defaultMinPartSize :: Int Source #
Configuration Options -----------------------------------------------------