Bit-vectors over nullables, typed

Each lifted operator has its plain counterpart's signature with an Option around every argument and around the result, and nothing else changed. The lift is strict: none unless every argument is some.

Only the non-indexed operators lift: bvExtract, bvRepeat and the other indexed ones have no lifted form.

def Cvc.Typed.Term.bvUdiv? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvUdiv lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUdiv? rgt = Cvc.Untyped.Term.bvUdiv? lft rgt

def Cvc.Typed.Term.bvXor? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvXor lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvXor? rgt = Cvc.Untyped.Term.bvXor? lft rgt

def Cvc.Typed.Term.bvXnor? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvXnor lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvXnor? rgt = Cvc.Untyped.Term.bvXnor? lft rgt

def Cvc.Typed.Term.bvSgt? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSgt lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSgt? rgt = Cvc.Untyped.Term.bvSgt? lft rgt

def Cvc.Typed.Term.bvComp? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec 1)))

bvComp lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvComp? rgt = Cvc.Untyped.Term.bvComp? lft rgt

def Cvc.Typed.Term.bvNor? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvNor lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvNor? rgt = Cvc.Untyped.Term.bvNor? lft rgt

def Cvc.Typed.Term.bvRedor? [Ω] {n : Nat} (bv : Term (Option (BitVec n))) : Env (Term (Option (BitVec 1)))

bvRedor lifted over nullables, strictly: none unless every argument is some.

Equations

• bv.bvRedor? = Cvc.Untyped.Term.bvRedor? bv

def Cvc.Typed.Term.bvUaddo? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvUaddo lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUaddo? rgt = Cvc.Untyped.Term.bvUaddo? lft rgt

def Cvc.Typed.Term.bvSaddo? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSaddo lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSaddo? rgt = Cvc.Untyped.Term.bvSaddo? lft rgt

