Testable SBool | |
Boolean SBool | |
BVDivisible SInteger | |
BVDivisible SInt64 | |
BVDivisible SInt32 | |
BVDivisible SInt16 | |
BVDivisible SInt8 | |
BVDivisible SWord64 | |
BVDivisible SWord32 | |
BVDivisible SWord16 | |
BVDivisible SWord8 | |
FromBits SInt64 | |
FromBits SInt32 | |
FromBits SInt16 | |
FromBits SInt8 | |
FromBits SWord64 | |
FromBits SWord32 | |
FromBits SWord16 | |
FromBits SWord8 | |
FromBits SBool | |
Polynomial SWord64 | |
Polynomial SWord32 | |
Polynomial SWord16 | |
Polynomial SWord8 | |
Provable SBool | |
Provable Predicate | |
SignCast SWord64 SInt64 | |
SignCast SWord32 SInt32 | |
SignCast SWord16 SInt16 | |
SignCast SWord8 SInt8 | |
Splittable SWord64 SWord32 | |
Splittable SWord32 SWord16 | |
Splittable SWord16 SWord8 | |
(SymWord a, Bounded a) => Bounded (SBV a) | |
(Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) | |
Eq (SBV a) | |
(Ord a, Num a, SymWord a) => Num (SBV a) | |
Show (SBV a) | |
Testable (Symbolic SBool) | |
(SymWord a, Arbitrary a) => Arbitrary (SBV a) | |
(Bits a, SymWord a) => Bits (SBV a) | |
NFData a => NFData (SBV a) | |
(Random a, SymWord a) => Random (SBV a) | |
Outputtable (SBV a) | |
HasSignAndSize a => HasSignAndSize (SBV a) | |
HasSignAndSize a => Uninterpreted (SBV a) | |
SymWord a => Mergeable (SBV a) | |
SymWord a => OrdSymbolic (SBV a) | |
EqSymbolic (SBV a) | |
(SymWord a, PrettyNum a) => PrettyNum (SBV a) | |
(SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) | |
(SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) | |
(SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) | |
(SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) | |
(SymWord b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) | |
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) | |
(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) | |
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) | |
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) | |
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) | |
(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) | |
(SymWord a, EqSymbolic z) => Equality (SBV a -> z) | |
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) | |
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) | |
(SymWord a, Provable p) => Provable (SBV a -> p) | |