CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_uf
uf_proof_rules.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file uf_proof_rules.h
4
*\brief Abstract interface for uninterpreted function/predicate proof rules
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Tue Aug 31 23:12:01 2004
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: UFProofRules
20
*
21
*/
22
/*****************************************************************************/
23
24
#ifndef _cvc3__theory_uf__uf_proof_rules_h_
25
#define _cvc3__theory_uf__uf_proof_rules_h_
26
27
namespace
CVC3 {
28
29
class
Expr;
30
class
Theorem;
31
32
class
UFProofRules
{
33
public
:
34
// Destructor
35
virtual
~UFProofRules
() { }
36
37
////////////////////////////////////////////////////////////////////
38
// Proof rules
39
////////////////////////////////////////////////////////////////////
40
41
virtual
Theorem
relToClosure
(
const
Theorem
& rel) = 0;
42
virtual
Theorem
relTrans
(
const
Theorem
& t1,
const
Theorem
& t2) = 0;
43
44
//! Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
45
virtual
Theorem
applyLambda
(
const
Expr
& e) = 0;
46
//! Replace LETDECL in the operator with the definition
47
virtual
Theorem
rewriteOpDef
(
const
Expr
& e) = 0;
48
49
};
// end of class UFProofRules
50
51
}
// end of namespace CVC3
52
53
#endif
Generated on Mon Aug 19 2013 14:42:45 for CVC3 by
1.8.4