CVC3

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_eqNext) {
00051     CDO<Theorem>* eqNext = d_eqNext;
00052     d_eqNext = NULL;
00053     delete eqNext;
00054     free(eqNext);
00055   }
00056   if(d_notifyList != NULL) {
00057     NotifyList* nl = d_notifyList;
00058     d_notifyList = NULL;
00059     delete nl;
00060   }
00061   // Set all smart pointers to Null
00062   d_type = Type();
00063   d_simpCache=Theorem();
00064   //  d_simpFrom=Expr();
00065 }
00066 
00067 // Equality between any two ExprValue objects (including subclasses)
00068 bool ExprValue::operator==(const ExprValue& ev2) const {
00069   DebugAssert(getMMIndex() == EXPR_VALUE,
00070         "ExprValue::operator==() called from a subclass");
00071   if(getMMIndex() != ev2.getMMIndex())
00072     return false;
00073 
00074   return (d_kind == ev2.d_kind);
00075 }
00076 
00077 
00078 ExprValue* ExprValue::copy(ExprManager* em, ExprIndex idx) const {
00079   DebugAssert(getMMIndex() == EXPR_VALUE,
00080         "ExprValue::copy() called from a subclass");
00081   return new(em->getMM(EXPR_VALUE)) ExprValue(em, d_kind, idx);
00082 }
00083 
00084 
00085 bool ExprNodeTmp::operator==(const ExprValue& ev2) const {
00086   return getMMIndex() == ev2.getMMIndex() &&
00087     d_kind == ev2.getKind() &&
00088     getKids() == ev2.getKids();
00089 }
00090 
00091 ExprValue* ExprNodeTmp::copy(ExprManager* em, ExprIndex idx) const {
00092   if (d_em != em) {
00093     vector<Expr> children;
00094     vector<Expr>::const_iterator
00095       i = d_children.begin(), iend = d_children.end();
00096     for (; i != iend; ++i)
00097       children.push_back(rebuild(*i, em));
00098     return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, children, idx);
00099   }
00100   return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, d_children, idx);
00101 }
00102 
00103 
00104 ExprNode::~ExprNode()
00105 {
00106   // Be careful deleting the attributes: first set them to NULL, then
00107   // delete, to avoid circular destructor calls
00108   if (d_sig) {
00109     CDO<Theorem>* sig = d_sig;
00110     d_sig = NULL;
00111     delete sig;
00112     free(sig);
00113   }
00114   if (d_rep) {
00115     CDO<Theorem>* rep = d_rep;
00116     d_rep = NULL;
00117     delete rep;
00118     free(rep);
00119   }
00120 }
00121 
00122 
00123 bool ExprNode::operator==(const ExprValue& ev2) const {
00124   if(getMMIndex() != ev2.getMMIndex())
00125     return false;
00126 
00127   return (d_kind == ev2.getKind())
00128     && (getKids() == ev2.getKids());
00129 }
00130 
00131 ExprValue* ExprNode::copy(ExprManager* em, ExprIndex idx) const {
00132   if (d_em != em) {
00133     vector<Expr> children;
00134     vector<Expr>::const_iterator
00135       i = d_children.begin(), iend = d_children.end();
00136     for (; i != iend; ++i)
00137       children.push_back(rebuild(*i, em));
00138     return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, children, idx);
00139   }
00140   return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, d_children, idx);
00141 }
00142 
00143 
00144 bool ExprString::operator==(const ExprValue& ev2) const {
00145   if(getMMIndex() != ev2.getMMIndex())
00146     return false;
00147 
00148   return (getString() == ev2.getString());
00149 }
00150 
00151 ExprValue* ExprString::copy(ExprManager* em, ExprIndex idx) const {
00152   return new(em->getMM(getMMIndex())) ExprString(em, d_str, idx);
00153 }
00154 
00155 
00156 bool ExprSkolem::operator==(const ExprValue& ev2) const {
00157   if(getMMIndex() != ev2.getMMIndex())
00158     return false;
00159 
00160   return (getBoundIndex() == ev2.getBoundIndex()
00161     && getExistential() == ev2.getExistential());
00162 }
00163 
00164 ExprValue* ExprSkolem::copy(ExprManager* em, ExprIndex idx) const {
00165   if (d_em != em) {
00166     return new(em->getMM(getMMIndex()))
00167       ExprSkolem(em, getBoundIndex(), rebuild(getExistential(), em), idx);
00168   }
00169   return new(em->getMM(getMMIndex()))
00170     ExprSkolem(em, getBoundIndex(), getExistential(), idx);
00171 }
00172 
00173 
00174 bool ExprRational::operator==(const ExprValue& ev2) const {
00175   if(getMMIndex() != ev2.getMMIndex())
00176     return false;
00177 
00178   return (getRational() == ev2.getRational());
00179 }
00180 
00181 ExprValue* ExprRational::copy(ExprManager* em, ExprIndex idx) const {
00182   return new(em->getMM(getMMIndex())) ExprRational(em, d_r, idx);
00183 }
00184 
00185 
00186 bool ExprVar::operator==(const ExprValue& ev2) const {
00187   if(getMMIndex() != ev2.getMMIndex())
00188     return false;
00189 
00190   return (getKind() == ev2.getKind() && getName() == ev2.getName());
00191 }
00192 
00193 ExprValue* ExprVar::copy(ExprManager* em, ExprIndex idx) const {
00194   return new(em->getMM(getMMIndex())) ExprVar(em, d_name, idx);
00195 }
00196 
00197 
00198 bool ExprSymbol::operator==(const ExprValue& ev2) const {
00199   if(getMMIndex() != ev2.getMMIndex())
00200     return false;
00201 
00202   return (getKind() == ev2.getKind() && getName() == ev2.getName());
00203 }
00204 
00205 ExprValue* ExprSymbol::copy(ExprManager* em, ExprIndex idx) const {
00206   return new(em->getMM(getMMIndex())) ExprSymbol(em, d_kind, d_name, idx);
00207 }
00208 
00209 
00210 bool ExprBoundVar::operator==(const ExprValue& ev2) const {
00211   if(getMMIndex() != ev2.getMMIndex())
00212     return false;
00213 
00214   return (getKind() == ev2.getKind() && getName() == ev2.getName()
00215     && getUid() == ev2.getUid());
00216 }
00217 
00218 ExprValue* ExprBoundVar::copy(ExprManager* em, ExprIndex idx) const {
00219   return new(em->getMM(getMMIndex())) ExprBoundVar(em, d_name, d_uid, idx);
00220 }
00221 
00222 
00223 bool ExprApply::operator==(const ExprValue& ev2) const {
00224   if(getMMIndex() != ev2.getMMIndex())
00225     return false;
00226 
00227   return (getOp() == ev2.getOp())
00228       && (getKids() == ev2.getKids());
00229 }
00230 
00231 ExprValue* ExprApply::copy(ExprManager* em, ExprIndex idx) const {
00232   if (d_em != em) {
00233     vector<Expr> children;
00234     vector<Expr>::const_iterator
00235       i = d_children.begin(), iend = d_children.end();
00236     for (; i != iend; ++i)
00237       children.push_back(rebuild(*i, em));
00238     return new(em->getMM(getMMIndex()))
00239       ExprApply(em, Op(rebuild(d_opExpr, em)), children, idx);
00240   }
00241   return new(em->getMM(getMMIndex()))
00242     ExprApply(em, Op(d_opExpr), d_children, idx);
00243 }
00244 
00245 
00246 bool ExprApplyTmp::operator==(const ExprValue& ev2) const {
00247   if(getMMIndex() != ev2.getMMIndex())
00248     return false;
00249 
00250   return (getOp() == ev2.getOp())
00251       && (getKids() == ev2.getKids());
00252 }
00253 
00254 ExprValue* ExprApplyTmp::copy(ExprManager* em, ExprIndex idx) const {
00255   if (d_em != em) {
00256     vector<Expr> children;
00257     vector<Expr>::const_iterator
00258       i = d_children.begin(), iend = d_children.end();
00259     for (; i != iend; ++i)
00260       children.push_back(rebuild(*i, em));
00261     return new(em->getMM(getMMIndex()))
00262       ExprApply(em, Op(rebuild(d_opExpr, em)), children, idx);
00263   }
00264   return new(em->getMM(getMMIndex()))
00265     ExprApply(em, Op(d_opExpr), d_children, idx);
00266 }
00267 
00268 
00269 bool ExprClosure::operator==(const ExprValue& ev2) const {
00270   if(getMMIndex() != ev2.getMMIndex())
00271     return false;
00272 
00273   return (getKind() == ev2.getKind())
00274       && (getBody() == ev2.getBody())
00275       && (getVars() == ev2.getVars());
00276 }
00277 
00278 ExprValue* ExprClosure::copy(ExprManager* em, ExprIndex idx) const {
00279   if (d_em != em) {
00280     vector<Expr> vars;
00281     vector<Expr>::const_iterator i = d_vars.begin(), iend = d_vars.end();
00282     for (; i != iend; ++i)
00283       vars.push_back(rebuild(*i, em));
00284 
00285     vector<vector<Expr> > manual_trigs;
00286     vector<vector<Expr> >::const_iterator j = d_manual_triggers.begin(), jend = d_manual_triggers.end();
00287     for (; j != jend; ++j) {
00288       vector<Expr >::const_iterator k = j->begin(), kend = j->end();
00289       vector<Expr> cur_trig;
00290       for (; k != kend; ++k){
00291   cur_trig.push_back(rebuild(*k,em));
00292       }
00293       //      manual_trigs.push_back(rebuild(*j, em));
00294       manual_trigs.push_back(cur_trig);
00295     }
00296 
00297     return new(em->getMM(getMMIndex()))
00298       ExprClosure(em, d_kind, vars, rebuild(d_body, em), manual_trigs, idx);
00299   }
00300   return new(em->getMM(getMMIndex()))
00301     ExprClosure(em, d_kind, d_vars, d_body, d_manual_triggers, idx);
00302 }
00303 
00304 
00305 ////////////////////////////////////////////////////////////////////////
00306 // Methods of subclasses of ExprValue
00307 ////////////////////////////////////////////////////////////////////////
00308 
00309 // Hash function for subclasses with kids.
00310 size_t ExprValue::hash(const int kind, const std::vector<Expr>& kids) {
00311   size_t res(s_intHash((long int)kind));
00312   for(std::vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
00313       i!=iend; ++i) {
00314     void* ptr = i->d_expr;
00315     res = res*PRIME + pointerHash(ptr);
00316   }
00317   return res;
00318 }
00319 
00320 
00321 // Size function for subclasses with kids.
00322 Unsigned ExprValue::sizeWithChildren(const std::vector<Expr>& kids)
00323 {
00324   Unsigned res = 1;
00325   for(vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
00326       i!=iend; ++i) {
00327     res += (*i).d_expr->getSize();
00328   }
00329   return res;
00330 }
00331 
00332 
00333 size_t ExprClosure::computeHash() const {
00334   return d_body.hash()*PRIME + ExprValue::hash(d_kind, d_vars);
00335 }
00336 
00337 
00338 } // end of namespace CVC3