| 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 | [inline, virtual] |
