expr_value.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_value.cpp
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Fri Feb  7 22:29:04 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
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 // Class ExprValue static members
00030 ////////////////////////////////////////////////////////////////////////
00031 
00032 std::hash<char*> ExprValue::s_charHash;
00033 std::hash<long int> ExprValue::s_intHash;
00034 
00035 ////////////////////////////////////////////////////////////////////////
00036 // Class ExprValue methods
00037 ////////////////////////////////////////////////////////////////////////
00038 
00039 
00040 // Destructor
00041 ExprValue::~ExprValue() {
00042   // Be careful deleting the attributes: first set them to NULL, then
00043   // delete, to avoid circular destructor calls
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   // Set all smart pointers to Null
00056   d_type = Type();
00057   d_simpCache=Theorem();
00058   //  d_simpFrom=Expr();
00059 }
00060 
00061 // Equality between any two ExprValue objects (including subclasses)
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   // Be careful deleting the attributes: first set them to NULL, then
00101   // delete, to avoid circular destructor calls
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 // Methods of subclasses of ExprValue
00301 ////////////////////////////////////////////////////////////////////////
00302 
00303 // Hash function for subclasses with kids.
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 } // end of namespace CVC3

Generated on Tue Jul 3 14:33:37 2007 for CVC3 by  doxygen 1.5.1