{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE DeriveGeneric             #-}

module Language.Fixpoint.Types.Config (
    Config  (..)
  , defConfig
  , withPragmas

  , getOpts

  -- * SMT Solver options
  , SMTSolver (..)

  -- REST Options
  , RESTOrdering (..)
  , restOC

  -- * Eliminate options
  , Eliminate (..)
  , useElim

  -- * Scrape options
  , Scrape (..)

  -- * parallel solving options
  , defaultMinPartSize
  , defaultMaxPartSize
  , multicore

  , queryFile
) where

import qualified Data.Store as S
import qualified Data.List as L
import Data.Serialize                (Serialize (..))
import Control.DeepSeq
import GHC.Generics
import System.Console.CmdArgs
import System.Console.CmdArgs.Explicit

import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3
import Language.Fixpoint.Utils.Files


--------------------------------------------------------------------------------
withPragmas :: Config -> [String] -> IO Config
--------------------------------------------------------------------------------
withPragmas :: Config -> [FilePath] -> IO Config
withPragmas Config
c [FilePath]
s =
    forall a. Mode a -> [FilePath] -> IO a
processValueIO
      Mode (CmdArgs Config)
config { modeValue :: CmdArgs Config
modeValue = (forall a. Mode a -> a
modeValue Mode (CmdArgs Config)
config) { cmdArgsValue :: Config
cmdArgsValue = Config
c } }
      [FilePath]
s
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      forall a. CmdArgs a -> IO a
cmdArgsApply

--------------------------------------------------------------------------------
-- | Configuration Options -----------------------------------------------------
--------------------------------------------------------------------------------

defaultMinPartSize :: Int
defaultMinPartSize :: Int
defaultMinPartSize = Int
500

defaultMaxPartSize :: Int
defaultMaxPartSize :: Int
defaultMaxPartSize = Int
700


data Config = Config
  { Config -> FilePath
srcFile     :: FilePath            -- ^ src file (*.hs, *.ts, *.c, or even *.fq or *.bfq)
  , Config -> Maybe Int
cores       :: Maybe Int           -- ^ number of cores used to solve constraints
  , Config -> Int
minPartSize :: Int                 -- ^ Minimum size of a partition
  , Config -> Int
maxPartSize :: Int                 -- ^ Maximum size of a partition. Overrides minPartSize
  , Config -> SMTSolver
solver      :: SMTSolver           -- ^ which SMT solver to use
  , Config -> Bool
linear      :: Bool                -- ^ not interpret div and mul in SMT
  , Config -> Bool
stringTheory :: Bool               -- ^ interpretation of string theory by SMT
  , Config -> Bool
defunction  :: Bool                -- ^ defunctionalize (use 'apply' for all uninterpreted applications)
  , Config -> Bool
allowHO     :: Bool                -- ^ allow higher order binders in the logic environment
  , Config -> Bool
allowHOqs   :: Bool                -- ^ allow higher order qualifiers
  , Config -> Eliminate
eliminate   :: Eliminate           -- ^ eliminate non-cut KVars
  , Config -> Scrape
scrape      :: Scrape              -- ^ configure auto-scraping of qualifiers from constraints
  , Config -> Maybe Int
elimBound   :: Maybe Int           -- ^ maximum length of KVar chain to eliminate
  , Config -> Maybe Int
smtTimeout  :: Maybe Int           -- ^ smt timeout in msec
  , Config -> Bool
elimStats   :: Bool                -- ^ print eliminate stats
  , Config -> Bool
solverStats :: Bool                -- ^ print solver stats
  , Config -> Bool
metadata    :: Bool                -- ^ print meta-data associated with constraints
  , Config -> Bool
stats       :: Bool                -- ^ compute constraint statistics
  , Config -> Bool
parts       :: Bool                -- ^ partition FInfo into separate fq files
  , Config -> Bool
save        :: Bool                -- ^ save FInfo as .bfq and .fq file
  , Config -> Bool
minimize    :: Bool                -- ^ min .fq by delta debug (unsat with min constraints)
  , Config -> Bool
minimizeQs  :: Bool                -- ^ min .fq by delta debug (sat with min qualifiers)
  , Config -> Bool
minimizeKs  :: Bool                -- ^ min .fq by delta debug (sat with min kvars)
  , Config -> Bool
minimalSol  :: Bool                -- ^ shrink final solution by pruning redundant qualfiers from fixpoint
  , Config -> Bool
etaElim     :: Bool                -- ^ eta eliminate function definitions
  , Config -> Bool
gradual     :: Bool                -- ^ solve "gradual" constraints
  , Config -> Bool
ginteractive :: Bool                -- ^ interactive gradual solving
  , Config -> Bool
autoKuts         :: Bool           -- ^ ignore given kut variables
  , Config -> Bool
nonLinCuts       :: Bool           -- ^ Treat non-linear vars as cuts
  , Config -> Bool
noslice          :: Bool           -- ^ Disable non-concrete KVar slicing
  , Config -> Bool
rewriteAxioms    :: Bool           -- ^ Allow axiom instantiation via rewriting
  , Config -> Bool
pleWithUndecidedGuards :: Bool     -- ^ Unfold invocations with undecided guards in PLE
  , Config -> Bool
interpreter      :: Bool           -- ^ Do not use the interpreter to assist PLE
  , Config -> Bool
oldPLE           :: Bool           -- ^ Use old version of PLE
  , Config -> Bool
noIncrPle        :: Bool           -- ^ Use incremental PLE
  , Config -> Bool
noEnvironmentReduction :: Bool     -- ^ Don't use environment reduction
  , Config -> Bool
inlineANFBindings :: Bool          -- ^ Inline ANF bindings.
                                       -- Sometimes improves performance and sometimes worsens it.
  , Config -> [Integer]
checkCstr        :: [Integer]      -- ^ Only check these specific constraints
  , Config -> Bool
extensionality   :: Bool           -- ^ Enable extensional interpretation of function equality
  , Config -> Bool
rwTerminationCheck  :: Bool        -- ^ Enable termination checking for rewriting
  , Config -> Bool
stdin               :: Bool        -- ^ Read input query from stdin
  , Config -> Bool
json                :: Bool        -- ^ Render output in JSON format
  , Config -> Bool
noLazyPLE           :: Bool
  , Config -> Maybe Int
fuel                :: Maybe Int   -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite)
  , Config -> FilePath
restOrdering        :: String      -- ^ Term ordering for use in REST
  } deriving (Config -> Config -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c== :: Config -> Config -> Bool
Eq,Typeable Config
Config -> DataType
Config -> Constr
(forall b. Data b => b -> b) -> Config -> Config
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Config -> u
forall u. (forall d. Data d => d -> u) -> Config -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Config -> m Config
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Config -> m Config
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Config
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Config -> c Config
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Config)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Config -> m Config
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Config -> m Config
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Config -> m Config
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Config -> m Config
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Config -> m Config
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Config -> m Config
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Config -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Config -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Config -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Config -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r
gmapT :: (forall b. Data b => b -> b) -> Config -> Config
$cgmapT :: (forall b. Data b => b -> b) -> Config -> Config
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Config)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Config)
dataTypeOf :: Config -> DataType
$cdataTypeOf :: Config -> DataType
toConstr :: Config -> Constr
$ctoConstr :: Config -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Config
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Config
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Config -> c Config
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Config -> c Config
Data,Typeable,Int -> Config -> ShowS
[Config] -> ShowS
Config -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Config] -> ShowS
$cshowList :: [Config] -> ShowS
show :: Config -> FilePath
$cshow :: Config -> FilePath
showsPrec :: Int -> Config -> ShowS
$cshowsPrec :: Int -> Config -> ShowS
Show,forall x. Rep Config x -> Config
forall x. Config -> Rep Config x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Config x -> Config
$cfrom :: forall x. Config -> Rep Config x
Generic)

