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

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

  , getOpts

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

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

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

  , queryFile
) where

import Data.Serialize                (Serialize (..))
import Control.Monad
import GHC.Generics
import System.Console.CmdArgs
import System.Console.CmdArgs.Explicit
import System.Environment

import Language.Fixpoint.Utils.Files


--------------------------------------------------------------------------------
withPragmas :: Config -> [String] -> IO Config
--------------------------------------------------------------------------------
withPragmas :: Config -> [String] -> IO Config
withPragmas = (Config -> String -> IO Config) -> Config -> [String] -> IO Config
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Config -> String -> IO Config
withPragma

withPragma :: Config -> String -> IO Config
withPragma :: Config -> String -> IO Config
withPragma Config
c String
s = [String] -> IO Config -> IO Config
forall a. [String] -> IO a -> IO a
withArgs [String
s] (IO Config -> IO Config) -> IO Config -> IO Config
forall a b. (a -> b) -> a -> b
$ Mode (CmdArgs Config) -> IO Config
forall a. Mode (CmdArgs a) -> IO a
cmdArgsRun
          Mode (CmdArgs Config)
config { modeValue :: CmdArgs Config
modeValue = (Mode (CmdArgs Config) -> CmdArgs Config
forall a. Mode a -> a
modeValue Mode (CmdArgs Config)
config) { cmdArgsValue :: Config
cmdArgsValue = Config
c } }

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

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

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


data Config = Config
  { Config -> String
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 -> 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
oldPLE           :: Bool           -- ^ Use old version of PLE
  , Config -> Bool
noIncrPle        :: Bool           -- ^ Use incremental PLE
  , Config -> [Integer]
checkCstr        :: [Integer]      -- ^ Only check these specific constraints 
  , Config -> Bool
extensionality   :: Bool           -- ^ Enable extensional interpretation of function equality
  , Config -> Maybe Int
maxRWOrderingConstraints :: Maybe Int
  , Config -> Bool
rwTerminationCheck     :: Bool
  } deriving (Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
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
DataType
Constr
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 -> DataType
Config -> Constr
(forall b. Data b => b -> b) -> Config -> Config
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Config -> c Config
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cConfig :: Constr
$tConfig :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Config -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Config -> u
gmapQ :: (forall d. Data d => d -> u) -> Config -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Config -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Config
Data,Typeable,Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
(Int -> Config -> ShowS)
-> (Config -> String) -> ([Config] -> ShowS) -> Show Config
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Config] -> ShowS
$cshowList :: [Config] -> ShowS
show :: Config -> String
$cshow :: Config -> String
showsPrec :: Int -> Config -> ShowS
$cshowsPrec :: Int -> 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
$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 SMTSolver = Z3 | Cvc4 | Mathsat
                 deriving (SMTSolver -> SMTSolver -> Bool
(SMTSolver -> SMTSolver -> Bool)
-> (SMTSolver -> SMTSolver -> Bool) -> Eq SMTSolver
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
DataType
Constr
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 -> DataType
SMTSolver -> Constr
(forall b. Data b => b -> b) -> SMTSolver -> SMTSolver
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTSolver -> c SMTSolver
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cMathsat :: Constr
$cCvc4 :: Constr
$cZ3 :: Constr
$tSMTSolver :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> SMTSolver -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTSolver -> u
gmapQ :: (forall d. Data d => d -> u) -> SMTSolver -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTSolver -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable 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
$cto :: forall x. Rep SMTSolver x -> SMTSolver
$cfrom :: forall x. SMTSolver -> Rep SMTSolver x
Generic)

instance Default SMTSolver where
  def :: SMTSolver
def = SMTSolver
Z3

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

---------------------------------------------------------------------------------------
-- | 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
/= :: Eliminate -> Eliminate -> Bool
$c/= :: Eliminate -> Eliminate -> Bool
== :: Eliminate -> Eliminate -> Bool
$c== :: Eliminate -> Eliminate -> Bool
Eq, Typeable Eliminate
DataType
Constr
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 -> DataType
Eliminate -> Constr
(forall b. Data b => b -> b) -> Eliminate -> Eliminate
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Eliminate -> c Eliminate
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cExistentials :: Constr
$cHorn :: Constr
$cAll :: Constr
$cSome :: Constr
$cNone :: Constr
$tEliminate :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Eliminate -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Eliminate -> u
gmapQ :: (forall d. Data d => d -> u) -> Eliminate -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Eliminate -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable 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
$cto :: forall x. Rep Eliminate x -> Eliminate
$cfrom :: forall x. Eliminate -> Rep Eliminate x
Generic)

instance Serialize Eliminate

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

