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

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Config

Documentation

data Config Source

Constructors

Config
Fields inFile :: FilePath outFile :: FilePath solver :: SMTSolver genSorts :: GenQualifierSort ueqAllSorts :: UeqAllSorts native :: Bool real :: Bool

Instances

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

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

withUEqAllSorts :: Config -> Bool -> Config Source