liquid-fixpoint-0.8.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 # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

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

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

Data Config Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

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 # 
Instance details

Defined in Language.Fixpoint.Types.Config

Generic Config Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Associated Types

type Rep Config :: Type -> Type #

Methods

from :: Config -> Rep Config x #

to :: Rep Config x -> Config #

Default Config Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

def :: Config #

type Rep Config Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

type Rep Config = D1 (MetaData "Config" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "Config" PrefixI True) (((((S1 (MetaSel (Just "srcFile") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath) :*: S1 (MetaSel (Just "cores") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int))) :*: (S1 (MetaSel (Just "minPartSize") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int) :*: S1 (MetaSel (Just "maxPartSize") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) :*: ((S1 (MetaSel (Just "solver") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SMTSolver) :*: S1 (MetaSel (Just "linear") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :*: (S1 (MetaSel (Just "stringTheory") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: (S1 (MetaSel (Just "defunction") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "allowHO") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))) :*: (((S1 (MetaSel (Just "allowHOqs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "eliminate") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Eliminate)) :*: (S1 (MetaSel (Just "elimBound") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)) :*: S1 (MetaSel (Just "smtTimeout") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)))) :*: ((S1 (MetaSel (Just "elimStats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "solverStats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :*: (S1 (MetaSel (Just "metadata") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: (S1 (MetaSel (Just "stats") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "parts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))))) :*: ((((S1 (MetaSel (Just "save") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "minimize") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :*: (S1 (MetaSel (Just "minimizeQs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "minimizeKs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) :*: ((S1 (MetaSel (Just "minimalSol") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "etaElim") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :*: (S1 (MetaSel (Just "gradual") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: (S1 (MetaSel (Just "ginteractive") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "autoKuts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))) :*: (((S1 (MetaSel (Just "nonLinCuts") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "noslice") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) :*: (S1 (MetaSel (Just "rewriteAxioms") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "oldPLE") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) :*: ((S1 (MetaSel (Just "noIncrPle") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: S1 (MetaSel (Just "checkCstr") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Integer])) :*: (S1 (MetaSel (Just "extensionality") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool) :*: (S1 (MetaSel (Just "maxRWOrderingConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)) :*: S1 (MetaSel (Just "rwTerminationCheck") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))))))))

SMT Solver options

data SMTSolver Source #

Constructors

Z3 
Cvc4 
Mathsat 
Instances
Eq SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Data SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

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 # 
Instance details

Defined in Language.Fixpoint.Types.Config

Generic SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Associated Types

type Rep SMTSolver :: Type -> Type #

Binary SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Default SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

def :: SMTSolver #

NFData SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: SMTSolver -> () #

type Rep SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

type Rep SMTSolver = D1 (MetaData "SMTSolver" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "Z3" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Cvc4" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Mathsat" PrefixI False) (U1 :: Type -> Type)))

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 Horn = eliminate kvars using the Horn solver Existentials = eliminate kvars and existentials

Constructors

None 
Some 
All 
Horn 
Existentials 
Instances
Eq Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Data Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

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 # 
Instance details

Defined in Language.Fixpoint.Types.Config

Generic Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Associated Types

type Rep Eliminate :: Type -> Type #

Binary Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Serialize Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Default Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

def :: Eliminate #

NFData Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: Eliminate -> () #

type Rep Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

type Rep Eliminate = D1 (MetaData "Eliminate" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) ((C1 (MetaCons "None" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Some" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "All" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Horn" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Existentials" PrefixI False) (U1 :: Type -> Type))))

parallel solving options

defaultMinPartSize :: Int Source #

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