CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_datatype
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
33
class
DatatypeTheoremProducer
:
public
DatatypeProofRules
,
public
TheoremProducer
{
34
TheoryDatatype
*
d_theoryDatatype
;
35
private
:
36
public
:
37
//! Constructor
38
DatatypeTheoremProducer
(
TheoryDatatype
* theoryDatatype) :
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
Generated on Tue May 14 2013 15:43:25 for CVC3 by
1.8.3.1