CVC3  2.4.1
CVC3::BitvectorTheoremProducer Member List

This is the complete list of members for CVC3::BitvectorTheoremProducer, 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::BitvectorTheoremProducervirtual
bitblastBVPlus(const std::vector< Theorem > &a_bits, const std::vector< Theorem > &b_bits, const Expr &a_plus_b, std::vector< Theorem > &output_bits)CVC3::BitvectorTheoremProducervirtual
bitBlastDisEqnRule(const Theorem &e, const Expr &f)CVC3::BitvectorTheoremProducervirtual
bitBlastEqnRule(const Expr &e, const Expr &f)CVC3::BitvectorTheoremProducervirtual
bitExtractAllToConstEq(std::vector< Theorem > &thms)CVC3::BitvectorTheoremProducervirtual
bitExtractBitwise(const Expr &x, int i, int kind)CVC3::BitvectorTheoremProducervirtual
bitExtractBVASHR(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractBVLSHR(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractBVMult(const Expr &t, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractBVPlus(const std::vector< Theorem > &t1, const std::vector< Theorem > &t2, const Expr &bvPlusTerm, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractBVPlusPreComputed(const Theorem &t1_i, const Theorem &t2_i, const Expr &bvPlusTerm, int bitPos, int precomputed)CVC3::BitvectorTheoremProducervirtual
bitExtractBVSHL(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractConcatenation(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractConstant(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractConstBVMult(const Expr &t, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractExtraction(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractFixedLeftShift(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractFixedRightShift(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractNot(const Expr &x, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractRewrite(const Expr &x)CVC3::BitvectorTheoremProducervirtual
bitExtractSXRule(const Expr &e, int i)CVC3::BitvectorTheoremProducervirtual
bitExtractToExtract(const Theorem &thm)CVC3::BitvectorTheoremProducervirtual
bitvectorFalseRule(const Theorem &thm)CVC3::BitvectorTheoremProducervirtual
BitvectorTheoremProducer(TheoryBitvector *theoryBitvector)CVC3::BitvectorTheoremProducer
bitvectorTrueRule(const Theorem &thm)CVC3::BitvectorTheoremProducervirtual
bitwiseConcat(const Expr &e, int kind)CVC3::BitvectorTheoremProducervirtual
bitwiseConst(const Expr &e, const std::vector< int > &idxs, int kind)CVC3::BitvectorTheoremProducervirtual
bitwiseConstElim(const Expr &e, int idx, int kind)CVC3::BitvectorTheoremProducervirtual
bitwiseFlatten(const Expr &e, int kind)CVC3::BitvectorTheoremProducervirtual
buildPlusTerm(int bv_size, Rational &known_term, ExprMap< Rational > &sumHashMap)CVC3::BitvectorTheoremProducerprivate
bvashrToConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvConstIneqn(const Expr &e, int kind)CVC3::BitvectorTheoremProducervirtual
bvConstMultAssocRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvlshrToConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
BVMult_order_subterms(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvMultAssocRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvmultBVUminus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvmultConst(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvMultDistRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvOne() const CVC3::BitvectorTheoremProducerinlineprivate
bvPlusAssociativityRule(const Expr &bvPlusTerm)CVC3::BitvectorTheoremProducervirtual
bvplusConst(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvplusZeroConcatRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvSDivRewrite(const Expr &sDivExpr)CVC3::BitvectorTheoremProducervirtual
bvShiftZero(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvshlSplit(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvshlToConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvSModRewrite(const Expr &sModExpr)CVC3::BitvectorTheoremProducervirtual
bvSRemRewrite(const Expr &sRemExpr)CVC3::BitvectorTheoremProducervirtual
bvUDivConst(const Expr &divExpr)CVC3::BitvectorTheoremProducervirtual
bvUDivTheorem(const Expr &divExpr)CVC3::BitvectorTheoremProducervirtual
bvuminusBVConst(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvuminusBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvuminusBVPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvuminusBVUminus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvuminusToBVPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvuminusVar(const Expr &e)CVC3::BitvectorTheoremProducervirtual
bvURemConst(const Expr &remExpr)CVC3::BitvectorTheoremProducervirtual
bvURemRewrite(const Expr &remExpr)CVC3::BitvectorTheoremProducervirtual
bvZero() const CVC3::BitvectorTheoremProducerinlineprivate
canonBVEQ(const Expr &e, int maxEffort=3)CVC3::BitvectorTheoremProducervirtual
canonBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
canonBVPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
canonBVUMinus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
chopConcat(int bv_size, Rational c, std::vector< Expr > &concatKids)CVC3::BitvectorTheoremProducerprivate
collectLikeTermsOfPlus(const Expr &e, ExprMap< Rational > &likeTerms, Rational &plusConstant)CVC3::BitvectorTheoremProducerprivate
collectOneTermOfPlus(const Rational &coefficient, const Expr &var, ExprMap< Rational > &likeTerms, Rational &plusConstant)CVC3::BitvectorTheoremProducerprivate
combineLikeTermsRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
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::BitvectorTheoremProducervirtual
concatFlatten(const Expr &e)CVC3::BitvectorTheoremProducervirtual
concatMergeExtract(const Expr &e)CVC3::BitvectorTheoremProducervirtual
constEq(const Expr &eq)CVC3::BitvectorTheoremProducervirtual
constMultToPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
constWidthLeftShiftToConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
createNewPlusCollection(const Expr &e, const ExprMap< Rational > &likeTerms, Rational &plusConstant, std::vector< Expr > &result)CVC3::BitvectorTheoremProducerprivate
d_bvOneCVC3::BitvectorTheoremProducerprivate
d_bvZeroCVC3::BitvectorTheoremProducerprivate
d_checkProofsCVC3::TheoremProducerprotected
d_emCVC3::TheoremProducerprotected
d_holeCVC3::TheoremProducerprotected
d_pfOpCVC3::TheoremProducerprotected
d_theoryBitvectorCVC3::BitvectorTheoremProducerprivate
d_tmCVC3::TheoremProducerprotected
distributive_rule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
eqConst(const Expr &e)CVC3::BitvectorTheoremProducervirtual
eqToBits(const Theorem &eq)CVC3::BitvectorTheoremProducervirtual
expandTypePred(const Theorem &tp)CVC3::BitvectorTheoremProducervirtual
extractAnd(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractBitwise(const Expr &e, int kind, const std::string &name)CVC3::BitvectorTheoremProducervirtual
extractBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractBVPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractConst(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractExtract(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractNeg(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractOr(const Expr &e)CVC3::BitvectorTheoremProducervirtual
extractWhole(const Expr &e)CVC3::BitvectorTheoremProducervirtual
flattenBVPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
flipBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
generalIneqn(const Expr &e, const Theorem &lhs_i, const Theorem &rhs_i, int kind)CVC3::BitvectorTheoremProducervirtual
getPlusTerms(const Expr &e, Rational &known_term, ExprMap< Rational > &sumHashMap)CVC3::BitvectorTheoremProducerprivate
isolate_var(const Expr &e)CVC3::BitvectorTheoremProducervirtual
iteBVnegRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
iteExtractRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
leftShiftToConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
lhsEqRhsIneqn(const Expr &e, int kind)CVC3::BitvectorTheoremProducervirtual
lhsMinusRhsRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
liftConcatBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
liftConcatBVPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
MarkNonSolvableEq(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negBVand(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negBVor(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negBVxnor(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negBVxor(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negConst(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negElim(const Expr &e)CVC3::BitvectorTheoremProducervirtual
negNeg(const Expr &e)CVC3::BitvectorTheoremProducervirtual
newAssumption(const Expr &thm, const Proof &pf, int scope=-1)CVC3::TheoremProducerinlineprotected
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::TheoremProducerinlineprotected
newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
notBVEQ1Rule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
notBVLTRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
okToSplit(const Expr &e)CVC3::BitvectorTheoremProducerprivate
oneBVAND(const Expr &andEqOne)CVC3::BitvectorTheoremProducervirtual
oneCoeffBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
pad(int rat, const Expr &e)CVC3::BitvectorTheoremProducer
padBVLTRule(const Expr &e, int len)CVC3::BitvectorTheoremProducervirtual
padBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
padBVPlus(const Expr &e)CVC3::BitvectorTheoremProducervirtual
padBVSLTRule(const Expr &e, int len)CVC3::BitvectorTheoremProducervirtual
processExtract(const Theorem &e, bool &solvedForm)CVC3::BitvectorTheoremProducervirtual
rat(const Rational &r)CVC3::BitvectorTheoremProducerinline
repeatRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rewriteBVCOMP(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rewriteBVSub(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rewriteNAND(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rewriteNOR(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rewriteXNOR(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rightShiftToConcat(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rotlRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
rotrRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
sameKidCheck(const Expr &e, ExprMap< int > &likeTerms)CVC3::BitvectorTheoremProducer
signBVLTRule(const Expr &e, const Theorem &topBit0, const Theorem &topBit1)CVC3::BitvectorTheoremProducervirtual
signExtendRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
solveExtractOverlap(const Expr &eq)CVC3::BitvectorTheoremProducervirtual
solveExtractOverlapApplies(const Expr &eq)CVC3::BitvectorTheoremProducervirtual
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducerprotected
sumNormalizedElements(int bvplusLength, const std::vector< Expr > &elements)CVC3::BitvectorTheoremProducerprivate
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
typePredBit(const Expr &e)CVC3::BitvectorTheoremProducervirtual
withAssumptions()CVC3::TheoremProducerinline
withProof()CVC3::TheoremProducerinline
zeroBVOR(const Expr &orEqZero)CVC3::BitvectorTheoremProducervirtual
zeroCoeffBVMult(const Expr &e)CVC3::BitvectorTheoremProducervirtual
zeroExtendRule(const Expr &e)CVC3::BitvectorTheoremProducervirtual
zeroLeq(const Expr &e)CVC3::BitvectorTheoremProducervirtual
zeroPaddingRule(const Expr &e, int r)CVC3::BitvectorTheoremProducervirtual
~BitvectorProofRules()CVC3::BitvectorProofRulesinlinevirtual
~BitvectorTheoremProducer()CVC3::BitvectorTheoremProducerinline
~TheoremProducer()CVC3::TheoremProducerinlinevirtual