    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs             #-}
    {-# LANGUAGE LambdaCase        #-}
    {-# LANGUAGE NamedFieldPuns    #-}
    {-# LANGUAGE RankNTypes        #-}
    {-# LANGUAGE Trustworthy       #-}

    -- | Connections to various SMT solvers and theorem provers.
    module Copilot.Theorem.Prover.SMT
      (

        -- * Backends
        Backend
      , SmtFormat
      , SmtLib
      , Tptp
      , yices, dReal, altErgo, metit, z3, cvc4, mathsat

        -- * Tactics
      , Options (..)
      , induction, kInduction, onlySat, onlyValidity

        -- * Auxiliary
      , module Data.Default
      ) where

    import Copilot.Theorem.IL.Translate
    import Copilot.Theorem.IL
    import Copilot.Theorem.Prove (Output (..), check, Proof, Universal, Existential)
    import qualified Copilot.Theorem.Prove as P

    import Copilot.Theorem.Prover.Backend
    import qualified Copilot.Theorem.Prover.SMTIO as SMT

    import Copilot.Theorem.Prover.SMTLib (SmtLib)
    import Copilot.Theorem.Prover.TPTP (Tptp)
    import qualified Copilot.Theorem.Prover.SMTLib as SMTLib
    import qualified Copilot.Theorem.Prover.TPTP as TPTP

    import Control.Monad (msum, unless, mzero)
    import Control.Monad.State (StateT, runStateT, lift, get, modify)
    import Control.Monad.IO.Class (liftIO)
    import Control.Monad.Trans.Maybe (MaybeT (..))

    import Data.Word
    import Data.Maybe (fromJust, fromMaybe)
    import Data.Function (on)
    import Data.Default (Default(..))
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Copilot.Theorem.Misc.Utils

    import System.IO (hClose)

    -- * Tactics

    -- | Options to configure the provers.
    data Options = Options
      { Options -> Word32
    startK :: Word32
        -- ^ Initial @k@ for the k-induction algorithm.

      , Options -> Word32
    maxK :: Word32
        -- ^ The maximum number of steps of the k-induction algorithm the prover runs
        -- before giving up.

      , Options -> Bool
    debug :: Bool
        -- ^ If @debug@ is set to @True@, the SMTLib/TPTP queries produced by the
        -- prover are displayed in the standard output.
      }

    -- | Default 'Options' with a @0@ @k@ and a max of @10@ steps, and that produce
    -- no debugging info.
    instance Default Options where
      def :: Options
    def = Options
        { startK :: Word32
    startK = Word32
    0
        , maxK :: Word32
    maxK   = Word32
    10
        , debug :: Bool
    debug  = Bool
    False
        }

    -- | Tactic to find only a proof of satisfiability.
    onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
    onlySat :: forall a. SmtFormat a => Options -> Backend a -> Proof Existential
    onlySat Options
    opts Backend a
    backend = Prover -> Proof Existential
    forall a. Prover -> Proof a
    check P.Prover
      { proverName :: PropId
    P.proverName  = PropId
    "OnlySat"
      , startProver :: Spec -> IO (ProofState a)
    P.startProver = ProofState a -> IO (ProofState a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProofState a -> IO (ProofState a))
    -> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Options
    -> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
    forall b.
    Options
    -> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
    ProofState Options
    opts Backend a
    backend Map SolverId (Solver a)
    forall k a. Map k a
    Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Spec -> IL
    translateWithBounds
      , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
    P.askProver   = ProofState a -> [PropId] -> [PropId] -> IO Output
    forall b.
    SmtFormat b =>
    ProofState b -> [PropId] -> [PropId] -> IO Output
    onlySat'
      , closeProver :: ProofState a -> IO ()
    P.closeProver = IO () -> ProofState a -> IO ()
    forall a b. a -> b -> a
    const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      }

    -- | Tactic to find only a proof of validity.
    onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
    onlyValidity :: forall a. SmtFormat a => Options -> Backend a -> Proof Universal
    onlyValidity Options
    opts Backend a
    backend = Prover -> Proof Universal
    forall a. Prover -> Proof a
    check P.Prover
      { proverName :: PropId
    P.proverName  = PropId
    "OnlyValidity"
      , startProver :: Spec -> IO (ProofState a)
    P.startProver = ProofState a -> IO (ProofState a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProofState a -> IO (ProofState a))
    -> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Options
    -> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
    forall b.
    Options
    -> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
    ProofState Options
    opts Backend a
    backend Map SolverId (Solver a)
    forall k a. Map k a
    Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Spec -> IL
    translateWithBounds
      , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
    P.askProver   = ProofState a -> [PropId] -> [PropId] -> IO Output
    forall b.
    SmtFormat b =>
    ProofState b -> [PropId] -> [PropId] -> IO Output
    onlyValidity'
      , closeProver :: ProofState a -> IO ()
    P.closeProver = IO () -> ProofState a -> IO ()
    forall a b. a -> b -> a
    const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      }

    -- | Tactic to find a proof by standard 1-induction.
    --
    -- The values for @startK@ and @maxK@ in the options are ignored.
    induction :: SmtFormat a => Options -> Backend a -> Proof Universal
    induction :: forall a. SmtFormat a => Options -> Backend a -> Proof Universal
    induction Options
    opts Backend a
    backend = Prover -> Proof Universal
    forall a. Prover -> Proof a
    check P.Prover
      { proverName :: PropId
    P.proverName  = PropId
    "Induction"
      , startProver :: Spec -> IO (ProofState a)
    P.startProver = ProofState a -> IO (ProofState a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProofState a -> IO (ProofState a))
    -> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Options
    -> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
    forall b.
    Options
    -> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
    ProofState Options
    opts Backend a
    backend Map SolverId (Solver a)
    forall k a. Map k a
    Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Spec -> IL
    translateWithBounds
      , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
    P.askProver   = Word32
    -> Word32 -> ProofState a -> [PropId] -> [PropId] -> IO Output
    forall b.
    SmtFormat b =>
    Word32
    -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
    kInduction' Word32
    0 Word32
    0
      , closeProver :: ProofState a -> IO ()
    P.closeProver = IO () -> ProofState a -> IO ()
    forall a b. a -> b -> a
    const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      }

    -- | Tactic to find a proof by k-induction.
    kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
    kInduction :: forall a. SmtFormat a => Options -> Backend a -> Proof Universal
    kInduction Options
    opts Backend a
    backend = Prover -> Proof Universal
    forall a. Prover -> Proof a
    check P.Prover
      { proverName :: PropId
    P.proverName  = PropId
    "K-Induction"
      , startProver :: Spec -> IO (ProofState a)
    P.startProver = ProofState a -> IO (ProofState a)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProofState a -> IO (ProofState a))
    -> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Options
    -> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
    forall b.
    Options
    -> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
    ProofState Options
    opts Backend a
    backend Map SolverId (Solver a)
    forall k a. Map k a
    Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Spec -> IL
    translateWithBounds
      , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
    P.askProver   = Word32
    -> Word32 -> ProofState a -> [PropId] -> [PropId] -> IO Output
    forall b.
    SmtFormat b =>
    Word32
    -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
    kInduction' (Options -> Word32
    startK Options
    opts) (Options -> Word32
    maxK Options
    opts)
      , closeProver :: ProofState a -> IO ()
    P.closeProver = IO () -> ProofState a -> IO ()
    forall a b. a -> b -> a
    const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      }

    -- * Backends

    -- | Backend to the Yices 2 SMT solver.
    --
    -- It enables non-linear arithmetic (@QF_NRA@), which means MCSat will be used.
    --
    -- The command @yices-smt2@ must be in the user's @PATH@.
    yices :: Backend SmtLib
    yices :: Backend SmtLib
    yices = Backend
      { name :: PropId
    name            = PropId
    "Yices"
      , cmd :: PropId
    cmd             = PropId
    "yices-smt2"
      , cmdOpts :: [PropId]
    cmdOpts         = [PropId
    "--incremental"]
      , inputTerminator :: Handle -> IO ()
    inputTerminator = IO () -> Handle -> IO ()
    forall a b. a -> b -> a
    const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      , incremental :: Bool
    incremental     = Bool
    True
      , logic :: PropId
    logic           = PropId
    "QF_NRA"
      , interpret :: PropId -> Maybe SatResult
    interpret       = PropId -> Maybe SatResult
    SMTLib.interpret
      }

    -- | Backend to the cvc4 SMT solver.
    --
    -- It enables support for uninterpreted functions and mixed nonlinear
    -- arithmetic (@QF_NIRA@).
    --
    -- The command @cvc4@ must be in the user's @PATH@.
    cvc4 :: Backend SmtLib
    cvc4 :: Backend SmtLib
    cvc4 = Backend
      { name :: PropId
    name            = PropId
    "CVC4"
      , cmd :: PropId
    cmd             = PropId
    "cvc4"
      , cmdOpts :: [PropId]
    cmdOpts         = [PropId
    "--incremental", PropId
    "--lang=smt2", PropId
    "--tlimit-per=5000"]
      , inputTerminator :: Handle -> IO ()
    inputTerminator = IO () -> Handle -> IO ()
    forall a b. a -> b -> a
    const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      , incremental :: Bool
    incremental     = Bool
    True
      , logic :: PropId
    logic           = PropId
    "QF_UFNIRA"
      , interpret :: PropId -> Maybe SatResult
    interpret       = PropId -> Maybe SatResult
    SMTLib.interpret
      }

    -- | Backend to the Alt-Ergo SMT solver.
    --
    -- It enables support for uninterpreted functions and mixed nonlinear
    -- arithmetic (@QF_NIRA@).
    --
    -- The command @alt-ergo.opt@ must be in the user's @PATH@.
    altErgo :: Backend SmtLib
    altErgo :: Backend SmtLib
    altErgo = Backend
      { name :: PropId
    name            = PropId
    "Alt-Ergo"
      , cmd :: PropId
    cmd             = PropId
    "alt-ergo.opt"
      , cmdOpts :: [PropId]
    cmdOpts         = []
      , inputTerminator :: Handle -> IO ()
    inputTerminator = Handle -> IO ()
    hClose
      , incremental :: Bool
    incremental     = Bool
    False
      , logic :: PropId
    logic           = PropId
    "QF_UFNIRA"
      , interpret :: PropId -> Maybe SatResult
    interpret       = PropId -> Maybe SatResult
    SMTLib.interpret
      }

    -- | Backend to the Z3 theorem prover.
    --
    -- The command @z3@ must be in the user's @PATH@.
    z3 :: Backend SmtLib
    z3 :: Backend SmtLib
    z3 = Backend
      { name :: PropId
    name            = PropId
    "Z3"
      , cmd :: PropId
    cmd             = PropId
    "z3"
      , cmdOpts :: [PropId]
    cmdOpts         = [PropId
    "-smt2", PropId
    "-in"]
      , inputTerminator :: Handle -> IO ()
    inputTerminator = IO () -> Handle -> IO ()
    forall a b. a -> b -> a
    const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      , incremental :: Bool
    incremental     = Bool
    True
      , logic :: PropId
    logic           = PropId
    ""
      , interpret :: PropId -> Maybe SatResult
    interpret       = PropId -> Maybe SatResult
    SMTLib.interpret
      }

    -- | Backend to the dReal SMT solver.
    --
    -- It enables non-linear arithmetic (@QF_NRA@).
    --
    -- The libraries for dReal must be installed and @perl@ must be in the user's
    -- @PATH@.
    dReal :: Backend SmtLib
    dReal :: Backend SmtLib
    dReal = Backend
      { name :: PropId
    name            = PropId
    "dReal"
      , cmd :: PropId
    cmd             = PropId
    "perl"
      , cmdOpts :: [PropId]
    cmdOpts         = [PropId
    "-e", PropId
    "alarm 10; exec dReal"]
      , inputTerminator :: Handle -> IO ()
    inputTerminator = Handle -> IO ()
    hClose
      , incremental :: Bool
    incremental     = Bool
    False
      , logic :: PropId
    logic           = PropId
    "QF_NRA"
      , interpret :: PropId -> Maybe SatResult
    interpret       = PropId -> Maybe SatResult
    SMTLib.interpret
      }

    -- | Backend to the Mathsat SMT solver.
    --
    -- It enables non-linear arithmetic (@QF_NRA@).
    --
    -- The command @mathsat@ must be in the user's @PATH@.
    mathsat :: Backend SmtLib
    mathsat :: Backend SmtLib
    mathsat = Backend
      { name :: PropId
    name            = PropId
    "MathSAT"
      , cmd :: PropId
    cmd             = PropId
    "mathsat"
      , cmdOpts :: [PropId]
    cmdOpts         = []
      , inputTerminator :: Handle -> IO ()
    inputTerminator = IO () -> Handle -> IO ()
    forall a b. a -> b -> a
    const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
    forall a b. (a -> b) -> a -> b
    $ () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      , incremental :: Bool
    incremental     = Bool
    True
      , logic :: PropId
    logic           = PropId
    "QF_NRA"
      , interpret :: PropId -> Maybe SatResult
    interpret       = PropId -> Maybe SatResult
    SMTLib.interpret
      }

    -- | Backend to the MetiTaski theorem prover.
    --
    -- The command @metit@ must be in the user's @PATH@.
    --
    -- The argument string is the path to the @tptp@ subdirectory of the metitarski
    -- install location.
    metit :: String -> Backend Tptp
    metit :: PropId -> Backend Tptp
    metit PropId
    installDir = Backend
      { name :: PropId
    name            = PropId
    "MetiTarski"
      , cmd :: PropId
    cmd             = PropId
    "metit"
      , cmdOpts :: [PropId]
    cmdOpts         =
          [ PropId
    "--time", PropId
    "5"
          , PropId
    "--autoInclude"
          , PropId
    "--tptp", PropId
    installDir
          , PropId
    "/dev/stdin"
          ]
      , inputTerminator :: Handle -> IO ()
    inputTerminator = Handle -> IO ()
    hClose
      , incremental :: Bool
    incremental     = Bool
    False
      , logic :: PropId
    logic           = PropId
    ""
      , interpret :: PropId -> Maybe SatResult
    interpret       = PropId -> Maybe SatResult
    TPTP.interpret
      }

    -- | Checks the Copilot specification with k-induction

    type ProofScript b = MaybeT (StateT (ProofState b) IO)

    runPS :: ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
    runPS :: forall b a.
    ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
    runPS ProofScript b a
    ps = StateT (ProofState b) IO (Maybe a)
    -> ProofState b -> IO (Maybe a, ProofState b)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (ProofScript b a -> StateT (ProofState b) IO (Maybe a)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT ProofScript b a
    ps)

    data ProofState b = ProofState
      { forall b. ProofState b -> Options
    options :: Options
      , forall b. ProofState b -> Backend b
    backend :: Backend b
      , forall b. ProofState b -> Map SolverId (Solver b)
    solvers :: Map SolverId (SMT.Solver b)
      , forall b. ProofState b -> IL
    spec    :: IL
      }

    data SolverId = Base | Step
      deriving (Int -> SolverId -> ShowS
    [SolverId] -> ShowS
    SolverId -> PropId
    (Int -> SolverId -> ShowS)
    -> (SolverId -> PropId) -> ([SolverId] -> ShowS) -> Show SolverId
    forall a.
    (Int -> a -> ShowS) -> (a -> PropId) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SolverId -> ShowS
    showsPrec :: Int -> SolverId -> ShowS
    $cshow :: SolverId -> PropId
    show :: SolverId -> PropId
    $cshowList :: [SolverId] -> ShowS
    showList :: [SolverId] -> ShowS
    Show, Eq SolverId
    Eq SolverId =>
    (SolverId -> SolverId -> Ordering)
    -> (SolverId -> SolverId -> Bool)
    -> (SolverId -> SolverId -> Bool)
    -> (SolverId -> SolverId -> Bool)
    -> (SolverId -> SolverId -> Bool)
    -> (SolverId -> SolverId -> SolverId)
    -> (SolverId -> SolverId -> SolverId)
    -> Ord SolverId
    SolverId -> SolverId -> Bool
    SolverId -> SolverId -> Ordering
    SolverId -> SolverId -> SolverId
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SolverId -> SolverId -> Ordering
    compare :: SolverId -> SolverId -> Ordering
    $c< :: SolverId -> SolverId -> Bool
    < :: SolverId -> SolverId -> Bool
    $c<= :: SolverId -> SolverId -> Bool
    <= :: SolverId -> SolverId -> Bool
    $c> :: SolverId -> SolverId -> Bool
    > :: SolverId -> SolverId -> Bool
    $c>= :: SolverId -> SolverId -> Bool
    >= :: SolverId -> SolverId -> Bool
    $cmax :: SolverId -> SolverId -> SolverId
    max :: SolverId -> SolverId -> SolverId
    $cmin :: SolverId -> SolverId -> SolverId
    min :: SolverId -> SolverId -> SolverId
    Ord, SolverId -> SolverId -> Bool
    (SolverId -> SolverId -> Bool)
    -> (SolverId -> SolverId -> Bool) -> Eq SolverId
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SolverId -> SolverId -> Bool
    == :: SolverId -> SolverId -> Bool
    $c/= :: SolverId -> SolverId -> Bool
    /= :: SolverId -> SolverId -> Bool
    Eq)

    getModels :: [PropId] -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    getModels :: forall b.
    [PropId]
    -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    getModels [PropId]
    assumptionIds [PropId]
    toCheckIds = do
      IL {modelInit, modelRec, properties, inductive} <- ProofState b -> IL
    forall b. ProofState b -> IL
    spec (ProofState b -> IL)
    -> MaybeT (StateT (ProofState b) IO) (ProofState b)
    -> MaybeT (StateT (ProofState b) IO) IL
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (StateT (ProofState b) IO) (ProofState b)
    forall s (m :: * -> *). MonadState s m => m s
    get
      let (as, as')       = selectProps assumptionIds properties
          (as'', toCheck) = selectProps toCheckIds properties
          modelRec'       = [Expr]
    modelRec [Expr] -> [Expr] -> [Expr]
    forall a. [a] -> [a] -> [a]
    ++ [Expr]
    as [Expr] -> [Expr] -> [Expr]
    forall a. [a] -> [a] -> [a]
    ++ [Expr]
    as' [Expr] -> [Expr] -> [Expr]
    forall a. [a] -> [a] -> [a]
    ++ [Expr]
    as''
      return (modelInit, modelRec', toCheck, inductive)

    getSolver :: SmtFormat b => SolverId -> ProofScript b (SMT.Solver b)
    getSolver :: forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
    getSolver SolverId
    sid = do
      solvers <- ProofState b -> Map SolverId (Solver b)
    forall b. ProofState b -> Map SolverId (Solver b)
    solvers (ProofState b -> Map SolverId (Solver b))
    -> MaybeT (StateT (ProofState b) IO) (ProofState b)
    -> MaybeT (StateT (ProofState b) IO) (Map SolverId (Solver b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (StateT (ProofState b) IO) (ProofState b)
    forall s (m :: * -> *). MonadState s m => m s
    get
      case Map.lookup sid solvers of
        Maybe (Solver b)
    Nothing -> SolverId -> MaybeT (StateT (ProofState b) IO) (Solver b)
    forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
    startNewSolver SolverId
    sid
        Just Solver b
    solver -> Solver b -> MaybeT (StateT (ProofState b) IO) (Solver b)
    forall a. a -> MaybeT (StateT (ProofState b) IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Solver b
    solver

    setSolver :: SolverId -> SMT.Solver b -> ProofScript b ()
    setSolver :: forall b. SolverId -> Solver b -> ProofScript b ()
    setSolver SolverId
    sid Solver b
    solver =
      (StateT (ProofState b) IO () -> MaybeT (StateT (ProofState b) IO) ()
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT (ProofState b) IO ()
     -> MaybeT (StateT (ProofState b) IO) ())
    -> ((ProofState b -> ProofState b) -> StateT (ProofState b) IO ())
    -> (ProofState b -> ProofState b)
    -> MaybeT (StateT (ProofState b) IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProofState b -> ProofState b) -> StateT (ProofState b) IO ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify) ((ProofState b -> ProofState b)
     -> MaybeT (StateT (ProofState b) IO) ())
    -> (ProofState b -> ProofState b)
    -> MaybeT (StateT (ProofState b) IO) ()
    forall a b. (a -> b) -> a -> b
    $ \ProofState b
    s -> ProofState b
    s { solvers = Map.insert sid solver (solvers s) }

    deleteSolver :: SolverId -> ProofScript b ()
    deleteSolver :: forall b. SolverId -> ProofScript b ()
    deleteSolver SolverId
    sid =
      (StateT (ProofState b) IO () -> MaybeT (StateT (ProofState b) IO) ()
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT (ProofState b) IO ()
     -> MaybeT (StateT (ProofState b) IO) ())
    -> ((ProofState b -> ProofState b) -> StateT (ProofState b) IO ())
    -> (ProofState b -> ProofState b)
    -> MaybeT (StateT (ProofState b) IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ProofState b -> ProofState b) -> StateT (ProofState b) IO ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify) ((ProofState b -> ProofState b)
     -> MaybeT (StateT (ProofState b) IO) ())
    -> (ProofState b -> ProofState b)
    -> MaybeT (StateT (ProofState b) IO) ()
    forall a b. (a -> b) -> a -> b
    $ \ProofState b
    s -> ProofState b
    s { solvers = Map.delete sid (solvers s) }

    startNewSolver :: SmtFormat b => SolverId -> ProofScript b (SMT.Solver b)
    startNewSolver :: forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
    startNewSolver SolverId
    sid = do
      dbg <- (ProofState b -> Options
    forall b. ProofState b -> Options
    options (ProofState b -> Options)
    -> MaybeT (StateT (ProofState b) IO) (ProofState b)
    -> MaybeT (StateT (ProofState b) IO) Options
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (StateT (ProofState b) IO) (ProofState b)
    forall s (m :: * -> *). MonadState s m => m s
    get MaybeT (StateT (ProofState b) IO) Options
    -> (Options -> MaybeT (StateT (ProofState b) IO) Bool)
    -> MaybeT (StateT (ProofState b) IO) Bool
    forall a b.
    MaybeT (StateT (ProofState b) IO) a
    -> (a -> MaybeT (StateT (ProofState b) IO) b)
    -> MaybeT (StateT (ProofState b) IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Bool -> MaybeT (StateT (ProofState b) IO) Bool
    forall a. a -> MaybeT (StateT (ProofState b) IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> MaybeT (StateT (ProofState b) IO) Bool)
    -> (Options -> Bool)
    -> Options
    -> MaybeT (StateT (ProofState b) IO) Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Options -> Bool
    debug)
      backend <- backend <$> get
      s <- liftIO $ SMT.startNewSolver (show sid) dbg backend
      setSolver sid s
      return s

    declVars :: SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
    declVars :: forall b. SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
    declVars SolverId
    sid [VarDescr]
    vs = do
      s <- SolverId -> ProofScript b (Solver b)
    forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
    getSolver SolverId
    sid
      s' <- liftIO $ SMT.declVars s vs
      setSolver sid s'

    assume :: SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
    assume :: forall b. SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
    assume SolverId
    sid [Expr]
    cs = do
      s <- SolverId -> ProofScript b (Solver b)
    forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
    getSolver SolverId
    sid
      s' <- liftIO $ SMT.assume s cs
      setSolver sid s'

    entailed :: SmtFormat b => SolverId -> [Expr] -> ProofScript b SatResult
    entailed :: forall b.
    SmtFormat b =>
    SolverId -> [Expr] -> ProofScript b SatResult
    entailed SolverId
    sid [Expr]
    cs = do
      backend <- ProofState b -> Backend b
    forall b. ProofState b -> Backend b
    backend (ProofState b -> Backend b)
    -> MaybeT (StateT (ProofState b) IO) (ProofState b)
    -> MaybeT (StateT (ProofState b) IO) (Backend b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (StateT (ProofState b) IO) (ProofState b)
    forall s (m :: * -> *). MonadState s m => m s
    get
      s <- getSolver sid
      result <- liftIO $ SMT.entailed s cs
      unless (incremental backend) $ stop sid
      return result

    stop :: SmtFormat b => SolverId -> ProofScript b ()
    stop :: forall b. SmtFormat b => SolverId -> ProofScript b ()
    stop SolverId
    sid = do
      s <- SolverId -> ProofScript b (Solver b)
    forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
    getSolver SolverId
    sid
      deleteSolver sid
      liftIO $ SMT.stop s

    proofKind :: Integer -> String
    proofKind :: Integer -> PropId
    proofKind Integer
    0 = PropId
    "induction"
    proofKind Integer
    k = PropId
    "k-induction (k = " PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> PropId
    forall a. Show a => a -> PropId
    show Integer
    k PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ PropId
    ")"

    stopSolvers :: SmtFormat b => ProofScript b ()
    stopSolvers :: forall b. SmtFormat b => ProofScript b ()
    stopSolvers = do
      solvers <- ProofState b -> Map SolverId (Solver b)
    forall b. ProofState b -> Map SolverId (Solver b)
    solvers (ProofState b -> Map SolverId (Solver b))
    -> MaybeT (StateT (ProofState b) IO) (ProofState b)
    -> MaybeT (StateT (ProofState b) IO) (Map SolverId (Solver b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MaybeT (StateT (ProofState b) IO) (ProofState b)
    forall s (m :: * -> *). MonadState s m => m s
    get
      mapM_ stop (fst <$> Map.toList solvers)

    entailment :: SmtFormat b => SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
    entailment :: forall b.
    SmtFormat b =>
    SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
    entailment SolverId
    sid [Expr]
    assumptions [Expr]
    props = do
      SolverId -> [VarDescr] -> ProofScript b ()
    forall b. SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
    declVars SolverId
    sid ([VarDescr] -> ProofScript b ()) -> [VarDescr] -> ProofScript b ()
    forall a b. (a -> b) -> a -> b
    $ [VarDescr] -> [VarDescr]
    forall a. Ord a => [a] -> [a]
    nub' ([VarDescr] -> [VarDescr]) -> [VarDescr] -> [VarDescr]
    forall a b. (a -> b) -> a -> b
    $ [Expr] -> [VarDescr]
    getVars [Expr]
    assumptions [VarDescr] -> [VarDescr] -> [VarDescr]
    forall a. [a] -> [a] -> [a]
    ++ [Expr] -> [VarDescr]
    getVars [Expr]
    props
      SolverId -> [Expr] -> ProofScript b ()
    forall b. SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
    assume SolverId
    sid [Expr]
    assumptions
      SolverId -> [Expr] -> ProofScript b SatResult
    forall b.
    SmtFormat b =>
    SolverId -> [Expr] -> ProofScript b SatResult
    entailed SolverId
    sid [Expr]
    props

    getVars :: [Expr] -> [VarDescr]
    getVars :: [Expr] -> [VarDescr]
    getVars = (VarDescr -> VarDescr -> Ordering) -> [VarDescr] -> [VarDescr]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    nubBy' (PropId -> PropId -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (PropId -> PropId -> Ordering)
    -> (VarDescr -> PropId) -> VarDescr -> VarDescr -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` VarDescr -> PropId
    varName) ([VarDescr] -> [VarDescr])
    -> ([Expr] -> [VarDescr]) -> [Expr] -> [VarDescr]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> [VarDescr]) -> [Expr] -> [VarDescr]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Expr -> [VarDescr]
    getVars'
      where
        getVars' :: Expr -> [VarDescr]
        getVars' :: Expr -> [VarDescr]
    getVars' = \case
          ConstB Bool
    _             -> []
          ConstI Type
    _ Integer
    _           -> []
          ConstR Double
    _             -> []
          Ite Type
    _ Expr
    e1 Expr
    e2 Expr
    e3       -> Expr -> [VarDescr]
    getVars' Expr
    e1 [VarDescr] -> [VarDescr] -> [VarDescr]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [VarDescr]
    getVars' Expr
    e2 [VarDescr] -> [VarDescr] -> [VarDescr]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [VarDescr]
    getVars' Expr
    e3
          Op1 Type
    _ Op1
    _ Expr
    e            -> Expr -> [VarDescr]
    getVars' Expr
    e
          Op2 Type
    _ Op2
    _ Expr
    e1 Expr
    e2        -> Expr -> [VarDescr]
    getVars' Expr
    e1 [VarDescr] -> [VarDescr] -> [VarDescr]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [VarDescr]
    getVars' Expr
    e2
          SVal Type
    t PropId
    seq (Fixed Integer
    i) -> [PropId -> Type -> [Type] -> VarDescr
    VarDescr (PropId
    seq PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ PropId
    "_" PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> PropId
    forall a. Show a => a -> PropId
    show Integer
    i) Type
    t []]
          SVal Type
    t PropId
    seq (Var Integer
    i)   -> [PropId -> Type -> [Type] -> VarDescr
    VarDescr (PropId
    seq PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ PropId
    "_n" PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> PropId
    forall a. Show a => a -> PropId
    show Integer
    i) Type
    t []]
          FunApp Type
    t PropId
    name [Expr]
    args   -> [PropId -> Type -> [Type] -> VarDescr
    VarDescr PropId
    name Type
    t ((Expr -> Type) -> [Expr] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Type
    typeOf [Expr]
    args)]
                                  [VarDescr] -> [VarDescr] -> [VarDescr]
    forall a. [a] -> [a] -> [a]
    ++ (Expr -> [VarDescr]) -> [Expr] -> [VarDescr]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Expr -> [VarDescr]
    getVars' [Expr]
    args

    unknown :: ProofScript b a
    unknown :: forall b a. ProofScript b a
    unknown = MaybeT (StateT (ProofState b) IO) a
    forall a. MaybeT (StateT (ProofState b) IO) a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    unknown' :: String -> ProofScript b Output
    unknown' :: forall b. PropId -> ProofScript b Output
    unknown' PropId
    msg = Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a. a -> MaybeT (StateT (ProofState b) IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Output -> MaybeT (StateT (ProofState b) IO) Output)
    -> Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a b. (a -> b) -> a -> b
    $ Status -> [PropId] -> Output
    Output Status
    P.Unknown [PropId
    msg]

    invalid :: String -> ProofScript b Output
    invalid :: forall b. PropId -> ProofScript b Output
    invalid PropId
    msg = Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a. a -> MaybeT (StateT (ProofState b) IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Output -> MaybeT (StateT (ProofState b) IO) Output)
    -> Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a b. (a -> b) -> a -> b
    $ Status -> [PropId] -> Output
    Output Status
    P.Invalid [PropId
    msg]

    sat :: String -> ProofScript b Output
    sat :: forall b. PropId -> ProofScript b Output
    sat PropId
    msg = Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a. a -> MaybeT (StateT (ProofState b) IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Output -> MaybeT (StateT (ProofState b) IO) Output)
    -> Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a b. (a -> b) -> a -> b
    $ Status -> [PropId] -> Output
    Output Status
    P.Sat [PropId
    msg]

    valid :: String -> ProofScript b Output
    valid :: forall b. PropId -> ProofScript b Output
    valid PropId
    msg = Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a. a -> MaybeT (StateT (ProofState b) IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Output -> MaybeT (StateT (ProofState b) IO) Output)
    -> Output -> MaybeT (StateT (ProofState b) IO) Output
    forall a b. (a -> b) -> a -> b
    $ Status -> [PropId] -> Output
    Output Status
    P.Valid [PropId
    msg]

    kInduction' :: SmtFormat b => Word32 -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
    kInduction' :: forall b.
    SmtFormat b =>
    Word32
    -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
    kInduction' Word32
    startK Word32
    maxK ProofState b
    s [PropId]
    as [PropId]
    ps = (Output -> Maybe Output -> Output
    forall a. a -> Maybe a -> a
    fromMaybe (Status -> [PropId] -> Output
    Output Status
    P.Unknown [PropId
    "proof by k-induction failed"]) (Maybe Output -> Output)
    -> ((Maybe Output, ProofState b) -> Maybe Output)
    -> (Maybe Output, ProofState b)
    -> Output
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Output, ProofState b) -> Maybe Output
    forall a b. (a, b) -> a
    fst)
      ((Maybe Output, ProofState b) -> Output)
    -> IO (Maybe Output, ProofState b) -> IO Output
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProofScript b Output
    -> ProofState b -> IO (Maybe Output, ProofState b)
    forall b a.
    ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
    runPS ([ProofScript b Output] -> ProofScript b Output
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ((Integer -> ProofScript b Output)
    -> [Integer] -> [ProofScript b Output]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> ProofScript b Output
    induction [(Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger Word32
    startK) .. (Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger Word32
    maxK)]) ProofScript b Output
    -> MaybeT (StateT (ProofState b) IO) () -> ProofScript b Output
    forall a b.
    MaybeT (StateT (ProofState b) IO) a
    -> MaybeT (StateT (ProofState b) IO) b
    -> MaybeT (StateT (ProofState b) IO) a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* MaybeT (StateT (ProofState b) IO) ()
    forall b. SmtFormat b => ProofScript b ()
    stopSolvers) ProofState b
    s
      where
        induction :: Integer -> ProofScript b Output
    induction Integer
    k = do
          (modelInit, modelRec, toCheck, inductive) <- [PropId]
    -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    forall b.
    [PropId]
    -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    getModels [PropId]
    as [PropId]
    ps

          let base    = [SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    Fixed Integer
    i) Expr
    m | Expr
    m <- [Expr]
    modelRec, Integer
    i <- [Integer
    0 .. Integer
    k]]
              baseInv = [SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    Fixed Integer
    k) Expr
    m | Expr
    m <- [Expr]
    toCheck]

          let step    = [SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    forall a. Integral a => a -> SeqIndex
    _n_plus Integer
    i) Expr
    m | Expr
    m <- [Expr]
    modelRec, Integer
    i <- [Integer
    0 .. Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1]]
                        [Expr] -> [Expr] -> [Expr]
    forall a. [a] -> [a] -> [a]
    ++ [SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    forall a. Integral a => a -> SeqIndex
    _n_plus Integer
    i) Expr
    m | Expr
    m <- [Expr]
    toCheck, Integer
    i <- [Integer
    0 .. Integer
    k]]
              stepInv = [SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    forall a. Integral a => a -> SeqIndex
    _n_plus (Integer -> SeqIndex) -> Integer -> SeqIndex
    forall a b. (a -> b) -> a -> b
    $ Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) Expr
    m | Expr
    m <- [Expr]
    toCheck]

          entailment Base (modelInit ++ base) baseInv >>= \case
            SatResult
    Sat     -> PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    invalid (PropId -> ProofScript b Output) -> PropId -> ProofScript b Output
    forall a b. (a -> b) -> a -> b
    $ PropId
    "base case failed for " PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> PropId
    proofKind Integer
    k
            SatResult
    Unknown -> ProofScript b Output
    forall b a. ProofScript b a
    unknown
            SatResult
    Unsat   ->
              if Bool -> Bool
    not Bool
    inductive then PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    valid (PropId
    "proved without induction")
              else SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
    forall b.
    SmtFormat b =>
    SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
    entailment SolverId
    Step [Expr]
    step [Expr]
    stepInv ProofScript b SatResult
    -> (SatResult -> ProofScript b Output) -> ProofScript b Output
    forall a b.
    MaybeT (StateT (ProofState b) IO) a
    -> (a -> MaybeT (StateT (ProofState b) IO) b)
    -> MaybeT (StateT (ProofState b) IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                SatResult
    Sat     -> ProofScript b Output
    forall b a. ProofScript b a
    unknown
                SatResult
    Unknown -> ProofScript b Output
    forall b a. ProofScript b a
    unknown
                SatResult
    Unsat   -> PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    valid (PropId -> ProofScript b Output) -> PropId -> ProofScript b Output
    forall a b. (a -> b) -> a -> b
    $ PropId
    "proved with " PropId -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> PropId
    proofKind Integer
    k

    onlySat' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
    onlySat' :: forall b.
    SmtFormat b =>
    ProofState b -> [PropId] -> [PropId] -> IO Output
    onlySat' ProofState b
    s [PropId]
    as [PropId]
    ps = (Maybe Output -> Output
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Output -> Output)
    -> ((Maybe Output, ProofState b) -> Maybe Output)
    -> (Maybe Output, ProofState b)
    -> Output
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Output, ProofState b) -> Maybe Output
    forall a b. (a, b) -> a
    fst) ((Maybe Output, ProofState b) -> Output)
    -> IO (Maybe Output, ProofState b) -> IO Output
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProofScript b Output
    -> ProofState b -> IO (Maybe Output, ProofState b)
    forall b a.
    ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
    runPS (ProofScript b Output
    script ProofScript b Output
    -> MaybeT (StateT (ProofState b) IO) () -> ProofScript b Output
    forall a b.
    MaybeT (StateT (ProofState b) IO) a
    -> MaybeT (StateT (ProofState b) IO) b
    -> MaybeT (StateT (ProofState b) IO) a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* MaybeT (StateT (ProofState b) IO) ()
    forall b. SmtFormat b => ProofScript b ()
    stopSolvers) ProofState b
    s
      where
        script :: ProofScript b Output
    script  = do
          (modelInit, modelRec, toCheck, inductive) <- [PropId]
    -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    forall b.
    [PropId]
    -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    getModels [PropId]
    as [PropId]
    ps

          let base    = (Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    Fixed Integer
    0)) [Expr]
    modelRec
              baseInv = (Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    Fixed Integer
    0)) [Expr]
    toCheck

          if inductive
            then unknown' "proposition requires induction to prove."
            else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case
              SatResult
    Unsat   -> PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    invalid PropId
    "prop not satisfiable"
              SatResult
    Unknown -> PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    unknown' PropId
    "failed to find a satisfying model"
              SatResult
    Sat     -> PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    sat PropId
    "prop is satisfiable"

    onlyValidity' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
    onlyValidity' :: forall b.
    SmtFormat b =>
    ProofState b -> [PropId] -> [PropId] -> IO Output
    onlyValidity' ProofState b
    s [PropId]
    as [PropId]
    ps = (Maybe Output -> Output
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Output -> Output)
    -> ((Maybe Output, ProofState b) -> Maybe Output)
    -> (Maybe Output, ProofState b)
    -> Output
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Output, ProofState b) -> Maybe Output
    forall a b. (a, b) -> a
    fst) ((Maybe Output, ProofState b) -> Output)
    -> IO (Maybe Output, ProofState b) -> IO Output
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProofScript b Output
    -> ProofState b -> IO (Maybe Output, ProofState b)
    forall b a.
    ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
    runPS (ProofScript b Output
    script ProofScript b Output
    -> MaybeT (StateT (ProofState b) IO) () -> ProofScript b Output
    forall a b.
    MaybeT (StateT (ProofState b) IO) a
    -> MaybeT (StateT (ProofState b) IO) b
    -> MaybeT (StateT (ProofState b) IO) a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* MaybeT (StateT (ProofState b) IO) ()
    forall b. SmtFormat b => ProofScript b ()
    stopSolvers) ProofState b
    s
      where
        script :: ProofScript b Output
    script  = do
          (modelInit, modelRec, toCheck, inductive) <- [PropId]
    -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    forall b.
    [PropId]
    -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
    getModels [PropId]
    as [PropId]
    ps

          let base    = (Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    Fixed Integer
    0)) [Expr]
    modelRec
              baseInv = (Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (SeqIndex -> Expr -> Expr
    evalAt (Integer -> SeqIndex
    Fixed Integer
    0)) [Expr]
    toCheck

          if inductive
            then unknown' "proposition requires induction to prove."
            else entailment Base (modelInit ++ base) baseInv >>= \case
              SatResult
    Unsat   -> PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    valid PropId
    "proof by SMT solver"
              SatResult
    Unknown -> ProofScript b Output
    forall b a. ProofScript b a
    unknown
              SatResult
    Sat     -> PropId -> ProofScript b Output
    forall b. PropId -> ProofScript b Output
    invalid PropId
    "SMT solver found a counter-example."

    selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
    selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
    selectProps [PropId]
    propIds Map PropId ([Expr], Expr)
    properties =
      (([[Expr]], [Expr]) -> ([Expr], [Expr])
    forall {t :: * -> *} {a} {b}. Foldable t => (t [a], b) -> ([a], b)
    squash (([[Expr]], [Expr]) -> ([Expr], [Expr]))
    -> ([([Expr], Expr)] -> ([[Expr]], [Expr]))
    -> [([Expr], Expr)]
    -> ([Expr], [Expr])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [([Expr], Expr)] -> ([[Expr]], [Expr])
    forall a b. [(a, b)] -> ([a], [b])
    unzip) [([Expr]
    as, Expr
    p) | (PropId
    id, ([Expr]
    as, Expr
    p)) <- Map PropId ([Expr], Expr) -> [(PropId, ([Expr], Expr))]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map PropId ([Expr], Expr)
    properties, PropId
    id PropId -> [PropId] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [PropId]
    propIds]
        where
          squash :: (t [a], b) -> ([a], b)
    squash (t [a]
    a, b
    b) = (t [a] -> [a]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat t [a]
    a, b
    b)