Documentation

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