, including all inherited members.
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] |
CVC3::BitvectorProofRules::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) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::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) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitBlastDisEqnRule(const Theorem &e, const Expr &f)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitBlastEqnRule(const Expr &e, const Expr &f) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitBlastEqnRule(const Expr &e, const Expr &f)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractAllToConstEq(std::vector< Theorem > &thms) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractAllToConstEq(std::vector< Theorem > &thms)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractBitwise(const Expr &x, int i, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractBitwise(const Expr &x, int i, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractBVASHR(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractBVASHR(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractBVLSHR(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractBVLSHR(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractBVMult(const Expr &t, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::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) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::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) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::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) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractBVSHL(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractConcatenation(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractConcatenation(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractConstant(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractConstant(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractConstBVMult(const Expr &t, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractConstBVMult(const Expr &t, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractExtraction(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractExtraction(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractFixedLeftShift(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractFixedLeftShift(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractFixedRightShift(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractFixedRightShift(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractNot(const Expr &x, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractNot(const Expr &x, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractRewrite(const Expr &x) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractRewrite(const Expr &x)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractSXRule(const Expr &e, int i) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractSXRule(const Expr &e, int i)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitExtractToExtract(const Theorem &thm) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitExtractToExtract(const Theorem &thm)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitvectorFalseRule(const Theorem &thm) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitvectorFalseRule(const Theorem &thm)=0 | CVC3::BitvectorProofRules | [pure virtual] |
BitvectorTheoremProducer(TheoryBitvector *theoryBitvector) | CVC3::BitvectorTheoremProducer | |
bitvectorTrueRule(const Theorem &thm) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitvectorTrueRule(const Theorem &thm)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitwiseConcat(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitwiseConcat(const Expr &e, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitwiseConst(const Expr &e, const std::vector< int > &idxs, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitwiseConst(const Expr &e, const std::vector< int > &idxs, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitwiseConstElim(const Expr &e, int idx, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitwiseConstElim(const Expr &e, int idx, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bitwiseFlatten(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bitwiseFlatten(const Expr &e, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
buildPlusTerm(int bv_size, Rational &known_term, ExprMap< Rational > &sumHashMap) | CVC3::BitvectorTheoremProducer | [private] |
bvashrToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvashrToConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvConstIneqn(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvConstIneqn(const Expr &e, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvConstMultAssocRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvConstMultAssocRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvlshrToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvlshrToConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
BVMult_order_subterms(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::BVMult_order_subterms(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvMultAssocRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvMultAssocRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvmultBVUminus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvmultBVUminus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvmultConst(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvmultConst(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvMultDistRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvMultDistRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvOne() const | CVC3::BitvectorTheoremProducer | [inline, private] |
bvPlusAssociativityRule(const Expr &bvPlusTerm) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvPlusAssociativityRule(const Expr &bvPlusTerm)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvplusConst(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvplusConst(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvplusZeroConcatRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvplusZeroConcatRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvSDivRewrite(const Expr &sDivExpr) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::bvSDivRewrite(const Expr &sDivExpr)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvShiftZero(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvShiftZero(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvshlSplit(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvshlSplit(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvshlToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvshlToConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvSModRewrite(const Expr &sModExpr) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::bvSModRewrite(const Expr &sModExpr)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvSRemRewrite(const Expr &sRemExpr) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::bvSRemRewrite(const Expr &sRemExpr)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvUDivConst(const Expr &divExpr) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::bvUDivConst(const Expr &divExpr)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvUDivTheorem(const Expr &divExpr) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::bvUDivTheorem(const Expr &divExpr)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvuminusBVConst(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvuminusBVConst(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvuminusBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvuminusBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvuminusBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvuminusBVPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvuminusBVUminus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvuminusBVUminus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvuminusToBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvuminusToBVPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvuminusVar(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::bvuminusVar(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvURemConst(const Expr &remExpr) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::bvURemConst(const Expr &remExpr)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvURemRewrite(const Expr &remExpr) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::bvURemRewrite(const Expr &divExpr)=0 | CVC3::BitvectorProofRules | [pure virtual] |
bvZero() const | CVC3::BitvectorTheoremProducer | [inline, private] |
canonBVEQ(const Expr &e, int maxEffort=3) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::canonBVEQ(const Expr &e, int maxEffort=3)=0 | CVC3::BitvectorProofRules | [pure virtual] |
canonBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::canonBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
canonBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::canonBVPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
canonBVUMinus(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::canonBVUMinus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure 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 | |
CVC3::BitvectorProofRules::combineLikeTermsRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure 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 | |
CVC3::BitvectorProofRules::concatConst(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
concatFlatten(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::concatFlatten(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
concatMergeExtract(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::concatMergeExtract(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
constEq(const Expr &eq) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::constEq(const Expr &eq)=0 | CVC3::BitvectorProofRules | [pure virtual] |
constMultToPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::constMultToPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
constWidthLeftShiftToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::constWidthLeftShiftToConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure 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] |
CVC3::BitvectorProofRules::distributive_rule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
eqConst(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::eqConst(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
eqToBits(const Theorem &eq) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::eqToBits(const Theorem &eq)=0 | CVC3::BitvectorProofRules | [pure virtual] |
expandTypePred(const Theorem &tp) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::expandTypePred(const Theorem &tp)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractAnd(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractAnd(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractBitwise(const Expr &e, int kind, const std::string &name) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractBitwise(const Expr &e, int kind, const std::string &name)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractBVPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractConst(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractConst(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractExtract(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractExtract(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractNeg(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractNeg(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractOr(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractOr(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
extractWhole(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::extractWhole(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
flattenBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::flattenBVPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
flipBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::flipBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
generalIneqn(const Expr &e, const Theorem &lhs_i, const Theorem &rhs_i, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::generalIneqn(const Expr &e, const Theorem &e0, const Theorem &e1, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
getPlusTerms(const Expr &e, Rational &known_term, ExprMap< Rational > &sumHashMap) | CVC3::BitvectorTheoremProducer | [private] |
isolate_var(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::isolate_var(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
iteBVnegRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::iteBVnegRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
iteExtractRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::iteExtractRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
leftShiftToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::leftShiftToConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
lhsEqRhsIneqn(const Expr &e, int kind) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::lhsEqRhsIneqn(const Expr &e, int kind)=0 | CVC3::BitvectorProofRules | [pure virtual] |
lhsMinusRhsRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::lhsMinusRhsRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
liftConcatBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::liftConcatBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
liftConcatBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::liftConcatBVPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
MarkNonSolvableEq(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::MarkNonSolvableEq(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negBVand(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negBVand(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negBVor(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negBVor(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negBVxnor(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negBVxnor(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negBVxor(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negBVxor(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negConst(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negConst(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negElim(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negElim(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
negNeg(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::negNeg(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure 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 | |
CVC3::BitvectorProofRules::notBVEQ1Rule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
notBVLTRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::notBVLTRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
okToSplit(const Expr &e) | CVC3::BitvectorTheoremProducer | [private] |
oneBVAND(const Expr &andEqOne) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::oneBVAND(const Expr &andEqOne)=0 | CVC3::BitvectorProofRules | [pure virtual] |
oneCoeffBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::oneCoeffBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
pad(int rat, const Expr &e) | CVC3::BitvectorTheoremProducer | |
padBVLTRule(const Expr &e, int len) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::padBVLTRule(const Expr &e, int len)=0 | CVC3::BitvectorProofRules | [pure virtual] |
padBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::padBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
padBVPlus(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::padBVPlus(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
padBVSLTRule(const Expr &e, int len) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::padBVSLTRule(const Expr &e, int len)=0 | CVC3::BitvectorProofRules | [pure virtual] |
processExtract(const Theorem &e, bool &solvedForm) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::processExtract(const Theorem &e, bool &solvedForm)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rat(const Rational &r) | CVC3::BitvectorTheoremProducer | [inline] |
repeatRule(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::repeatRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rewriteBVCOMP(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::rewriteBVCOMP(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rewriteBVSub(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::rewriteBVSub(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rewriteNAND(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::rewriteNAND(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rewriteNOR(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::rewriteNOR(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rewriteXNOR(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::rewriteXNOR(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rightShiftToConcat(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::rightShiftToConcat(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rotlRule(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::rotlRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
rotrRule(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::rotrRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
sameKidCheck(const Expr &e, ExprMap< int > &likeTerms) | CVC3::BitvectorTheoremProducer | |
signBVLTRule(const Expr &e, const Theorem &topBit0, const Theorem &topBit1) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::signBVLTRule(const Expr &e, const Theorem &topBit0, const Theorem &topBit1)=0 | CVC3::BitvectorProofRules | [pure virtual] |
signExtendRule(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::signExtendRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
solveExtractOverlap(const Expr &eq) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::solveExtractOverlap(const Expr &eq)=0 | CVC3::BitvectorProofRules | [pure virtual] |
solveExtractOverlapApplies(const Expr &eq) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::solveExtractOverlapApplies(const Expr &eq)=0 | CVC3::BitvectorProofRules | [pure 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 | |
CVC3::BitvectorProofRules::typePredBit(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
withAssumptions() | CVC3::TheoremProducer | [inline] |
withProof() | CVC3::TheoremProducer | [inline] |
zeroBVOR(const Expr &orEqZero) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::zeroBVOR(const Expr &orEqZero)=0 | CVC3::BitvectorProofRules | [pure virtual] |
zeroCoeffBVMult(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::zeroCoeffBVMult(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
zeroExtendRule(const Expr &e) | CVC3::BitvectorTheoremProducer | [virtual] |
CVC3::BitvectorProofRules::zeroExtendRule(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
zeroLeq(const Expr &e) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::zeroLeq(const Expr &e)=0 | CVC3::BitvectorProofRules | [pure virtual] |
zeroPaddingRule(const Expr &e, int r) | CVC3::BitvectorTheoremProducer | |
CVC3::BitvectorProofRules::zeroPaddingRule(const Expr &e, int r)=0 | CVC3::BitvectorProofRules | [pure virtual] |
~BitvectorProofRules() | CVC3::BitvectorProofRules | [inline, virtual] |
~BitvectorTheoremProducer() | CVC3::BitvectorTheoremProducer | [inline] |
~TheoremProducer() | CVC3::TheoremProducer | [inline, virtual] |