instance Default Config where
  def :: Config
def = Config
defConfig

---------------------------------------------------------------------------------------

data RESTOrdering = RESTKBO | RESTLPO | RESTRPO | RESTFuel Int
                 deriving (RESTOrdering -> RESTOrdering -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RESTOrdering -> RESTOrdering -> Bool
$c/= :: RESTOrdering -> RESTOrdering -> Bool
== :: RESTOrdering -> RESTOrdering -> Bool
$c== :: RESTOrdering -> RESTOrdering -> Bool
Eq, Typeable RESTOrdering
RESTOrdering -> DataType
RESTOrdering -> Constr
(forall b. Data b => b -> b) -> RESTOrdering -> RESTOrdering
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RESTOrdering -> u
forall u. (forall d. Data d => d -> u) -> RESTOrdering -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RESTOrdering
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RESTOrdering -> c RESTOrdering
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RESTOrdering)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RESTOrdering)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RESTOrdering -> m RESTOrdering
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RESTOrdering -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RESTOrdering -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> RESTOrdering -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RESTOrdering -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RESTOrdering -> r
gmapT :: (forall b. Data b => b -> b) -> RESTOrdering -> RESTOrdering
$cgmapT :: (forall b. Data b => b -> b) -> RESTOrdering -> RESTOrdering
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RESTOrdering)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RESTOrdering)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RESTOrdering)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RESTOrdering)
dataTypeOf :: RESTOrdering -> DataType
$cdataTypeOf :: RESTOrdering -> DataType
toConstr :: RESTOrdering -> Constr
$ctoConstr :: RESTOrdering -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RESTOrdering
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RESTOrdering
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RESTOrdering -> c RESTOrdering
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RESTOrdering -> c RESTOrdering
Data, Typeable, forall x. Rep RESTOrdering x -> RESTOrdering
forall x. RESTOrdering -> Rep RESTOrdering x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RESTOrdering x -> RESTOrdering
$cfrom :: forall x. RESTOrdering -> Rep RESTOrdering x
Generic)

