Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.KnuckleDragger.Basics

Description

Some basic KD usage.

Synopsis

trueIsProvable :: IO Proof
falseIsn'tProvable :: IO ()
largerIntegerExists :: IO Proof
data T
type ST = SBV T
forallConjunction :: IO Proof
existsDisjunction :: IO Proof
forallDisjunctionNot :: IO ()
existsConjunctionNot :: IO ()

Documentation

trueIsProvable :: IO Proof Source #

sTrue is provable.

We have:

>>> trueIsProvable
Lemma: true                             Q.E.D.
[Proven] true

falseIsn'tProvable :: IO () Source #

sFalse isn't provable.

We have:

>>> falseIsn'tProvable `catch` (\(_ :: SomeException) -> pure ())
Lemma: sFalse
*** Failed to prove sFalse.
Falsifiable

largerIntegerExists :: IO Proof Source #

Basic quantification example: For every integer, there's a larger integer.

We have: >>> largerIntegerExists Lemma: largerIntegerExists Q.E.D. [Proven] largerIntegerExists

data T Source #

Use an uninterpreted type for the domain

Instances

Instances details

Data T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Basics Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> T -> c T # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c T # toConstr :: T -> Constr # dataTypeOf :: T -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c T) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T) # gmapT :: (forall b. Data b => b -> b) -> T -> T # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r # gmapQ :: (forall d. Data d => d -> u) -> T -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> T -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> T -> m T # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> T -> m T # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> T -> m T #
Read T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Basics Methods readsPrec :: Int -> ReadS T # readList :: ReadS [T] # readPrec :: ReadPrec T # readListPrec :: ReadPrec [T] #
Show T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Basics Methods showsPrec :: Int -> T -> ShowS # show :: T -> String # showList :: [T] -> ShowS #
SymVal T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Basics Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV T) Source # literal :: T -> SBV T Source # fromCV :: CV -> T Source # isConcretely :: SBV T -> (T -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV T) Source # free_ :: MonadSymbolic m => m (SBV T) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV T] Source # symbolic :: MonadSymbolic m => String -> m (SBV T) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV T] Source # unliteral :: SBV T -> Maybe T Source # isConcrete :: SBV T -> Bool Source # isSymbolic :: SBV T -> Bool Source #
HasKind T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Basics Methods kindOf :: T -> Kind Source # hasSign :: T -> Bool Source # intSizeOf :: T -> Int Source # isBoolean :: T -> Bool Source # isBounded :: T -> Bool Source # isReal :: T -> Bool Source # isFloat :: T -> Bool Source # isDouble :: T -> Bool Source # isRational :: T -> Bool Source # isFP :: T -> Bool Source # isUnbounded :: T -> Bool Source # isUserSort :: T -> Bool Source # isChar :: T -> Bool Source # isString :: T -> Bool Source # isList :: T -> Bool Source # isSet :: T -> Bool Source # isTuple :: T -> Bool Source # isMaybe :: T -> Bool Source # isEither :: T -> Bool Source # isArray :: T -> Bool Source # showType :: T -> String Source #
SatModel T Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Basics Methods parseCVs :: [CV] -> Maybe (T, [CV]) Source # cvtModel :: (T -> Maybe b) -> Maybe (T, [CV]) -> Maybe (b, [CV]) Source #

type ST = SBV T Source #

Symbolic version of the type T.

forallConjunction :: IO Proof Source #

Pushing a universal through conjunction. We have:

>>> forallConjunction
Lemma: forallConjunction                Q.E.D.
[Proven] forallConjunction

existsDisjunction :: IO Proof Source #

Pushing an existential through disjunction. We have:

>>> existsDisjunction
Lemma: existsDisjunction                Q.E.D.
[Proven] existsDisjunction

forallDisjunctionNot :: IO () Source #

We cannot push a universal through a disjunction. We have:

>>> forallDisjunctionNot `catch` (\(_ :: SomeException) -> pure ())
Lemma: forallConjunctionNot
*** Failed to prove forallConjunctionNot.
Falsifiable. Counter-example:
  p :: T -> Bool
  p T_2 = True
  p T_0 = True
  p _   = False

  q :: T -> Bool
  q T_2 = False
  q T_0 = False
  q _   = True

Note how p assigns two selected values to True and everything else to False, while q does the exact opposite. So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds a model with two distinct values, as one would have sufficed. But it is still a valud model.)

existsConjunctionNot :: IO () Source #

We cannot push an existential through conjunction. We have:

>>> existsConjunctionNot `catch` (\(_ :: SomeException) -> pure ())
Lemma: existsConjunctionNot
*** Failed to prove existsConjunctionNot.
Falsifiable. Counter-example:
  p :: T -> Bool
  p T_1 = False
  p _   = True

  q :: T -> Bool
  q T_1 = True
  q _   = False

In this case, we again have a predicate That disagree at every point, providing a counter-example.