Searched refs:BaseBVType (Results 1 – 18 of 18) sorted by relevance
41 BVAnd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)42 BVOr :: Binop (WT.BaseBVType w) (WT.BaseBVType w)43 BVXor :: Binop (WT.BaseBVType w) (WT.BaseBVType w)44 BVAdd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)45 BVSub :: Binop (WT.BaseBVType w) (WT.BaseBVType w)46 BVMul :: Binop (WT.BaseBVType w) (WT.BaseBVType w)47 BVDiv :: Binop (WT.BaseBVType w) (WT.BaseBVType w)48 BVRem :: Binop (WT.BaseBVType w) (WT.BaseBVType w)49 BVPow :: Binop (WT.BaseBVType w) (WT.BaseBVType w)50 BVShiftL :: Binop (WT.BaseBVType w) (WT.BaseBVType w)[all …]
266 -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)271 -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)278 (EmptyCtx ::> BaseBVType w ::> BaseBVType w)286 (EmptyCtx ::> BaseBVType w ::> BaseBVType w)294 (EmptyCtx ::> BaseBVType w ::> BaseBVType w)302 (EmptyCtx ::> BaseBVType w ::> BaseBVType w)310 (EmptyCtx ::> BaseBVType w ::> BaseBVType w)318 (EmptyCtx ::> BaseBVType w ::> BaseBVType w)327 -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)343 -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)[all …]
1141 => !(e (BaseBVType w))1247 !(e (BaseBVType w)) ->1248 App e (BaseBVType w)1253 !(e (BaseBVType w)) ->1254 App e (BaseBVType w)1259 !(e (BaseBVType w)) ->1260 App e (BaseBVType w)1357 -> !(e (BaseBVType w))1363 -> !(e (BaseBVType w))1375 -> App e (BaseBVType w)[all …]
81 GroundValue (BaseBVType w) = BV.BV w
833 -> (NatRepr w -> BVExpr t w -> BVExpr t w -> App (Expr t) (BaseBVType w))3440 inSameBVSemiRing :: Expr t (BaseBVType w) -> Expr t (BaseBVType w) -> Maybe (Some SR.BVFlavorRepr)3610 BaseBVType (FloatInfoToBitWidth fi)
41 , BaseBVType124 | BaseBVType TypeNats.Nat constructor145 type BaseBVType = 'BaseBVType -- ^ @:: 'TypeNats.Nat' -> 'BaseType'@. type178 BaseBVRepr :: (1 <= w) => !(NatRepr w) -> BaseTypeRepr (BaseBVType w)216 -> BaseTypeRepr (BaseBVType (eb + sb))238 instance (1 <= w, KnownNat w) => KnownRepr BaseTypeRepr (BaseBVType w) where
36 (BaseArrayType (EmptyCtx ::> BaseBVType w) BaseBoolType))38 (BaseArrayType (EmptyCtx ::> BaseBVType w) tp))
77 ConcreteVal (BaseBVType w)103 fromConcreteBV :: ConcreteVal (BaseBVType w) -> BV.BV w
19 BVIndexLit :: (1 <= w) => !(NatRepr w) -> !(BV.BV w) -> IndexLit (BaseBVType w)
130 SemiRingBase (SemiRingBV fv w) = BaseBVType w
160 :: FloatInfoRepr fi -> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
251 type SymBV sym n = SymExpr sym (BaseBVType n)325 asBV :: e (BaseBVType w) -> Maybe (BV.BV w)330 unsignedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)334 signedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)363 bvWidth :: e (BaseBVType w) -> NatRepr w
320 W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::>321 W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32325 W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::>326 W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64510 … (EmptyCtx ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32)
170 TestTemplate (BaseBVType (eb + sb)) ->175 TestTemplate (BaseBVType (eb + sb))181 TestTemplate (BaseBVType w) ->189 TestTemplate (BaseBVType w)293 (TVar (knownRepr :: BaseTypeRepr (BaseBVType 32))))295 (TVar (knownRepr :: BaseTypeRepr (BaseBVType 32))))
102 calcBVIte :: ITETestCond -> CalcReturn (BaseBVType 16)
577 AbstractValue (BaseBVType w) = BVDomain w596 ConcreteValue (BaseBVType w) = Integer689 instance (1 <= w) => Abstractable (BaseBVType w) where
793 -> m (Maybe (GroundArray (Ctx.SingleCtx (BaseBVType w)) (BaseBVType v)))
171 BVTypeMap :: (1 <= w) => !(NatRepr w) -> TypeMap (BaseBVType w)2829 -> IO (Maybe (GroundArray (Ctx.SingleCtx (BaseBVType w)) (BaseBVType v)))