CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 *\file datatype_theorem_producer.h 00004 *\brief TRUSTED implementation of recursive datatype proof rules 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Mon Jan 10 15:42:22 2005 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 * 00019 * CLASS: DatatypeTheoremProducer 00020 * 00021 */ 00022 /*****************************************************************************/ 00023 #ifndef _cvc3__theory_datatype__datatype_theorem_producer_h_ 00024 #define _cvc3__theory_datatype__datatype_theorem_producer_h_ 00025 00026 #include "datatype_proof_rules.h" 00027 #include "theorem_producer.h" 00028 #include "theory_datatype.h" 00029 #include "theory_core.h" 00030 00031 namespace CVC3 { 00032 00033 class DatatypeTheoremProducer: public DatatypeProofRules, public TheoremProducer { 00034 TheoryDatatype* d_theoryDatatype; 00035 private: 00036 public: 00037 //! Constructor 00038 DatatypeTheoremProducer(TheoryDatatype* theoryDatatype) : 00039 TheoremProducer(theoryDatatype->theoryCore()->getTM()), 00040 d_theoryDatatype(theoryDatatype) { } 00041 00042 Theorem dummyTheorem(const CDList<Theorem>& facts, const Expr& e); 00043 Theorem rewriteSelCons(const CDList<Theorem>& facts, const Expr& e); 00044 Theorem rewriteTestCons(const Expr& e); 00045 Theorem decompose(const Theorem& e); 00046 Theorem noCycle(const Expr& e); 00047 00048 }; // end of class DatatypeTheoremProducer 00049 } // end of namespace CVC3 00050 00051 #endif 00052