CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_datatype
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
33
class
DatatypeProofRules
{
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
Generated on Sat May 18 2013 12:01:24 for CVC3 by
1.8.3.1