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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Config

Documentation

data Config Source

Constructors

Config 

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