CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
proof.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file proof.h
4
*
5
* Author: Sergey Berezin
6
*
7
* Created: Dec 10 00:37:49 GMT 2002
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
*/
19
/*****************************************************************************/
20
// CLASS: Proof
21
//
22
// AUTHOR: Sergey Berezin, 12/03/2002
23
//
24
// Abstract:
25
//
26
// Proof is a wrapper around Expr, to prevent accidental mix-up. Only
27
// proof rules and adaptors are supposed to use any of its methods.
28
///////////////////////////////////////////////////////////////////////////////
29
#ifndef _cvc3__expr_h_
30
#include "
expr.h
"
31
#endif
32
33
#ifndef _cvc3__proof_h_
34
#define _cvc3__proof_h_
35
36
namespace
CVC3 {
37
38
class
Proof
{
39
private
:
40
Expr
d_proof
;
41
// unsigned d_insts; //by yeting, this is to store the number of instantiations. debug only
42
public
:
43
Proof
(
const
Expr
&e) :
d_proof
(e) { }
// Constructor
44
Proof
(
const
Proof
& p) :
d_proof
(p.
d_proof
) { }
// Copy constructor
45
Proof
() :
d_proof
() { }
// Null proof constructor
46
Expr
getExpr
()
const
{
return
d_proof
; }
// Extract the expr handle
47
bool
isNull
()
const
{
return
d_proof
.
isNull
(); }
48
// Printing
49
friend
std::ostream&
operator<<
(std::ostream& os,
const
Proof
& pf);
50
std::string
toString
()
const
{
51
std::ostringstream ss;
52
ss<<(*this);
53
return
ss.str();
54
}
55
};
// End of class Proof
56
57
inline
std::ostream&
operator<<
(std::ostream& os,
const
Proof
& pf) {
58
return
os <<
"Proof("
<< pf.
getExpr
() <<
")"
;
59
}
60
61
inline
bool
operator==
(
const
Proof
& pf1,
const
Proof
& pf2) {
62
return
pf1.
getExpr
() == pf2.
getExpr
();
63
}
64
65
}
// end of namespace CVC3
66
#endif
Generated on Tue May 14 2013 15:43:30 for CVC3 by
1.8.3.1