def Cvc.Typed.Term.bvNot? [Ω] {n : Nat} (bv : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvNot lifted over nullables, strictly: none unless every argument is some.

Equations

• bv.bvNot? = Cvc.Untyped.Term.bvNot? bv

def Cvc.Typed.Term.bvUge? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvUge lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUge? rgt = Cvc.Untyped.Term.bvUge? lft rgt

def Cvc.Typed.Term.bvUgt? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvUgt lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUgt? rgt = Cvc.Untyped.Term.bvUgt? lft rgt

def Cvc.Typed.Term.bvSdiv? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvSdiv lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSdiv? rgt = Cvc.Untyped.Term.bvSdiv? lft rgt

def Cvc.Typed.Term.bvSlt? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSlt lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSlt? rgt = Cvc.Untyped.Term.bvSlt? lft rgt

def Cvc.Typed.Term.bvUlt? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvUlt lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUlt? rgt = Cvc.Untyped.Term.bvUlt? lft rgt

def Cvc.Typed.Term.bvAnd? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvAnd lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvAnd? rgt = Cvc.Untyped.Term.bvAnd? lft rgt

def Cvc.Typed.Term.bvAdd? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvAdd lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvAdd? rgt = Cvc.Untyped.Term.bvAdd? lft rgt

def Cvc.Typed.Term.bvSmulo? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSmulo lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSmulo? rgt = Cvc.Untyped.Term.bvSmulo? lft rgt

def Cvc.Typed.Term.bvSbvToInt? [Ω] {n : Nat} (bv : Term (Option (BitVec n))) : Env (Term (Option Int))

bvSbvToInt lifted over nullables, strictly: none unless every argument is some.

Equations

• bv.bvSbvToInt? = Cvc.Untyped.Term.bvSbvToInt? bv

def Cvc.Typed.Term.bvOr? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvOr lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvOr? rgt = Cvc.Untyped.Term.bvOr? lft rgt

def Cvc.Typed.Term.bvNand? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvNand lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvNand? rgt = Cvc.Untyped.Term.bvNand? lft rgt

def Cvc.Typed.Term.bvUsubo? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvUsubo lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUsubo? rgt = Cvc.Untyped.Term.bvUsubo? lft rgt

def Cvc.Typed.Term.bvConcat? [Ω] {n m : Nat} (lft : Term (Option (BitVec n))) (rgt : Term (Option (BitVec m))) : Env (Term (Option (BitVec (n + m))))

bvConcat lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvConcat? rgt = Cvc.Untyped.Term.bvConcat? lft rgt

def Cvc.Typed.Term.bvAshr? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvAshr lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvAshr? rgt = Cvc.Untyped.Term.bvAshr? lft rgt

def Cvc.Typed.Term.bvSub? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvSub lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSub? rgt = Cvc.Untyped.Term.bvSub? lft rgt

def Cvc.Typed.Term.bvNego? [Ω] {n : Nat} (bv : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvNego lifted over nullables, strictly: none unless every argument is some.

Equations

• bv.bvNego? = Cvc.Untyped.Term.bvNego? bv

def Cvc.Typed.Term.bvUle? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvUle lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUle? rgt = Cvc.Untyped.Term.bvUle? lft rgt

def Cvc.Typed.Term.bvUrem? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvUrem lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUrem? rgt = Cvc.Untyped.Term.bvUrem? lft rgt

def Cvc.Typed.Term.bvNeg? [Ω] {n : Nat} (bv : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvNeg lifted over nullables, strictly: none unless every argument is some.

Equations

• bv.bvNeg? = Cvc.Untyped.Term.bvNeg? bv

def Cvc.Typed.Term.bvIte? [Ω] {n : Nat} (cnd : Term (Option (BitVec 1))) (thn els : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvIte lifted over nullables, strictly: none unless every argument is some.

Equations

• cnd.bvIte? thn els = Cvc.Untyped.Term.bvIte? cnd thn els

def Cvc.Typed.Term.bvSrem? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvSrem lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSrem? rgt = Cvc.Untyped.Term.bvSrem? lft rgt

def Cvc.Typed.Term.bvRedand? [Ω] {n : Nat} (bv : Term (Option (BitVec n))) : Env (Term (Option (BitVec 1)))

bvRedand lifted over nullables, strictly: none unless every argument is some.

Equations

• bv.bvRedand? = Cvc.Untyped.Term.bvRedand? bv

def Cvc.Typed.Term.bvSdivo? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSdivo lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSdivo? rgt = Cvc.Untyped.Term.bvSdivo? lft rgt

def Cvc.Typed.Term.bvUltbv? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec 1)))

bvUltbv lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUltbv? rgt = Cvc.Untyped.Term.bvUltbv? lft rgt

def Cvc.Typed.Term.bvSsubo? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSsubo lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSsubo? rgt = Cvc.Untyped.Term.bvSsubo? lft rgt

def Cvc.Typed.Term.bvSmod? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvSmod lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSmod? rgt = Cvc.Untyped.Term.bvSmod? lft rgt

def Cvc.Typed.Term.bvShl? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvShl lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvShl? rgt = Cvc.Untyped.Term.bvShl? lft rgt

def Cvc.Typed.Term.bvMul? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvMul lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvMul? rgt = Cvc.Untyped.Term.bvMul? lft rgt

def Cvc.Typed.Term.bvUmulo? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvUmulo lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvUmulo? rgt = Cvc.Untyped.Term.bvUmulo? lft rgt

def Cvc.Typed.Term.bvSle? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSle lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSle? rgt = Cvc.Untyped.Term.bvSle? lft rgt

def Cvc.Typed.Term.bvSge? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option Bool))

bvSge lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSge? rgt = Cvc.Untyped.Term.bvSge? lft rgt

def Cvc.Typed.Term.bvLshr? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec n)))

bvLshr lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvLshr? rgt = Cvc.Untyped.Term.bvLshr? lft rgt

def Cvc.Typed.Term.bvSltbv? [Ω] {n : Nat} (lft rgt : Term (Option (BitVec n))) : Env (Term (Option (BitVec 1)))

bvSltbv lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.bvSltbv? rgt = Cvc.Untyped.Term.bvSltbv? lft rgt

def Cvc.Typed.Term.bvUbvToInt? [Ω] {n : Nat} (bv : Term (Option (BitVec n))) : Env (Term (Option Int))

bvUbvToInt lifted over nullables, strictly: none unless every argument is some.

Equations

• bv.bvUbvToInt? = Cvc.Untyped.Term.bvUbvToInt? bv