expandEq(const Theorem &eqThrm)=0 | CVCL::RecordsProofRules | [pure virtual] |
expandNeq(const Theorem &neqThrm)=0 | CVCL::RecordsProofRules | [pure virtual] |
expandRecord(const Expr &e)=0 | CVCL::RecordsProofRules | [pure virtual] |
expandTuple(const Expr &e)=0 | CVCL::RecordsProofRules | [pure virtual] |
rewriteLitSelect(const Expr &e)=0 | CVCL::RecordsProofRules | [pure virtual] |
rewriteLitUpdate(const Expr &e)=0 | CVCL::RecordsProofRules | [pure virtual] |
rewriteUpdateSelect(const Expr &e)=0 | CVCL::RecordsProofRules | [pure virtual] |
~RecordsProofRules() | CVCL::RecordsProofRules | [inline, virtual] |