instance Show Eliminate where
  show :: Eliminate -> String
show Eliminate
None = String
"none"
  show Eliminate
Some = String
"some"
  show Eliminate
All  = String
"all"
  show Eliminate
Horn  = String
"horn"
  show Eliminate
Existentials  = String
"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 :: String
-> Maybe Int
-> Int
-> Int
-> SMTSolver
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Eliminate
-> Maybe Int
-> Maybe Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> [Integer]
-> Bool
-> Maybe Int
-> Bool
-> Config
Config {
    srcFile :: String
srcFile                  = String
"out"   String -> Ann -> String
forall val. Data val => val -> Ann -> val
&= Ann
args    String -> Ann -> String
forall val. Data val => val -> Ann -> val
&= Ann
typFile
  , defunction :: Bool
defunction               = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"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
&= String -> Ann
help String
"Name of SMT Solver"
  , linear :: Bool
linear                   = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use uninterpreted integer multiplication and division"
  , stringTheory :: Bool
stringTheory             = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Interpretation of String Theory by SMT"
  , allowHO :: Bool
allowHO                  = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow higher order binders into fixpoint environment"
  , allowHOqs :: Bool
allowHOqs                = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow higher order qualifiers"
  , eliminate :: Eliminate
eliminate                = Eliminate
None    Eliminate -> Ann -> Eliminate
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]"
  , elimBound :: Maybe Int
elimBound                = Maybe Int
forall a. Maybe a
Nothing Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"elimBound"   Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"(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
&= String -> Ann
name String
"smtTimeout"  Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"smt timeout in msec"
  , elimStats :: Bool
elimStats                = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"(alpha) Print eliminate stats"
  , solverStats :: Bool
solverStats              = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print solver stats"
  , save :: Bool
save                     = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Save Query as .fq and .bfq files"
  , metadata :: Bool
metadata                 = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print meta-data associated with constraints"
  , stats :: Bool
stats                    = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Compute constraint statistics"
  , etaElim :: Bool
etaElim                  = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"eta elimination in function definition"
  , parts :: Bool
parts                    = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"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
&= String -> Ann
help String
"(numeric) Number of threads to use"
  , minPartSize :: Int
minPartSize              = Int
defaultMinPartSize Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"(numeric) Minimum partition size when solving in parallel"
  , maxPartSize :: Int
maxPartSize              = Int
defaultMaxPartSize Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"(numeric) Maximum partiton size when solving in parallel."
  , minimize :: Bool
minimize                 = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"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
&= String -> Ann
help String
"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
&= String -> Ann
help String
"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
&= String -> Ann
help String
"Shrink fixpoint by removing implied qualifiers"
  , gradual :: Bool
gradual                  = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Solve gradual-refinement typing constraints"
  , ginteractive :: Bool
ginteractive             = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Interactive Gradual Solving"
  , autoKuts :: Bool
autoKuts                 = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Ignore given Kut vars, compute from scratch"
  , nonLinCuts :: Bool
nonLinCuts               = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Treat non-linear kvars as cuts"
  , noslice :: Bool
noslice                  = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable non-concrete KVar slicing"
  , rewriteAxioms :: Bool
rewriteAxioms            = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"allow axiom instantiation via rewriting"
  , oldPLE :: Bool
oldPLE                   = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use old version of PLE"
  , noIncrPle :: Bool
noIncrPle                = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't use incremental PLE"
  , checkCstr :: [Integer]
checkCstr                = []    [Integer] -> Ann -> [Integer]
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Only check these specific constraint-ids" 
  , extensionality :: Bool
extensionality           = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow extensional interpretation of extensionality"
  , maxRWOrderingConstraints :: Maybe Int
maxRWOrderingConstraints = Maybe Int
forall a. Maybe a
Nothing Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Maximum number of functions to consider in rewrite orderings"
  , rwTerminationCheck :: Bool
rwTerminationCheck       = Bool
False   Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable rewrite divergence checker"
  }
  Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= Ann
verbosity
  Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= String -> Ann
program String
"fixpoint"
  Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= String -> Ann
help    String
"Predicate Abstraction Based Horn-Clause Solver"
  Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= String -> Ann
summary String
"fixpoint Copyright 2009-15 Regents of the University of California."
  Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= [String] -> Ann
details [ String
"Predicate Abstraction Based Horn-Clause Solver"
             , String
""
             , String
"To check a file foo.fq type:"
             , String
"  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
             String -> IO ()
putStrLn String
banner
             Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return Config
md

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

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 -> String
queryFile Ext
e = Ext -> ShowS
extFileName Ext
e ShowS -> (Config -> String) -> Config -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> String
srcFile