Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Config

Contents

SMT Solver options
Eliminate options
Scrape options
parallel solving options

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
- scrape :: Scrape
- 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
- etabeta :: Bool
- localRewrites :: 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
- noSmtHorn :: Bool
}
defConfig :: Config
withPragmas :: Config -> [String] -> IO Config
getOpts :: IO Config
data SMTSolver
- = Z3
- | Z3mem
- | Cvc4
- | Cvc5
- | Mathsat
solverFlags :: SMTSolver -> ElabFlags
newtype ElabFlags = ElabFlags {
- elabSetBag :: Bool
}
data RESTOrdering
- = RESTKBO
- | RESTLPO
- | RESTRPO
- | RESTFuel Int
restOC :: Config -> RESTOrdering
data Eliminate
- = None
- | Some
- | All
- | Horn
- | Existentials
useElim :: Config -> Bool
data Scrape
- = No
- | Head
- | Both
defaultMinPartSize :: Int
defaultMaxPartSize :: Int
multicore :: Config -> Bool
queryFile :: Ext -> Config -> FilePath

Documentation

data Config Source #

Constructors

Config

Fields

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
scrape :: Scrape
configure auto-scraping of qualifiers from constraints
elimBound :: Maybe Int
maximum length of KVar chain to eliminate
smtTimeout :: Maybe Int
smt timeout in msec
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
etaElim :: Bool
eta eliminate function definitions
gradual :: Bool
solve "gradual" constraints
ginteractive :: Bool
interactive gradual solving
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
pleWithUndecidedGuards :: Bool
Unfold invocations with undecided guards in PLE
etabeta :: Bool
Eta expand and beta reduce terms to aid PLE
localRewrites :: Bool
Eta expand and beta reduce terms to aid PLE
interpreter :: Bool
Do not use the interpreter to assist PLE
oldPLE :: Bool
Use old version of PLE
noIncrPle :: Bool
Use incremental PLE
noEnvironmentReduction :: Bool
Don't use environment reduction
inlineANFBindings :: Bool
Inline ANF bindings. Sometimes improves performance and sometimes worsens it.
checkCstr :: [Integer]
Only check these specific constraints
extensionality :: Bool
Enable extensional interpretation of function equality
rwTerminationCheck :: Bool
Enable termination checking for rewriting
stdin :: Bool
Read input query from stdin
json :: Bool
Render output in JSON format
noLazyPLE :: Bool
fuel :: Maybe Int
Maximum PLE "fuel" (unfold depth) (default=infinite)
restOrdering :: String
Term ordering for use in REST
noSmtHorn :: Bool
Do not use (new) SMTLIB horn parser

Instances

Instances details