instance Default RESTOrdering where
  def :: RESTOrdering
def = RESTOrdering
RESTRPO

instance Show RESTOrdering where
  show :: RESTOrdering -> FilePath
show RESTOrdering
RESTKBO      = FilePath
"kbo"
  show RESTOrdering
RESTLPO      = FilePath
"lpo"
  show RESTOrdering
RESTRPO      = FilePath
"rpo"
  show (RESTFuel Int
n) = FilePath
"fuel" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Int
n

instance Read RESTOrdering where
  readsPrec :: Int -> ReadS RESTOrdering
readsPrec Int
_ FilePath
s | FilePath
"kbo" forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = [(RESTOrdering
RESTKBO, forall a. Int -> [a] -> [a]
drop Int
3 FilePath
s)]
  readsPrec Int
_ FilePath
s | FilePath
"lbo" forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = [(RESTOrdering
RESTLPO, forall a. Int -> [a] -> [a]
drop Int
3 FilePath
s)]
  readsPrec Int
_ FilePath
s | FilePath
"rpo" forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = [(RESTOrdering
RESTRPO, forall a. Int -> [a] -> [a]
drop Int
3 FilePath
s)]
  readsPrec Int
n FilePath
s | FilePath
"fuel" forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = do
                        (Int
fuel', FilePath
rest) <- forall a. Read a => Int -> ReadS a
readsPrec Int
n (forall a. Int -> [a] -> [a]
drop Int
4 FilePath
s)
                        forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> RESTOrdering
RESTFuel Int
fuel', FilePath
rest)
  readsPrec Int
_ FilePath
_ = []

---------------------------------------------------------------------------------------

data SMTSolver = Z3 | Z3mem | Cvc4 | Mathsat
                 deriving (SMTSolver -> SMTSolver -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTSolver -> SMTSolver -> Bool
$c/= :: SMTSolver -> SMTSolver -> Bool
== :: SMTSolver -> SMTSolver -> Bool
$c== :: SMTSolver -> SMTSolver -> Bool
Eq, Typeable SMTSolver
SMTSolver -> DataType
SMTSolver -> Constr
(forall b. Data b => b -> b) -> SMTSolver -> SMTSolver
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SMTSolver -> u
forall u. (forall d. Data d => d -> u) -> SMTSolver -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTSolver -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTSolver -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTSolver
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTSolver -> c SMTSolver
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTSolver)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTSolver)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTSolver -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTSolver -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SMTSolver -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTSolver -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTSolver -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTSolver -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTSolver -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTSolver -> r
gmapT :: (forall b. Data b => b -> b) -> SMTSolver -> SMTSolver
$cgmapT :: (forall b. Data b => b -> b) -> SMTSolver -> SMTSolver
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTSolver)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTSolver)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTSolver)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTSolver)
dataTypeOf :: SMTSolver -> DataType
$cdataTypeOf :: SMTSolver -> DataType
toConstr :: SMTSolver -> Constr
$ctoConstr :: SMTSolver -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTSolver
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTSolver
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTSolver -> c SMTSolver
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTSolver -> c SMTSolver
Data, Typeable, forall x. Rep SMTSolver x -> SMTSolver
forall x. SMTSolver -> Rep SMTSolver x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SMTSolver x -> SMTSolver
$cfrom :: forall x. SMTSolver -> Rep SMTSolver x
Generic)

