CVC3
CVC3::TheoryBitvector Member List

This is the complete list of members for CVC3::TheoryBitvector, including all inherited members.

addBoundVar(const std::string &name, const Type &type)CVC3::Theory
addBoundVar(const std::string &name, const Type &type, const Expr &def)CVC3::Theory
addGlobalLemma(const Theorem &thm, int priority=0)CVC3::Theory
additionalRewriteConstraintsCVC3::TheoryBitvector
addSharedTerm(const Expr &e)CVC3::TheoryBitvectorvirtual
addSplitter(const Expr &e, int priority=0)CVC3::Theory
assertEqualities(const Theorem &e)CVC3::Theoryvirtual
assertFact(const Theorem &e)CVC3::TheoryBitvectorvirtual
assertTypePred(const Expr &e, const Theorem &pred)CVC3::TheoryBitvectorvirtual
assignValue(const Expr &t, const Expr &val)CVC3::Theoryvirtual
assignValue(const Theorem &thm)CVC3::Theoryvirtual
bitBlastDisEqn(const Theorem &notE)CVC3::TheoryBitvectorprivate
bitBlastEqn(const Expr &e)CVC3::TheoryBitvectorprivate
bitBlastIneqn(const Expr &e)CVC3::TheoryBitvectorprivate
bitBlastTerm(const Expr &t, int bitPosition)CVC3::TheoryBitvectorprivate
boolType()CVC3::Theoryinline
bvOne() const CVC3::TheoryBitvectorinlineprivate
BVSize(const Expr &e)CVC3::TheoryBitvector
bvZero() const CVC3::TheoryBitvectorinlineprivate
canSolveFor(const Expr &term, const Expr &e)CVC3::TheoryBitvector
check_linear(const Expr &e)CVC3::TheoryBitvectorprivate
checkAssertEqInvariant(const Theorem &e)CVC3::Theoryinlinevirtual
checkSat(bool fullEffort)CVC3::TheoryBitvectorvirtual
checkType(const Expr &e)CVC3::TheoryBitvectorvirtual
comparebv(const Expr &e1, const Expr &e2)CVC3::TheoryBitvector
computeBaseType(const Type &tp)CVC3::Theoryinlinevirtual
computeBVConst(const Expr &e)CVC3::TheoryBitvector
computeModel(const Expr &e, std::vector< Expr > &vars)CVC3::TheoryBitvectorvirtual
computeModelBasic(const std::vector< Expr > &v)CVC3::Theoryinlinevirtual
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::TheoryBitvectorvirtual
computeNegBVConst(const Expr &e)CVC3::TheoryBitvector
computeTCC(const Expr &e)CVC3::TheoryBitvectorvirtual
computeType(const Expr &e)CVC3::TheoryBitvectorvirtual
computeTypePred(const Type &t, const Expr &e)CVC3::TheoryBitvectorvirtual
countTermIn(const Expr &term, const Expr &e)CVC3::TheoryBitvectorprivate
createProofRules()CVC3::TheoryBitvector
d_bb_indexCVC3::TheoryBitvectorprivate
d_bitblastCVC3::TheoryBitvectorprivate
d_bitvecCacheCVC3::TheoryBitvectorprivate
d_booleanRWFlagCVC3::TheoryBitvectorprivate
d_boolExtractCacheFlagCVC3::TheoryBitvectorprivate
d_bv32FlagCVC3::TheoryBitvectorprivate
d_bvAssertDiseqCVC3::TheoryBitvectorprivate
d_bvAssertEqCVC3::TheoryBitvectorprivate
d_bvBitBlastDiseqCVC3::TheoryBitvectorprivate
d_bvBitBlastEqCVC3::TheoryBitvectorprivate
d_bvConstExprIndexCVC3::TheoryBitvectorprivate
d_bvDelayDiseqCVC3::TheoryBitvectorprivate
d_bvDelayEqCVC3::TheoryBitvectorprivate
d_bvDelayTypePredsCVC3::TheoryBitvectorprivate
d_bvOneCVC3::TheoryBitvectorprivate
d_bvParameterExprIndexCVC3::TheoryBitvectorprivate
d_bvPlusCarryCacheLeftBVCVC3::TheoryBitvector
d_bvPlusCarryCacheRightBVCVC3::TheoryBitvector
d_bvPlusExprIndexCVC3::TheoryBitvectorprivate
d_bvTypePredExprIndexCVC3::TheoryBitvectorprivate
d_bvTypePredsCVC3::TheoryBitvectorprivate
d_bvZeroCVC3::TheoryBitvectorprivate
d_eqCVC3::TheoryBitvectorprivate
d_eq_indexCVC3::TheoryBitvectorprivate
d_eqPendingCVC3::TheoryBitvectorprivate
d_index1CVC3::TheoryBitvectorprivate
d_index2CVC3::TheoryBitvectorprivate
d_maxLengthCVC3::TheoryBitvectorprivate
d_pushNegCacheCVC3::TheoryBitvectorprivate
d_rulesCVC3::TheoryBitvectorprivate
d_sharedSubtermsCVC3::TheoryBitvectorprivate
d_sharedSubtermsListCVC3::TheoryBitvectorprivate
d_theoryUsedCVC3::Theoryprotected
enqueueFact(const Theorem &e)CVC3::Theoryvirtual
enqueueSE(const Theorem &e)CVC3::Theoryvirtual
extract_vars(const Expr &e, std::vector< Expr > &vars)CVC3::TheoryBitvector
falseExpr()CVC3::Theoryinline
find(const Expr &e)CVC3::Theory
findExpr(const Expr &e)CVC3::Theoryinline
findReduce(const Expr &e)CVC3::Theory
findReduced(const Expr &e)CVC3::Theory
findRef(const Expr &e)CVC3::Theory
finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)CVC3::TheoryBitvectorvirtual
generalBitBlast(const Theorem &thm)CVC3::TheoryBitvectorprivate
getBaseType(const Expr &e)CVC3::Theory
getBaseType(const Type &tp)CVC3::Theory
getBitvectorTypeParam(const Expr &e)CVC3::TheoryBitvector
getBitvectorTypeParam(const Type &t)CVC3::TheoryBitvectorinline
getBoolExtractIndex(const Expr &e)CVC3::TheoryBitvector
getBVConstSize(const Expr &e)CVC3::TheoryBitvector
getBVConstValue(const Expr &e, int i)CVC3::TheoryBitvector
getBVIndex(const Expr &e)CVC3::TheoryBitvector
getBVMultParam(const Expr &e)CVC3::TheoryBitvector
getBVPlusParam(const Expr &e)CVC3::TheoryBitvector
getCommonRules()CVC3::Theoryinline
getEM()CVC3::Theoryinline
getExtractHi(const Expr &e)CVC3::TheoryBitvector
getExtractLow(const Expr &e)CVC3::TheoryBitvector
getFixedLeftShiftParam(const Expr &e)CVC3::TheoryBitvector
getFixedRightShiftParam(const Expr &e)CVC3::TheoryBitvector
getMaxSize()CVC3::TheoryBitvectorinline
getModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory
getModelValue(const Expr &e)CVC3::Theory
getName() const CVC3::Theoryinline
getNumTheories()CVC3::Theory
getSXIndex(const Expr &e)CVC3::TheoryBitvector
getTCC(const Expr &e)CVC3::Theory
getTypePred(const Type &t, const Expr &e)CVC3::Theory
getTypePredExpr(const Expr &tp)CVC3::TheoryBitvector
getTypePredType(const Expr &tp)CVC3::TheoryBitvector
hasTheory(int kind)CVC3::Theory
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::Theoryinline
inconsistent()CVC3::Theoryvirtual
installID(const std::string &name, const Expr &e)CVC3::Theory
isLeaf(const Expr &e)CVC3::Theoryinline
isLeafIn(const Expr &e1, const Expr &e2)CVC3::Theory
isLinearTerm(const Expr &e)CVC3::TheoryBitvector
isTermIn(const Expr &e1, const Expr &e2)CVC3::TheoryBitvectorprivate
leavesAreSimp(const Expr &e)CVC3::Theory
lookupFunction(const std::string &name, Type *type)CVC3::Theory
lookupTypeExpr(const std::string &name)CVC3::Theory
lookupVar(const std::string &name, Type *type)CVC3::Theory
min(std::vector< Rational > list)CVC3::TheoryBitvectorprivate
multiplicative_inverse(Rational r, int n_bits)CVC3::TheoryBitvector
multiply_coeff(Rational mult_inv, const Expr &e)CVC3::TheoryBitvectorprivate
newBitvectorType(int i)CVC3::TheoryBitvectorinline
newBitvectorTypeExpr(int i)CVC3::TheoryBitvector
newBitvectorTypePred(const Type &t, const Expr &e)CVC3::TheoryBitvector
newBoolExtractExpr(const Expr &t1, int r)CVC3::TheoryBitvector
newBVAndExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVAndExpr(const std::vector< Expr > &kids)CVC3::TheoryBitvector
newBVCompExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVConstExpr(const std::string &s, int base=2)CVC3::TheoryBitvector
newBVConstExpr(const std::vector< bool > &bits)CVC3::TheoryBitvector
newBVConstExpr(const Rational &r, int len=0)CVC3::TheoryBitvector
newBVExtractExpr(const Expr &e, int hi, int low)CVC3::TheoryBitvector
newBVIndexExpr(int kind, const Expr &t1, int len)CVC3::TheoryBitvector
newBVLEExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVLTExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVMultExpr(int bvLength, const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVMultExpr(int bvLength, const std::vector< Expr > &kids)CVC3::TheoryBitvector
newBVMultPadExpr(int bvLength, const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVMultPadExpr(int bvLength, const std::vector< Expr > &kids)CVC3::TheoryBitvector
newBVNandExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVNegExpr(const Expr &t1)CVC3::TheoryBitvector
newBVNorExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVOneString(int r)CVC3::TheoryBitvector
newBVOrExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVOrExpr(const std::vector< Expr > &kids)CVC3::TheoryBitvector
newBVPlusExpr(int numbits, const Expr &k1, const Expr &k2)CVC3::TheoryBitvector
newBVPlusExpr(int numbits, const std::vector< Expr > &k)CVC3::TheoryBitvector
newBVPlusPadExpr(int bvLength, const std::vector< Expr > &k)CVC3::TheoryBitvector
newBVSDivExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVSLEExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVSLTExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVSModExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVSRemExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVSubExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVUDivExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVUminusExpr(const Expr &t1)CVC3::TheoryBitvector
newBVURemExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVXnorExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVXnorExpr(const std::vector< Expr > &kids)CVC3::TheoryBitvector
newBVXorExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newBVXorExpr(const std::vector< Expr > &kids)CVC3::TheoryBitvector
newBVZeroString(int r)CVC3::TheoryBitvector
newConcatExpr(const Expr &t1, const Expr &t2)CVC3::TheoryBitvector
newConcatExpr(const Expr &t1, const Expr &t2, const Expr &t3)CVC3::TheoryBitvector
newConcatExpr(const std::vector< Expr > &kids)CVC3::TheoryBitvector
newFixedConstWidthLeftShiftExpr(const Expr &t1, int r)CVC3::TheoryBitvector
newFixedLeftShiftExpr(const Expr &t1, int r)CVC3::TheoryBitvector
newFixedRightShiftExpr(const Expr &t1, int r)CVC3::TheoryBitvector
newFunction(const std::string &name, const Type &type, bool computeTransClosure)CVC3::Theory
newFunction(const std::string &name, const Type &type, const Expr &def)CVC3::Theory
newSubtypeExpr(const Expr &pred, const Expr &witness)CVC3::Theory
newSXExpr(const Expr &t1, int len)CVC3::TheoryBitvector
newTypeExpr(const std::string &name)CVC3::Theory
newTypeExpr(const std::string &name, const Type &def)CVC3::Theory
newVar(const std::string &name, const Type &type)CVC3::Theory
newVar(const std::string &name, const Type &type, const Expr &def)CVC3::Theory
notifyInconsistent(const Theorem &thm)CVC3::Theoryinlinevirtual
Odd_coeff(const Expr &e)CVC3::TheoryBitvectorprivate
pad(int len, const Expr &e)CVC3::TheoryBitvector
parseExpr(const Expr &e)CVC3::Theoryvirtual
parseExprOp(const Expr &e)CVC3::TheoryBitvectorvirtual
print(ExprStream &os, const Expr &e)CVC3::TheoryBitvectorvirtual
printSmtLibShared(ExprStream &os, const Expr &e)CVC3::TheoryBitvectorprivate
pushNegation(const Expr &e)CVC3::TheoryBitvectorprivate
pushNegationRec(const Expr &e)CVC3::TheoryBitvector
rat(const Rational &r)CVC3::TheoryBitvectorinline
refineCounterExample()CVC3::Theoryinlinevirtual
reflexivityRule(const Expr &a)CVC3::Theoryinline
registerAtom(const Expr &e, const Theorem &thm)CVC3::Theoryvirtual
registerAtom(const Expr &e)CVC3::Theoryinlinevirtual
registerKinds(Theory *theory, std::vector< int > &kinds)CVC3::Theory
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)CVC3::Theory
renameExpr(const Expr &e)CVC3::Theory
resolveID(const std::string &name)CVC3::Theory
rewrite(const Expr &e)CVC3::TheoryBitvectorvirtual
rewriteAnd(const Expr &e)CVC3::Theoryinline
rewriteAtomic(const Expr &e)CVC3::TheoryBitvectorvirtual
rewriteBoolean(const Expr &e)CVC3::TheoryBitvectorprivate
rewriteBV(const Expr &e, ExprMap< Theorem > &cache, int n=1)CVC3::TheoryBitvectorprivate
rewriteBV(const Expr &e, int n=1)CVC3::TheoryBitvectorprivate
rewriteBV(const Theorem &t, ExprMap< Theorem > &cache, int n=1)CVC3::TheoryBitvectorinlineprivate
rewriteBV(const Theorem &t, int n=1)CVC3::TheoryBitvectorinlineprivate
rewriteCC(const Expr &e)CVC3::Theory
rewriteIte(const Expr &e)CVC3::Theory
rewriteOr(const Expr &e)CVC3::Theoryinline
setIncomplete(const std::string &reason)CVC3::Theoryvirtual
setInconsistent(const Theorem &e)CVC3::Theoryvirtual
setup(const Expr &e)CVC3::TheoryBitvectorvirtual
setupCC(const Expr &e)CVC3::Theory
setUsed()CVC3::Theoryinlinevirtual
signed_newBVConstExpr(Rational c, int bv_size)CVC3::TheoryBitvector
simplify(const Expr &e)CVC3::Theoryvirtual
simplifyExpr(const Expr &e)CVC3::Theoryinline
simplifyOp(const Expr &e)CVC3::TheoryBitvectorprivatevirtual
simplifyPendingEq(const Theorem &thm, int maxEffort)CVC3::TheoryBitvectorprivate
solve(const Theorem &e)CVC3::TheoryBitvectorvirtual
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVC3::Theoryinline
substitutivityRule(const Expr &e, const Theorem &t)CVC3::Theoryinline
substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2)CVC3::Theoryinline
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVC3::Theoryinline
substitutivityRule(const Expr &e, int changed, const Theorem &thm)CVC3::Theoryinline
symmetryRule(const Theorem &a1_eq_a2)CVC3::Theoryinline
Theory(TheoryCore *theoryCore, const std::string &name)CVC3::Theory
TheoryBitvector(TheoryCore *core)CVC3::TheoryBitvector
theoryCore()CVC3::Theoryinline
theoryOf(int kind)CVC3::Theory
theoryOf(const Type &e)CVC3::Theory
theoryOf(const Expr &e)CVC3::Theory
theoryPreprocess(const Expr &e)CVC3::Theoryinlinevirtual
theoryUsed()CVC3::Theoryinlinevirtual
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::Theoryinline
trueExpr()CVC3::Theoryinline
typePred(const Expr &e)CVC3::Theory
unregisterKinds(Theory *theory, std::vector< int > &kinds)CVC3::Theory
unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver)CVC3::Theory
update(const Theorem &e, const Expr &d)CVC3::TheoryBitvectorvirtual
updateCC(const Theorem &e, const Expr &d)CVC3::Theory
updateHelper(const Expr &e)CVC3::Theory
updateSubterms(const Expr &d)CVC3::TheoryBitvectorprivate
~Theory(void)CVC3::Theoryvirtual
~TheoryBitvector()CVC3::TheoryBitvector