| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Config
Synopsis
- 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
- smtTimeout :: Maybe Int
- elimStats :: Bool
- solverStats :: Bool
- metadata :: Bool
- stats :: Bool
- parts :: Bool
- save :: Bool
- minimize :: Bool
- minimizeQs :: Bool
- minimizeKs :: Bool
- minimalSol :: Bool
- etaElim :: Bool
- gradual :: Bool
- ginteractive :: Bool
- autoKuts :: Bool
- nonLinCuts :: Bool
- noslice :: Bool
- rewriteAxioms :: Bool
- pleWithUndecidedGuards :: Bool
- interpreter :: Bool
- oldPLE :: Bool
- noIncrPle :: Bool
- noEnvironmentReduction :: Bool
- inlineANFBindings :: Bool
- checkCstr :: [Integer]
- extensionality :: Bool
- rwTerminationCheck :: Bool
- stdin :: Bool
- json :: Bool
- noLazyPLE :: Bool
- fuel :: Maybe Int
- restOrdering :: String
- defConfig :: Config
- withPragmas :: Config -> [String] -> IO Config
- getOpts :: IO Config
- data SMTSolver
- data RESTOrdering
- restOC :: Config -> RESTOrdering
- data Eliminate
- = None
- | Some
- | All
- | Horn
- | Existentials
- useElim :: Config -> Bool
- defaultMinPartSize :: Int
- defaultMaxPartSize :: Int
- multicore :: Config -> Bool
- queryFile :: Ext -> Config -> FilePath
Documentation
Constructors
| Config | |
Fields
| |
Instances
SMT Solver options
Instances
| Data SMTSolver Source # | |
Defined in Language.Fixpoint.Types.Config Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SMTSolver -> c SMTSolver # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SMTSolver # toConstr :: SMTSolver -> Constr # dataTypeOf :: SMTSolver -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SMTSolver) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTSolver) # gmapT :: (forall b. Data b => b -> b) -> SMTSolver -> SMTSolver # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SMTSolver -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SMTSolver -> r # gmapQ :: (forall d. Data d => d -> u) -> SMTSolver -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SMTSolver -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver # | |
| Generic SMTSolver Source # | |
| Show SMTSolver Source # | |
| Default SMTSolver Source # | |
Defined in Language.Fixpoint.Types.Config | |
| NFData SMTSolver Source # | |
Defined in Language.Fixpoint.Types.Config | |
| Eq SMTSolver Source # | |
| Store SMTSolver Source # | |
| type Rep SMTSolver Source # | |
Defined in Language.Fixpoint.Types.Config type Rep SMTSolver = D1 ('MetaData "SMTSolver" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.0.2.1-GsxNcg91pufGtKM5ikXQaF" 'False) (C1 ('MetaCons "Z3" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Cvc4" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Mathsat" 'PrefixI 'False) (U1 :: Type -> Type))) | |
data RESTOrdering Source #
Instances
restOC :: Config -> RESTOrdering Source #
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 Horn = eliminate kvars using the Horn solver Existentials = eliminate kvars and existentials
Constructors
| None | |
| Some | |
| All | |
| Horn | |
| Existentials |
Instances
| Data Eliminate Source # | |
Defined in Language.Fixpoint.Types.Config Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Eliminate -> c Eliminate # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Eliminate # toConstr :: Eliminate -> Constr # dataTypeOf :: Eliminate -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Eliminate) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Eliminate) # gmapT :: (forall b. Data b => b -> b) -> Eliminate -> Eliminate # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Eliminate -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Eliminate -> r # gmapQ :: (forall d. Data d => d -> u) -> Eliminate -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Eliminate -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Eliminate -> m Eliminate # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Eliminate -> m Eliminate # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Eliminate -> m Eliminate # | |
| Generic Eliminate Source # | |
| Show Eliminate Source # | |
| Serialize Eliminate Source # | |
| Default Eliminate Source # | |
Defined in Language.Fixpoint.Types.Config | |
| NFData Eliminate Source # | |
Defined in Language.Fixpoint.Types.Config | |
| Eq Eliminate Source # | |
| Store Eliminate Source # | |
| type Rep Eliminate Source # | |
Defined in Language.Fixpoint.Types.Config type Rep Eliminate = D1 ('MetaData "Eliminate" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.0.2.1-GsxNcg91pufGtKM5ikXQaF" 'False) ((C1 ('MetaCons "None" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Some" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "All" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Horn" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Existentials" 'PrefixI 'False) (U1 :: Type -> Type)))) | |
parallel solving options
defaultMinPartSize :: Int Source #
Configuration Options -----------------------------------------------------