Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Config

Documentation

Constructors

Fields

inFile :: FilePath: target fq-file
outFile :: FilePath: output file
srcFile :: FilePath: src file (*.hs, *.ts, *.c)
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
genSorts :: GenQualifierSort: generalize qualifier sorts
ueqAllSorts :: UeqAllSorts: use UEq on all sorts
linear :: Bool: not interpret div and mul in SMT
allowHO :: Bool: not interpret div and mul in SMT
newcheck :: Bool: new fixpoint sort check
eliminate :: Bool: eliminate non-cut KVars
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: use delta debug to min fq file , nontriv :: Bool -- ^ simplify using non-trivial sorts
gradual :: Bool: solve "gradual" constraints

Instances

class Command a where Source

Methods

Instances

Command SMTSolver Source
Command UeqAllSorts Source
Command GenQualifierSort Source
Command Config Source

Constructors

Instances

Constructors

Instances

Eq GenQualifierSort Source
Data GenQualifierSort Source
Show GenQualifierSort Source
Default GenQualifierSort Source
Command GenQualifierSort Source

Constructors

Instances