-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | k-induction for Copilot.
--   
--   Some tools to prove properties on Copilot programs with k-induction
--   model checking.
@package copilot-theorem
@version 2.2.0

module Copilot.Theorem.Prove
data Output
Output :: Status -> [String] -> Output
data Status
Sat :: Status
Valid :: Status
Invalid :: Status
Unknown :: Status
Error :: Status
data Prover
Prover :: String -> (Spec -> IO r) -> (r -> [PropId] -> [PropId] -> IO Output) -> (r -> IO ()) -> Prover
[proverName] :: Prover -> String
[startProver] :: Prover -> Spec -> IO r
[askProver] :: Prover -> r -> [PropId] -> [PropId] -> IO Output
[closeProver] :: Prover -> r -> IO ()
type PropId = String
data PropRef a
PropRef :: PropId -> PropRef a
type Proof a = ProofScheme a ()
type UProof = Writer [Action] ()
data ProofScheme a b
Proof :: Writer [Action] b -> ProofScheme a b
data Action
Check :: Prover -> Action
Assume :: PropId -> Action
Admit :: Action
data Universal
data Existential
check :: Prover -> Proof a
prove :: Spec -> PropId -> UProof -> IO Bool
instance GHC.Base.Functor (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.Base.Applicative (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.Base.Monad (Copilot.Theorem.Prove.ProofScheme a)

module Copilot.Theorem.Prover.SMT

-- | Tactics
data Options
Options :: Word32 -> Word32 -> Bool -> Options
[startK] :: Options -> Word32
[maxK] :: Options -> Word32
[debug] :: Options -> Bool
induction :: SmtFormat a => Options -> Backend a -> Proof Universal
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal

-- | Backends
yices :: Backend SmtLib
dReal :: Backend SmtLib
altErgo :: Backend SmtLib
metit :: String -> Backend Tptp
z3 :: Backend SmtLib
cvc4 :: Backend SmtLib
mathsat :: Backend SmtLib
data Backend a
class Show a => SmtFormat a
data SmtLib
data Tptp
instance GHC.Classes.Eq Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Classes.Ord Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Show.Show Copilot.Theorem.Prover.SMT.SolverId
instance Data.Default.Class.Default Copilot.Theorem.Prover.SMT.Options

module Copilot.Theorem.Prover.Z3

-- | Tactics
data Options
Options :: Bool -> Word32 -> Word32 -> Bool -> Options
[nraNLSat] :: Options -> Bool
[startK] :: Options -> Word32
[maxK] :: Options -> Word32
[debug] :: Options -> Bool
induction :: Options -> Proof Universal
kInduction :: Options -> Proof Universal
onlySat :: Options -> Proof Existential
onlyValidity :: Options -> Proof Universal
instance GHC.Classes.Eq Copilot.Theorem.Prover.Z3.SolverId
instance GHC.Classes.Ord Copilot.Theorem.Prover.Z3.SolverId
instance GHC.Show.Show Copilot.Theorem.Prover.Z3.SolverId
instance Data.Default.Class.Default Copilot.Theorem.Prover.Z3.Options
instance (Language.SMTLib2.Internals.SMTBackend b m, Control.Monad.IO.Class.MonadIO m) => Language.SMTLib2.Internals.SMTBackend (Copilot.Theorem.Prover.Z3.DebugBackend b) m

module Copilot.Theorem.Kind2.Prover
data Options
Options :: Int -> Options
[bmcMax] :: Options -> Int
kind2Prover :: Options -> Prover
instance Data.Default.Class.Default Copilot.Theorem.Kind2.Prover.Options

module Copilot.Theorem.Kind2

module Copilot.Theorem
type Proof a = ProofScheme a ()
type PropId = String
data PropRef a
data Universal
data Existential