| bitblastBVMult(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_times_b, std::vector< Theorem > &output_bits) | CVC3::BitvectorTheoremProducer | virtual |
| bitblastBVPlus(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_plus_b, std::vector< Theorem > &output_bits) | CVC3::BitvectorTheoremProducer | virtual |
| bitBlastDisEqnRule(const Theorem &e, const Expr &f) | CVC3::BitvectorTheoremProducer | virtual |
| bitBlastEqnRule(const Expr &e, const Expr &f) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractAllToConstEq(std::vector< Theorem > &thms) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractBitwise(const Expr &x, int i, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractBVASHR(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractBVLSHR(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractBVMult(const Expr &t, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractBVPlus(const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractBVPlusPreComputed(const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractBVSHL(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractConcatenation(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractConstant(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractConstBVMult(const Expr &t, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractExtraction(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractFixedLeftShift(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractFixedRightShift(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractNot(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractRewrite(const Expr &x) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractSXRule(const Expr &e, int i) | CVC3::BitvectorTheoremProducer | virtual |
| bitExtractToExtract(const Theorem &thm) | CVC3::BitvectorTheoremProducer | virtual |
| bitvectorFalseRule(const Theorem &thm) | CVC3::BitvectorTheoremProducer | virtual |
| BitvectorTheoremProducer(TheoryBitvector *theoryBitvector) | CVC3::BitvectorTheoremProducer | |
| bitvectorTrueRule(const Theorem &thm) | CVC3::BitvectorTheoremProducer | virtual |
| bitwiseConcat(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| bitwiseConst(const Expr &e, const std::vector< int > &idxs, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| bitwiseConstElim(const Expr &e, int idx, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| bitwiseFlatten(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| buildPlusTerm(int bv_size, Rational &known_term, ExprMap< Rational > &sumHashMap) | CVC3::BitvectorTheoremProducer | private |
| bvashrToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvConstIneqn(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| bvConstMultAssocRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvlshrToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| BVMult_order_subterms(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvMultAssocRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvmultBVUminus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvmultConst(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvMultDistRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvOne() const | CVC3::BitvectorTheoremProducer | inlineprivate |
| bvPlusAssociativityRule(const Expr &bvPlusTerm) | CVC3::BitvectorTheoremProducer | virtual |
| bvplusConst(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvplusZeroConcatRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvSDivRewrite(const Expr &sDivExpr) | CVC3::BitvectorTheoremProducer | virtual |
| bvShiftZero(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvshlSplit(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvshlToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvSModRewrite(const Expr &sModExpr) | CVC3::BitvectorTheoremProducer | virtual |
| bvSRemRewrite(const Expr &sRemExpr) | CVC3::BitvectorTheoremProducer | virtual |
| bvUDivConst(const Expr &divExpr) | CVC3::BitvectorTheoremProducer | virtual |
| bvUDivTheorem(const Expr &divExpr) | CVC3::BitvectorTheoremProducer | virtual |
| bvuminusBVConst(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvuminusBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvuminusBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvuminusBVUminus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvuminusToBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvuminusVar(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| bvURemConst(const Expr &remExpr) | CVC3::BitvectorTheoremProducer | virtual |
| bvURemRewrite(const Expr &remExpr) | CVC3::BitvectorTheoremProducer | virtual |
| bvZero() const | CVC3::BitvectorTheoremProducer | inlineprivate |
| canonBVEQ(const Expr &e, int maxEffort=3) | CVC3::BitvectorTheoremProducer | virtual |
| canonBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| canonBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| canonBVUMinus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| chopConcat(int bv_size, Rational c, std::vector< Expr > &concatKids) | CVC3::BitvectorTheoremProducer | private |
| collectLikeTermsOfPlus(const Expr &e, ExprMap< Rational > &likeTerms, Rational &plusConstant) | CVC3::BitvectorTheoremProducer | private |
| collectOneTermOfPlus(const Rational &coefficient, const Expr &var, ExprMap< Rational > &likeTerms, Rational &plusConstant) | CVC3::BitvectorTheoremProducer | private |
| combineLikeTermsRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| computeCarry(const std::vector< Theorem > &t1BitExtractThms, const std::vector< Theorem > &t2BitExtractThms, int bitPos) | CVC3::BitvectorTheoremProducer | |
| computeCarryPreComputed(const Theorem &t1_i, const Theorem &t2_i, int bitPos, int precomputedFlag) | CVC3::BitvectorTheoremProducer | |
| concatConst(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| concatFlatten(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| concatMergeExtract(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| constEq(const Expr &eq) | CVC3::BitvectorTheoremProducer | virtual |
| constMultToPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| constWidthLeftShiftToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| createNewPlusCollection(const Expr &e, const ExprMap< Rational > &likeTerms, Rational &plusConstant, std::vector< Expr > &result) | CVC3::BitvectorTheoremProducer | private |
| d_bvOne | CVC3::BitvectorTheoremProducer | private |
| d_bvZero | CVC3::BitvectorTheoremProducer | private |
| d_checkProofs | CVC3::TheoremProducer | protected |
| d_em | CVC3::TheoremProducer | protected |
| d_hole | CVC3::TheoremProducer | protected |
| d_pfOp | CVC3::TheoremProducer | protected |
| d_theoryBitvector | CVC3::BitvectorTheoremProducer | private |
| d_tm | CVC3::TheoremProducer | protected |
| distributive_rule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| eqConst(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| eqToBits(const Theorem &eq) | CVC3::BitvectorTheoremProducer | virtual |
| expandTypePred(const Theorem &tp) | CVC3::BitvectorTheoremProducer | virtual |
| extractAnd(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractBitwise(const Expr &e, int kind, const std::string &name) | CVC3::BitvectorTheoremProducer | virtual |
| extractBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractConst(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractExtract(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractNeg(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractOr(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| extractWhole(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| flattenBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| flipBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| generalIneqn(const Expr &e, const Theorem &lhs_i, const Theorem &rhs_i, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| getPlusTerms(const Expr &e, Rational &known_term, ExprMap< Rational > &sumHashMap) | CVC3::BitvectorTheoremProducer | private |
| isolate_var(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| iteBVnegRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| iteExtractRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| leftShiftToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| lhsEqRhsIneqn(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | virtual |
| lhsMinusRhsRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| liftConcatBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| liftConcatBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| MarkNonSolvableEq(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negBVand(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negBVor(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negBVxnor(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negBVxor(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negConst(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negElim(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| negNeg(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| newAssumption(const Expr &thm, const Proof &pf, int scope=-1) | CVC3::TheoremProducer | inlineprotected |
| newLabel(const Expr &e) | CVC3::TheoremProducer | |
| newPf(const std::string &name) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Proof &pf) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const Proof &pf) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf) | CVC3::TheoremProducer | |
| newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end) | CVC3::TheoremProducer | |
| newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const std::vector< Expr > &args) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args, const Proof &pf) | CVC3::TheoremProducer | |
| newPf(const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs) | CVC3::TheoremProducer | |
| newPf(const Proof &label, const Expr &frm, const Proof &pf) | CVC3::TheoremProducer | |
| newPf(const Proof &label, const Proof &pf) | CVC3::TheoremProducer | |
| newPf(const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf) | CVC3::TheoremProducer | |
| newPf(const std::vector< Proof > &labels, const Proof &pf) | CVC3::TheoremProducer | |
| newReflTheorem(const Expr &e) | CVC3::TheoremProducer | inlineprotected |
| newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| notBVEQ1Rule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| notBVLTRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| okToSplit(const Expr &e) | CVC3::BitvectorTheoremProducer | private |
| oneBVAND(const Expr &andEqOne) | CVC3::BitvectorTheoremProducer | virtual |
| oneCoeffBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| pad(int rat, const Expr &e) | CVC3::BitvectorTheoremProducer | |
| padBVLTRule(const Expr &e, int len) | CVC3::BitvectorTheoremProducer | virtual |
| padBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| padBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| padBVSLTRule(const Expr &e, int len) | CVC3::BitvectorTheoremProducer | virtual |
| processExtract(const Theorem &e, bool &solvedForm) | CVC3::BitvectorTheoremProducer | virtual |
| rat(const Rational &r) | CVC3::BitvectorTheoremProducer | inline |
| repeatRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rewriteBVCOMP(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rewriteBVSub(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rewriteNAND(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rewriteNOR(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rewriteXNOR(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rightShiftToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rotlRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| rotrRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| sameKidCheck(const Expr &e, ExprMap< int > &likeTerms) | CVC3::BitvectorTheoremProducer | |
| signBVLTRule(const Expr &e, const Theorem &topBit0, const Theorem &topBit1) | CVC3::BitvectorTheoremProducer | virtual |
| signExtendRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| solveExtractOverlap(const Expr &eq) | CVC3::BitvectorTheoremProducer | virtual |
| solveExtractOverlapApplies(const Expr &eq) | CVC3::BitvectorTheoremProducer | virtual |
| soundError(const std::string &file, int line, const std::string &cond, const std::string &msg) | CVC3::TheoremProducer | protected |
| sumNormalizedElements(int bvplusLength, const std::vector< Expr > &elements) | CVC3::BitvectorTheoremProducer | private |
| TheoremProducer(TheoremManager *tm) | CVC3::TheoremProducer | |
| typePredBit(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| withAssumptions() | CVC3::TheoremProducer | inline |
| withProof() | CVC3::TheoremProducer | inline |
| zeroBVOR(const Expr &orEqZero) | CVC3::BitvectorTheoremProducer | virtual |
| zeroCoeffBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| zeroExtendRule(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| zeroLeq(const Expr &e) | CVC3::BitvectorTheoremProducer | virtual |
| zeroPaddingRule(const Expr &e, int r) | CVC3::BitvectorTheoremProducer | virtual |
| ~BitvectorProofRules() | CVC3::BitvectorProofRules | inlinevirtual |
| ~BitvectorTheoremProducer() | CVC3::BitvectorTheoremProducer | inline |
| ~TheoremProducer() | CVC3::TheoremProducer | inlinevirtual |
