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

Documentation.SBV.Examples.ADT.Expr

Description

A basic expression ADT example.

Synopsis

data Expr
- = Val Integer
- | Var String
- | Add Expr Expr
- | Mul Expr Expr
- | Let String Expr Expr
cv2Expr :: String -> [CV] -> Expr
_undefiner_Expr :: a
type SExpr = SBV Expr
sVal :: SBV Integer -> SBV Expr
sVar :: SBV [Char] -> SBV Expr
sAdd :: SBV Expr -> SBV Expr -> SBV Expr
sMul :: SBV Expr -> SBV Expr -> SBV Expr
sLet :: SBV [Char] -> SBV Expr -> SBV Expr -> SBV Expr
isVal :: SBV Expr -> SBool
isVar :: SBV Expr -> SBool
isAdd :: SBV Expr -> SBool
isMul :: SBV Expr -> SBool
isLet :: SBV Expr -> SBool
getVal_1 :: SBV Expr -> SBV Integer
getVar_1 :: SBV Expr -> SBV [Char]
getAdd_1 :: SBV Expr -> SBV Expr
getAdd_2 :: SBV Expr -> SBV Expr
getMul_1 :: SBV Expr -> SBV Expr
getMul_2 :: SBV Expr -> SBV Expr
getLet_1 :: SBV Expr -> SBV [Char]
getLet_2 :: SBV Expr -> SBV Expr
getLet_3 :: SBV Expr -> SBV Expr
sCaseExpr :: Mergeable result => SBV Expr -> (SBV Integer -> result) -> (SBV [Char] -> result) -> (SBV Expr -> SBV Expr -> result) -> (SBV Expr -> SBV Expr -> result) -> (SBV [Char] -> SBV Expr -> SBV Expr -> result) -> result
isValid :: SExpr -> SBool
eval :: SExpr -> SInteger
evalPlus5 :: IO ThmResult
evalSat :: IO SatResult
genE :: IO SatResult
queryE :: IO ()

Documentation

data Expr Source #

A basic arithmetic expression type.

Constructors

Val Integer
Var String
Add Expr Expr
Mul Expr Expr
Let String Expr Expr

Instances

Instances details

