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