pub enum SpecOp {
Show 86 variants
Eq,
And,
Or,
Not,
Imp,
Add,
Sub,
Mul,
Lt,
Lte,
Gt,
Gte,
BVNot,
BVAnd,
BVOr,
BVXor,
BVNeg,
BVAdd,
BVSub,
BVMul,
BVUdiv,
BVUrem,
BVSdiv,
BVSrem,
BVShl,
BVLshr,
BVAshr,
BVUle,
BVUlt,
BVUgt,
BVUge,
BVSlt,
BVSle,
BVSgt,
BVSge,
BVSaddo,
Rotr,
Rotl,
Extract,
ZeroExt,
SignExt,
Concat,
Replicate,
FPEq,
FPNe,
FPLt,
FPGt,
FPLe,
FPGe,
FPPositiveInfinity,
FPNegativeInfinity,
FPPositiveZero,
FPNegativeZero,
FPNaN,
FPAdd,
FPSub,
FPMul,
FPDiv,
FPMin,
FPMax,
FPNeg,
FPCeil,
FPFloor,
FPSqrt,
FPTrunc,
FPNearest,
FPIsZero,
FPIsInfinite,
FPIsNaN,
FPIsNegative,
FPIsPositive,
Popcnt,
Clz,
Cls,
Rev,
ConvTo,
Int2BV,
BV2Nat,
ToFP,
ToFPUnsigned,
ToFPFromFP,
FPToUBV,
FPToSBV,
WidthOf,
If,
Switch,
}Expand description
An operation used to specify term semantics, similar to SMT-LIB syntax.
Variants§
Eq
And
Or
Not
Imp
Add
Sub
Mul
Lt
Lte
Gt
Gte
BVNot
BVAnd
BVOr
BVXor
BVNeg
BVAdd
BVSub
BVMul
BVUdiv
BVUrem
BVSdiv
BVSrem
BVShl
BVLshr
BVAshr
BVUle
BVUlt
BVUgt
BVUge
BVSlt
BVSle
BVSgt
BVSge
BVSaddo
Rotr
Rotl
Extract
ZeroExt
SignExt
Concat
Replicate
FPEq
FPNe
FPLt
FPGt
FPLe
FPGe
FPPositiveInfinity
FPNegativeInfinity
FPPositiveZero
FPNegativeZero
FPNaN
FPAdd
FPSub
FPMul
FPDiv
FPMin
FPMax
FPNeg
FPCeil
FPFloor
FPSqrt
FPTrunc
FPNearest
FPIsZero
FPIsInfinite
FPIsNaN
FPIsNegative
FPIsPositive
Popcnt
Clz
Cls
Rev
ConvTo
Int2BV
BV2Nat
ToFP
ToFPUnsigned
ToFPFromFP
FPToUBV
FPToSBV
WidthOf
If
Switch
Trait Implementations§
impl Eq for SpecOp
impl StructuralPartialEq for SpecOp
Auto Trait Implementations§
impl Freeze for SpecOp
impl RefUnwindSafe for SpecOp
impl Send for SpecOp
impl Sync for SpecOp
impl Unpin for SpecOp
impl UnsafeUnpin for SpecOp
impl UnwindSafe for SpecOp
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more