CVC3
datatype_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file datatype_theorem_producer.h
4  *\brief TRUSTED implementation of recursive datatype proof rules
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Mon Jan 10 15:42:22 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: DatatypeTheoremProducer
20  *
21  */
22 /*****************************************************************************/
23 #ifndef _cvc3__theory_datatype__datatype_theorem_producer_h_
24 #define _cvc3__theory_datatype__datatype_theorem_producer_h_
25 
26 #include "datatype_proof_rules.h"
27 #include "theorem_producer.h"
28 #include "theory_datatype.h"
29 #include "theory_core.h"
30 
31 namespace CVC3 {
32 
35 private:
36 public:
37  //! Constructor
39  TheoremProducer(theoryDatatype->theoryCore()->getTM()),
40  d_theoryDatatype(theoryDatatype) { }
41 
42  Theorem dummyTheorem(const CDList<Theorem>& facts, const Expr& e);
43  Theorem rewriteSelCons(const CDList<Theorem>& facts, const Expr& e);
44  Theorem rewriteTestCons(const Expr& e);
45  Theorem decompose(const Theorem& e);
46  Theorem noCycle(const Expr& e);
47 
48  }; // end of class DatatypeTheoremProducer
49 } // end of namespace CVC3
50 
51 #endif
52