#include <datatype_theorem_producer.h>
Inheritance diagram for CVC3::DatatypeTheoremProducer:
Definition at line 33 of file datatype_theorem_producer.h.
CVC3::DatatypeTheoremProducer::DatatypeTheoremProducer | ( | TheoryDatatype * | theoryDatatype | ) | [inline] |
Theorem DatatypeTheoremProducer::dummyTheorem | ( | const CDList< Theorem > & | facts, | |
const Expr & | e | |||
) | [virtual] |
Implements CVC3::DatatypeProofRules.
Definition at line 52 of file datatype_theorem_producer.cpp.
References CVC3::TheoremProducer::newTheorem(), and CVC3::CDList< T >::size().
Theorem DatatypeTheoremProducer::rewriteSelCons | ( | const CDList< Theorem > & | facts, | |
const Expr & | e | |||
) | [virtual] |
Implements CVC3::DatatypeProofRules.
Definition at line 63 of file datatype_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::TheoryDatatype::canCollapse(), CHECK_PROOFS, CHECK_SOUND, d_theoryDatatype, CVC3::Assumptions::emptyAssump(), CVC3::TheoryDatatype::getConstant(), CVC3::getConstructor(), CVC3::Type::getExpr(), CVC3::Expr::getOpExpr(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::Expr::getType(), CVC3::isConstructor(), CVC3::isSelector(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CDList< T >::size(), and CVC3::TheoremProducer::withProof().
Implements CVC3::DatatypeProofRules.
Definition at line 99 of file datatype_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, d_theoryDatatype, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::TheoryDatatype::getConsForTester(), CVC3::getConstructor(), CVC3::Expr::getOpExpr(), CVC3::isConstructor(), CVC3::isTester(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().
Implements CVC3::DatatypeProofRules.
Definition at line 118 of file datatype_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getLHS(), CVC3::Expr::getOpExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::isApply(), CVC3::isConstructor(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Implements CVC3::DatatypeProofRules.
Definition at line 147 of file datatype_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::Type::arity(), CHECK_PROOFS, CHECK_SOUND, d_theoryDatatype, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpExpr(), CVC3::TheoryDatatype::getReachablePredicate(), CVC3::Expr::getType(), CVC3::isConstructor(), CVC3::isDatatype(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Definition at line 34 of file datatype_theorem_producer.h.
Referenced by noCycle(), rewriteSelCons(), and rewriteTestCons().