Arbitrary Expr Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods arbitrary :: Gen Expr # shrink :: Expr -> [Expr] #
Num Expr Source #	Num instance, simplifies construction of values
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods (+) :: Expr -> Expr -> Expr # (-) :: Expr -> Expr -> Expr # (*) :: Expr -> Expr -> Expr # negate :: Expr -> Expr # abs :: Expr -> Expr # signum :: Expr -> Expr # fromInteger :: Integer -> Expr #
Num SExpr Source #	Num instance for the symbolic version
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods (+) :: SExpr -> SExpr -> SExpr # (-) :: SExpr -> SExpr -> SExpr # (*) :: SExpr -> SExpr -> SExpr # negate :: SExpr -> SExpr # abs :: SExpr -> SExpr # signum :: SExpr -> SExpr # fromInteger :: Integer -> SExpr #
Show Expr Source #	Show instance for `Expr`.
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
SymVal Expr Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Expr) Source # mkSymValInit :: State -> SBV Expr -> IO () Source # literal :: Expr -> SBV Expr Source # fromCV :: CV -> Expr Source # isConcretely :: SBV Expr -> (Expr -> Bool) -> Bool Source # minMaxBound :: Maybe (Expr, Expr) Source # free :: MonadSymbolic m => String -> m (SBV Expr) Source # free_ :: MonadSymbolic m => m (SBV Expr) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Expr] Source # symbolic :: MonadSymbolic m => String -> m (SBV Expr) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Expr] Source # unliteral :: SBV Expr -> Maybe Expr Source # unlitCV :: SBV Expr -> Maybe (Kind, CVal) Source # isConcrete :: SBV Expr -> Bool Source # isSymbolic :: SBV Expr -> Bool Source #
HasKind Expr Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods kindOf :: Expr -> Kind Source # hasSign :: Expr -> Bool Source # intSizeOf :: Expr -> Int Source # isBoolean :: Expr -> Bool Source # isBounded :: Expr -> Bool Source # isReal :: Expr -> Bool Source # isFloat :: Expr -> Bool Source # isDouble :: Expr -> Bool Source # isRational :: Expr -> Bool Source # isFP :: Expr -> Bool Source # isUnbounded :: Expr -> Bool Source # isADT :: Expr -> Bool Source # isChar :: Expr -> Bool Source # isString :: Expr -> Bool Source # isList :: Expr -> Bool Source # isSet :: Expr -> Bool Source # isTuple :: Expr -> Bool Source # isArray :: Expr -> Bool Source # isRoundingMode :: Expr -> Bool Source # isUninterpreted :: Expr -> Bool Source # showType :: Expr -> String Source #
HasInductionSchema (Forall ta Expr -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods inductionSchema :: (Forall ta Expr -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Expr -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods inductionSchema :: (Forall ta Expr -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods inductionSchema :: (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods inductionSchema :: (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods inductionSchema :: (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Expr Methods inductionSchema :: (Forall ta Expr -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Expr :: String -> [CV] -> Expr Source #

Conversion from SMT values to Expr values.

_undefiner_Expr :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SExpr = SBV Expr Source #

Symbolic version of the type Expr.

sVal :: SBV Integer -> SBV Expr Source #

Symbolic version of the constructor Val.

sVar :: SBV [Char] -> SBV Expr Source #

Symbolic version of the constructor Var.

sAdd :: SBV Expr -> SBV Expr -> SBV Expr Source #

Symbolic version of the constructor Add.

sMul :: SBV Expr -> SBV Expr -> SBV Expr Source #

Symbolic version of the constructor Mul.

sLet :: SBV [Char] -> SBV Expr -> SBV Expr -> SBV Expr Source #

Symbolic version of the constructor Let.

isVal :: SBV Expr -> SBool Source #

Field recognizer predicate.

isVar :: SBV Expr -> SBool Source #

Field recognizer predicate.

isAdd :: SBV Expr -> SBool Source #

Field recognizer predicate.

isMul :: SBV Expr -> SBool Source #

Field recognizer predicate.

isLet :: SBV Expr -> SBool Source #

Field recognizer predicate.

getVal_1 :: SBV Expr -> SBV Integer Source #

Field accessor function.

getVar_1 :: SBV Expr -> SBV [Char] Source #

Field accessor function.

getAdd_1 :: SBV Expr -> SBV Expr Source #

Field accessor function.

getAdd_2 :: SBV Expr -> SBV Expr Source #

Field accessor function.

getMul_1 :: SBV Expr -> SBV Expr Source #

Field accessor function.

getMul_2 :: SBV Expr -> SBV Expr Source #

Field accessor function.

getLet_1 :: SBV Expr -> SBV [Char] Source #

Field accessor function.

getLet_2 :: SBV Expr -> SBV Expr Source #

Field accessor function.

getLet_3 :: SBV Expr -> SBV Expr Source #

Field accessor function.

sCaseExpr :: Mergeable result => SBV Expr -> (SBV Integer -> result) -> (SBV [Char] -> result) -> (SBV Expr -> SBV Expr -> result) -> (SBV Expr -> SBV Expr -> result) -> (SBV [Char] -> SBV Expr -> SBV Expr -> result) -> result Source #

Case analyzer for the type Expr.

isValid :: SExpr -> SBool Source #

Validity: We require each variable appearing to be an identifier (lowercase letter followed by any number of upper-lower case letters and digits), and all expressions are closed; i.e., any variable referenced is introduced by an enclosing let expression.

eval :: SExpr -> SInteger Source #

Evaluate an expression.

evalPlus5 :: IO ThmResult Source #

A basic theorem about eval. >>> evalPlus5 Q.E.D.

evalSat :: IO SatResult Source #

A simple sat result example.

>>> evalSat
Satisfiable. Model:
  e = Let "k" (Val 1) (Var "k") :: Expr
  a =                         9 :: Integer
  b =                        10 :: Integer

genE :: IO SatResult Source #

Another test, generating some (mildly) interesting examples.

>>> genE
Satisfiable. Model:
  e1 = Let "p" (Val 5) (Val 3) :: Expr
  e2 =                Val (-2) :: Expr

queryE :: IO () Source #

Query mode example.

>>> queryE
e1: (let p = 5 in 3)
e2: -2