Data Config Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Config -> c Config # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Config # toConstr :: Config -> Constr # dataTypeOf :: Config -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Config) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config) # gmapT :: (forall b. Data b => b -> b) -> Config -> Config # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r # gmapQ :: (forall d. Data d => d -> u) -> Config -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Config -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Config -> m Config # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Config -> m Config # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Config -> m Config #
Generic Config Source #
Instance details Defined in Language.Fixpoint.Types.Config Associated Types type Rep Config :: Type -> Type # Methods from :: Config -> Rep Config x # to :: Rep Config x -> Config #
Show Config Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> Config -> ShowS # show :: Config -> String # showList :: [Config] -> ShowS #
Default Config Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods def :: Config #
Eq Config Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods (==) :: Config -> Config -> Bool # (/=) :: Config -> Config -> Bool #
type Rep Config Source #
Instance details Defined in Language.Fixpoint.Types.Config type Rep Config = D1 ('MetaData "Config" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.3-1dn9W1nkW9y4chrgX9jmF4" 'False) (C1 ('MetaCons "Config" 'PrefixI 'True) (((((S1 ('MetaSel ('Just "srcFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :: (S1 ('MetaSel ('Just "cores") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: S1 ('MetaSel ('Just "minPartSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :: (S1 ('MetaSel ('Just "maxPartSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: (S1 ('MetaSel ('Just "solver") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SMTSolver) :: S1 ('MetaSel ('Just "linear") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :: ((S1 ('MetaSel ('Just "stringTheory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "defunction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "allowHO") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: (S1 ('MetaSel ('Just "allowHOqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "eliminate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Eliminate) :: S1 ('MetaSel ('Just "scrape") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Scrape))))) :: (((S1 ('MetaSel ('Just "elimBound") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: (S1 ('MetaSel ('Just "smtTimeout") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: S1 ('MetaSel ('Just "elimStats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: (S1 ('MetaSel ('Just "solverStats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "metadata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "stats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :: ((S1 ('MetaSel ('Just "parts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "save") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "minimize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: (S1 ('MetaSel ('Just "minimizeQs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "minimizeKs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "minimalSol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))) :: ((((S1 ('MetaSel ('Just "etaElim") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "gradual") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "ginteractive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: (S1 ('MetaSel ('Just "autoKuts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "nonLinCuts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "noslice") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :: ((S1 ('MetaSel ('Just "rewriteAxioms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "pleWithUndecidedGuards") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "etabeta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: (S1 ('MetaSel ('Just "localRewrites") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "interpreter") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "oldPLE") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :: (((S1 ('MetaSel ('Just "noIncrPle") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "noEnvironmentReduction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "inlineANFBindings") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: (S1 ('MetaSel ('Just "checkCstr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Integer]) :: (S1 ('MetaSel ('Just "extensionality") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "rwTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :: ((S1 ('MetaSel ('Just "stdin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "json") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "noLazyPLE") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: (S1 ('MetaSel ('Just "fuel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: (S1 ('MetaSel ('Just "restOrdering") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "noSmtHorn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))))))

defConfig :: Config Source #

withPragmas :: Config -> [String] -> IO Config Source #

getOpts :: IO Config Source #

SMT Solver options

data SMTSolver Source #

Constructors

Z3
Z3mem
Cvc4
Cvc5
Mathsat

Instances

Instances details

Data SMTSolver Source #
Instance details 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 #
Instance details Defined in Language.Fixpoint.Types.Config Associated Types type Rep SMTSolver :: Type -> Type # Methods from :: SMTSolver -> Rep SMTSolver x # to :: Rep SMTSolver x -> SMTSolver #
Show SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> SMTSolver -> ShowS # show :: SMTSolver -> String # showList :: [SMTSolver] -> ShowS #
Default SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods def :: SMTSolver #
NFData SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods rnf :: SMTSolver -> () #
Eq SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods (==) :: SMTSolver -> SMTSolver -> Bool # (/=) :: SMTSolver -> SMTSolver -> Bool #
TheorySymbols SMTSolver Source #	Theory Symbols : `uninterpSEnv` should be disjoint from see `interpSEnv` to avoid duplicate SMT definitions. `uninterpSEnv` is for uninterpreted symbols, and `interpSEnv` is for interpreted symbols.
Instance details Defined in Language.Fixpoint.Smt.Theories Methods theorySymbols :: SMTSolver -> SEnv TheorySymbol Source #
Store SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods size :: Size SMTSolver # poke :: SMTSolver -> Poke () # peek :: Peek SMTSolver #
type Rep SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config type Rep SMTSolver = D1 ('MetaData "SMTSolver" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.3-1dn9W1nkW9y4chrgX9jmF4" 'False) ((C1 ('MetaCons "Z3" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Z3mem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Cvc4" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Cvc5" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Mathsat" 'PrefixI 'False) (U1 :: Type -> Type))))

solverFlags :: SMTSolver -> ElabFlags Source #

newtype ElabFlags Source #

Constructors

ElabFlags
Fields elabSetBag :: Bool

data RESTOrdering Source #

Constructors

RESTKBO
RESTLPO
RESTRPO
RESTFuel Int

Instances

Instances details

Data RESTOrdering Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RESTOrdering -> c RESTOrdering # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RESTOrdering # toConstr :: RESTOrdering -> Constr # dataTypeOf :: RESTOrdering -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RESTOrdering) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RESTOrdering) # gmapT :: (forall b. Data b => b -> b) -> RESTOrdering -> RESTOrdering # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r # gmapQ :: (forall d. Data d => d -> u) -> RESTOrdering -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RESTOrdering -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering #
Generic RESTOrdering Source #
Instance details Defined in Language.Fixpoint.Types.Config Associated Types type Rep RESTOrdering :: Type -> Type # Methods from :: RESTOrdering -> Rep RESTOrdering x # to :: Rep RESTOrdering x -> RESTOrdering #
Read RESTOrdering Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods readsPrec :: Int -> ReadS RESTOrdering # readList :: ReadS [RESTOrdering] # readPrec :: ReadPrec RESTOrdering # readListPrec :: ReadPrec [RESTOrdering] #
Show RESTOrdering Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> RESTOrdering -> ShowS # show :: RESTOrdering -> String # showList :: [RESTOrdering] -> ShowS #
Default RESTOrdering Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods def :: RESTOrdering #
Eq RESTOrdering Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods (==) :: RESTOrdering -> RESTOrdering -> Bool # (/=) :: RESTOrdering -> RESTOrdering -> Bool #
type Rep RESTOrdering Source #
Instance details Defined in Language.Fixpoint.Types.Config type Rep RESTOrdering = D1 ('MetaData "RESTOrdering" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.3-1dn9W1nkW9y4chrgX9jmF4" 'False) ((C1 ('MetaCons "RESTKBO" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RESTLPO" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RESTRPO" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RESTFuel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))

restOC :: Config -> RESTOrdering Source #

Eliminate options

data Eliminate Source #

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

Instances details

Data Eliminate Source #
Instance details 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 #
Instance details Defined in Language.Fixpoint.Types.Config Associated Types type Rep Eliminate :: Type -> Type # Methods from :: Eliminate -> Rep Eliminate x # to :: Rep Eliminate x -> Eliminate #
Show Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> Eliminate -> ShowS # show :: Eliminate -> String # showList :: [Eliminate] -> ShowS #
Serialize Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods put :: Putter Eliminate # get :: Get Eliminate #
Default Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods def :: Eliminate #
NFData Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods rnf :: Eliminate -> () #
Eq Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods (==) :: Eliminate -> Eliminate -> Bool # (/=) :: Eliminate -> Eliminate -> Bool #
Store Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods size :: Size Eliminate # poke :: Eliminate -> Poke () # peek :: Peek Eliminate #
type Rep Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config type Rep Eliminate = D1 ('MetaData "Eliminate" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.3-1dn9W1nkW9y4chrgX9jmF4" '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))))

useElim :: Config -> Bool Source #

Scrape options

data Scrape Source #

Scrape describes which (Horn) constraints to scrape qualifiers from None = do not scrape, only use the supplied qualifiers Head = scrape only from the constraint heads (i.e. "rhs") All = scrape all concrete predicates (i.e. "rhs" + "lhs")

Constructors

No
Head
Both

Instances

Instances details

Data Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Scrape -> c Scrape # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Scrape # toConstr :: Scrape -> Constr # dataTypeOf :: Scrape -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Scrape) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scrape) # gmapT :: (forall b. Data b => b -> b) -> Scrape -> Scrape # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r # gmapQ :: (forall d. Data d => d -> u) -> Scrape -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Scrape -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scrape -> m Scrape # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scrape -> m Scrape # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scrape -> m Scrape #
Generic Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Associated Types type Rep Scrape :: Type -> Type # Methods from :: Scrape -> Rep Scrape x # to :: Rep Scrape x -> Scrape #
Show Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> Scrape -> ShowS # show :: Scrape -> String # showList :: [Scrape] -> ShowS #
Serialize Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods put :: Putter Scrape # get :: Get Scrape #
Default Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods def :: Scrape #
NFData Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods rnf :: Scrape -> () #
Eq Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods (==) :: Scrape -> Scrape -> Bool # (/=) :: Scrape -> Scrape -> Bool #
Store Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods size :: Size Scrape # poke :: Scrape -> Poke () # peek :: Peek Scrape #
type Rep Scrape Source #
Instance details Defined in Language.Fixpoint.Types.Config type Rep Scrape = D1 ('MetaData "Scrape" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.3-1dn9W1nkW9y4chrgX9jmF4" 'False) (C1 ('MetaCons "No" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Head" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Both" 'PrefixI 'False) (U1 :: Type -> Type)))

parallel solving options

defaultMinPartSize :: Int Source #

Configuration Options -----------------------------------------------------

defaultMaxPartSize :: Int Source #

multicore :: Config -> Bool Source #

queryFile :: Ext -> Config -> FilePath Source #