CVC3
expr_value.h
Go to the documentation of this file.
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 /*****************************************************************************/
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
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)
89 
90  //! Equality between this term and next term in ring of all terms in the equivalence class
92 
93  //! The cached type of the expression (may be Null)
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)
104 
105  //! For caching calls to Simplify
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
113 
114  //! Size of dag rooted at this expression
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
133 
134  // End of data members
135 
136 private:
137 
138  //! Set the ExprIndex
139  void setIndex(ExprIndex idx) { d_index = idx; }
140 
141  //! Increment reference counter
142  void incRefcount() { ++d_refcount; }
143 
144  //! Decrement reference counter
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  */
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
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.
184 
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
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)
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
201  ExprValue* rebuild(ExprManager* em) const
202  { return copy(em, 0); }
203 
204  //! Make a clean copy of the expr using the given ExprManager
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 */
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 */
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)
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
250  int getKind() const { return d_kind; }
251 
252  //! Overload operator new
253  void* operator new(size_t size, MemoryManager* mm)
254  { return mm->newData(size); }
255  void operator delete(void* pMem, MemoryManager* mm) {
256  mm->deleteData(pMem);
257  }
258 
259  //! Overload operator delete
260  void operator delete(void*) { }
261 
262  //! Get unique memory manager ID
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  */
275  virtual const ExprValue* getExprValue() const
276  { throw Exception("Illegal call to getExprValue()"); }
277  //! String expression tester
278  virtual bool isString() const { return false; }
279  //! Rational number expression tester
280  virtual bool isRational() const { return false; }
281  //! Uninterpreted constants
282  virtual bool isVar() const { return false; }
283  //! Application of another expression
284  virtual bool isApply() const { return false; }
285  //! Special named symbol
286  virtual bool isSymbol() const { return false; }
287  //! A LAMBDA-expression or a quantifier
288  virtual bool isClosure() const { return false; }
289  //! Special Expr holding a theorem
290  virtual bool isTheorem() const { return false; }
291 
292  //! Get kids: by default, returns a ref to an empty vector
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
299  virtual unsigned arity() const { return 0; }
300 
301  //! Special attributes for uninterpreted functions
302  virtual CDO<Theorem>* getSig() const {
303  DebugAssert(false, "getSig() is called on ExprValue");
304  return NULL;
305  }
306 
307  virtual CDO<Theorem>* getRep() const {
308  DebugAssert(false, "getRep() is called on ExprValue");
309  return NULL;
310  }
311 
312  virtual void setSig(CDO<Theorem>* sig) {
313  DebugAssert(false, "setSig() is called on ExprValue");
314  }
315 
316  virtual void setRep(CDO<Theorem>* rep) {
317  DebugAssert(false, "setRep() is called on ExprValue");
318  }
319 
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 
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 
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.
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)
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
353  virtual Op getOp() const {
354  DebugAssert(false, "getOp() is called on ExprValue");
355  return Op(NULL_KIND);
356  }
357 
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 
364  virtual const Expr& getBody() const {
365  DebugAssert(false, "getBody() is called on ExprValue");
366  static Expr null;
367  return null;
368  }
369 
370  virtual void setTriggers(const std::vector<std::vector<Expr> >& triggers) {
371  DebugAssert(false, "setTriggers() is called on ExprValue");
372  }
373 
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 
381  virtual const Expr& getExistential() const {
382  DebugAssert(false, "getExistential() is called on ExprValue");
383  static Expr null;
384  return null;
385  }
386  virtual int getBoundIndex() const {
387  DebugAssert(false, "getIndex() is called on ExprValue");
388  return 0;
389  }
390 
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  }
396  virtual const std::string& getField() const {
397  DebugAssert(false, "getField() is called on ExprValue");
398  static std::string null;
399  return null;
400  }
401  virtual int getTupleIndex() const {
402  DebugAssert(false, "getTupleIndex() is called on ExprValue");
403  return 0;
404  }
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
425 
426 private:
427 
428  //! Tell ExprManager who we are
429  size_t getMMIndex() const { return EXPR_NODE; }
430 
431 protected:
432  //! Return number of children
433  unsigned arity() const { return d_children.size(); }
434 
435  //! Return reference to children
436  std::vector<Expr>& getKids1() { return d_children; }
437 
438  //! Return reference to children
439  const std::vector<Expr>& getKids() const { return d_children; }
440 
441  //! Use our static hash() for the member method
442  size_t computeHash() const {
443  return ExprValue::hash(d_kind, d_children);
444  }
445 
446  //! Use our static sizeWithChildren() for the member method
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)
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)
461  : ExprValue(em, kind, idx), d_children(kids), d_sig(NULL), d_rep(NULL) { }
462  //! Destructor
463  virtual ~ExprNode();
464 
465  //! Overload operator new
466  void* operator new(size_t size, MemoryManager* mm)
467  { return mm->newData(size); }
468  void operator delete(void* pMem, MemoryManager* mm) {
469  mm->deleteData(pMem);
470  }
471 
472  //! Overload operator delete
473  void operator delete(void*) { }
474 
475  //! Compare with another ExprValue
476  virtual bool operator==(const ExprValue& ev2) const;
477 
478  virtual CDO<Theorem>* getSig() const { return d_sig; }
479  virtual CDO<Theorem>* getRep() const { return d_rep; }
480 
481  virtual void setRep(CDO<Theorem>* rep) { d_rep = rep; }
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
498  size_t getMMIndex() const { return EXPR_NODE; }
499 
500 protected:
501  //! Return number of children
502  unsigned arity() const { return d_children.size(); }
503 
504  //! Return reference to children
505  const std::vector<Expr>& getKids() const { return d_children; }
506 
507  //! Use our static hash() for the member method
508  size_t computeHash() const {
510  }
511 
512  //! Use our static sizeWithChildren() for the member method
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
522  ExprNodeTmp(ExprManager* em, int kind, const std::vector<Expr>& kids)
523  : ExprValue(em, kind, 0), d_children(kids) { }
524 
525  //! Destructor
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:
539 protected:
540  size_t getMMIndex() const { return EXPR_APPLY; }
541  size_t computeHash() const {
543  }
544  Op getOp() const { return Op(d_opExpr); }
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
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; }
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:
565 protected:
566  size_t getMMIndex() const { return EXPR_APPLY; }
567  size_t computeHash() const {
568  return PRIME*ExprNode::computeHash() + d_opExpr.hash();
569  }
570  Op getOp() const { return Op(d_opExpr); }
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)
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)
582  : ExprNode(em, NULL_KIND, kids, idx), d_opExpr(op.getExpr())
583  { DebugAssert(!op.getExpr().isNull(), "Expected non-null Op");
584  d_kind = APPLY; }
585  virtual ~ExprApply() { }
586 
587  bool operator==(const ExprValue& ev2) const;
588  // Memory management
589  void* operator new(size_t size, MemoryManager* mm) {
590  return mm->newData(size);
591  }
592  void operator delete(void* pMem, MemoryManager* mm) {
593  mm->deleteData(pMem);
594  }
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
666  static size_t hash(const std::string& str) {
667  return s_charHash(str.c_str());
668  }
669 
670  // Tell ExprManager who we are
671  virtual size_t getMMIndex() const { return EXPR_STRING; }
672 
673 protected:
674  // Use our static hash() for the member method
675  virtual size_t computeHash() const { return hash(d_str); }
676 
677  virtual bool isString() const { return true; }
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)
685  : ExprValue(em, STRING_EXPR, idx), d_str(s) { }
686  // Destructor
687  virtual ~ExprString() { }
688 
689  virtual bool operator==(const ExprValue& ev2) const;
690  // Memory management
691  void* operator new(size_t size, MemoryManager* mm) {
692  return mm->newData(size);
693  }
694  void operator delete(void* pMem, MemoryManager* mm) {
695  mm->deleteData(pMem);
696  }
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
706  const Expr& getExistential() const {return d_quant;}
707  int getBoundIndex() const {return d_idx;}
708 
709  // Tell ExprManager who we are
710  size_t getMMIndex() const { return EXPR_SKOLEM;}
711 
712 protected:
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;
723  bool isVar() const { return true; }
724 
725 public:
726  // Constructor
727  ExprSkolem(ExprManager* em, int index, const Expr& exist, ExprIndex idx = 0)
728  : ExprValue(em, SKOLEM_VAR, idx), d_quant(exist), d_idx(index) { }
729  // Destructor
730  virtual ~ExprSkolem() { }
731  // Memory management
732  void* operator new(size_t size, MemoryManager* mm) {
733  return mm->newData(size);
734  }
735  void operator delete(void* pMem, MemoryManager* mm) {
736  mm->deleteData(pMem);
737  }
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:
746 
747  virtual const Rational& getRational() const { return d_r; }
748 
749  // Hash function for this subclass
750  static size_t hash(const Rational& r) {
751  return s_charHash(r.toString().c_str());
752  }
753 
754  // Tell ExprManager who we are
755  virtual size_t getMMIndex() const { return EXPR_RATIONAL; }
756 
757 protected:
758 
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;
763  virtual bool isRational() const { return true; }
764 
765 public:
766  // Constructor
767  ExprRational(ExprManager* em, const Rational& r, ExprIndex idx = 0)
768  : ExprValue(em, RATIONAL_EXPR, idx), d_r(r) { }
769  // Destructor
770  virtual ~ExprRational() { }
771  // Memory management
772  void* operator new(size_t size, MemoryManager* mm) {
773  return mm->newData(size);
774  }
775  void operator delete(void* pMem, MemoryManager* mm) {
776  mm->deleteData(pMem);
777  }
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 
788  virtual const std::string& getName() const { return d_name; }
789 
790  // Tell ExprManager who we are
791  virtual size_t getMMIndex() const { return EXPR_UCONST; }
792 protected:
793 
794  virtual size_t computeHash() const {
795  return s_charHash(d_name.c_str());
796  }
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)
805  : ExprValue(em, UCONST, idx), d_name(name) { }
806  // Destructor
807  virtual ~ExprVar() { }
808 
809  virtual bool operator==(const ExprValue& ev2) const;
810  // Memory management
811  void* operator new(size_t size, MemoryManager* mm) {
812  return mm->newData(size);
813  }
814  void operator delete(void* pMem, MemoryManager* mm) {
815  mm->deleteData(pMem);
816  }
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 
827  virtual const std::string& getName() const { return d_name; }
828 
829  // Tell ExprManager who we are
830  virtual size_t getMMIndex() const { return EXPR_SYMBOL; }
831 protected:
832 
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;
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)
844  : ExprValue(em, kind, idx), d_name(name) { }
845  // Destructor
846  virtual ~ExprSymbol() { }
847 
848  virtual bool operator==(const ExprValue& ev2) const;
849  // Memory management
850  void* operator new(size_t size, MemoryManager* mm) {
851  return mm->newData(size);
852  }
853  void operator delete(void* pMem, MemoryManager* mm) {
854  mm->deleteData(pMem);
855  }
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 
866  virtual const std::string& getName() const { return d_name; }
867  virtual const std::string& getUid() const { return d_uid; }
868 
869  // Tell ExprManager who we are
870  virtual size_t getMMIndex() const { return EXPR_BOUND_VAR; }
871 protected:
872 
873  virtual size_t computeHash() const {
874  return s_charHash(d_name.c_str())*PRIME + s_charHash(d_uid.c_str());
875  }
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)
884  : ExprValue(em, BOUND_VAR, idx), d_name(name), d_uid(uid) { }
885  // Destructor
886  virtual ~ExprBoundVar() { }
887 
888  virtual bool operator==(const ExprValue& ev2) const;
889  // Memory management
890  void* operator new(size_t size, MemoryManager* mm) {
891  return mm->newData(size);
892  }
893  void operator delete(void* pMem, MemoryManager* mm) {
894  mm->deleteData(pMem);
895  }
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
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
913  virtual size_t getMMIndex() const { return EXPR_CLOSURE; }
914 
915  virtual const std::vector<Expr>& getVars() const { return d_vars; }
916  virtual const Expr& getBody() const { return d_body; }
917  virtual void setTriggers(const std::vector<std::vector<Expr> >& triggers) { d_manual_triggers = triggers; }
918  virtual const std::vector<std::vector<Expr> >& getTriggers() const { return d_manual_triggers; }
919 
920 protected:
921 
922  size_t computeHash() const;
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)
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)
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)
939  : ExprValue(em, kind, idx), d_vars(vars), d_body(body), d_manual_triggers(trigs) { }
940 
941  // Destructor
942  virtual ~ExprClosure() { }
943 
944  bool operator==(const ExprValue& ev2) const;
945  // Memory management
946  void* operator new(size_t size, MemoryManager* mm) {
947  return mm->newData(size);
948  }
949  void operator delete(void* pMem, MemoryManager* mm) {
950  mm->deleteData(pMem);
951  }
952  void operator delete(void*) { }
953  virtual bool isClosure() const { return true; }
954 }; // end of class ExprClosure
955 
956 
957 } // end of namespace CVC3
958 
959 #endif