|
CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 *\file datatype_proof_rules.h 00004 *\brief Abstract interface for recursive datatype proof rules 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Mon Jan 10 15:40:24 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: DatatypeProofRules 00020 * 00021 */ 00022 /*****************************************************************************/ 00023 00024 #ifndef _cvc3__theory_datatype__datatype_proof_rules_h_ 00025 #define _cvc3__theory_datatype__datatype_proof_rules_h_ 00026 00027 namespace CVC3 { 00028 00029 class Expr; 00030 class Theorem; 00031 template<class T> class CDList; 00032 00033 class DatatypeProofRules { 00034 public: 00035 // Destructor 00036 virtual ~DatatypeProofRules() { } 00037 00038 //////////////////////////////////////////////////////////////////// 00039 // Proof rules 00040 //////////////////////////////////////////////////////////////////// 00041 00042 virtual Theorem dummyTheorem(const CDList<Theorem>& facts, 00043 const Expr& e) = 0; 00044 virtual Theorem rewriteSelCons(const CDList<Theorem>& facts, const Expr& e) = 0; 00045 virtual Theorem rewriteTestCons(const Expr& e) = 0; 00046 virtual Theorem decompose(const Theorem& e) = 0; 00047 virtual Theorem noCycle(const Expr& e) = 0; 00048 00049 }; // end of class DatatypeProofRules 00050 00051 } // end of namespace CVC3 00052 00053 #endif
1.7.3