SMTStabilizer API
Public API documentation for SMTStabilizer
Loading...
Searching...
No Matches
Static Public Member Functions | List of all members
stabilizer::parser::BitVectorUtils Class Reference

Bitvector conversion and arithmetic helpers on SMT bitstring forms. More...

#include <util.h>

Static Public Member Functions

static Integer bvToNat (const std::string &bv)
 
static std::string natToBv (const Integer &i, const Integer &n)
 
static std::string natToBv (const std::string &i, const Integer &n)
 
static Integer bvToInt (const std::string &bv)
 
static std::string intToBv (const Integer &i, const Integer &n)
 
static std::string bvNot (const std::string &bv)
 
static std::string bvAnd (const std::string &bv1, const std::string &bv2)
 
static std::string bvOr (const std::string &bv1, const std::string &bv2)
 
static std::string bvXor (const std::string &bv1, const std::string &bv2)
 
static std::string bvNand (const std::string &bv1, const std::string &bv2)
 
static std::string bvNor (const std::string &bv1, const std::string &bv2)
 
static std::string bvXnor (const std::string &bv1, const std::string &bv2)
 
static std::string bvNeg (const std::string &bv)
 
static std::string bvAdd (const std::string &bv1, const std::string &bv2)
 
static std::string bvSub (const std::string &bv1, const std::string &bv2)
 
static std::string bvMul (const std::string &bv1, const std::string &bv2)
 
static std::string bvUdiv (const std::string &bv1, const std::string &bv2)
 
static std::string bvUrem (const std::string &bv1, const std::string &bv2)
 
static std::string bvUmod (const std::string &bv1, const std::string &bv2)
 
static std::string bvSdiv (const std::string &bv1, const std::string &bv2)
 
static std::string bvSrem (const std::string &bv1, const std::string &bv2)
 
static std::string bvSmod (const std::string &bv1, const std::string &bv2)
 
static std::string bvShl (const std::string &bv, const std::string &n)
 
static std::string bvLshr (const std::string &bv, const std::string &n)
 
static std::string bvAshr (const std::string &bv, const std::string &n)
 
static std::string bvConcat (const std::string &bv1, const std::string &bv2)
 
static std::string bvExtract (const std::string &bv, const Integer &i, const Integer &j)
 
static std::string bvRepeat (const std::string &bv, const Integer &n)
 
static std::string bvZeroExtend (const std::string &bv, const Integer &n)
 
static std::string bvSignExtend (const std::string &bv, const Integer &n)
 
static std::string bvRotateLeft (const std::string &bv, const Integer &n)
 
static std::string bvRotateRight (const std::string &bv, const Integer &n)
 
static bool bvComp (const std::string &bv1, const std::string &bv2, const NODE_KIND &kind)
 
static bool bvIsMinSigned (const std::string &bv)
 
static bool bvIsMaxSigned (const std::string &bv)
 
static bool bvIsMaxUnsigned (const std::string &bv)
 
static bool bvIsNegOne (const std::string &bv)
 
static int bvCompareToUint (const std::string &bv, const uint64_t &u)
 
static std::string mkOnes (const Integer &n)
 

Detailed Description

Bitvector conversion and arithmetic helpers on SMT bitstring forms.

Definition at line 86 of file util.h.

Member Function Documentation

◆ bvAdd()

