CVC3
2.4.1
|
#include <datatype_theorem_producer.h>
CVC3::DatatypeTheoremProducer::DatatypeTheoremProducer | ( | TheoryDatatype * | theoryDatatype | ) | [inline] |
Constructor.
Definition at line 38 of file datatype_theorem_producer.h.
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::CDList::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 CHECK_PROOFS, CHECK_SOUND, CVC3::isSelector(), CVC3::Expr::getOpExpr(), CVC3::isConstructor(), CVC3::getConstructor(), CVC3::Expr::getType(), CVC3::Type::getExpr(), CVC3::Expr::arity(), and CVC3::CDList::size().
Implements CVC3::DatatypeProofRules.
Definition at line 99 of file datatype_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::isTester(), CVC3::isConstructor(), CVC3::Expr::getOpExpr(), and CVC3::getConstructor().
Implements CVC3::DatatypeProofRules.
Definition at line 118 of file datatype_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::isRewrite(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::isConstructor(), CVC3::Expr::isApply(), CVC3::Expr::getOpExpr(), CVC3::Expr::arity(), CVC3::Expr::eqExpr(), CVC3::andExpr(), and CVC3::Theorem::getProof().
Implements CVC3::DatatypeProofRules.
Definition at line 147 of file datatype_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::isConstructor(), CVC3::Expr::isApply(), CVC3::Expr::arity(), CVC3::Expr::getOpExpr(), CVC3::Expr::getType(), CVC3::Type::arity(), CVC3::isDatatype(), and CVC3::andExpr().
Definition at line 34 of file datatype_theorem_producer.h.