{-# 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 =
    Mode (CmdArgs Config) -> [FilePath] -> IO (CmdArgs Config)
forall a. Mode a -> [FilePath] -> IO a
processValueIO
      Mode (CmdArgs Config)
config { modeValue = (modeValue config) { cmdArgsValue = c } }
      [FilePath]
s
    IO (CmdArgs Config) -> (CmdArgs Config -> IO Config) -> IO Config
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      CmdArgs Config -> IO Config
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
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
/= :: Config -> Config -> Bool
Eq,Typeable Config
Typeable Config =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Config -> c Config)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Config)
-> (Config -> Constr)
-> (Config -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Config -> Config)
-> (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 u. (forall d. Data d => d -> u) -> Config -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Config -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Config -> m Config)
-> Data Config
Config -> Constr
Config -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Config -> c Config
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Config -> c Config
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Config
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Config
$ctoConstr :: Config -> Constr
toConstr :: Config -> Constr
$cdataTypeOf :: Config -> DataType
dataTypeOf :: Config -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Config)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Config)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config)
$cgmapT :: (forall b. Data b => b -> b) -> Config -> Config
gmapT :: (forall b. Data b => b -> b) -> Config -> Config
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Config -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Config -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Config -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Config -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Config -> m Config
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Config -> m Config
Data,Typeable,Int -> Config -> ShowS
[Config] -> ShowS
Config -> FilePath
(Int -> Config -> ShowS)
-> (Config -> FilePath) -> ([Config] -> ShowS) -> Show Config
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Config -> ShowS
showsPrec :: Int -> Config -> ShowS
$cshow :: Config -> FilePath
show :: Config -> FilePath
$cshowList :: [Config] -> ShowS
showList :: [Config] -> ShowS
Show,(forall x. Config -> Rep Config x)
-> (forall x. Rep Config x -> Config) -> Generic Config
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
$cfrom :: forall x. Config -> Rep Config x
from :: forall x. Config -> Rep Config x
$cto :: forall x. Rep Config x -> Config
to :: forall x. Rep Config x -> Config
Generic)

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

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

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

instance Read RESTOrdering where
  readsPrec :: Int -> ReadS RESTOrdering
readsPrec Int
_ FilePath
s | FilePath
"kbo" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = [(RESTOrdering
RESTKBO, Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
3 FilePath
s)]
  readsPrec Int
_ FilePath
s | FilePath
"lbo" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = [(RESTOrdering
RESTLPO, Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
3 FilePath
s)]
  readsPrec Int
_ FilePath
s | FilePath
"rpo" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = [(RESTOrdering
RESTRPO, Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
3 FilePath
s)]
  readsPrec Int
n FilePath
s | FilePath
"fuel" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
s = do
                        (Int
fuel', FilePath
rest) <- Int -> ReadS Int
forall a. Read a => Int -> ReadS a
readsPrec Int
n (Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
4 FilePath
s)
                        (RESTOrdering, FilePath) -> [(RESTOrdering, FilePath)]
