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