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

Documentation.SBV.Examples.ADT.Param

Description

A basic parameterized expression ADT example.

Synopsis

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

Documentation

data Expr nm val Source #

A basic arithmetic expression type.

Constructors

Val val
Var nm
Add (Expr nm val) (Expr nm val)
Mul (Expr nm val) (Expr nm val)
Let nm (Expr nm val) (Expr nm val)

Instances

Instances details

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

cv2Expr :: (SymVal nm, SymVal val) => String -> [CV] -> Expr nm val Source #

Conversion from SMT values to Expr values.

_undefiner_Expr :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SExpr nm val = SBV (Expr nm val) Source #

Symbolic version of the type Expr.

sVal :: (SymVal nm, SymVal val) => SBV val -> SBV (Expr nm val) Source #

Symbolic version of the constructor Val.

sVar :: (SymVal nm, SymVal val) => SBV nm -> SBV (Expr nm val) Source #

Symbolic version of the constructor Var.

sAdd :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Add.

sMul :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Mul.

sLet :: (SymVal nm, SymVal val) => SBV nm -> SBV (Expr nm val) -> SBV (Expr nm val) -> SBV (Expr nm val) Source #

Symbolic version of the constructor Let.

isVal :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

isVar :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

isAdd :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

isMul :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

isLet :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBool Source #

Field recognizer predicate.

getVal_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV val Source #

Field accessor function.

getVar_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm Source #

Field accessor function.

getAdd_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getAdd_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getMul_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getMul_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getLet_1 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV nm Source #

Field accessor function.

getLet_2 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

getLet_3 :: (SymVal nm, SymVal val) => SBV (Expr nm val) -> SBV (Expr nm val) Source #

Field accessor function.

sCaseExpr :: (Mergeable result, SymVal nm, SymVal val) => SBV (Expr nm val) -> (SBV val -> result) -> (SBV nm -> result) -> (SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> (SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> (SBV nm -> SBV (Expr nm val) -> SBV (Expr nm val) -> result) -> result Source #

Case analyzer for the type Expr.

isValid :: (SymVal nm, Eq nm, SymVal val) => (SBV nm -> SBool) -> SExpr nm val -> SBool Source #

Validity: We require each variable appearing to be an identifier to satisfy the predicate given. 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 :: (SymVal nm, SymVal val, Num (SBV val)) => SExpr nm val -> SBV val Source #

Evaluate an expression.

evalPlus5 :: IO ThmResult Source #

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

isId :: SString -> SBool Source #

Is this a string identifier? Lowercase letter followed by any number of upeer-lower case letters nd digits.

evalSat :: IO SatResult Source #

A simple sat result example.

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

genE :: IO SatResult Source #

Another test, generating some (mildly) interesting examples.

>>> genE
Satisfiable. Model:
  e1 =                      Let "s" (Val 6) (Val 3) :: Expr String Integer
  e2 = Let "h" (Val (-1)) (Add (Var "h") (Var "h")) :: Expr String Integer

queryE :: IO () Source #

Query mode example.

>>> queryE
e1: (let p = (-3 * -1) in (1 * p))
e2: -2
e3: (let q = 96 % 97 in q)