forall a. a -> [a]
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
(SMTSolver -> SMTSolver -> Bool)
-> (SMTSolver -> SMTSolver -> Bool) -> Eq SMTSolver
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SMTSolver -> SMTSolver -> Bool
== :: SMTSolver -> SMTSolver -> Bool
$c/= :: SMTSolver -> SMTSolver -> Bool
/= :: SMTSolver -> SMTSolver -> Bool
Eq, Typeable SMTSolver
Typeable SMTSolver =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SMTSolver -> c SMTSolver)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SMTSolver)
-> (SMTSolver -> Constr)
-> (SMTSolver -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> SMTSolver -> SMTSolver)
-> (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 u. (forall d. Data d => d -> u) -> SMTSolver -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SMTSolver -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver)
-> Data SMTSolver
SMTSolver -> Constr
SMTSolver -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTSolver -> c SMTSolver
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTSolver -> c SMTSolver
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTSolver
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTSolver
$ctoConstr :: SMTSolver -> Constr
toConstr :: SMTSolver -> Constr
$cdataTypeOf :: SMTSolver -> DataType
dataTypeOf :: SMTSolver -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTSolver)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTSolver)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTSolver)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTSolver)
$cgmapT :: (forall b. Data b => b -> b) -> SMTSolver -> SMTSolver
gmapT :: (forall b. Data b => b -> b) -> SMTSolver -> SMTSolver
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTSolver -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SMTSolver -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTSolver -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTSolver -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTSolver -> m SMTSolver
Data, Typeable, (forall x. SMTSolver -> Rep SMTSolver x)
-> (forall x. Rep SMTSolver x -> SMTSolver) -> Generic SMTSolver
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
$cfrom :: forall x. SMTSolver -> Rep SMTSolver x
from :: forall x. SMTSolver -> Rep SMTSolver x
$cto :: forall x. Rep SMTSolver x -> SMTSolver
to :: forall x. Rep SMTSolver x -> SMTSolver
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
(Scrape -> Scrape -> Bool)
-> (Scrape -> Scrape -> Bool) -> Eq Scrape
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Scrape -> Scrape -> Bool
== :: Scrape -> Scrape -> Bool
$c/= :: Scrape -> Scrape -> Bool
/= :: Scrape -> Scrape -> Bool
Eq, Typeable Scrape
Typeable Scrape =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Scrape -> c Scrape)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Scrape)
-> (Scrape -> Constr)
-> (Scrape -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Scrape -> Scrape)
-> (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 u. (forall d. Data d => d -> u) -> Scrape -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Scrape -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Scrape -> m Scrape)
-> Data Scrape
Scrape -> Constr
Scrape -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scrape -> c Scrape
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scrape -> c Scrape
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scrape
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scrape
$ctoConstr :: Scrape -> Constr
toConstr :: Scrape -> Constr
$cdataTypeOf :: Scrape -> DataType
dataTypeOf :: Scrape -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scrape)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scrape)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scrape)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scrape)
$cgmapT :: (forall b. Data b => b -> b) -> Scrape -> Scrape
gmapT :: (forall b. Data b => b -> b) -> Scrape -> Scrape
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Scrape -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Scrape -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Scrape -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Scrape -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scrape -> m Scrape
Data, Typeable, (forall x. Scrape -> Rep Scrape x)
-> (forall x. Rep Scrape x -> Scrape) -> Generic Scrape
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
$cfrom :: forall x. Scrape -> Rep Scrape x
from :: forall x. Scrape -> Rep Scrape x
$cto :: forall x. Rep Scrape x -> Scrape
to :: forall x. Rep Scrape x -> Scrape
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
(Eliminate -> Eliminate -> Bool)
-> (Eliminate -> Eliminate -> Bool) -> Eq Eliminate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Eliminate -> Eliminate -> Bool
== :: Eliminate -> Eliminate -> Bool
$c/= :: Eliminate -> Eliminate -> Bool
/= :: Eliminate -> Eliminate -> Bool
Eq, Typeable Eliminate
Typeable Eliminate =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Eliminate -> c Eliminate)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Eliminate)
-> (Eliminate -> Constr)
-> (Eliminate -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Eliminate -> Eliminate)
-> (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 u. (forall d. Data d => d -> u) -> Eliminate -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Eliminate -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Eliminate -> m Eliminate)
-> Data Eliminate
Eliminate -> Constr
Eliminate -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Eliminate -> c Eliminate
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Eliminate -> c Eliminate
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Eliminate
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Eliminate
$ctoConstr :: Eliminate -> Constr
toConstr :: Eliminate -> Constr
$cdataTypeOf :: Eliminate -> DataType
dataTypeOf :: Eliminate -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Eliminate)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Eliminate)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Eliminate)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Eliminate)
$cgmapT :: (forall b. Data b => b -> b) -> Eliminate -> Eliminate
gmapT :: (forall b. Data b => b -> b) -> Eliminate -> Eliminate
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Eliminate -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Eliminate -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Eliminate -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Eliminate -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Eliminate -> m Eliminate
Data, Typeable, (forall x. Eliminate -> Rep Eliminate x)
-> (forall x. Rep Eliminate x -> Eliminate) -> Generic Eliminate
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
$cfrom :: forall x. Eliminate -> Rep Eliminate x
from :: forall x. Eliminate -> Rep Eliminate x
$cto :: forall x. Rep Eliminate x -> Eliminate
to :: forall x. Rep Eliminate x -> Eliminate
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 Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
/= Eliminate
None

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

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

getOpts :: IO Config
getOpts :: IO Config
getOpts = do
  Config
md <- Config -> IO Config
forall a. Data a => a -> IO a
cmdArgs Config
defConfig
  IO () -> IO ()
whenNormal (FilePath -> IO ()
putStrLn FilePath
banner)
  Config -> IO Config
forall a. a -> IO a
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"
       FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"All Rights Reserved.\n"

restOC :: Config -> RESTOrdering
restOC :: Config -> RESTOrdering
restOC Config
cfg = FilePath -> RESTOrdering
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 Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1

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