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

Safe Haskell	None

Language.Fixpoint.Config

Documentation

data Config Source

Constructors

Config
Fields inFile :: FilePath outFile :: FilePath solver :: SMTSolver genSorts :: GenQualifierSort

Instances

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

class Command a whereSource

Methods

command :: a -> String Source

Instances

Command SMTSolver
Command GenQualifierSort
Command Config

data SMTSolver Source

Constructors

Z3
Cvc4
Mathsat
Z3mem

Instances

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

newtype GenQualifierSort Source

Constructors

Instances

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

withTarget :: Config -> FilePath -> Config Source