| 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 | |
| additionalRewriteConstraints | CVC3::TheoryBitvector | |
| addSharedTerm(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| addSplitter(const Expr &e, int priority=0) | CVC3::Theory | |
| assertEqualities(const Theorem &e) | CVC3::Theory | [virtual] |
| assertFact(const Theorem &e) | CVC3::TheoryBitvector | [virtual] |
| assertTypePred(const Expr &e, const Theorem &pred) | CVC3::TheoryBitvector | [virtual] |
| assignValue(const Expr &t, const Expr &val) | CVC3::Theory | [virtual] |
| assignValue(const Theorem &thm) | CVC3::Theory | [virtual] |
| bitBlastDisEqn(const Theorem ¬E) | CVC3::TheoryBitvector | [private] |
| bitBlastEqn(const Expr &e) | CVC3::TheoryBitvector | [private] |
| bitBlastIneqn(const Expr &e) | CVC3::TheoryBitvector | [private] |
| bitBlastTerm(const Expr &t, int bitPosition) | CVC3::TheoryBitvector | [private] |
| boolType() | CVC3::Theory | [inline] |
| bvOne() const | CVC3::TheoryBitvector | [inline, private] |
| BVSize(const Expr &e) | CVC3::TheoryBitvector | |
| bvZero() const | CVC3::TheoryBitvector | [inline, private] |
| canSolveFor(const Expr &term, const Expr &e) | CVC3::TheoryBitvector | |
| check_linear(const Expr &e) | CVC3::TheoryBitvector | [private] |
| checkAssertEqInvariant(const Theorem &e) | CVC3::Theory | [inline, virtual] |
| checkSat(bool fullEffort) | CVC3::TheoryBitvector | [virtual] |
| checkType(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| comparebv(const Expr &e1, const Expr &e2) | CVC3::TheoryBitvector | |
| computeBaseType(const Type &tp) | CVC3::Theory | [inline, virtual] |
| computeBVConst(const Expr &e) | CVC3::TheoryBitvector | |
| computeModel(const Expr &e, std::vector< Expr > &vars) | CVC3::TheoryBitvector | [virtual] |
| computeModelBasic(const std::vector< Expr > &v) | CVC3::Theory | [inline, virtual] |
| computeModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::TheoryBitvector | [virtual] |
| computeNegBVConst(const Expr &e) | CVC3::TheoryBitvector | |
| computeTCC(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| computeType(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| computeTypePred(const Type &t, const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| countTermIn(const Expr &term, const Expr &e) | CVC3::TheoryBitvector | [private] |
| createProofRules() | CVC3::TheoryBitvector | |
| d_bb_index | CVC3::TheoryBitvector | [private] |
| d_bitblast | CVC3::TheoryBitvector | [private] |
| d_bitvecCache | CVC3::TheoryBitvector | [private] |
| d_booleanRWFlag | CVC3::TheoryBitvector | [private] |
| d_boolExtractCacheFlag | CVC3::TheoryBitvector | [private] |
| d_bv32Flag | CVC3::TheoryBitvector | [private] |
| d_bvAssertDiseq | CVC3::TheoryBitvector | [private] |
| d_bvAssertEq | CVC3::TheoryBitvector | [private] |
| d_bvBitBlastDiseq | CVC3::TheoryBitvector | [private] |
| d_bvBitBlastEq | CVC3::TheoryBitvector | [private] |
| d_bvConstExprIndex | CVC3::TheoryBitvector | [private] |
| d_bvDelayDiseq | CVC3::TheoryBitvector | [private] |
| d_bvDelayEq | CVC3::TheoryBitvector | [private] |
| d_bvDelayTypePreds | CVC3::TheoryBitvector | [private] |
| d_bvOne | CVC3::TheoryBitvector | [private] |
| d_bvParameterExprIndex | CVC3::TheoryBitvector | [private] |
| d_bvPlusCarryCacheLeftBV | CVC3::TheoryBitvector | |
| d_bvPlusCarryCacheRightBV | CVC3::TheoryBitvector | |
| d_bvPlusExprIndex | CVC3::TheoryBitvector | [private] |
| d_bvTypePredExprIndex | CVC3::TheoryBitvector | [private] |
| d_bvTypePreds | CVC3::TheoryBitvector | [private] |
| d_bvZero | CVC3::TheoryBitvector | [private] |
| d_eq | CVC3::TheoryBitvector | [private] |
| d_eq_index | CVC3::TheoryBitvector | [private] |
| d_eqPending | CVC3::TheoryBitvector | [private] |
| d_index1 | CVC3::TheoryBitvector | [private] |
| d_index2 | CVC3::TheoryBitvector | [private] |
| d_maxLength | CVC3::TheoryBitvector | [private] |
| d_pushNegCache | CVC3::TheoryBitvector | [private] |
| d_rules | CVC3::TheoryBitvector | [private] |
| d_sharedSubterms | CVC3::TheoryBitvector | [private] |
| d_sharedSubtermsList | CVC3::TheoryBitvector | [private] |
| d_theoryUsed | CVC3::Theory | [protected] |
| enqueueFact(const Theorem &e) | CVC3::Theory | [virtual] |
| enqueueSE(const Theorem &e) | CVC3::Theory | [virtual] |
| extract_vars(const Expr &e, std::vector< Expr > &vars) | CVC3::TheoryBitvector | |
| falseExpr() | CVC3::Theory | [inline] |
| find(const Expr &e) | CVC3::Theory | |
| findExpr(const Expr &e) | CVC3::Theory | [inline] |
| 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::TheoryBitvector | [virtual] |
| generalBitBlast(const Theorem &thm) | CVC3::TheoryBitvector | [private] |
| getBaseType(const Expr &e) | CVC3::Theory | |
| getBaseType(const Type &tp) | CVC3::Theory | |
| getBitvectorTypeParam(const Expr &e) | CVC3::TheoryBitvector | |
| getBitvectorTypeParam(const Type &t) | CVC3::TheoryBitvector | [inline] |
| 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::Theory | [inline] |
| getEM() | CVC3::Theory | [inline] |
| 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::TheoryBitvector | [inline] |
| getModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::Theory | |
| getModelValue(const Expr &e) | CVC3::Theory | |
| getName() const | CVC3::Theory | [inline] |
| 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::Theory | [inline] |
| inconsistent() | CVC3::Theory | [virtual] |
| installID(const std::string &name, const Expr &e) | CVC3::Theory | |
| isLeaf(const Expr &e) | CVC3::Theory | [inline] |
| isLeafIn(const Expr &e1, const Expr &e2) | CVC3::Theory | |
| isLinearTerm(const Expr &e) | CVC3::TheoryBitvector | |
| isTermIn(const Expr &e1, const Expr &e2) | CVC3::TheoryBitvector | [private] |
| 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::TheoryBitvector | [private] |
| multiplicative_inverse(Rational r, int n_bits) | CVC3::TheoryBitvector | |
| multiply_coeff(Rational mult_inv, const Expr &e) | CVC3::TheoryBitvector | [private] |
| newBitvectorType(int i) | CVC3::TheoryBitvector | [inline] |
| 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::Theory | [inline, virtual] |
| Odd_coeff(const Expr &e) | CVC3::TheoryBitvector | [private] |
| pad(int len, const Expr &e) | CVC3::TheoryBitvector | |
| parseExpr(const Expr &e) | CVC3::Theory | [virtual] |
| parseExprOp(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| print(ExprStream &os, const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| pushNegation(const Expr &e) | CVC3::TheoryBitvector | [private] |
| pushNegationRec(const Expr &e) | CVC3::TheoryBitvector | |
| rat(const Rational &r) | CVC3::TheoryBitvector | [inline] |
| refineCounterExample() | CVC3::Theory | [inline, virtual] |
| reflexivityRule(const Expr &a) | CVC3::Theory | [inline] |
| registerAtom(const Expr &e, const Theorem &thm) | CVC3::Theory | [virtual] |
| registerAtom(const Expr &e) | CVC3::Theory | [inline, virtual] |
| registerKinds(Theory *theory, std::vector< int > &kinds) | CVC3::Theory | |
| registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false) | CVC3::Theory | |
| resolveID(const std::string &name) | CVC3::Theory | |
| rewrite(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| rewriteAnd(const Expr &e) | CVC3::Theory | [inline] |
| rewriteAtomic(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| rewriteBoolean(const Expr &e) | CVC3::TheoryBitvector | [private] |
| rewriteBV(const Expr &e, ExprMap< Theorem > &cache, int n=1) | CVC3::TheoryBitvector | [private] |
| rewriteBV(const Expr &e, int n=1) | CVC3::TheoryBitvector | [private] |
| rewriteBV(const Theorem &t, ExprMap< Theorem > &cache, int n=1) | CVC3::TheoryBitvector | [inline, private] |
| rewriteBV(const Theorem &t, int n=1) | CVC3::TheoryBitvector | [inline, private] |
| rewriteCC(const Expr &e) | CVC3::Theory | |
| rewriteIte(const Expr &e) | CVC3::Theory | |
| rewriteOr(const Expr &e) | CVC3::Theory | [inline] |
| setIncomplete(const std::string &reason) | CVC3::Theory | [virtual] |
| setInconsistent(const Theorem &e) | CVC3::Theory | [virtual] |
| setup(const Expr &e) | CVC3::TheoryBitvector | [virtual] |
| setupCC(const Expr &e) | CVC3::Theory | |
| setUsed() | CVC3::Theory | [inline, virtual] |
| signed_newBVConstExpr(Rational c, int bv_size) | CVC3::TheoryBitvector | |
| simplify(const Expr &e) | CVC3::Theory | [virtual] |
| simplifyExpr(const Expr &e) | CVC3::Theory | [inline] |
| simplifyOp(const Expr &e) | CVC3::TheoryBitvector | [private, virtual] |
| simplifyPendingEq(const Theorem &thm, int maxEffort) | CVC3::TheoryBitvector | [private] |
| solve(const Theorem &e) | CVC3::TheoryBitvector | [virtual] |
| substitutivityRule(const Op &op, const std::vector< Theorem > &thms) | CVC3::Theory | [inline] |
| substitutivityRule(const Expr &e, const Theorem &t) | CVC3::Theory | [inline] |
| substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2) | CVC3::Theory | [inline] |
| substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms) | CVC3::Theory | [inline] |
| substitutivityRule(const Expr &e, int changed, const Theorem &thm) | CVC3::Theory | [inline] |
| symmetryRule(const Theorem &a1_eq_a2) | CVC3::Theory | [inline] |
| Theory(TheoryCore *theoryCore, const std::string &name) | CVC3::Theory | |
| TheoryBitvector(TheoryCore *core) | CVC3::TheoryBitvector | |
| theoryCore() | CVC3::Theory | [inline] |
| theoryOf(int kind) | CVC3::Theory | |
| theoryOf(const Type &e) | CVC3::Theory | |
| theoryOf(const Expr &e) | CVC3::Theory | |
| theoryPreprocess(const Expr &e) | CVC3::Theory | [inline, virtual] |
| theoryUsed() | CVC3::Theory | [inline, virtual] |
| transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) | CVC3::Theory | [inline] |
| trueExpr() | CVC3::Theory | [inline] |
| 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::TheoryBitvector | [virtual] |
| updateCC(const Theorem &e, const Expr &d) | CVC3::Theory | |
| updateHelper(const Expr &e) | CVC3::Theory | |
| updateSubterms(const Expr &d) | CVC3::TheoryBitvector | [private] |
| ~Theory(void) | CVC3::Theory | [virtual] |
| ~TheoryBitvector() | CVC3::TheoryBitvector | |
