CVC3  2.4.1
datatype_proof_rules.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file datatype_proof_rules.h
4  *\brief Abstract interface for recursive datatype proof rules
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Mon Jan 10 15:40:24 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  * CLASS: DatatypeProofRules
20  *
21  */
22 /*****************************************************************************/
23 
24 #ifndef _cvc3__theory_datatype__datatype_proof_rules_h_
25 #define _cvc3__theory_datatype__datatype_proof_rules_h_
26 
27 namespace CVC3 {
28 
29  class Expr;
30  class Theorem;
31  template<class T> class CDList;
32 
34  public:
35  // Destructor
36  virtual ~DatatypeProofRules() { }
37 
38  ////////////////////////////////////////////////////////////////////
39  // Proof rules
40  ////////////////////////////////////////////////////////////////////
41 
42  virtual Theorem dummyTheorem(const CDList<Theorem>& facts,
43  const Expr& e) = 0;
44  virtual Theorem rewriteSelCons(const CDList<Theorem>& facts, const Expr& e) = 0;
45  virtual Theorem rewriteTestCons(const Expr& e) = 0;
46  virtual Theorem decompose(const Theorem& e) = 0;
47  virtual Theorem noCycle(const Expr& e) = 0;
48 
49  }; // end of class DatatypeProofRules
50 
51 } // end of namespace CVC3
52 
53 #endif
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem rewriteSelCons(const CDList< Theorem > &facts, const Expr &e)=0
virtual Theorem decompose(const Theorem &e)=0
virtual Theorem noCycle(const Expr &e)=0
virtual Theorem dummyTheorem(const CDList< Theorem > &facts, const Expr &e)=0
virtual Theorem rewriteTestCons(const Expr &e)=0
Definition: expr.cpp:35