CVC3
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