00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035 #ifndef _cvc3__expr_h_
00036 #include "expr.h"
00037 #endif
00038
00039 #ifndef _cvc3__assumptions_h_
00040 #define _cvc3__assumptions_h_
00041
00042 namespace CVC3 {
00043
00044 class Assumptions {
00045 private:
00046 std::vector<Theorem> d_vector;
00047 static Assumptions s_empty;
00048
00049 private:
00050
00051
00052
00053
00054 const Theorem& findTheorem(const Expr& e) const;
00055
00056 static bool findExpr(const Assumptions& a, const Expr& e,
00057 std::vector<Theorem>& gamma);
00058 static bool findExprs(const Assumptions& a, const std::vector<Expr>& es,
00059 std::vector<Theorem>& gamma);
00060
00061 void add(const std::vector<Theorem>& thms);
00062
00063 public:
00064
00065 Assumptions() { }
00066
00067 Assumptions(const std::vector<Theorem>& v);
00068
00069 Assumptions(const Theorem& t) { d_vector.push_back(t); }
00070
00071 Assumptions(const Theorem& t1, const Theorem& t2);
00072
00073
00074 ~Assumptions() {}
00075
00076 Assumptions(const Assumptions &assump) : d_vector(assump.d_vector) {}
00077
00078 Assumptions &operator=(const Assumptions &assump)
00079 { d_vector = assump.d_vector; return *this; }
00080
00081 static const Assumptions& emptyAssump() { return s_empty; }
00082
00083 void add1(const Theorem& t) {
00084 DebugAssert(d_vector.empty(), "expected empty vector");
00085 d_vector.push_back(t);
00086 }
00087 void add(const Theorem& t);
00088 void add(const Assumptions& a) { add(a.d_vector); }
00089
00090 void clear() { d_vector.clear(); }
00091
00092 unsigned size() const { return d_vector.size(); }
00093 bool empty() const { return d_vector.empty(); }
00094
00095
00096 Theorem& getFirst() {
00097 DebugAssert(size() > 0, "Expected size > 0");
00098 return d_vector[0];
00099 }
00100
00101
00102 std::string toString() const;
00103 void print() const;
00104
00105
00106
00107
00108
00109 const Theorem& operator[](const Expr& e) const;
00110
00111
00112 const Theorem& find(const Expr& e) const;
00113
00114
00115
00116 class iterator : public std::iterator<std::input_iterator_tag,Theorem,ptrdiff_t> {
00117
00118 friend class Assumptions;
00119 private:
00120 std::vector<Theorem>::const_iterator d_it;
00121
00122 iterator(const std::vector<Theorem>::const_iterator& i): d_it(i) { }
00123 public:
00124
00125 iterator() { }
00126
00127 ~iterator() { }
00128
00129 bool operator==(const iterator& i) const { return (d_it == i.d_it); }
00130
00131 bool operator!=(const iterator& i) const { return (d_it != i.d_it); }
00132
00133 const Theorem& operator*() const { return *d_it; }
00134
00135 const Theorem* operator->() const { return &(operator*()); }
00136
00137 iterator& operator++() { ++d_it; return *this; }
00138
00139 class Proxy {
00140 const Theorem* d_t;
00141 public:
00142 Proxy(const Theorem& t) : d_t(&t) { }
00143 const Theorem& operator*() { return *d_t; }
00144 };
00145
00146 Proxy operator++(int) { return Proxy(*(d_it++)); }
00147 };
00148
00149 iterator begin() const { return iterator(d_vector.begin()); }
00150 iterator end() const { return iterator(d_vector.end()); }
00151
00152
00153
00154
00155
00156 friend Assumptions operator-(const Assumptions& a, const Expr& e);
00157
00158 friend Assumptions operator-(const Assumptions& a,
00159 const std::vector<Expr>& es);
00160
00161 friend std::ostream& operator<<(std::ostream& os,
00162 const Assumptions &assump);
00163
00164 friend bool operator==(const Assumptions& a1, const Assumptions& a2)
00165 { return a1.d_vector == a2.d_vector; }
00166 friend bool operator!=(const Assumptions& a1, const Assumptions& a2)
00167 { return a1.d_vector != a2.d_vector; }
00168
00169 };
00170
00171 }
00172
00173 #endif