00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #include "expr_value.h"
00022 #include "notifylist.h"
00023
00024 using namespace std;
00025
00026 namespace CVC3 {
00027
00028
00029
00030
00031
00032 std::hash<char*> ExprValue::s_charHash;
00033 std::hash<long int> ExprValue::s_intHash;
00034
00035
00036
00037
00038
00039
00040
00041 ExprValue::~ExprValue() {
00042
00043
00044 if (d_find) {
00045 CDO<Theorem>* find = d_find;
00046 d_find = NULL;
00047 delete find;
00048 free(find);
00049 }
00050 if(d_notifyList != NULL) {
00051 NotifyList* nl = d_notifyList;
00052 d_notifyList = NULL;
00053 delete nl;
00054 }
00055
00056 d_type = Type();
00057 d_simpCache=Theorem();
00058
00059 }
00060
00061
00062 bool ExprValue::operator==(const ExprValue& ev2) const {
00063 DebugAssert(getMMIndex() == EXPR_VALUE,
00064 "ExprValue::operator==() called from a subclass");
00065 if(getMMIndex() != ev2.getMMIndex())
00066 return false;
00067
00068 return (d_kind == ev2.d_kind);
00069 }
00070
00071
00072 ExprValue* ExprValue::copy(ExprManager* em, ExprIndex idx) const {
00073 DebugAssert(getMMIndex() == EXPR_VALUE,
00074 "ExprValue::copy() called from a subclass");
00075 return new(em->getMM(EXPR_VALUE)) ExprValue(em, d_kind, idx);
00076 }
00077
00078
00079 bool ExprNodeTmp::operator==(const ExprValue& ev2) const {
00080 return getMMIndex() == ev2.getMMIndex() &&
00081 d_kind == ev2.getKind() &&
00082 getKids() == ev2.getKids();
00083 }
00084
00085 ExprValue* ExprNodeTmp::copy(ExprManager* em, ExprIndex idx) const {
00086 if (d_em != em) {
00087 vector<Expr> children;
00088 vector<Expr>::const_iterator
00089 i = d_children.begin(), iend = d_children.end();
00090 for (; i != iend; ++i)
00091 children.push_back(rebuild(*i, em));
00092 return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, children, idx);
00093 }
00094 return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, d_children, idx);
00095 }
00096
00097
00098 ExprNode::~ExprNode()
00099 {
00100
00101
00102 if (d_sig) {
00103 CDO<Theorem>* sig = d_sig;
00104 d_sig = NULL;
00105 delete sig;
00106 free(sig);
00107 }
00108 if (d_rep) {
00109 CDO<Theorem>* rep = d_rep;
00110 d_rep = NULL;
00111 delete rep;
00112 free(rep);
00113 }
00114 }
00115
00116
00117 bool ExprNode::operator==(const ExprValue& ev2) const {
00118 if(getMMIndex() != ev2.getMMIndex())
00119 return false;
00120
00121 return (d_kind == ev2.getKind())
00122 && (getKids() == ev2.getKids());
00123 }
00124
00125 ExprValue* ExprNode::copy(ExprManager* em, ExprIndex idx) const {
00126 if (d_em != em) {
00127 vector<Expr> children;
00128 vector<Expr>::const_iterator
00129 i = d_children.begin(), iend = d_children.end();
00130 for (; i != iend; ++i)
00131 children.push_back(rebuild(*i, em));
00132 return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, children, idx);
00133 }
00134 return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, d_children, idx);
00135 }
00136
00137
00138 bool ExprString::operator==(const ExprValue& ev2) const {
00139 if(getMMIndex() != ev2.getMMIndex())
00140 return false;
00141
00142 return (getString() == ev2.getString());
00143 }
00144
00145 ExprValue* ExprString::copy(ExprManager* em, ExprIndex idx) const {
00146 return new(em->getMM(getMMIndex())) ExprString(em, d_str, idx);
00147 }
00148
00149
00150 bool ExprSkolem::operator==(const ExprValue& ev2) const {
00151 if(getMMIndex() != ev2.getMMIndex())
00152 return false;
00153
00154 return (getBoundIndex() == ev2.getBoundIndex()
00155 && getExistential() == ev2.getExistential());
00156 }
00157
00158 ExprValue* ExprSkolem::copy(ExprManager* em, ExprIndex idx) const {
00159 if (d_em != em) {
00160 return new(em->getMM(getMMIndex()))
00161 ExprSkolem(em, getBoundIndex(), rebuild(getExistential(), em), idx);
00162 }
00163 return new(em->getMM(getMMIndex()))
00164 ExprSkolem(em, getBoundIndex(), getExistential(), idx);
00165 }
00166
00167
00168 bool ExprRational::operator==(const ExprValue& ev2) const {
00169 if(getMMIndex() != ev2.getMMIndex())
00170 return false;
00171
00172 return (getRational() == ev2.getRational());
00173 }
00174
00175 ExprValue* ExprRational::copy(ExprManager* em, ExprIndex idx) const {
00176 return new(em->getMM(getMMIndex())) ExprRational(em, d_r, idx);
00177 }
00178
00179
00180 bool ExprVar::operator==(const ExprValue& ev2) const {
00181 if(getMMIndex() != ev2.getMMIndex())
00182 return false;
00183
00184 return (getKind() == ev2.getKind() && getName() == ev2.getName());
00185 }
00186
00187 ExprValue* ExprVar::copy(ExprManager* em, ExprIndex idx) const {
00188 return new(em->getMM(getMMIndex())) ExprVar(em, d_name, idx);
00189 }
00190
00191
00192 bool ExprSymbol::operator==(const ExprValue& ev2) const {
00193 if(getMMIndex() != ev2.getMMIndex())
00194 return false;
00195
00196 return (getKind() == ev2.getKind() && getName() == ev2.getName());
00197 }
00198
00199 ExprValue* ExprSymbol::copy(ExprManager* em, ExprIndex idx) const {
00200 return new(em->getMM(getMMIndex())) ExprSymbol(em, d_kind, d_name, idx);
00201 }
00202
00203
00204 bool ExprBoundVar::operator==(const ExprValue& ev2) const {
00205 if(getMMIndex() != ev2.getMMIndex())
00206 return false;
00207
00208 return (getKind() == ev2.getKind() && getName() == ev2.getName()
00209 && getUid() == ev2.getUid());
00210 }
00211
00212 ExprValue* ExprBoundVar::copy(ExprManager* em, ExprIndex idx) const {
00213 return new(em->getMM(getMMIndex())) ExprBoundVar(em, d_name, d_uid, idx);
00214 }
00215
00216
00217 bool ExprApply::operator==(const ExprValue& ev2) const {
00218 if(getMMIndex() != ev2.getMMIndex())
00219 return false;
00220
00221 return (getOp() == ev2.getOp())
00222 && (getKids() == ev2.getKids());
00223 }
00224
00225 ExprValue* ExprApply::copy(ExprManager* em, ExprIndex idx) const {
00226 if (d_em != em) {
00227 vector<Expr> children;
00228 vector<Expr>::const_iterator
00229 i = d_children.begin(), iend = d_children.end();
00230 for (; i != iend; ++i)
00231 children.push_back(rebuild(*i, em));
00232 return new(em->getMM(getMMIndex()))
00233 ExprApply(em, Op(rebuild(d_opExpr, em)), children, idx);
00234 }
00235 return new(em->getMM(getMMIndex()))
00236 ExprApply(em, Op(d_opExpr), d_children, idx);
00237 }
00238
00239
00240 bool ExprApplyTmp::operator==(const ExprValue& ev2) const {
00241 if(getMMIndex() != ev2.getMMIndex())
00242 return false;
00243
00244 return (getOp() == ev2.getOp())
00245 && (getKids() == ev2.getKids());
00246 }
00247
00248 ExprValue* ExprApplyTmp::copy(ExprManager* em, ExprIndex idx) const {
00249 if (d_em != em) {
00250 vector<Expr> children;
00251 vector<Expr>::const_iterator
00252 i = d_children.begin(), iend = d_children.end();
00253 for (; i != iend; ++i)
00254 children.push_back(rebuild(*i, em));
00255 return new(em->getMM(getMMIndex()))
00256 ExprApply(em, Op(rebuild(d_opExpr, em)), children, idx);
00257 }
00258 return new(em->getMM(getMMIndex()))
00259 ExprApply(em, Op(d_opExpr), d_children, idx);
00260 }
00261
00262
00263 bool ExprClosure::operator==(const ExprValue& ev2) const {
00264 if(getMMIndex() != ev2.getMMIndex())
00265 return false;
00266
00267 return (getKind() == ev2.getKind())
00268 && (getBody() == ev2.getBody())
00269 && (getVars() == ev2.getVars());
00270 }
00271
00272 ExprValue* ExprClosure::copy(ExprManager* em, ExprIndex idx) const {
00273 if (d_em != em) {
00274 vector<Expr> vars;
00275 vector<Expr>::const_iterator i = d_vars.begin(), iend = d_vars.end();
00276 for (; i != iend; ++i)
00277 vars.push_back(rebuild(*i, em));
00278 return new(em->getMM(getMMIndex()))
00279 ExprClosure(em, d_kind, vars, rebuild(d_body, em), idx);
00280 }
00281 return new(em->getMM(getMMIndex()))
00282 ExprClosure(em, d_kind, d_vars, d_body, idx);
00283 }
00284
00285
00286 bool ExprTheorem::operator==(const ExprValue& ev2) const
00287 {
00288 if(getMMIndex() != ev2.getMMIndex())
00289 return false;
00290 return (getTheorem() == ev2.getTheorem());
00291 }
00292
00293
00294 ExprValue* ExprTheorem::copy(ExprManager* em, ExprIndex idx) const {
00295 return new(em->getMM(getMMIndex())) ExprTheorem(em, d_thm, idx);
00296 }
00297
00298
00299
00300
00301
00302
00303
00304 size_t ExprValue::hash(const int kind, const std::vector<Expr>& kids) {
00305 size_t res(s_intHash((long int)kind));
00306 for(std::vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
00307 i!=iend; ++i) {
00308 void* ptr = i->d_expr;
00309 res = res*PRIME + pointerHash(ptr);
00310 }
00311 return res;
00312 }
00313
00314 size_t ExprClosure::computeHash() const {
00315 return d_body.hash()*PRIME + ExprValue::hash(d_kind, d_vars);
00316 }
00317
00318
00319 }