| addIndex(const Expr &e) | CVC3::CompleteInstPreProcessor | [private] |
| collect_forall_index(const Expr &forall_quant) | CVC3::CompleteInstPreProcessor | [private] |
| collect_shield_index(const Expr &e) | CVC3::CompleteInstPreProcessor | [private] |
| collectHeads(const Expr &assert, std::set< Expr > &heads) | CVC3::CompleteInstPreProcessor | [private] |
| collectIndex(const Expr &e) | CVC3::CompleteInstPreProcessor | |
| CompleteInstPreProcessor(TheoryCore *, QuantProofRules *) | CVC3::CompleteInstPreProcessor | |
| d_all_good | CVC3::CompleteInstPreProcessor | [private] |
| d_allIndex | CVC3::CompleteInstPreProcessor | [private] |
| d_expr_pol | CVC3::CompleteInstPreProcessor | [private] |
| d_gnd_cache | CVC3::CompleteInstPreProcessor | [private] |
| d_is_macro_def | CVC3::CompleteInstPreProcessor | [private] |
| d_macro_def | CVC3::CompleteInstPreProcessor | [private] |
| d_macro_lhs | CVC3::CompleteInstPreProcessor | [private] |
| d_macro_quant | CVC3::CompleteInstPreProcessor | [private] |
| d_quant_equiv_map | CVC3::CompleteInstPreProcessor | [private] |
| d_quant_rules | CVC3::CompleteInstPreProcessor | [private] |
| d_theoryCore | CVC3::CompleteInstPreProcessor | [private] |
| hasMacros(const std::vector< Expr > &asserts) | CVC3::CompleteInstPreProcessor | |
| inst(const Expr &e) | CVC3::CompleteInstPreProcessor | |
| instMacros(const Expr &, const Expr) | CVC3::CompleteInstPreProcessor | |
| isGood(const Expr &e) | CVC3::CompleteInstPreProcessor | |
| isGoodQuant(const Expr &e) | CVC3::CompleteInstPreProcessor | [private] |
| isMacro(const Expr &assert) | CVC3::CompleteInstPreProcessor | [private] |
| isShield(const Expr &e) | CVC3::CompleteInstPreProcessor | [private] |
| minusOne(const Expr &e) | CVC3::CompleteInstPreProcessor | [private] |
| plusOne(const Expr &e) | CVC3::CompleteInstPreProcessor | [private] |
| pullVarOut(const Expr &) | CVC3::CompleteInstPreProcessor | [private] |
| recInstMacros(const Expr &assert) | CVC3::CompleteInstPreProcessor | [private] |
| recRewriteNot(const Expr &, ExprMap< Polarity > &) | CVC3::CompleteInstPreProcessor | [private] |
| recSkolemize(const Expr &, ExprMap< Polarity > &) | CVC3::CompleteInstPreProcessor | [private] |
| rewriteNot(const Expr &) | CVC3::CompleteInstPreProcessor | [private] |
| simplifyEq(const Expr &) | CVC3::CompleteInstPreProcessor | |
| simplifyQuant(const Expr &) | CVC3::CompleteInstPreProcessor | |
| substMacro(const Expr &) | CVC3::CompleteInstPreProcessor | [private] |
