CVC3  2.4.1
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
RefPtr()
Definition: Object.h:32
static ofstream errs
Definition: Object.h:70
Obj()
Definition: Object.h:82
RefPtr(const RefPtr &rp)
Definition: Object.h:34
static void initialize()
Definition: Object.h:111
STL namespace.
void Unref()
unreference
Definition: Object.h:89
Definition: Object.h:63
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void indent(std::ostream &s, int ind=0)
Definition: Object.h:73
void Ref()
reference
Definition: Object.h:87
T element_type
Definition: Object.h:31
static void print_error(const char *c, std::ostream &s)
Definition: Object.h:95
ostringstream oignore
Definition: Object.h:66
static bool errsInit
Definition: Object.h:69
T * operator->()
Definition: Object.h:54
const T & operator*() const
Definition: Object.h:53
T & operator*()
Definition: Object.h:52
virtual ~Obj()
Definition: Object.h:83
int GetRefCount()
get ref count
Definition: Object.h:85
RefPtr(T *t)
Definition: Object.h:33
T * _ptr
Definition: Object.h:59
const T * operator->() const
Definition: Object.h:55
~RefPtr()
Definition: Object.h:35
int refCount
Definition: Object.h:67
Definition: expr.cpp:35
static bool indentFlag
Definition: Object.h:71
static void print_warning(const char *c)
Definition: Object.h:104
Definition: Object.h:28