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