xor package:what4

xor :: [Term] -> Term
what4 What4.Protocol.SMTLib2.Syntax
Xor of all terms
xor :: BVDomain w -> BVDomain w -> BVDomain w
what4 What4.Utils.BVDomain
xor :: Domain w -> Domain w -> Domain w
what4 What4.Utils.BVDomain.Bitwise What4.Utils.BVDomain.XOR
Xor :: Binop BaseBoolType BaseBoolType
what4 What4.Protocol.VerilogWriter.AST
module What4.Utils.BVDomain.XOR
what4
Provides an implementation of bitvector abstract domains optimized for performing XOR operations.
xorPred :: IsExprBuilder sym => sym -> Pred sym -> Pred sym -> IO (Pred sym)
what4 What4.Interface
Exclusive-or operation
xorToBitwiseDomain :: Domain w -> Domain w
what4 What4.Utils.BVDomain
bvXorBits :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
what4 What4.Interface
Bitwise logical exclusive or.
bvxor :: Term -> [Term] -> Term
what4 What4.Protocol.SMTLib2.Syntax
Bitvector exclusive or of all arguments.
bvXor :: SupportTermOps v => v -> v -> v
what4 What4.Protocol.SMTWriter
BVXor :: Binop (BaseBVType w) (BaseBVType w)
what4 What4.Protocol.VerilogWriter.AST
bvXor :: SWordBin
what4 What4.SWord
Bitwise logical exclusive or.
arithToXorDomain :: Domain w -> Domain w
what4 What4.Utils.BVDomain
asXorDomain :: BVDomain w -> Domain w
what4 What4.Utils.BVDomain
bitwiseToXorDomain :: Domain w -> Domain w
what4 What4.Utils.BVDomain
correct_arithToXorDomain :: NatRepr n -> (Domain n, Integer) -> Property
what4 What4.Utils.BVDomain
correct_asXorDomain :: NatRepr n -> (BVDomain n, Integer) -> Property
what4 What4.Utils.BVDomain
correct_bitwiseToXorDomain :: NatRepr n -> (Domain n, Integer) -> Property
what4 What4.Utils.BVDomain
correct_fromXorDomain :: NatRepr n -> (Domain n, Integer) -> Property
what4 What4.Utils.BVDomain
correct_xorToBitwiseDomain :: NatRepr n -> (Domain n, Integer) -> Property
what4 What4.Utils.BVDomain
fromXorDomain :: Domain w -> BVDomain w
what4 What4.Utils.BVDomain
BVDXor :: Integer -> Integer -> Integer -> Domain (w :: Nat)
what4 What4.Utils.BVDomain.XOR
BVDXor mask hi unknown represents a set of values where hi is a bitwise high bound, and unknown represents the bits whose values are not known. The value mask caches the value 2^w-1.