CVC3
CVC3::BitvectorProofRules Member List

This is the complete list of members for CVC3::BitvectorProofRules, including all inherited members.

bitblastBVMult(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_times_b, std::vector< Theorem > &output_bits)=0CVC3::BitvectorProofRulespure virtual
bitblastBVPlus(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_plus_b, std::vector< Theorem > &output_bits)=0CVC3::BitvectorProofRulespure virtual
bitBlastDisEqnRule(const Theorem &e, const Expr &f)=0CVC3::BitvectorProofRulespure virtual
bitBlastEqnRule(const Expr &e, const Expr &f)=0CVC3::BitvectorProofRulespure virtual
bitExtractAllToConstEq(std::vector< Theorem > &thms)=0CVC3::BitvectorProofRulespure virtual
bitExtractBitwise(const Expr &x, int i, int kind)=0CVC3::BitvectorProofRulespure virtual
bitExtractBVASHR(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractBVLSHR(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractBVMult(const Expr &t, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractBVPlus(const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractBVPlusPreComputed(const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)=0CVC3::BitvectorProofRulespure virtual
bitExtractBVSHL(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractConcatenation(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractConstant(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractConstBVMult(const Expr &t, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractExtraction(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractFixedLeftShift(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractFixedRightShift(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractNot(const Expr &x, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractRewrite(const Expr &x)=0CVC3::BitvectorProofRulespure virtual
bitExtractSXRule(const Expr &e, int i)=0CVC3::BitvectorProofRulespure virtual
bitExtractToExtract(const Theorem &thm)=0CVC3::BitvectorProofRulespure virtual
bitvectorFalseRule(const Theorem &thm)=0CVC3::BitvectorProofRulespure virtual
bitvectorTrueRule(const Theorem &thm)=0CVC3::BitvectorProofRulespure virtual
bitwiseConcat(const Expr &e, int kind)=0CVC3::BitvectorProofRulespure virtual
bitwiseConst(const Expr &e, const std::vector< int > &idxs, int kind)=0CVC3::BitvectorProofRulespure virtual
bitwiseConstElim(const Expr &e, int idx, int kind)=0CVC3::BitvectorProofRulespure virtual
bitwiseFlatten(const Expr &e, int kind)=0CVC3::BitvectorProofRulespure virtual
bvashrToConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvConstIneqn(const Expr &e, int kind)=0CVC3::BitvectorProofRulespure virtual
bvConstMultAssocRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvlshrToConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
BVMult_order_subterms(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvMultAssocRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvmultBVUminus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvmultConst(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvMultDistRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvPlusAssociativityRule(const Expr &bvPlusTerm)=0CVC3::BitvectorProofRulespure virtual
bvplusConst(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvplusZeroConcatRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvSDivRewrite(const Expr &sDivExpr)=0CVC3::BitvectorProofRulespure virtual
bvShiftZero(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvshlSplit(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvshlToConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvSModRewrite(const Expr &sModExpr)=0CVC3::BitvectorProofRulespure virtual
bvSRemRewrite(const Expr &sRemExpr)=0CVC3::BitvectorProofRulespure virtual
bvUDivConst(const Expr &divExpr)=0CVC3::BitvectorProofRulespure virtual
bvUDivTheorem(const Expr &divExpr)=0CVC3::BitvectorProofRulespure virtual
bvuminusBVConst(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvuminusBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvuminusBVPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvuminusBVUminus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvuminusToBVPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvuminusVar(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
bvURemConst(const Expr &remExpr)=0CVC3::BitvectorProofRulespure virtual
bvURemRewrite(const Expr &divExpr)=0CVC3::BitvectorProofRulespure virtual
canonBVEQ(const Expr &e, int maxEffort=3)=0CVC3::BitvectorProofRulespure virtual
canonBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
canonBVPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
canonBVUMinus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
combineLikeTermsRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
concatConst(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
concatFlatten(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
concatMergeExtract(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
constEq(const Expr &eq)=0CVC3::BitvectorProofRulespure virtual
constMultToPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
constWidthLeftShiftToConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
distributive_rule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
eqConst(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
eqToBits(const Theorem &eq)=0CVC3::BitvectorProofRulespure virtual
expandTypePred(const Theorem &tp)=0CVC3::BitvectorProofRulespure virtual
extractAnd(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractBitwise(const Expr &e, int kind, const std::string &name)=0CVC3::BitvectorProofRulespure virtual
extractBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractBVPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractConst(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractExtract(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractNeg(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractOr(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
extractWhole(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
flattenBVPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
flipBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
generalIneqn(const Expr &e, const Theorem &e0, const Theorem &e1, int kind)=0CVC3::BitvectorProofRulespure virtual
isolate_var(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
iteBVnegRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
iteExtractRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
leftShiftToConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
lhsEqRhsIneqn(const Expr &e, int kind)=0CVC3::BitvectorProofRulespure virtual
lhsMinusRhsRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
liftConcatBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
liftConcatBVPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
MarkNonSolvableEq(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negBVand(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negBVor(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negBVxnor(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negBVxor(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negConst(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negElim(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
negNeg(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
notBVEQ1Rule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
notBVLTRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
oneBVAND(const Expr &andEqOne)=0CVC3::BitvectorProofRulespure virtual
oneCoeffBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
padBVLTRule(const Expr &e, int len)=0CVC3::BitvectorProofRulespure virtual
padBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
padBVPlus(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
padBVSLTRule(const Expr &e, int len)=0CVC3::BitvectorProofRulespure virtual
processExtract(const Theorem &e, bool &solvedForm)=0CVC3::BitvectorProofRulespure virtual
repeatRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rewriteBVCOMP(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rewriteBVSub(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rewriteNAND(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rewriteNOR(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rewriteXNOR(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rightShiftToConcat(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rotlRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
rotrRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
signBVLTRule(const Expr &e, const Theorem &topBit0, const Theorem &topBit1)=0CVC3::BitvectorProofRulespure virtual
signExtendRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
solveExtractOverlap(const Expr &eq)=0CVC3::BitvectorProofRulespure virtual
solveExtractOverlapApplies(const Expr &eq)=0CVC3::BitvectorProofRulespure virtual
typePredBit(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
zeroBVOR(const Expr &orEqZero)=0CVC3::BitvectorProofRulespure virtual
zeroCoeffBVMult(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
zeroExtendRule(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
zeroLeq(const Expr &e)=0CVC3::BitvectorProofRulespure virtual
zeroPaddingRule(const Expr &e, int r)=0CVC3::BitvectorProofRulespure virtual
~BitvectorProofRules()CVC3::BitvectorProofRulesinlinevirtual