Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Config

Contents

SMT Solver options
Eliminate options
parallel solving options

Synopsis

data Config = Config {
- srcFile :: FilePath
- cores :: Maybe Int
- minPartSize :: Int
- maxPartSize :: Int
- solver :: SMTSolver
- linear :: Bool
- stringTheory :: Bool
- defunction :: Bool
- allowHO :: Bool
- allowHOqs :: Bool
- eliminate :: Eliminate
- elimBound :: Maybe Int
- smtTimeout :: Maybe Int
- elimStats :: Bool
- solverStats :: Bool
- metadata :: Bool
- stats :: Bool
- parts :: Bool
- save :: Bool
- minimize :: Bool
- minimizeQs :: Bool
- minimizeKs :: Bool
- minimalSol :: Bool
- etaElim :: Bool
- gradual :: Bool
- ginteractive :: Bool
- autoKuts :: Bool
- nonLinCuts :: Bool
- noslice :: Bool
- rewriteAxioms :: Bool
- oldPLE :: Bool
- noIncrPle :: Bool
- checkCstr :: [Integer]
- extensionality :: Bool
- maxRWOrderingConstraints :: Maybe Int
- rwTerminationCheck :: Bool
}
defConfig :: Config
withPragmas :: Config -> [String] -> IO Config
getOpts :: IO Config
data SMTSolver
- = Z3
- | Cvc4
- | Mathsat
data Eliminate
- = None
- | Some
- | All
- | Horn
- | Existentials
useElim :: Config -> Bool
defaultMinPartSize :: Int
defaultMaxPartSize :: Int
multicore :: Config -> Bool
queryFile :: Ext -> Config -> FilePath

Documentation

data Config Source #

Constructors

Config

Fields

srcFile :: FilePath
src file (*.hs, *.ts, *.c, or even *.fq or *.bfq)
cores :: Maybe Int
number of cores used to solve constraints
minPartSize :: Int
Minimum size of a partition
maxPartSize :: Int
Maximum size of a partition. Overrides minPartSize
solver :: SMTSolver
which SMT solver to use
linear :: Bool
not interpret div and mul in SMT
stringTheory :: Bool
interpretation of string theory by SMT
defunction :: Bool
defunctionalize (use apply for all uninterpreted applications)
allowHO :: Bool
allow higher order binders in the logic environment
allowHOqs :: Bool
allow higher order qualifiers
eliminate :: Eliminate
eliminate non-cut KVars
elimBound :: Maybe Int
maximum length of KVar chain to eliminate
smtTimeout :: Maybe Int
smt timeout in msec
elimStats :: Bool
print eliminate stats
solverStats :: Bool
print solver stats
metadata :: Bool
print meta-data associated with constraints
stats :: Bool
compute constraint statistics
parts :: Bool
partition FInfo into separate fq files
save :: Bool
save FInfo as .bfq and .fq file
minimize :: Bool
min .fq by delta debug (unsat with min constraints)
minimizeQs :: Bool
min .fq by delta debug (sat with min qualifiers)
minimizeKs :: Bool
min .fq by delta debug (sat with min kvars)
minimalSol :: Bool
shrink final solution by pruning redundant qualfiers from fixpoint
etaElim :: Bool
eta eliminate function definitions
gradual :: Bool
solve "gradual" constraints
ginteractive :: Bool
interactive gradual solving
autoKuts :: Bool
ignore given kut variables
nonLinCuts :: Bool
Treat non-linear vars as cuts
noslice :: Bool
Disable non-concrete KVar slicing
rewriteAxioms :: Bool
Allow axiom instantiation via rewriting
oldPLE :: Bool
Use old version of PLE
noIncrPle :: Bool
Use incremental PLE
checkCstr :: [Integer]
Only check these specific constraints
extensionality :: Bool
Enable extensional interpretation of function equality
maxRWOrderingConstraints :: Maybe Int
rwTerminationCheck :: Bool

Instances

Instances details

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 :: 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 #
Show Config Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> Config -> ShowS # show :: Config -> String # showList :: [Config] -> ShowS #
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.10.2-inplace" '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))))))))

defConfig :: Config Source #

withPragmas :: Config -> [String] -> IO Config Source #

getOpts :: IO Config Source #

SMT Solver options

data SMTSolver Source #

Constructors

Z3
Cvc4
Mathsat

Instances

Instances details

Eq SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods (==) :: SMTSolver -> SMTSolver -> Bool # (/=) :: SMTSolver -> SMTSolver -> Bool #
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 #
Show SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> SMTSolver -> ShowS # show :: SMTSolver -> String # showList :: [SMTSolver] -> ShowS #
Generic SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Associated Types type Rep SMTSolver :: Type -> Type # Methods from :: SMTSolver -> Rep SMTSolver x # to :: Rep SMTSolver x -> SMTSolver #
Binary SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods put :: SMTSolver -> Put # get :: Get SMTSolver # putList :: [SMTSolver] -> Put #
NFData SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods rnf :: SMTSolver -> () #
Default SMTSolver Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods def :: 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.10.2-inplace" '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

Instances details

Eq Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods (==) :: Eliminate -> Eliminate -> Bool # (/=) :: Eliminate -> Eliminate -> Bool #
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 #
Show Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods showsPrec :: Int -> Eliminate -> ShowS # show :: Eliminate -> String # showList :: [Eliminate] -> ShowS #
Generic Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Associated Types type Rep Eliminate :: Type -> Type # Methods from :: Eliminate -> Rep Eliminate x # to :: Rep Eliminate x -> Eliminate #
Binary Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods put :: Eliminate -> Put # get :: Get Eliminate # putList :: [Eliminate] -> Put #
NFData Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods rnf :: Eliminate -> () #
Serialize Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods put :: Putter Eliminate get :: Get Eliminate
Default Eliminate Source #
Instance details Defined in Language.Fixpoint.Types.Config Methods def :: 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.10.2-inplace" '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))))

useElim :: Config -> Bool Source #

parallel solving options

defaultMinPartSize :: Int Source #

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

defaultMaxPartSize :: Int Source #

multicore :: Config -> Bool Source #

queryFile :: Ext -> Config -> FilePath Source #