liquid-fixpoint-0.4.0.0: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Config

Documentation

data Config Source

Constructors

Fields

inFile :: FilePath: target fq-file
outFile :: FilePath: output file
srcFile :: FilePath: src file (*.hs, *.ts, *.c)
solver :: SMTSolver: which SMT solver to use
genSorts :: GenQualifierSort: generalize qualifier sorts
ueqAllSorts :: UeqAllSorts: use UEq on all sorts
native :: Bool: use haskell solver
real :: Bool: interpret div and mul in SMT
eliminate :: Bool: eliminate non-cut KVars
metadata :: Bool: print meta-data associated with constraints
stats :: Bool: compute constraint statistics
parts :: Bool: partition FInfo into separate fq files

Instances

Eq Config
Data Config
Show Config
Default Config
Command Config
Typeable * Config

getOpts :: IO Config Source

class Command a where Source

Methods

command :: a -> String Source

Instances

Command SMTSolver
Command UeqAllSorts
Command GenQualifierSort
Command Config

data SMTSolver Source

Constructors

Z3
Cvc4
Mathsat
Z3mem

Instances

Eq SMTSolver
Data SMTSolver
Show SMTSolver
Default SMTSolver
Command SMTSolver
Typeable * SMTSolver

newtype GenQualifierSort Source

Constructors

Instances

Eq GenQualifierSort
Data GenQualifierSort
Show GenQualifierSort
Default GenQualifierSort
Command GenQualifierSort
Typeable * GenQualifierSort

newtype UeqAllSorts Source

Constructors

Instances

Eq UeqAllSorts
Data UeqAllSorts
Show UeqAllSorts
Default UeqAllSorts
Command UeqAllSorts
Typeable * UeqAllSorts

withTarget :: Config -> FilePath -> Config Source