Safe Haskell	Trustworthy
Language	Haskell2010

Copilot.Theorem.Prover.SMT

Synopsis

class Default a where
- def :: a
data Options = Options {
- startK :: Word32
- maxK :: Word32
- debug :: 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
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

Documentation

class Default a where #

A class for types with a default value.

Minimal complete definition

Nothing

Methods

def :: a #

The default value for this type.

Instances

Instances details

Default Double
Instance details Defined in Data.Default.Class Methods def :: Double #
Default Float
Instance details Defined in Data.Default.Class Methods def :: Float #
Default Int
Instance details Defined in Data.Default.Class Methods def :: Int #
Default Int8
Instance details Defined in Data.Default.Class Methods def :: Int8 #
Default Int16
Instance details Defined in Data.Default.Class Methods def :: Int16 #
Default Int32
Instance details Defined in Data.Default.Class Methods def :: Int32 #
Default Int64
Instance details Defined in Data.Default.Class Methods def :: Int64 #
Default Integer
Instance details Defined in Data.Default.Class Methods def :: Integer #
Default Ordering
Instance details Defined in Data.Default.Class Methods def :: Ordering #
Default Word
Instance details Defined in Data.Default.Class Methods def :: Word #
Default Word8
Instance details Defined in Data.Default.Class Methods def :: Word8 #
Default Word16
Instance details Defined in Data.Default.Class Methods def :: Word16 #
Default Word32
Instance details Defined in Data.Default.Class Methods def :: Word32 #
Default Word64
Instance details Defined in Data.Default.Class Methods def :: Word64 #
Default ()
Instance details Defined in Data.Default.Class Methods def :: () #
Default All
Instance details Defined in Data.Default.Class Methods def :: All #
Default Any
Instance details Defined in Data.Default.Class Methods def :: Any #
Default CShort
Instance details Defined in Data.Default.Class Methods def :: CShort #
Default CUShort
Instance details Defined in Data.Default.Class Methods def :: CUShort #
Default CInt
Instance details Defined in Data.Default.Class Methods def :: CInt #
Default CUInt
Instance details Defined in Data.Default.Class Methods def :: CUInt #
Default CLong
Instance details Defined in Data.Default.Class Methods def :: CLong #
Default CULong
Instance details Defined in Data.Default.Class Methods def :: CULong #
Default CLLong
Instance details Defined in Data.Default.Class Methods def :: CLLong #
Default CULLong
Instance details Defined in Data.Default.Class Methods def :: CULLong #
Default CFloat
Instance details Defined in Data.Default.Class Methods def :: CFloat #
Default CDouble
Instance details Defined in Data.Default.Class Methods def :: CDouble #
Default CPtrdiff
Instance details Defined in Data.Default.Class Methods def :: CPtrdiff #
Default CSize
Instance details Defined in Data.Default.Class Methods def :: CSize #
Default CSigAtomic
Instance details Defined in Data.Default.Class Methods def :: CSigAtomic #
Default CClock
Instance details Defined in Data.Default.Class Methods def :: CClock #
Default CTime
Instance details Defined in Data.Default.Class Methods def :: CTime #
Default CUSeconds
Instance details Defined in Data.Default.Class Methods def :: CUSeconds #
Default CSUSeconds
Instance details Defined in Data.Default.Class Methods def :: CSUSeconds #
Default CIntPtr
Instance details Defined in Data.Default.Class Methods def :: CIntPtr #
Default CUIntPtr
Instance details Defined in Data.Default.Class Methods def :: CUIntPtr #
Default CIntMax
Instance details Defined in Data.Default.Class Methods def :: CIntMax #
Default CUIntMax
Instance details Defined in Data.Default.Class Methods def :: CUIntMax #
Default Options Source #
Instance details Defined in Copilot.Theorem.Prover.SMT Methods def :: Options #
Default Options Source #
Instance details Defined in Copilot.Theorem.Kind2.Prover Methods def :: Options #
Default [a]
Instance details Defined in Data.Default.Class Methods def :: [a] #
Default (Maybe a)
Instance details Defined in Data.Default.Class Methods def :: Maybe a #
Integral a => Default (Ratio a)
Instance details Defined in Data.Default.Class Methods def :: Ratio a #
Default a => Default (IO a)
Instance details Defined in Data.Default.Class Methods def :: IO a #
(Default a, RealFloat a) => Default (Complex a)
Instance details Defined in Data.Default.Class Methods def :: Complex a #
Default (First a)
Instance details Defined in Data.Default.Class Methods def :: First a #
Default (Last a)
Instance details Defined in Data.Default.Class Methods def :: Last a #
Default a => Default (Dual a)
Instance details Defined in Data.Default.Class Methods def :: Dual a #
Default (Endo a)
Instance details Defined in Data.Default.Class Methods def :: Endo a #
Num a => Default (Sum a)
Instance details Defined in Data.Default.Class Methods def :: Sum a #
Num a => Default (Product a)
Instance details Defined in Data.Default.Class Methods def :: Product a #
Default r => Default (e -> r)
Instance details Defined in Data.Default.Class Methods def :: e -> r #
(Default a, Default b) => Default (a, b)
Instance details Defined in Data.Default.Class Methods def :: (a, b) #
(Default a, Default b, Default c) => Default (a, b, c)
Instance details Defined in Data.Default.Class Methods def :: (a, b, c) #
(Default a, Default b, Default c, Default d) => Default (a, b, c, d)
Instance details Defined in Data.Default.Class Methods def :: (a, b, c, d) #
(Default a, Default b, Default c, Default d, Default e) => Default (a, b, c, d, e)
Instance details Defined in Data.Default.Class Methods def :: (a, b, c, d, e) #
(Default a, Default b, Default c, Default d, Default e, Default f) => Default (a, b, c, d, e, f)
Instance details Defined in Data.Default.Class Methods def :: (a, b, c, d, e, f) #
(Default a, Default b, Default c, Default d, Default e, Default f, Default g) => Default (a, b, c, d, e, f, g)
Instance details Defined in Data.Default.Class Methods def :: (a, b, c, d, e, f, g) #

data Options Source #

Tactics

Constructors

Options
Fields startK :: Word32 maxK :: Word32 debug :: Bool

Instances

Instances details

Default Options Source #
Instance details Defined in Copilot.Theorem.Prover.SMT Methods def :: Options #

induction :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential Source #

onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal Source #

yices :: Backend SmtLib Source #

Backends

dReal :: Backend SmtLib Source #

altErgo :: Backend SmtLib Source #

metit :: String -> Backend Tptp Source #

z3 :: Backend SmtLib Source #

cvc4 :: Backend SmtLib Source #

mathsat :: Backend SmtLib Source #

data Backend a Source #

class Show a => SmtFormat a Source #

Minimal complete definition

push, pop, checkSat, setLogic, declFun, assert

Instances

Instances details

SmtFormat SmtLib Source #
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods push :: SmtLib pop :: SmtLib checkSat :: SmtLib setLogic :: String -> SmtLib declFun :: String -> Type -> [Type] -> SmtLib assert :: Expr -> SmtLib
SmtFormat Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods push :: Tptp pop :: Tptp checkSat :: Tptp setLogic :: String -> Tptp declFun :: String -> Type -> [Type] -> Tptp assert :: Expr -> Tptp

data SmtLib Source #

Instances

Instances details

Show SmtLib Source #
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods showsPrec :: Int -> SmtLib -> ShowS # show :: SmtLib -> String # showList :: [SmtLib] -> ShowS #
SmtFormat SmtLib Source #
Instance details Defined in Copilot.Theorem.Prover.SMTLib Methods push :: SmtLib pop :: SmtLib checkSat :: SmtLib setLogic :: String -> SmtLib declFun :: String -> Type -> [Type] -> SmtLib assert :: Expr -> SmtLib

data Tptp Source #

Instances

Instances details

Show Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods showsPrec :: Int -> Tptp -> ShowS # show :: Tptp -> String # showList :: [Tptp] -> ShowS #
SmtFormat Tptp Source #
Instance details Defined in Copilot.Theorem.Prover.TPTP Methods push :: Tptp pop :: Tptp checkSat :: Tptp setLogic :: String -> Tptp declFun :: String -> Type -> [Type] -> Tptp assert :: Expr -> Tptp