Language.Fixpoint.Types.Config

Documentation

data Config

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

• 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

• gradual :: Bool

  solve "gradual" constraints

• ginteractive :: Bool

  interactive gradual solving

• extensionality :: Bool

  allow function extensionality

• alphaEquivalence :: Bool

  allow lambda alpha equivalence axioms

• betaEquivalence :: Bool

  allow lambda beta equivalence axioms

• normalForm :: Bool

  allow lambda normal-form equivalence axioms

• 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

Instances

Eq Config

Methods

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

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

Data 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

Methods

showsPrec :: Int -> Config -> ShowS

show :: Config -> String

showList :: [Config] -> ShowS

Generic Config

Associated Types

type Rep Config :: * -> *

Methods

from :: Config -> Rep Config x

to :: Rep Config x -> Config

Default Config

Methods

def :: Config

type Rep Config

type Rep Config = D1 * (MetaData "Config" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" 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))))))))

defConfig :: Config

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

getOpts :: IO Config

SMT Solver options

data SMTSolver

Constructors

Z3

Cvc4

Mathsat

Instances

Eq SMTSolver

Methods

(==) :: SMTSolver -> SMTSolver -> Bool

(/=) :: SMTSolver -> SMTSolver -> Bool

Data SMTSolver

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

Methods

showsPrec :: Int -> SMTSolver -> ShowS

show :: SMTSolver -> String

showList :: [SMTSolver] -> ShowS

Generic SMTSolver

Associated Types

type Rep SMTSolver :: * -> *

Methods

from :: SMTSolver -> Rep SMTSolver x

to :: Rep SMTSolver x -> SMTSolver

Default SMTSolver

Methods

def :: SMTSolver

type Rep SMTSolver

type Rep SMTSolver = D1 * (MetaData "SMTSolver" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) ((:+:) * (C1 * (MetaCons "Z3" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "Cvc4" PrefixI False) (U1 *)) (C1 * (MetaCons "Mathsat" PrefixI False) (U1 *))))

Eliminate options

data Eliminate

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

Methods

(==) :: Eliminate -> Eliminate -> Bool

(/=) :: Eliminate -> Eliminate -> Bool

Data Eliminate

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

Methods

showsPrec :: Int -> Eliminate -> ShowS

show :: Eliminate -> String

showList :: [Eliminate] -> ShowS

Generic Eliminate

Associated Types

type Rep Eliminate :: * -> *

Methods

from :: Eliminate -> Rep Eliminate x

to :: Rep Eliminate x -> Eliminate

Serialize Eliminate

Methods

put :: Putter Eliminate

get :: Get Eliminate

Default Eliminate

Methods

def :: Eliminate

type Rep Eliminate

type Rep Eliminate = D1 * (MetaData "Eliminate" "Language.Fixpoint.Types.Config" "liquid-fixpoint-0.7.0.6-7ekgo2vNzFQLD9cAgffOsC" False) ((:+:) * (C1 * (MetaCons "None" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "Some" PrefixI False) (U1 *)) (C1 * (MetaCons "All" PrefixI False) (U1 *))))

useElim :: Config -> Bool

parallel solving options

defaultMinPartSize :: Int

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

defaultMaxPartSize :: Int

multicore :: Config -> Bool

queryFile :: Ext -> Config -> FilePath