instance Default SMTSolver where
  def :: SMTSolver
def = if Bool
Conditional.Z3.builtWithZ3AsALibrary then SMTSolver
Z3mem else SMTSolver
Z3

instance Show SMTSolver where
  show :: SMTSolver -> FilePath
show SMTSolver
Z3      = FilePath
"z3"
  show SMTSolver
Z3mem   = FilePath
"z3 API"
  show SMTSolver
Cvc4    = FilePath
"cvc4"
  show SMTSolver
Mathsat = FilePath
"mathsat"

instance S.Store SMTSolver

---------------------------------------------------------------------------------------
-- | `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")

data Scrape = No | Head | Both
  deriving (Scrape -> Scrape -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Scrape -> Scrape -> Bool
$c/= :: Scrape -> Scrape -> Bool
== :: Scrape -> Scrape -> Bool
$c== :: Scrape -> Scrape -> Bool
Eq, Typeable Scrape
Scrape -> DataType
Scrape -> Constr
(forall b. Data b => b -> b) -> Scrape -> Scrape
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Scrape -> u
forall u. (forall d. Data d => d -> u) -> Scrape -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scrape
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scrape -> c Scrape
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scrape)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scrape)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Scrape -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Scrape -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Scrape -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Scrape -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scrape -> r
gmapT :: (forall b. Data b => b -> b) -> Scrape -> Scrape
$cgmapT :: (forall b. Data b => b -> b) -> Scrape -> Scrape
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scrape)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scrape)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scrape)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scrape)
dataTypeOf :: Scrape -> DataType
$cdataTypeOf :: Scrape -> DataType
toConstr :: Scrape -> Constr
$ctoConstr :: Scrape -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scrape
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scrape
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scrape -> c Scrape
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scrape -> c Scrape
Data, Typeable, forall x. Rep Scrape x -> Scrape
forall x. Scrape -> Rep Scrape x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Scrape x -> Scrape
$cfrom :: forall x. Scrape -> Rep Scrape x
Generic)

instance Serialize Scrape
instance S.Store Scrape
instance NFData Scrape

instance Default Scrape where
  def :: Scrape
def = Scrape
No

instance Show Scrape where
  show :: Scrape -> FilePath
show Scrape
No   = FilePath
"no"
  show Scrape
Head = FilePath
"head"
  show Scrape
Both = FilePath
"both"

---------------------------------------------------------------------------------------
-- | 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
---------------------------------------------------------------------------------------
data Eliminate
  = None
  | Some
  | All
  | Horn
  | Existentials
  deriving (Eliminate -> Eliminate -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Eliminate -> Eliminate -> Bool
$c/= :: Eliminate -> Eliminate -> Bool
== :: Eliminate -> Eliminate -> Bool
$c== :: Eliminate -> Eliminate -> Bool
Eq, Typeable Eliminate
Eliminate -> DataType
Eliminate -> Constr
(forall b. Data b => b -> b) -> Eliminate -> Eliminate
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Eliminate -> u
forall u. (forall d. Data d => d -> u) -> Eliminate -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Eliminate -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Eliminate -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Eliminate
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Eliminate -> c Eliminate
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Eliminate)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Eliminate)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Eliminate -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Eliminate -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Eliminate -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Eliminate -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Eliminate -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Eliminate -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Eliminate -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Eliminate -> r
gmapT :: (forall b. Data b => b -> b) -> Eliminate -> Eliminate
$cgmapT :: (forall b. Data b => b -> b) -> Eliminate -> Eliminate
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Eliminate)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Eliminate)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Eliminate)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Eliminate)
dataTypeOf :: Eliminate -> DataType
$cdataTypeOf :: Eliminate -> DataType
toConstr :: Eliminate -> Constr
$ctoConstr :: Eliminate -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Eliminate
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Eliminate
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Eliminate -> c Eliminate
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Eliminate -> c Eliminate
Data, Typeable, forall x. Rep Eliminate x -> Eliminate
forall x. Eliminate -> Rep Eliminate x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Eliminate x -> Eliminate
$cfrom :: forall x. Eliminate -> Rep Eliminate x
Generic)

instance Serialize Eliminate
instance S.Store Eliminate
instance NFData SMTSolver
instance NFData Eliminate

instance Default Eliminate where
  def :: Eliminate
def = Eliminate
None

instance Show Eliminate where
  show :: Eliminate -> FilePath
show Eliminate
None = FilePath
"none"
  show Eliminate
Some = FilePath
"some"
  show Eliminate
All  = FilePath
"all"
  show Eliminate
Horn  = FilePath
"horn"
  show Eliminate
Existentials  = FilePath
"existentials"


useElim :: Config -> Bool
useElim :: Config -> Bool
useElim Config
cfg = Config -> Eliminate
eliminate Config
cfg forall a. Eq a => a -> a -> Bool
/= Eliminate
None

---------------------------------------------------------------------------------------

defConfig :: Config
defConfig :: Config
defConfig = Config {
    srcFile :: FilePath
srcFile                  = FilePath
"out"   forall val. Data val => val -> Ann -> val
&= Ann
args    forall val. Data val => val -> Ann -> val
&= Ann
typFile
  , defunction :: Bool
defunction               = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Allow higher order binders into fixpoint environment"
  , solver :: SMTSolver
solver                   = forall a. Default a => a
def     forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Name of SMT Solver"
  , linear :: Bool
linear                   = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Use uninterpreted integer multiplication and division"
  , stringTheory :: Bool
stringTheory             = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Interpretation of String Theory by SMT"
  , allowHO :: Bool
allowHO                  = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Allow higher order binders into fixpoint environment"
  , allowHOqs :: Bool
allowHOqs                = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Allow higher order qualifiers"
  , eliminate :: Eliminate
eliminate                = Eliminate
None    forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]"
  , scrape :: Scrape
scrape                   = forall a. Default a => a
def     forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Scrape qualifiers from constraint (Horn format only) [ no = do not, head = scrape from heads, both = scrape from everywhere ]"
  , elimBound :: Maybe Int
elimBound                = forall a. Maybe a
Nothing forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"elimBound"   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"(alpha) Maximum eliminate-chain depth"
  , smtTimeout :: Maybe Int
smtTimeout               = forall a. Maybe a
Nothing forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"smtTimeout"  forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"smt timeout in msec"
  , elimStats :: Bool
elimStats                = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"(alpha) Print eliminate stats"
  , solverStats :: Bool
solverStats              = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Print solver stats"
  , save :: Bool
save                     = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Save Query as .fq and .bfq files"
  , metadata :: Bool
metadata                 = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Print meta-data associated with constraints"
  , stats :: Bool
stats                    = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Compute constraint statistics"
  , etaElim :: Bool
etaElim                  = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"eta elimination in function definition"
  , parts :: Bool
parts                    = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Partition constraints into indepdendent .fq files"
  , cores :: Maybe Int
cores                    = forall a. Default a => a
def     forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"(numeric) Number of threads to use"
  , minPartSize :: Int
minPartSize              = Int
defaultMinPartSize forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"(numeric) Minimum partition size when solving in parallel"
  , maxPartSize :: Int
maxPartSize              = Int
defaultMaxPartSize forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"(numeric) Maximum partiton size when solving in parallel."
  , minimize :: Bool
minimize                 = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Delta debug to minimize fq file (unsat with min constraints)"
  , minimizeQs :: Bool
minimizeQs               = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Delta debug to minimize fq file (sat with min qualifiers)"
  , minimizeKs :: Bool
minimizeKs               = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Delta debug to minimize fq file (sat with max kvars replaced by True)"
  , minimalSol :: Bool
minimalSol               = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Shrink fixpoint by removing implied qualifiers"
  , gradual :: Bool
gradual                  = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Solve gradual-refinement typing constraints"
  , ginteractive :: Bool
ginteractive             = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Interactive Gradual Solving"
  , autoKuts :: Bool
autoKuts                 = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Ignore given Kut vars, compute from scratch"
  , nonLinCuts :: Bool
nonLinCuts               = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Treat non-linear kvars as cuts"
  , noslice :: Bool
noslice                  = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Disable non-concrete KVar slicing"
  , rewriteAxioms :: Bool
rewriteAxioms            = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"allow axiom instantiation via rewriting (PLE)"
  , pleWithUndecidedGuards :: Bool
pleWithUndecidedGuards   =
      Bool
False
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"ple-with-undecided-guards"
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Unfold invocations with undecided guards in PLE"
        forall val. Data val => val -> Ann -> val
&= Ann
explicit
  , interpreter :: Bool
interpreter              =
      Bool
False
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"interpreter"
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Use the interpreter to assist PLE"
  , oldPLE :: Bool
oldPLE                   = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Use old version of PLE"
  , noIncrPle :: Bool
noIncrPle                = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Don't use incremental PLE"
  , noEnvironmentReduction :: Bool
noEnvironmentReduction   =
      Bool
False
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"no-environment-reduction"
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Don't perform environment reduction"
  , inlineANFBindings :: Bool
inlineANFBindings        =
      Bool
False
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"inline-anf-bindings"
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help ([FilePath] -> FilePath
unwords
          [ FilePath
"Inline ANF bindings."
          , FilePath
"Sometimes improves performance and sometimes worsens it."
          , FilePath
"Disabled by --no-environment-reduction"
          ])
  , checkCstr :: [Integer]
checkCstr                = []    forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Only check these specific constraint-ids"
  , extensionality :: Bool
extensionality           = Bool
False forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Allow extensional interpretation of extensionality"
  , rwTerminationCheck :: Bool
rwTerminationCheck       = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Enable rewrite divergence checker"
  , stdin :: Bool
stdin                    = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Read input query from stdin"
  , json :: Bool
json                     = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Render result in JSON"
  , noLazyPLE :: Bool
noLazyPLE                = Bool
False   forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Don't use lazy PLE"
  , fuel :: Maybe Int
fuel                     = forall a. Maybe a
Nothing forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Maximum fuel (per-function unfoldings) for PLE"
  , restOrdering :: FilePath
restOrdering             = FilePath
"rpo"
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"rest-ordering"
        forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Ordering Constraint Algebra to use for REST"
  }
  forall val. Data val => val -> Ann -> val
&= Ann
verbosity
  forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
program FilePath
"fixpoint"
  forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help    FilePath
"Predicate Abstraction Based Horn-Clause Solver"
  forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
summary FilePath
"fixpoint Copyright 2009-15 Regents of the University of California."
  forall val. Data val => val -> Ann -> val
&= [FilePath] -> Ann
details [ FilePath
"Predicate Abstraction Based Horn-Clause Solver"
             , FilePath
""
             , FilePath
"To check a file foo.fq type:"
             , FilePath
"  fixpoint foo.fq"
             ]

config :: Mode (CmdArgs Config)
config :: Mode (CmdArgs Config)
config = forall a. Data a => a -> Mode (CmdArgs a)
cmdArgsMode Config
defConfig

getOpts :: IO Config
getOpts :: IO Config
getOpts = do
  Config
md <- forall a. Data a => a -> IO a
cmdArgs Config
defConfig
  IO () -> IO ()
whenNormal (FilePath -> IO ()
putStrLn FilePath
banner)
  forall (m :: * -> *) a. Monad m => a -> m a
return Config
md

banner :: String
banner :: FilePath
banner =  FilePath
"\n\nLiquid-Fixpoint Copyright 2013-21 Regents of the University of California.\n"
       forall a. [a] -> [a] -> [a]
++ FilePath
"All Rights Reserved.\n"

restOC :: Config -> RESTOrdering
restOC :: Config -> RESTOrdering
restOC Config
cfg = forall a. Read a => FilePath -> a
read (Config -> FilePath
restOrdering Config
cfg)

multicore :: Config -> Bool
multicore :: Config -> Bool
multicore Config
cfg = Config -> Maybe Int
cores Config
cfg forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Int
1

queryFile :: Ext -> Config -> FilePath
queryFile :: Ext -> Config -> FilePath
queryFile Ext
e = Ext -> ShowS
extFileName Ext
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> FilePath
srcFile