| 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 | [inline, private] |
| 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 | [inline, private] |
| 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 | [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] |
| 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 | [inline, virtual] |
| ~BitvectorTheoremProducer() | CVC3::BitvectorTheoremProducer | [inline] |
| ~TheoremProducer() | CVC3::TheoremProducer | [inline, virtual] |