std::string stabilizer::parser::BitVectorUtils::bvAdd ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 435 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvadd(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvAnd()

std::string stabilizer::parser::BitVectorUtils::bvAnd ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 354 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvAshr()

std::string stabilizer::parser::BitVectorUtils::bvAshr ( const std::string &  bv,
const std::string &  n 
)
static

Definition at line 564 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvashr(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvComp()

bool stabilizer::parser::BitVectorUtils::bvComp ( const std::string &  bv1,
const std::string &  bv2,
const NODE_KIND &  kind 
)
static

Definition at line 637 of file util.cpp.

References bvToInt(), bvToNat(), condAssert, stabilizer::parser::NT_BV_SGE, stabilizer::parser::NT_BV_SGT, stabilizer::parser::NT_BV_SLE, stabilizer::parser::NT_BV_SLT, stabilizer::parser::NT_BV_UGE, stabilizer::parser::NT_BV_UGT, stabilizer::parser::NT_BV_ULE, stabilizer::parser::NT_BV_ULT, stabilizer::parser::NT_DISTINCT_OTHER, and stabilizer::parser::NT_EQ_OTHER.

Referenced by stabilizer::parser::Parser::mkBvSge(), stabilizer::parser::Parser::mkBvSgt(), stabilizer::parser::Parser::mkBvSle(), stabilizer::parser::Parser::mkBvSlt(), stabilizer::parser::Parser::mkBvUge(), stabilizer::parser::Parser::mkBvUgt(), stabilizer::parser::Parser::mkBvUle(), and stabilizer::parser::Parser::rewrite().

◆ bvCompareToUint()

int stabilizer::parser::BitVectorUtils::bvCompareToUint ( const std::string &  bv,
const uint64_t &  u 
)
static

Definition at line 704 of file util.cpp.

References bvToNat(), condAssert, and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvConcat()

std::string stabilizer::parser::BitVectorUtils::bvConcat ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 577 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvExtract()

std::string stabilizer::parser::BitVectorUtils::bvExtract ( const std::string &  bv,
const Integer &  i,
const Integer &  j 
)
static

Definition at line 585 of file util.cpp.

References condAssert, and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvIsMaxSigned()

bool stabilizer::parser::BitVectorUtils::bvIsMaxSigned ( const std::string &  bv)
static

Definition at line 676 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvIsMaxUnsigned()

bool stabilizer::parser::BitVectorUtils::bvIsMaxUnsigned ( const std::string &  bv)
static

Definition at line 692 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvIsMinSigned()

bool stabilizer::parser::BitVectorUtils::bvIsMinSigned ( const std::string &  bv)
static

Definition at line 684 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvIsNegOne()

bool stabilizer::parser::BitVectorUtils::bvIsNegOne ( const std::string &  bv)
static

Definition at line 698 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvLshr()

std::string stabilizer::parser::BitVectorUtils::bvLshr ( const std::string &  bv,
const std::string &  n 
)
static

Definition at line 552 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvshr(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvMul()

std::string stabilizer::parser::BitVectorUtils::bvMul ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 459 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvmul(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvNand()

std::string stabilizer::parser::BitVectorUtils::bvNand ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 390 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvNeg()

std::string stabilizer::parser::BitVectorUtils::bvNeg ( const std::string &  bv)
static

Definition at line 427 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvneg(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvNor()

std::string stabilizer::parser::BitVectorUtils::bvNor ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 402 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvNot()

std::string stabilizer::parser::BitVectorUtils::bvNot ( const std::string &  bv)
static

Definition at line 345 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvOr()

std::string stabilizer::parser::BitVectorUtils::bvOr ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 366 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvRepeat()

std::string stabilizer::parser::BitVectorUtils::bvRepeat ( const std::string &  bv,
const Integer &  n 
)
static

Definition at line 599 of file util.cpp.

References condAssert, and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvRotateLeft()

std::string stabilizer::parser::BitVectorUtils::bvRotateLeft ( const std::string &  bv,
const Integer &  n 
)
static

Definition at line 621 of file util.cpp.

References condAssert, and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvRotateRight()

std::string stabilizer::parser::BitVectorUtils::bvRotateRight ( const std::string &  bv,
const Integer &  n 
)
static

Definition at line 628 of file util.cpp.

References condAssert, and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvSdiv()

std::string stabilizer::parser::BitVectorUtils::bvSdiv ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 504 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvsdiv(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvShl()

std::string stabilizer::parser::BitVectorUtils::bvShl ( const std::string &  bv,
const std::string &  n 
)
static

Definition at line 541 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvshl(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvSignExtend()

std::string stabilizer::parser::BitVectorUtils::bvSignExtend ( const std::string &  bv,
const Integer &  n 
)
static

Definition at line 614 of file util.cpp.

References condAssert, and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvSmod()

std::string stabilizer::parser::BitVectorUtils::bvSmod ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 528 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvsmod(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvSrem()

std::string stabilizer::parser::BitVectorUtils::bvSrem ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 516 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvsrem(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvSub()

std::string stabilizer::parser::BitVectorUtils::bvSub ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 447 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvsub(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvToInt()

Integer stabilizer::parser::BitVectorUtils::bvToInt ( const std::string &  bv)
static

Definition at line 852 of file util.cpp.

References condAssert.

Referenced by bvComp(), and stabilizer::parser::Parser::rewrite().

◆ bvToNat()

Integer stabilizer::parser::BitVectorUtils::bvToNat ( const std::string &  bv)
static

Definition at line 724 of file util.cpp.

References condAssert.

Referenced by bvComp(), bvCompareToUint(), and stabilizer::parser::Parser::rewrite().

◆ bvUdiv()

std::string stabilizer::parser::BitVectorUtils::bvUdiv ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 472 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvudiv(), and stabilizer::util::BitVector::str().

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvUmod()

std::string stabilizer::parser::BitVectorUtils::bvUmod ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 495 of file util.cpp.

References bvUrem(), and condAssert.

◆ bvUrem()

std::string stabilizer::parser::BitVectorUtils::bvUrem ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 484 of file util.cpp.

References condAssert, stabilizer::util::BitVector::ibvurem(), and stabilizer::util::BitVector::str().

Referenced by bvUmod(), and stabilizer::parser::Parser::rewrite().

◆ bvXnor()

std::string stabilizer::parser::BitVectorUtils::bvXnor ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 414 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvXor()

std::string stabilizer::parser::BitVectorUtils::bvXor ( const std::string &  bv1,
const std::string &  bv2 
)
static

Definition at line 378 of file util.cpp.

References condAssert.

Referenced by stabilizer::parser::Parser::rewrite().

◆ bvZeroExtend()

std::string stabilizer::parser::BitVectorUtils::bvZeroExtend ( const std::string &  bv,
const Integer &  n 
)
static

Definition at line 608 of file util.cpp.

References condAssert, and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite().

◆ intToBv()

std::string stabilizer::parser::BitVectorUtils::intToBv ( const Integer &  i,
const Integer &  n 
)
static

Definition at line 870 of file util.cpp.

References stabilizer::parser::HighPrecisionInteger::toString(), and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite(), and stabilizer::parser::Parser::rewrite().

◆ mkOnes()

std::string stabilizer::parser::BitVectorUtils::mkOnes ( const Integer &  n)
static

Definition at line 720 of file util.cpp.

References stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::rewrite(), and stabilizer::parser::Parser::rewrite().

◆ natToBv() [1/2]

std::string stabilizer::parser::BitVectorUtils::natToBv ( const Integer &  i,
const Integer &  n 
)
static

Definition at line 733 of file util.cpp.

References stabilizer::parser::HighPrecisionInteger::toString(), and stabilizer::parser::HighPrecisionInteger::toULong().

Referenced by stabilizer::parser::Parser::mkConstBv(), natToBv(), and stabilizer::parser::Parser::rewrite().

◆ natToBv() [2/2]

std::string stabilizer::parser::BitVectorUtils::natToBv ( const std::string &  i,
const Integer &  n 
)
static

Definition at line 827 of file util.cpp.

References stabilizer::parser::decToBv(), stabilizer::parser::hexToBv(), natToBv(), and stabilizer::parser::HighPrecisionInteger::toULong().

The documentation for this class was generated from the following files: