Bit-vectors over nullables, sort-erased

One lifted constructor per liftable operator, <id>?, each answering none unless every argument is some.

Only the non-indexed operators lift. An indexed one — bvExtract, bvRepeat and the rest — is applied through an Op carrying its indices, and mkNullableLift takes a Kind, so there is no way to express it.

def Cvc.Untyped.Term.bvSdiv? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSdiv? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SDIV #[lft, rgt]

def Cvc.Untyped.Term.bvComp? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvComp? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_COMP #[lft, rgt]

def Cvc.Untyped.Term.bvRedand? [Ω] (bv : Term) : Env Term

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

Equations

• bv.bvRedand? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_REDAND #[bv]

def Cvc.Untyped.Term.bvNand? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvNand? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_NAND #[lft, rgt]

def Cvc.Untyped.Term.bvUltbv? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUltbv? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_ULTBV #[lft, rgt]

def Cvc.Untyped.Term.bvConcat? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvConcat? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_CONCAT #[lft, rgt]

def Cvc.Untyped.Term.bvSmulo? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSmulo? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SMULO #[lft, rgt]

def Cvc.Untyped.Term.bvSub? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSub? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SUB #[lft, rgt]

def Cvc.Untyped.Term.bvSmod? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSmod? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SMOD #[lft, rgt]

def Cvc.Untyped.Term.bvNot? [Ω] (bv : Term) : Env Term

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

Equations

• bv.bvNot? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_NOT #[bv]

def Cvc.Untyped.Term.bvSge? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSge? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SGE #[lft, rgt]

def Cvc.Untyped.Term.bvUdiv? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUdiv? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_UDIV #[lft, rgt]

def Cvc.Untyped.Term.bvAnd? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvAnd? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_AND #[lft, rgt]

def Cvc.Untyped.Term.bvSgt? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSgt? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SGT #[lft, rgt]

def Cvc.Untyped.Term.bvXor? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvXor? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_XOR #[lft, rgt]

def Cvc.Untyped.Term.bvOr? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvOr? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_OR #[lft, rgt]

def Cvc.Untyped.Term.bvUle? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUle? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_ULE #[lft, rgt]

def Cvc.Untyped.Term.bvShl? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvShl? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SHL #[lft, rgt]

def Cvc.Untyped.Term.bvUge? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUge? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_UGE #[lft, rgt]

def Cvc.Untyped.Term.bvUlt? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUlt? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_ULT #[lft, rgt]

def Cvc.Untyped.Term.bvSbvToInt? [Ω] (bv : Term) : Env Term

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

Equations

• bv.bvSbvToInt? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SBV_TO_INT #[bv]

def Cvc.Untyped.Term.bvAshr? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvAshr? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_ASHR #[lft, rgt]

def Cvc.Untyped.Term.bvIte? [Ω] (cnd thn els : Term) : Env Term

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

Equations

• cnd.bvIte? thn els = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_ITE #[cnd, thn, els]

def Cvc.Untyped.Term.bvSaddo? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSaddo? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SADDO #[lft, rgt]

def Cvc.Untyped.Term.bvRedor? [Ω] (bv : Term) : Env Term

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

Equations

• bv.bvRedor? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_REDOR #[bv]

def Cvc.Untyped.Term.bvLshr? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvLshr? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_LSHR #[lft, rgt]

def Cvc.Untyped.Term.bvUgt? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUgt? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_UGT #[lft, rgt]

def Cvc.Untyped.Term.bvSsubo? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSsubo? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SSUBO #[lft, rgt]

def Cvc.Untyped.Term.bvSltbv? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSltbv? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SLTBV #[lft, rgt]

def Cvc.Untyped.Term.bvUaddo? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUaddo? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_UADDO #[lft, rgt]

def Cvc.Untyped.Term.bvSlt? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSlt? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SLT #[lft, rgt]

def Cvc.Untyped.Term.bvUbvToInt? [Ω] (bv : Term) : Env Term

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

Equations

• bv.bvUbvToInt? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_UBV_TO_INT #[bv]

def Cvc.Untyped.Term.bvNego? [Ω] (bv : Term) : Env Term

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

Equations

• bv.bvNego? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_NEGO #[bv]

def Cvc.Untyped.Term.bvUsubo? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUsubo? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_USUBO #[lft, rgt]

def Cvc.Untyped.Term.bvXnor? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvXnor? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_XNOR #[lft, rgt]

def Cvc.Untyped.Term.bvAdd? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvAdd? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_ADD #[lft, rgt]

def Cvc.Untyped.Term.bvNeg? [Ω] (bv : Term) : Env Term

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

Equations

• bv.bvNeg? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_NEG #[bv]

def Cvc.Untyped.Term.bvSdivo? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSdivo? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SDIVO #[lft, rgt]

def Cvc.Untyped.Term.bvSrem? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSrem? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SREM #[lft, rgt]

def Cvc.Untyped.Term.bvUrem? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUrem? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_UREM #[lft, rgt]

def Cvc.Untyped.Term.bvSle? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvSle? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_SLE #[lft, rgt]

def Cvc.Untyped.Term.bvUmulo? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvUmulo? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_UMULO #[lft, rgt]

def Cvc.Untyped.Term.bvMul? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvMul? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_MULT #[lft, rgt]

def Cvc.Untyped.Term.bvNor? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.bvNor? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BITVECTOR_NOR #[lft, rgt]