Orphan instances

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r)) Source #

pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (IntN l) -> Term (IntN r) Source #

pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (IntN n) -> Term (IntN w) Source #

sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (IntN l) -> SBVType n (IntN r) -> SBVType n (IntN (l + r)) Source #

sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (IntN l) -> SBVType n (IntN r) Source #

sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (IntN n) -> SBVType int (IntN w) Source #

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r)) Source #

pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (WordN l) -> Term (WordN r) Source #

pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (WordN n) -> Term (WordN w) Source #

sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (WordN l) -> SBVType n (WordN r) -> SBVType n (WordN (l + r)) Source #

sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (WordN l) -> SBVType n (WordN r) Source #

sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (WordN n) -> SBVType int (WordN w) Source #

Methods

pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n) Source #

pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n) Source #

withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)), Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) => r) -> r Source #

sbvToSigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o WordN -> p n -> q integerBitwidth -> SBVType integerBitwidth (WordN n) -> SBVType integerBitwidth (IntN n) Source #

sbvToUnsigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o IntN -> p n -> q integerBitwidth -> SBVType integerBitwidth (IntN n) -> SBVType integerBitwidth (WordN n) Source #