Safe Haskell	None
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
- 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
- autoKuts :: Bool
- nonLinCuts :: Bool
- noslice :: Bool
- rewriteAxioms :: Bool
- pleUndecGuards :: Bool
- etabeta :: Bool
- localRewrites :: Bool
- interpreter :: Bool
- noEnvReduction :: Bool
- inlineANFBinds :: Bool
- checkCstr :: [Integer]
- extensionality :: Bool
- rwTermination :: Bool
- stdin :: Bool
- json :: Bool
- fuel :: Maybe Int
- restOrdering :: String
- noSmtHorn :: Bool
- noStringTheory :: Bool
- explicitKvars :: Bool
}
defConfig :: Config
withPragmas :: Config -> [String] -> IO Config
getOpts :: IO Config
data SMTSolver
- = Z3
- | Z3mem
- | Cvc4
- | Cvc5
- | Mathsat
solverFlags :: Config -> ElabFlags
mkElabFlags :: SMTSolver -> Bool -> ElabFlags
data ElabFlags = ElabFlags {
- elabSetBag :: Bool
- elabExplicitKvars :: 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
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
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
pleUndecGuards :: 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
noEnvReduction :: Bool
Don't use environment reduction
inlineANFBinds :: 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
rwTermination :: Bool
Enable termination checking for rewriting
stdin :: Bool
Read input query from stdin
json :: Bool
Render output in JSON format
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
noStringTheory :: Bool
disable interpretation of string theory by SMT
explicitKvars :: Bool
use explicitly declared kvars (horn style) which disables several "defensive simplifications"

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

Instance details

Defined in Language.Fixpoint.Types.Config

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

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

Instance details

Defined in Language.Fixpoint.Types.Config

type Rep SMTSolver = D1 ('MetaData "SMTSolver" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

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.4-CmH5CYTDh7gFBJNG3w2uNw" '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 :: Config -> ElabFlags Source #

mkElabFlags :: SMTSolver -> Bool -> ElabFlags Source #

data ElabFlags Source #

Constructors

ElabFlags
Fields elabSetBag :: Bool elabExplicitKvars :: 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

Instance details

Defined in Language.Fixpoint.Types.Config

type Rep RESTOrdering = D1 ('MetaData "RESTOrdering" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

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.4-CmH5CYTDh7gFBJNG3w2uNw" '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

Instance details

Defined in Language.Fixpoint.Types.Config

type Rep Eliminate = D1 ('MetaData "Eliminate" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

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.4-CmH5CYTDh7gFBJNG3w2uNw" '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 No = do not scrape, only use the supplied qualifiers Head = scrape only from the constraint heads (i.e. "rhs") Both = 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
Instance details Defined in Language.Fixpoint.Types.Config type Rep Scrape = D1 ('MetaData "Scrape" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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)))

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.4-CmH5CYTDh7gFBJNG3w2uNw" '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 #