liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Types.Config

Synopsis

Documentation

data Config Source #

Constructors

Config 

Fields

Instances

Instances details
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 :: forall r r'. (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 #

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 #

Show Config Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Default Config Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

def :: Config #

Eq Config Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

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

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

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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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 "scrape") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Scrape) :*: 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 "pleWithUndecidedGuards") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "interpreter") '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 "noEnvironmentReduction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: (S1 ('MetaSel ('Just "inlineANFBindings") '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 "rwTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "stdin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "json") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: (S1 ('MetaSel ('Just "noLazyPLE") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "fuel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :*: S1 ('MetaSel ('Just "restOrdering") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))))

SMT Solver options

data SMTSolver Source #

Constructors

Z3 
Z3mem 
Cvc4 
Mathsat 

Instances

Instances details
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 :: forall r r'. (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 #

Generic SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Associated Types

type Rep SMTSolver :: Type -> Type #

Show SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Default SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

def :: SMTSolver #

NFData SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

rnf :: SMTSolver -> () #

Eq SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Store SMTSolver Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) ((C1 ('MetaCons "Z3" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Z3mem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Cvc4" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Mathsat" 'PrefixI 'False) (U1 :: Type -> Type)))

data RESTOrdering Source #

Instances

Instances details
Data RESTOrdering 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) -> RESTOrdering -> c RESTOrdering #

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

toConstr :: RESTOrdering -> Constr #

dataTypeOf :: RESTOrdering -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic RESTOrdering Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Associated Types

type Rep RESTOrdering :: Type -> Type #

Read RESTOrdering Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Show RESTOrdering Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Default RESTOrdering Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

def :: RESTOrdering #

Eq RESTOrdering Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

type Rep RESTOrdering Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

type Rep RESTOrdering = D1 ('MetaData "RESTOrdering" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) ((C1 ('MetaCons "RESTKBO" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RESTLPO" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RESTRPO" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RESTFuel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))

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

Instances details
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 :: forall r r'. (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 #

Generic Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Associated Types

type Rep Eliminate :: Type -> Type #

Show Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

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.Config

Methods

rnf :: Eliminate -> () #

Eq Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Store Eliminate Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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))))

Scrape options

data Scrape Source #

Scrape describes which (Horn) constraints to scrape qualifiers from None = do not scrape, only use the supplied qualifiers Head = scrape only from the constraint heads (i.e. "rhs") All = scrape all concrete predicates (i.e. "rhs" + "lhs")

Constructors

No 
Head 
Both 

Instances

Instances details
Data Scrape 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) -> Scrape -> c Scrape #

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

toConstr :: Scrape -> Constr #

dataTypeOf :: Scrape -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Associated Types

type Rep Scrape :: Type -> Type #

Methods

from :: Scrape -> Rep Scrape x #

to :: Rep Scrape x -> Scrape #

Show Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Serialize Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Default Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

def :: Scrape #

NFData Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

rnf :: Scrape -> () #

Eq Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

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

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

Store Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

Methods

size :: Size Scrape #

poke :: Scrape -> Poke () #

peek :: Peek Scrape #

type Rep Scrape Source # 
Instance details

Defined in Language.Fixpoint.Types.Config

type Rep Scrape = D1 ('MetaData "Scrape" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "No" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Head" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Both" 'PrefixI 'False) (U1 :: Type -> Type)))

parallel solving options

defaultMinPartSize :: Int Source #

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