CVC3
2.4.1
|
#include <datatype_proof_rules.h>
Definition at line 33 of file datatype_proof_rules.h.
virtual CVC3::DatatypeProofRules::~DatatypeProofRules | ( | ) | [inline, virtual] |
Definition at line 36 of file datatype_proof_rules.h.
virtual Theorem CVC3::DatatypeProofRules::dummyTheorem | ( | const CDList< Theorem > & | facts, |
const Expr & | e | ||
) | [pure virtual] |
virtual Theorem CVC3::DatatypeProofRules::rewriteSelCons | ( | const CDList< Theorem > & | facts, |
const Expr & | e | ||
) | [pure virtual] |
Implemented in CVC3::DatatypeTheoremProducer.
Referenced by CVC3::TheoryDatatype::rewrite(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().
virtual Theorem CVC3::DatatypeProofRules::rewriteTestCons | ( | const Expr & | e | ) | [pure virtual] |
Implemented in CVC3::DatatypeTheoremProducer.
Referenced by CVC3::TheoryDatatype::rewrite(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().
virtual Theorem CVC3::DatatypeProofRules::decompose | ( | const Theorem & | e | ) | [pure virtual] |
Implemented in CVC3::DatatypeTheoremProducer.
Referenced by CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().
virtual Theorem CVC3::DatatypeProofRules::noCycle | ( | const Expr & | e | ) | [pure virtual] |
Implemented in CVC3::DatatypeTheoremProducer.
Referenced by CVC3::TheoryDatatypeLazy::setup(), and CVC3::TheoryDatatype::setup().