| andConcat(const Expr &e, int idx) | CVC3::BitvectorTheoremProducer | [virtual] |
| andConst(const Expr &e, const std::vector< int > &idxs) | CVC3::BitvectorTheoremProducer | [virtual] |
| andFlatten(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
| andOne(const Expr &e, const std::vector< int > idxs) | CVC3::BitvectorTheoremProducer | [virtual] |
| andZero(const Expr &e, int idx) | CVC3::BitvectorTheoremProducer | [virtual] |
| bitBlastDisEqnRule(const Theorem &e, const Expr &f) | CVC3::BitvectorTheoremProducer | [virtual] |
| bitBlastEqnRule(const Expr &e, const Expr &f) | CVC3::BitvectorTheoremProducer | [virtual] |
| bitExtractAnd(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | [virtual] |
| bitExtractBitwise(const Expr &x, int i, int kind) | CVC3::BitvectorTheoremProducer | |
| 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] |
| 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] |
| bitExtractOr(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 idx, bool isAnd) | CVC3::BitvectorTheoremProducer | |
| bitwiseConst(const Expr &e, const std::vector< int > &idxs, bool isAnd) | CVC3::BitvectorTheoremProducer | |
| bitwiseFlatten(const Expr &e, bool isAnd) | CVC3::BitvectorTheoremProducer | |
| bvConstIneqn(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | [virtual] |
| bvConstMultAssocRule(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 | [inline, private] |
| bvPlusAssociativityRule(const Expr &bvPlusTerm) | CVC3::BitvectorTheoremProducer | [virtual] |
| bvplusConst(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
| bvplusZeroConcatRule(const Expr &e) | 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] |
| bvZero() const | CVC3::BitvectorTheoremProducer | [inline, 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] |
| 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] |
| 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] |
| 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] |
| 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] |
| negNeg(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
| newAssumption(const Expr &thm, const Proof &pf, int scope=-1) | CVC3::TheoremProducer | [inline, protected] |
| 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 | [inline, protected] |
| newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | [inline, protected] |
| newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | [inline, protected] |
| newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | [inline, protected] |
| newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | [inline, protected] |
| notBVLTRule(const Expr &e, int Kind) | CVC3::BitvectorTheoremProducer | [virtual] |
| oneCoeffBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
| orConcat(const Expr &e, int idx) | CVC3::BitvectorTheoremProducer | [virtual] |
| orConst(const Expr &e, const std::vector< int > &idxs) | CVC3::BitvectorTheoremProducer | [virtual] |
| orFlatten(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
| orOne(const Expr &e, int idx) | CVC3::BitvectorTheoremProducer | [virtual] |
| orZero(const Expr &e, const std::vector< int > idxs) | 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] |
| rat(const Rational &r) | CVC3::BitvectorTheoremProducer | [inline] |
| 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] |
| rewriteXOR(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
| rightShiftToConcat(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] |
| 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] |
| zeroCoeffBVMult(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 | [inline, virtual] |
| ~BitvectorTheoremProducer() | CVC3::BitvectorTheoremProducer | [inline] |
| ~TheoremProducer() | CVC3::TheoremProducer | [inline, virtual] |
