CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_uf
uf_theorem_producer.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file uf_theorem_producer.h
4
*\brief TRUSTED implementation of uninterpreted function/predicate proof rules
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Tue Aug 31 23:14:54 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: UFTheoremProducer
20
*
21
*/
22
/*****************************************************************************/
23
#ifndef _cvc3__theory_uf__uf_theorem_producer_h_
24
#define _cvc3__theory_uf__uf_theorem_producer_h_
25
26
#include "
uf_proof_rules.h
"
27
#include "
theorem_producer.h
"
28
29
namespace
CVC3 {
30
31
class
TheoryUF;
32
33
class
UFTheoremProducer
:
public
UFProofRules
,
public
TheoremProducer
{
34
TheoryUF
*
d_theoryUF
;
35
private
:
36
public
:
37
//! Constructor
38
UFTheoremProducer
(
TheoremManager
* tm,
TheoryUF
* theoryUF) :
39
TheoremProducer
(tm),
d_theoryUF
(theoryUF) { }
40
41
Theorem
relToClosure
(
const
Theorem
& rel);
42
Theorem
relTrans
(
const
Theorem
& t1,
const
Theorem
& t2);
43
Theorem
applyLambda
(
const
Expr
& e);
44
Theorem
rewriteOpDef
(
const
Expr
& e);
45
46
};
// end of class UFTheoremProducer
47
}
// end of namespace CVC3
48
49
#endif
50
Generated on Tue May 14 2013 14:44:54 for CVC3 by
1.8.3.1