CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
Object.h
Go to the documentation of this file.
1
#ifndef OBJ_H_
2
#define OBJ_H_
3
4
#include "
theory_core.h
"
5
#include "
theorem_manager.h
"
6
#include "
common_proof_rules.h
"
7
#include "
command_line_flags.h
"
8
#include "
theory_arith.h
"
9
#include <fstream>
10
11
#define _CVC3_TRUSTED_
12
13
using namespace
std;
14
using namespace
CVC3;
15
16
17
//#define DEBUG_MEM_STATS
18
// flag for testing some cvc3 custom made prof rules
19
//#define PRINT_MAJOR_METHODS
20
//#define LRA2_PRIME
21
//#define OPTIMIZE
22
//#define IGNORE_NORMALIZE
23
//#define IGNORE_LETPF_VARS
24
//#define IGNORE_PRINT_MULTI_LAMBDA
25
26
//smart pointer class
27
template
<
class
T>
28
class
RefPtr
29
{
30
public
:
31
typedef
T
element_type
;
32
RefPtr
() :_ptr(0L) {}
33
RefPtr
(T* t):_ptr(t) {
if
(_ptr) _ptr->Ref(); }
34
RefPtr
(
const
RefPtr
& rp):_ptr(rp._ptr) {
if
(_ptr) _ptr->Ref(); }
35
~RefPtr
() {
if
(_ptr) _ptr->Unref(); _ptr=0; }
36
inline
RefPtr
& operator = (
const
RefPtr
& rp){
37
if
(_ptr==rp.
_ptr
)
return
*
this
;
38
T* tmp_ptr = _ptr;
39
_ptr = rp.
_ptr
;
40
if
(_ptr) _ptr->Ref();
41
if
(tmp_ptr) tmp_ptr->Unref();
42
return
*
this
;
43
}
44
inline
RefPtr
& operator = (T* ptr){
45
if
(_ptr==ptr)
return
*
this
;
46
T* tmp_ptr = _ptr;
47
_ptr = ptr;
48
if
(_ptr) _ptr->Ref();
49
if
(tmp_ptr) tmp_ptr->Unref();
50
return
*
this
;
51
}
52
inline
T&
operator*
() {
return
*_ptr; }
53
inline
const
T&
operator*
()
const
{
return
*_ptr; }
54
inline
T*
operator->
() {
return
_ptr; }
55
inline
const
T*
operator->
()
const
{
return
_ptr; }
56
inline
T*
get
() {
return
_ptr; }
57
inline
const
T*
get
()
const
{
return
_ptr; }
58
private
:
59
T*
_ptr
;
60
};
61
62
//standard (reference pointer) object
63
class
Obj
64
{
65
protected
:
66
ostringstream
oignore
;
67
int
refCount
;
68
69
static
bool
errsInit
;
70
static
ofstream
errs
;
71
static
bool
indentFlag
;
72
73
void
indent
( std::ostream& s,
int
ind = 0 ){
74
if
( ind>0 )
75
s <<
endl
;
76
if
( indentFlag ){
77
for
(
int
a=0; a<ind; a++ )
78
s <<
" "
;
79
}
80
}
81
public
:
82
Obj
(): refCount( 1 ) {}
83
virtual
~Obj
() {}
84
//! get ref count
85
int
GetRefCount
() {
return
refCount; }
86
//! reference
87
void
Ref
(){ refCount++; }
88
//! unreference
89
void
Unref
(){
90
refCount--;
91
if
( refCount==0 ){
92
delete
this
;
93
}
94
}
95
static
void
print_error
(
const
char
* c, std::ostream& s ){
96
if
( !errsInit ){
97
errs.open(
"errors.txt"
);
98
errsInit =
true
;
99
}
100
errs << c <<
std::endl
;
101
s << c;
102
exit( 1 );
103
}
104
static
void
print_warning
(
const
char
* c ){
105
if
( !errsInit ){
106
errs.open(
"errors.txt"
);
107
errsInit =
true
;
108
}
109
errs << c <<
std::endl
;
110
}
111
static
void
initialize
(){
112
errsInit =
false
;
113
}
114
};
115
116
#endif
Generated on Tue May 14 2013 15:43:30 for CVC3 by
1.8.3.1