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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Config

Contents

Synopsis

Documentation

data Config Source #

Constructors

Config 

Fields

Instances

Eq Config Source # 

Methods

(==) :: Config -> Config -> Bool #

(/=) :: Config -> Config -> Bool #

Data Config Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Config -> c Config #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Config #

toConstr :: Config -> Constr #

dataTypeOf :: Config -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Config) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config) #

gmapT :: (forall b. Data b => b -> b) -> Config -> Config #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r #

gmapQ :: (forall d. Data d => d -> u) -> Config -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Config -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Config -> m Config #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Config -> m Config #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Config -> m Config #

Show Config Source # 
Generic Config Source # 

Associated Types

type Rep Config :: * -> * #

Methods

from :: Config -> Rep Config x #

to :: Rep Config x -> Config #

Default Config Source # 

Methods

def :: Config #

type Rep Config Source # 
type Rep Config = D1 (MetaData "Config" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "Config" PrefixI True) ((:*:) ((:*:) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "srcFile") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath)) (S1 (MetaSel (Just Symbol "cores") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)))) ((:*:) (S1 (MetaSel (Just Symbol "minPartSize") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Just Symbol "maxPartSize") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "solver") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SMTSolver)) (S1 (MetaSel (Just Symbol "linear") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "stringTheory") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "defunction") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "allowHO") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "allowHOqs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "eliminate") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Eliminate)) (S1 (MetaSel (Just Symbol "elimBound") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int))))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "elimStats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "solverStats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "metadata") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "stats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))))) ((:*:) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "parts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "save") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "minimize") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "minimizeQs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "minimizeKs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "minimalSol") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "gradual") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "ginteractive") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "extensionality") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "alphaEquivalence") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "betaEquivalence") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "normalForm") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "autoKuts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "nonLinCuts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "noslice") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) ((:*:) (S1 (MetaSel (Just Symbol "rewriteAxioms") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "arithmeticAxioms") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))))))))

SMT Solver options

data SMTSolver Source #

Constructors

Z3 
Cvc4 
Mathsat 

Instances

Eq SMTSolver Source # 
Data SMTSolver Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SMTSolver -> c SMTSolver #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SMTSolver #

toConstr :: SMTSolver -> Constr #

dataTypeOf :: SMTSolver -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SMTSolver) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTSolver) #

gmapT :: (forall b. Data b => b -> b) -> SMTSolver -> SMTSolver #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SMTSolver -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SMTSolver -> r #

gmapQ :: (forall d. Data d => d -> u) -> SMTSolver -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SMTSolver -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver #

Show SMTSolver Source # 
Generic SMTSolver Source # 

Associated Types

type Rep SMTSolver :: * -> * #

Default SMTSolver Source # 

Methods

def :: SMTSolver #

type Rep SMTSolver Source # 
type Rep SMTSolver = D1 (MetaData "SMTSolver" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) ((:+:) (C1 (MetaCons "Z3" PrefixI False) U1) ((:+:) (C1 (MetaCons "Cvc4" PrefixI False) U1) (C1 (MetaCons "Mathsat" PrefixI False) U1)))

Eliminate options

data Eliminate Source #

Eliminate describes the number of KVars to eliminate: None = use PA/Quals for ALL k-vars, i.e. no eliminate Some = use PA/Quals for CUT k-vars, i.e. eliminate non-cuts All = eliminate ALL k-vars, solve cut-vars to TRUE

Constructors

None 
Some 
All 

Instances

Eq Eliminate Source # 
Data Eliminate Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Eliminate -> c Eliminate #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Eliminate #

toConstr :: Eliminate -> Constr #

dataTypeOf :: Eliminate -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Eliminate) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Eliminate) #

gmapT :: (forall b. Data b => b -> b) -> Eliminate -> Eliminate #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Eliminate -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Eliminate -> r #

gmapQ :: (forall d. Data d => d -> u) -> Eliminate -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Eliminate -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Eliminate -> m Eliminate #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Eliminate -> m Eliminate #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Eliminate -> m Eliminate #

Show Eliminate Source # 
Generic Eliminate Source # 

Associated Types

type Rep Eliminate :: * -> * #

Serialize Eliminate Source # 
Default Eliminate Source # 

Methods

def :: Eliminate #

type Rep Eliminate Source # 
type Rep Eliminate = D1 (MetaData "Eliminate" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) ((:+:) (C1 (MetaCons "None" PrefixI False) U1) ((:+:) (C1 (MetaCons "Some" PrefixI False) U1) (C1 (MetaCons "All" PrefixI False) U1)))

parallel solving options

defaultMinPartSize :: Int Source #

Configuration Options -----------------------------------------------------