1 /*****************************************************************************/ 2 /*! 3 * \file expr_value.h 4 * 5 * Author: Sergey Berezin 6 * 7 * Created: Fri Feb 7 15:07:18 2003 8 * 9 * <hr> 10 * 11 * License to use, copy, modify, sell and/or distribute this software 12 * and its documentation for any purpose is hereby granted without 13 * royalty, subject to the terms and conditions defined in the \ref 14 * LICENSE file provided with this distribution. 15 * 16 * <hr> 17 * 18 * Class ExprValue: the value holding class of Expr. No one should 19 * use it directly; use Expr API instead. To enforce that, the 20 * constructors are made protected, and only Expr, ExprManager, and 21 * subclasses can use them. 22 */ 23 /*****************************************************************************/ 24 25 // *** HACK ATTACK *** (trick from Aaron Stump's code) 26 27 // In order to inline the Expr constructors (for efficiency), this 28 // file (expr_value.h) must be included in expr.h. However, we also 29 // need to include expr.h here, hence, circular dependency. A way to 30 // break it is to include expr_value.h in the middle of expr.h after 31 // the definition of class Expr, but before the definition of its 32 // inlined methods. So, expr.h included below will also suck in 33 // expr_value.h recursively, meaning that we then should skip the rest 34 // of the file (since it's already been included). 35 36 // That's why expr.h is outside of #ifndef. The same is true for 37 // type.h and theorem.h. 38 39 #ifndef _cvc3__expr_h_ 40 #include "expr.h" 41 #endif 42 43 #ifndef _cvc3__expr_value_h_ 44 #define _cvc3__expr_value_h_ 45 46 #include "theorem.h" 47 #include "type.h" 48 49 // The prime number used in the hash function for a vector of elements 50 #define PRIME 131 51 52 namespace CVC3 { 53 54 /*****************************************************************************/ 55 /*! 56 *\class ExprValue 57 *\brief The base class for holding the actual data in expressions 58 * 59 * 60 * Author: Sergey Berezin 61 * 62 * Created: long time ago 63 * 64 * \anchor ExprValue The base class just holds the operator. 65 * All the additional data resides in subclasses. 66 * 67 */ 68 /*****************************************************************************/ 69 class CVC_DLL ExprValue { 70 friend class Expr; 71 friend class Expr::iterator; 72 friend class ExprManager; 73 friend class ::CInterface; 74 friend class ExprApply; 75 friend class Theorem; 76 friend class ExprClosure; 77 78 //! Unique expression id 79 ExprIndex d_index; 80 81 //! Reference counter for garbage collection 82 unsigned d_refcount; 83 84 //! Cached hash value (initially 0) 85 size_t d_hash; 86 87 //! The find attribute (may be NULL) 88 CDO<Theorem>* d_find; 89 90 //! Equality between this term and next term in ring of all terms in the equivalence class 91 CDO<Theorem>* d_eqNext; 92 93 //! The cached type of the expression (may be Null) 94 Type d_type; 95 96 //! The cached TCC of the expression (may be Null) 97 // Expr d_tcc; 98 99 //! Subtyping predicate for the expression and all subexpressions 100 // Theorem d_subtypePred; 101 102 //! Notify list may be NULL (== no such attribute) 103 NotifyList* d_notifyList; 104 105 //! For caching calls to Simplify 106 Theorem d_simpCache; 107 108 //! For checking whether simplify cache is valid 109 unsigned d_simpCacheTag; 110 111 //! context-dependent bit-vector for flags that are context-dependent 112 CDFlags d_dynamicFlags; 113 114 //! Size of dag rooted at this expression 115 Unsigned d_size; 116 117 //! Which child has the largest height 118 // int d_highestKid; 119 120 //! Most distant expression we were simplified *from* 121 // Expr d_simpFrom; 122 123 //! Generic flag for marking expressions (e.g. in DAG traversal) 124 unsigned d_flag; 125 126 protected: 127 /*! @brief The kind of the expression. In particular, it determines which 128 * subclass of ExprValue is used to store the expression. */ 129 int d_kind; 130 131 //! Our expr. manager 132 ExprManager* d_em; 133 134 // End of data members 135 136 private: 137 138 //! Set the ExprIndex setIndex(ExprIndex idx)139 void setIndex(ExprIndex idx) { d_index = idx; } 140 141 //! Increment reference counter incRefcount()142 void incRefcount() { ++d_refcount; } 143 144 //! Decrement reference counter decRefcount()145 void decRefcount() { 146 // Cannot be DebugAssert, since we are called in a destructor 147 // and should not throw an exception 148 IF_DEBUG(FatalAssert(d_refcount > 0, "Mis-handled the ref. counting");) 149 if((--d_refcount) == 0) d_em->gc(this); 150 } 151 152 //! Caching hash function 153 /*! Do NOT implement it in subclasses! Implement computeHash() instead. 154 */ hash()155 size_t hash() const { 156 if (d_hash == 0) 157 const_cast<ExprValue*>(this)->d_hash = computeHash(); 158 return d_hash; 159 } 160 161 //! Return DAG-size of Expr getSize()162 Unsigned getSize() const { 163 if (d_flag == d_em->getFlag()) return 0; 164 const_cast<ExprValue*>(this)->d_flag = d_em->getFlag(); 165 return computeSize(); 166 } 167 168 //! Return child with greatest height 169 // int getHighestKid() const { return d_highestKid; } 170 171 //! Get Expr simplified to obtain this expr 172 // const Expr& getSimpFrom() const { return d_simpFrom; } 173 174 //! Set Expr simplified to obtain this expr 175 // void setSimpFrom(const Expr& simpFrom) { d_simpFrom = simpFrom; } 176 177 protected: 178 179 // Static hash functions. They don't depend on the context 180 // (ExprManager and such), so it is still thread-safe to have them 181 // static. 182 static std::hash<char*> s_charHash; 183 static std::hash<long int> s_intHash; 184 pointerHash(void * p)185 static size_t pointerHash(void* p) { return s_intHash((long int)p); } 186 // Hash function for subclasses with children 187 static size_t hash(const int kind, const std::vector<Expr>& kids); 188 // Hash function for kinds hash(const int n)189 static size_t hash(const int n) { return s_intHash((long int)n); } 190 191 // Size function for subclasses with children 192 static Unsigned sizeWithChildren(const std::vector<Expr>& kids); 193 194 //! Return the memory manager (for the benefit of subclasses) getMM(size_t MMIndex)195 MemoryManager* getMM(size_t MMIndex) { 196 DebugAssert(d_em!=NULL, "ExprValue::getMM()"); 197 return d_em->getMM(MMIndex); 198 } 199 200 //! Make a clean copy of itself using the given ExprManager rebuild(ExprManager * em)201 ExprValue* rebuild(ExprManager* em) const 202 { return copy(em, 0); } 203 204 //! Make a clean copy of the expr using the given ExprManager rebuild(Expr e,ExprManager * em)205 Expr rebuild(Expr e, ExprManager* em) const 206 { return em->rebuildRec(e); } 207 208 // Protected API 209 210 //! Non-caching hash function which actually computes the hash. 211 /*! This is the method that all subclasses should implement */ computeHash()212 virtual size_t computeHash() const { return hash(d_kind); } 213 214 //! Non-caching size function which actually computes the size. 215 /*! This is the method that all subclasses should implement */ computeSize()216 virtual Unsigned computeSize() const { return 1; } 217 218 //! Make a clean copy of itself using the given ExprManager 219 virtual ExprValue* copy(ExprManager* em, ExprIndex idx) const; 220 221 public: 222 //! Constructor 223 ExprValue(ExprManager* em, int kind, ExprIndex idx = 0) d_index(idx)224 : d_index(idx), d_refcount(0), 225 d_hash(0), d_find(NULL), d_eqNext(NULL), d_notifyList(NULL), 226 d_simpCacheTag(0), 227 d_dynamicFlags(em->getCurrentContext()), 228 d_size(0), 229 // d_height(0), d_highestKid(-1), 230 d_flag(0), d_kind(kind), d_em(em) 231 { 232 DebugAssert(em != NULL, "NULL ExprManager is given to ExprValue()"); 233 DebugAssert(em->isKindRegistered(kind), 234 ("ExprValue(kind = " + int2string(kind) 235 + ")): kind is not registered").c_str()); 236 DebugAssert(kind != APPLY, "Only ExprApply should have APPLY kind"); 237 // #ifdef _CVC3_DEBUG_MODE //added by yeting, just hold a place to put my breakpoints in gdb 238 // if(idx != 0){ 239 // TRACE("expr", "expr created ", idx, "");//the line added by yeting 240 // // char * a; 241 // // a="a"; 242 // // a[999999]=255; 243 // } 244 // #endif 245 } 246 //! Destructor 247 virtual ~ExprValue(); 248 249 //! Get the kind of the expression getKind()250 int getKind() const { return d_kind; } 251 252 //! Overload operator new new(size_t size,MemoryManager * mm)253 void* operator new(size_t size, MemoryManager* mm) 254 { return mm->newData(size); } delete(void * pMem,MemoryManager * mm)255 void operator delete(void* pMem, MemoryManager* mm) { 256 mm->deleteData(pMem); 257 } 258 259 //! Overload operator delete delete(void *)260 void operator delete(void*) { } 261 262 //! Get unique memory manager ID getMMIndex()263 virtual size_t getMMIndex() const { return EXPR_VALUE; } 264 265 //! Equality between any two ExprValue objects (including subclasses) 266 virtual bool operator==(const ExprValue& ev2) const; 267 268 // Testers 269 270 //! Test whether the expression is a generic subclass 271 /*! 272 * \return 0 for the core classes, and getMMIndex() value for 273 * generic subclasses (those defined in DPs) 274 */ getExprValue()275 virtual const ExprValue* getExprValue() const 276 { throw Exception("Illegal call to getExprValue()"); } 277 //! String expression tester isString()278 virtual bool isString() const { return false; } 279 //! Rational number expression tester isRational()280 virtual bool isRational() const { return false; } 281 //! Uninterpreted constants isVar()282 virtual bool isVar() const { return false; } 283 //! Application of another expression isApply()284 virtual bool isApply() const { return false; } 285 //! Special named symbol isSymbol()286 virtual bool isSymbol() const { return false; } 287 //! A LAMBDA-expression or a quantifier isClosure()288 virtual bool isClosure() const { return false; } 289 //! Special Expr holding a theorem isTheorem()290 virtual bool isTheorem() const { return false; } 291 292 //! Get kids: by default, returns a ref to an empty vector getKids()293 virtual const std::vector<Expr>& getKids() const 294 { return d_em->getEmptyVector(); } 295 296 // Methods to access leaf data in subclasses 297 298 //! Default arity = 0 arity()299 virtual unsigned arity() const { return 0; } 300 301 //! Special attributes for uninterpreted functions getSig()302 virtual CDO<Theorem>* getSig() const { 303 DebugAssert(false, "getSig() is called on ExprValue"); 304 return NULL; 305 } 306 getRep()307 virtual CDO<Theorem>* getRep() const { 308 DebugAssert(false, "getRep() is called on ExprValue"); 309 return NULL; 310 } 311 setSig(CDO<Theorem> * sig)312 virtual void setSig(CDO<Theorem>* sig) { 313 DebugAssert(false, "setSig() is called on ExprValue"); 314 } 315 setRep(CDO<Theorem> * rep)316 virtual void setRep(CDO<Theorem>* rep) { 317 DebugAssert(false, "setRep() is called on ExprValue"); 318 } 319 getUid()320 virtual const std::string& getUid() const { 321 static std::string null; 322 DebugAssert(false, "ExprValue::getUid() called in base class"); 323 return null; 324 } 325 getString()326 virtual const std::string& getString() const { 327 DebugAssert(false, "getString() is called on ExprValue"); 328 static std::string s(""); 329 return s; 330 } 331 getRational()332 virtual const Rational& getRational() const { 333 DebugAssert(false, "getRational() is called on ExprValue"); 334 static Rational r(0); 335 return r; 336 } 337 338 //! Returns the string name of UCONST and BOUND_VAR expr's. getName()339 virtual const std::string& getName() const { 340 static std::string ret = ""; 341 DebugAssert(false, "getName() is called on ExprValue"); 342 return ret; 343 } 344 345 //! Returns the original Boolean variable (for BoolVarExprValue) getVar()346 virtual const Expr& getVar() const { 347 DebugAssert(false, "getVar() is called on ExprValue"); 348 static Expr null; 349 return null; 350 } 351 352 //! Get the Op from an Apply Expr getOp()353 virtual Op getOp() const { 354 DebugAssert(false, "getOp() is called on ExprValue"); 355 return Op(NULL_KIND); 356 } 357 getVars()358 virtual const std::vector<Expr>& getVars() const { 359 DebugAssert(false, "getVars() is called on ExprValue"); 360 static std::vector<Expr> null; 361 return null; 362 } 363 getBody()364 virtual const Expr& getBody() const { 365 DebugAssert(false, "getBody() is called on ExprValue"); 366 static Expr null; 367 return null; 368 } 369 setTriggers(const std::vector<std::vector<Expr>> & triggers)370 virtual void setTriggers(const std::vector<std::vector<Expr> >& triggers) { 371 DebugAssert(false, "setTriggers() is called on ExprValue"); 372 } 373 getTriggers()374 virtual const std::vector<std::vector<Expr> >& getTriggers() const { //by yeting 375 DebugAssert(false, "getTrigs() is called on ExprValue"); 376 static std::vector<std::vector<Expr> > null; 377 return null; 378 } 379 380 getExistential()381 virtual const Expr& getExistential() const { 382 DebugAssert(false, "getExistential() is called on ExprValue"); 383 static Expr null; 384 return null; 385 } getBoundIndex()386 virtual int getBoundIndex() const { 387 DebugAssert(false, "getIndex() is called on ExprValue"); 388 return 0; 389 } 390 getFields()391 virtual const std::vector<std::string>& getFields() const { 392 DebugAssert(false, "getFields() is called on ExprValue"); 393 static std::vector<std::string> null; 394 return null; 395 } getField()396 virtual const std::string& getField() const { 397 DebugAssert(false, "getField() is called on ExprValue"); 398 static std::string null; 399 return null; 400 } getTupleIndex()401 virtual int getTupleIndex() const { 402 DebugAssert(false, "getTupleIndex() is called on ExprValue"); 403 return 0; 404 } getTheorem()405 virtual const Theorem& getTheorem() const { 406 static Theorem null; 407 DebugAssert(false, "getTheorem() is called on ExprValue"); 408 return null; 409 } 410 411 }; // end of class ExprValue 412 413 // Class ExprNode; it's an expression with children 414 class CVC_DLL ExprNode: public ExprValue { 415 friend class Expr; 416 friend class ExprManager; 417 418 protected: 419 //! Vector of children 420 std::vector<Expr> d_children; 421 422 // Special attributes for helping with congruence closure 423 CDO<Theorem>* d_sig; 424 CDO<Theorem>* d_rep; 425 426 private: 427 428 //! Tell ExprManager who we are getMMIndex()429 size_t getMMIndex() const { return EXPR_NODE; } 430 431 protected: 432 //! Return number of children arity()433 unsigned arity() const { return d_children.size(); } 434 435 //! Return reference to children getKids1()436 std::vector<Expr>& getKids1() { return d_children; } 437 438 //! Return reference to children getKids()439 const std::vector<Expr>& getKids() const { return d_children; } 440 441 //! Use our static hash() for the member method computeHash()442 size_t computeHash() const { 443 return ExprValue::hash(d_kind, d_children); 444 } 445 446 //! Use our static sizeWithChildren() for the member method computeSize()447 Unsigned computeSize() const { 448 return ExprValue::sizeWithChildren(d_children); 449 } 450 451 //! Make a clean copy of itself using the given memory manager 452 virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 453 454 public: 455 //! Constructor 456 ExprNode(ExprManager* em, int kind, ExprIndex idx = 0) ExprValue(em,kind,idx)457 : ExprValue(em, kind, idx), d_sig(NULL), d_rep(NULL) { } 458 //! Constructor 459 ExprNode(ExprManager* em, int kind, const std::vector<Expr>& kids, 460 ExprIndex idx = 0) ExprValue(em,kind,idx)461 : ExprValue(em, kind, idx), d_children(kids), d_sig(NULL), d_rep(NULL) { } 462 //! Destructor 463 virtual ~ExprNode(); 464 465 //! Overload operator new new(size_t size,MemoryManager * mm)466 void* operator new(size_t size, MemoryManager* mm) 467 { return mm->newData(size); } delete(void * pMem,MemoryManager * mm)468 void operator delete(void* pMem, MemoryManager* mm) { 469 mm->deleteData(pMem); 470 } 471 472 //! Overload operator delete delete(void *)473 void operator delete(void*) { } 474 475 //! Compare with another ExprValue 476 virtual bool operator==(const ExprValue& ev2) const; 477 getSig()478 virtual CDO<Theorem>* getSig() const { return d_sig; } getRep()479 virtual CDO<Theorem>* getRep() const { return d_rep; } 480 setRep(CDO<Theorem> * rep)481 virtual void setRep(CDO<Theorem>* rep) { d_rep = rep; } setSig(CDO<Theorem> * sig)482 virtual void setSig(CDO<Theorem>* sig) { d_sig = sig; } 483 484 }; // end of class ExprNode 485 486 // Class ExprNodeTmp; special version of ExprNode for Expr constructor 487 class ExprNodeTmp: public ExprValue { 488 friend class Expr; 489 friend class ExprManager; 490 491 protected: 492 //! Vector of children 493 const std::vector<Expr>& d_children; 494 495 private: 496 497 //! Tell ExprManager who we are getMMIndex()498 size_t getMMIndex() const { return EXPR_NODE; } 499 500 protected: 501 //! Return number of children arity()502 unsigned arity() const { return d_children.size(); } 503 504 //! Return reference to children getKids()505 const std::vector<Expr>& getKids() const { return d_children; } 506 507 //! Use our static hash() for the member method computeHash()508 size_t computeHash() const { 509 return ExprValue::hash(d_kind, d_children); 510 } 511 512 //! Use our static sizeWithChildren() for the member method computeSize()513 Unsigned computeSize() const { 514 return ExprValue::sizeWithChildren(d_children); 515 } 516 517 //! Make a clean copy of itself using the given memory manager 518 virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 519 520 public: 521 //! Constructor ExprNodeTmp(ExprManager * em,int kind,const std::vector<Expr> & kids)522 ExprNodeTmp(ExprManager* em, int kind, const std::vector<Expr>& kids) 523 : ExprValue(em, kind, 0), d_children(kids) { } 524 525 //! Destructor ~ExprNodeTmp()526 virtual ~ExprNodeTmp() {} 527 528 //! Compare with another ExprValue 529 virtual bool operator==(const ExprValue& ev2) const; 530 531 }; // end of class ExprNodeTmp 532 533 // Special version for Expr Constructor 534 class ExprApplyTmp: public ExprNodeTmp { 535 friend class Expr; 536 friend class ExprManager; 537 private: 538 Expr d_opExpr; 539 protected: getMMIndex()540 size_t getMMIndex() const { return EXPR_APPLY; } computeHash()541 size_t computeHash() const { 542 return PRIME*ExprNodeTmp::computeHash() + d_opExpr.hash(); 543 } getOp()544 Op getOp() const { return Op(d_opExpr); } isApply()545 bool isApply() const { return true; } 546 // Make a clean copy of itself using the given memory manager 547 ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 548 public: 549 // Constructor ExprApplyTmp(ExprManager * em,const Op & op,const std::vector<Expr> & kids)550 ExprApplyTmp(ExprManager* em, const Op& op, 551 const std::vector<Expr>& kids) 552 : ExprNodeTmp(em, NULL_KIND, kids), d_opExpr(op.getExpr()) 553 { DebugAssert(!op.getExpr().isNull(), "Expected non-null Op"); 554 d_kind = APPLY; } ~ExprApplyTmp()555 virtual ~ExprApplyTmp() { } 556 557 bool operator==(const ExprValue& ev2) const; 558 }; // end of class ExprApply 559 560 class CVC_DLL ExprApply: public ExprNode { 561 friend class Expr; 562 friend class ExprManager; 563 private: 564 Expr d_opExpr; 565 protected: getMMIndex()566 size_t getMMIndex() const { return EXPR_APPLY; } computeHash()567 size_t computeHash() const { 568 return PRIME*ExprNode::computeHash() + d_opExpr.hash(); 569 } getOp()570 Op getOp() const { return Op(d_opExpr); } isApply()571 bool isApply() const { return true; } 572 // Make a clean copy of itself using the given memory manager 573 ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 574 public: 575 // Constructor 576 ExprApply(ExprManager* em, const Op& op, ExprIndex idx = 0) ExprNode(em,NULL_KIND,idx)577 : ExprNode(em, NULL_KIND, idx), d_opExpr(op.getExpr()) 578 { DebugAssert(!op.getExpr().isNull(), "Expected non-null Op"); 579 d_kind = APPLY; } 580 ExprApply(ExprManager* em, const Op& op, 581 const std::vector<Expr>& kids, ExprIndex idx = 0) ExprNode(em,NULL_KIND,kids,idx)582 : ExprNode(em, NULL_KIND, kids, idx), d_opExpr(op.getExpr()) 583 { DebugAssert(!op.getExpr().isNull(), "Expected non-null Op"); 584 d_kind = APPLY; } ~ExprApply()585 virtual ~ExprApply() { } 586 587 bool operator==(const ExprValue& ev2) const; 588 // Memory management new(size_t size,MemoryManager * mm)589 void* operator new(size_t size, MemoryManager* mm) { 590 return mm->newData(size); 591 } delete(void * pMem,MemoryManager * mm)592 void operator delete(void* pMem, MemoryManager* mm) { 593 mm->deleteData(pMem); 594 } delete(void *)595 void operator delete(void*) { } 596 }; // end of class ExprApply 597 598 /*****************************************************************************/ 599 /*! 600 *\class NamedExprValue 601 *\brief NamedExprValue 602 * 603 * Author: Clark Barrett 604 * 605 * Created: Thu Dec 2 23:18:17 2004 606 * 607 * Subclass of ExprValue for kinds that have a name associated with them. 608 */ 609 /*****************************************************************************/ 610 611 // class NamedExprValue : public ExprNode { 612 // friend class Expr; 613 // friend class ExprManager; 614 615 // private: 616 // std::string d_name; 617 618 // protected: 619 620 // ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const { 621 // return new(em->getMM(getMMIndex())) 622 // NamedExprValue(d_em, d_kind, d_name, d_children, idx); 623 // } 624 625 // ExprValue* copy(ExprManager* em, const std::vector<Expr>& kids, 626 // ExprIndex idx = 0) const { 627 // return new(em->getMM(getMMIndex())) 628 // NamedExprValue(d_em, d_kind, d_name, kids, idx); 629 // } 630 631 // size_t computeHash() const { 632 // return s_charHash(d_name.c_str())*PRIME + ExprNode::computeHash(); 633 // } 634 635 // size_t getMMIndex() const { return EXPR_NAMED; } 636 637 // public: 638 // // Constructor 639 // NamedExprValue(ExprManager *em, int kind, const std::string& name, 640 // const std::vector<Expr>& kids, ExprIndex idx = 0) 641 // : ExprNode(em, kind, kids, idx), d_name(name) { } 642 // // virtual ~NamedExprValue(); 643 // bool operator==(const ExprValue& ev2) const { 644 // if(getMMIndex() != ev2.getMMIndex()) return false; 645 // return (getName() == ev2.getName()) 646 // && ExprNode::operator==(ev2); 647 // } 648 649 // const std::string& getName() const { return d_name; } 650 651 // // Memory management 652 // void* operator new(size_t size, MemoryManager* mm) { 653 // return mm->newData(size); 654 // } 655 // void operator delete(void*) { } 656 // }; // end of class NamedExprValue 657 658 // Leaf expressions 659 class ExprString: public ExprValue { 660 friend class Expr; 661 friend class ExprManager; 662 private: 663 std::string d_str; 664 665 // Hash function for this subclass hash(const std::string & str)666 static size_t hash(const std::string& str) { 667 return s_charHash(str.c_str()); 668 } 669 670 // Tell ExprManager who we are getMMIndex()671 virtual size_t getMMIndex() const { return EXPR_STRING; } 672 673 protected: 674 // Use our static hash() for the member method computeHash()675 virtual size_t computeHash() const { return hash(d_str); } 676 isString()677 virtual bool isString() const { return true; } getString()678 virtual const std::string& getString() const { return d_str; } 679 680 //! Make a clean copy of itself using the given memory manager 681 virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 682 public: 683 // Constructor 684 ExprString(ExprManager* em, const std::string& s, ExprIndex idx = 0) ExprValue(em,STRING_EXPR,idx)685 : ExprValue(em, STRING_EXPR, idx), d_str(s) { } 686 // Destructor ~ExprString()687 virtual ~ExprString() { } 688 689 virtual bool operator==(const ExprValue& ev2) const; 690 // Memory management new(size_t size,MemoryManager * mm)691 void* operator new(size_t size, MemoryManager* mm) { 692 return mm->newData(size); 693 } delete(void * pMem,MemoryManager * mm)694 void operator delete(void* pMem, MemoryManager* mm) { 695 mm->deleteData(pMem); 696 } delete(void *)697 void operator delete(void*) { } 698 }; // end of class ExprString 699 700 class ExprSkolem: public ExprValue { 701 friend class Expr; 702 friend class ExprManager; 703 private: 704 Expr d_quant; //!< The quantified expression to skolemize 705 int d_idx; //!< Variable index in the quantified expression getExistential()706 const Expr& getExistential() const {return d_quant;} getBoundIndex()707 int getBoundIndex() const {return d_idx;} 708 709 // Tell ExprManager who we are getMMIndex()710 size_t getMMIndex() const { return EXPR_SKOLEM;} 711 712 protected: computeHash()713 size_t computeHash() const { 714 size_t res = getExistential().getBody().hash(); 715 res = PRIME*res + getBoundIndex(); 716 return res; 717 } 718 719 bool operator==(const ExprValue& ev2) const; 720 721 //! Make a clean copy of itself using the given memory manager 722 ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; isVar()723 bool isVar() const { return true; } 724 725 public: 726 // Constructor 727 ExprSkolem(ExprManager* em, int index, const Expr& exist, ExprIndex idx = 0) ExprValue(em,SKOLEM_VAR,idx)728 : ExprValue(em, SKOLEM_VAR, idx), d_quant(exist), d_idx(index) { } 729 // Destructor ~ExprSkolem()730 virtual ~ExprSkolem() { } 731 // Memory management new(size_t size,MemoryManager * mm)732 void* operator new(size_t size, MemoryManager* mm) { 733 return mm->newData(size); 734 } delete(void * pMem,MemoryManager * mm)735 void operator delete(void* pMem, MemoryManager* mm) { 736 mm->deleteData(pMem); 737 } delete(void *)738 void operator delete(void*) { } 739 }; // end of class ExprSkolem 740 741 class ExprRational: public ExprValue { 742 friend class Expr; 743 friend class ExprManager; 744 private: 745 Rational d_r; 746 getRational()747 virtual const Rational& getRational() const { return d_r; } 748 749 // Hash function for this subclass hash(const Rational & r)750 static size_t hash(const Rational& r) { 751 return s_charHash(r.toString().c_str()); 752 } 753 754 // Tell ExprManager who we are getMMIndex()755 virtual size_t getMMIndex() const { return EXPR_RATIONAL; } 756 757 protected: 758 computeHash()759 virtual size_t computeHash() const { return hash(d_r); } 760 virtual bool operator==(const ExprValue& ev2) const; 761 //! Make a clean copy of itself using the given memory manager 762 virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; isRational()763 virtual bool isRational() const { return true; } 764 765 public: 766 // Constructor 767 ExprRational(ExprManager* em, const Rational& r, ExprIndex idx = 0) ExprValue(em,RATIONAL_EXPR,idx)768 : ExprValue(em, RATIONAL_EXPR, idx), d_r(r) { } 769 // Destructor ~ExprRational()770 virtual ~ExprRational() { } 771 // Memory management new(size_t size,MemoryManager * mm)772 void* operator new(size_t size, MemoryManager* mm) { 773 return mm->newData(size); 774 } delete(void * pMem,MemoryManager * mm)775 void operator delete(void* pMem, MemoryManager* mm) { 776 mm->deleteData(pMem); 777 } delete(void *)778 void operator delete(void*) { } 779 }; // end of class ExprRational 780 781 // Uninterpreted constants (variables) 782 class ExprVar: public ExprValue { 783 friend class Expr; 784 friend class ExprManager; 785 private: 786 std::string d_name; 787 getName()788 virtual const std::string& getName() const { return d_name; } 789 790 // Tell ExprManager who we are getMMIndex()791 virtual size_t getMMIndex() const { return EXPR_UCONST; } 792 protected: 793 computeHash()794 virtual size_t computeHash() const { 795 return s_charHash(d_name.c_str()); 796 } isVar()797 virtual bool isVar() const { return true; } 798 799 //! Make a clean copy of itself using the given memory manager 800 virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 801 802 public: 803 // Constructor 804 ExprVar(ExprManager *em, const std::string& name, ExprIndex idx = 0) ExprValue(em,UCONST,idx)805 : ExprValue(em, UCONST, idx), d_name(name) { } 806 // Destructor ~ExprVar()807 virtual ~ExprVar() { } 808 809 virtual bool operator==(const ExprValue& ev2) const; 810 // Memory management new(size_t size,MemoryManager * mm)811 void* operator new(size_t size, MemoryManager* mm) { 812 return mm->newData(size); 813 } delete(void * pMem,MemoryManager * mm)814 void operator delete(void* pMem, MemoryManager* mm) { 815 mm->deleteData(pMem); 816 } delete(void *)817 void operator delete(void*) { } 818 }; // end of class ExprVar 819 820 // Interpreted symbols: similar to UCONST, but returns false for isVar(). 821 class ExprSymbol: public ExprValue { 822 friend class Expr; 823 friend class ExprManager; 824 private: 825 std::string d_name; 826 getName()827 virtual const std::string& getName() const { return d_name; } 828 829 // Tell ExprManager who we are getMMIndex()830 virtual size_t getMMIndex() const { return EXPR_SYMBOL; } 831 protected: 832 computeHash()833 virtual size_t computeHash() const { 834 return s_charHash(d_name.c_str())*PRIME + s_intHash(d_kind); 835 } 836 //! Make a clean copy of itself using the given memory manager 837 virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; isSymbol()838 bool isSymbol() const { return true; } 839 840 public: 841 // Constructor 842 ExprSymbol(ExprManager *em, int kind, const std::string& name, 843 ExprIndex idx = 0) ExprValue(em,kind,idx)844 : ExprValue(em, kind, idx), d_name(name) { } 845 // Destructor ~ExprSymbol()846 virtual ~ExprSymbol() { } 847 848 virtual bool operator==(const ExprValue& ev2) const; 849 // Memory management new(size_t size,MemoryManager * mm)850 void* operator new(size_t size, MemoryManager* mm) { 851 return mm->newData(size); 852 } delete(void * pMem,MemoryManager * mm)853 void operator delete(void* pMem, MemoryManager* mm) { 854 mm->deleteData(pMem); 855 } delete(void *)856 void operator delete(void*) { } 857 }; // end of class ExprSymbol 858 859 class ExprBoundVar: public ExprValue { 860 friend class Expr; 861 friend class ExprManager; 862 private: 863 std::string d_name; 864 std::string d_uid; 865 getName()866 virtual const std::string& getName() const { return d_name; } getUid()867 virtual const std::string& getUid() const { return d_uid; } 868 869 // Tell ExprManager who we are getMMIndex()870 virtual size_t getMMIndex() const { return EXPR_BOUND_VAR; } 871 protected: 872 computeHash()873 virtual size_t computeHash() const { 874 return s_charHash(d_name.c_str())*PRIME + s_charHash(d_uid.c_str()); 875 } isVar()876 virtual bool isVar() const { return true; } 877 //! Make a clean copy of itself using the given memory manager 878 virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 879 880 public: 881 // Constructor 882 ExprBoundVar(ExprManager *em, const std::string& name, 883 const std::string& uid, ExprIndex idx = 0) ExprValue(em,BOUND_VAR,idx)884 : ExprValue(em, BOUND_VAR, idx), d_name(name), d_uid(uid) { } 885 // Destructor ~ExprBoundVar()886 virtual ~ExprBoundVar() { } 887 888 virtual bool operator==(const ExprValue& ev2) const; 889 // Memory management new(size_t size,MemoryManager * mm)890 void* operator new(size_t size, MemoryManager* mm) { 891 return mm->newData(size); 892 } delete(void * pMem,MemoryManager * mm)893 void operator delete(void* pMem, MemoryManager* mm) { 894 mm->deleteData(pMem); 895 } delete(void *)896 void operator delete(void*) { } 897 }; // end of class ExprBoundVar 898 899 /*! @brief A "closure" expression which binds variables used in the 900 "body". Used by LAMBDA and quantifiers. */ 901 class ExprClosure: public ExprValue { 902 friend class Expr; 903 friend class ExprManager; 904 private: 905 //! Bound variables 906 std::vector<Expr> d_vars; 907 //! The body of the quantifier/lambda 908 Expr d_body; 909 //! Manual triggers. // added by yeting 910 // Note that due to expr caching, only the most recent triggers specified for a given formula will be used. 911 std::vector<std::vector<Expr> > d_manual_triggers; 912 //! Tell ExprManager who we are getMMIndex()913 virtual size_t getMMIndex() const { return EXPR_CLOSURE; } 914 getVars()915 virtual const std::vector<Expr>& getVars() const { return d_vars; } getBody()916 virtual const Expr& getBody() const { return d_body; } setTriggers(const std::vector<std::vector<Expr>> & triggers)917 virtual void setTriggers(const std::vector<std::vector<Expr> >& triggers) { d_manual_triggers = triggers; } getTriggers()918 virtual const std::vector<std::vector<Expr> >& getTriggers() const { return d_manual_triggers; } 919 920 protected: 921 922 size_t computeHash() const; computeSize()923 Unsigned computeSize() const { return d_body.d_expr->getSize() + 1; } 924 //! Make a clean copy of itself using the given memory manager 925 ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const; 926 927 public: 928 // Constructor 929 ExprClosure(ExprManager *em, int kind, const Expr& var, 930 const Expr& body, ExprIndex idx = 0) ExprValue(em,kind,idx)931 : ExprValue(em, kind, idx), d_body(body) { d_vars.push_back(var); } 932 933 ExprClosure(ExprManager *em, int kind, const std::vector<Expr>& vars, 934 const Expr& body, ExprIndex idx = 0) ExprValue(em,kind,idx)935 : ExprValue(em, kind, idx), d_vars(vars), d_body(body) { } 936 937 ExprClosure(ExprManager *em, int kind, const std::vector<Expr>& vars, 938 const Expr& body, const std::vector<std::vector<Expr> >& trigs, ExprIndex idx = 0) ExprValue(em,kind,idx)939 : ExprValue(em, kind, idx), d_vars(vars), d_body(body), d_manual_triggers(trigs) { } 940 941 // Destructor ~ExprClosure()942 virtual ~ExprClosure() { } 943 944 bool operator==(const ExprValue& ev2) const; 945 // Memory management new(size_t size,MemoryManager * mm)946 void* operator new(size_t size, MemoryManager* mm) { 947 return mm->newData(size); 948 } delete(void * pMem,MemoryManager * mm)949 void operator delete(void* pMem, MemoryManager* mm) { 950 mm->deleteData(pMem); 951 } delete(void *)952 void operator delete(void*) { } isClosure()953 virtual bool isClosure() const { return true; } 954 }; // end of class ExprClosure 955 956 957 } // end of namespace CVC3 958 959 #endif 960