CVC3  2.4.1
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
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 {
509  return ExprValue::hash(d_kind, d_children);
510  }
511 
512  //! Use our static sizeWithChildren() for the member method
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
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 {
542  return PRIME*ExprNodeTmp::computeHash() + d_opExpr.hash();
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
Unsigned computeSize() const
Non-caching size function which actually computes the size.
Definition: expr_value.h:923
Expr d_body
The body of the quantifier/lambda.
Definition: expr_value.h:908
CDFlags d_dynamicFlags
context-dependent bit-vector for flags that are context-dependent
Definition: expr_value.h:112
bool isNull() const
Definition: expr.h:1223
const Expr & getExpr() const
Definition: expr_op.h:84
CDO< Theorem > * d_eqNext
Equality between this term and next term in ring of all terms in the equivalence class.
Definition: expr_value.h:91
unsigned arity() const
Return number of children.
Definition: expr_value.h:502
size_t computeHash() const
Use our static hash() for the member method.
Definition: expr_value.h:442
Expr rebuildRec(const Expr &e)
Cached recursive descent. Must be called only during rebuild()
ExprValue * d_expr
The value. This is the only data member in this class.
Definition: expr.h:197
virtual const std::string & getUid() const
Definition: expr_value.h:867
bool isSymbol() const
Special named symbol.
Definition: expr_value.h:838
std::vector< Expr > & getKids1()
Return reference to children.
Definition: expr_value.h:436
ExprNodeTmp(ExprManager *em, int kind, const std::vector< Expr > &kids)
Constructor.
Definition: expr_value.h:522
ExprValue * rebuild(ExprManager *em) const
Make a clean copy of itself using the given ExprManager.
Definition: expr_value.h:201
virtual ~ExprVar()
Definition: expr_value.h:807
Data structure of expressions in CVC3.
Definition: expr.h:133
ExprIndex d_index
Unique expression id.
Definition: expr_value.h:79
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.h:212
#define CVC_DLL
Definition: type.h:43
virtual bool isRational() const
Rational number expression tester.
Definition: expr_value.h:280
std::vector< Expr > d_children
Vector of children.
Definition: expr_value.h:420
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
Definition: expr_value.h:866
virtual void setSig(CDO< Theorem > *sig)
Definition: expr_value.h:482
Op getOp() const
Get the Op from an Apply Expr.
Definition: expr_value.h:544
bool isVar() const
Uninterpreted constants.
Definition: expr_value.h:723
virtual bool operator==(const ExprValue &ev2) const
Compare with another ExprValue.
Definition: expr_value.cpp:85
static size_t pointerHash(void *p)
Definition: expr_value.h:185
virtual Op getOp() const
Get the Op from an Apply Expr.
Definition: expr_value.h:353
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.h:759
size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.cpp:333
ExprApply(ExprManager *em, const Op &op, const std::vector< Expr > &kids, ExprIndex idx=0)
Definition: expr_value.h:580
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:263
Expr rebuild(Expr e, ExprManager *em) const
Make a clean copy of the expr using the given ExprManager.
Definition: expr_value.h:205
Definition: cdo.h:39
CDO< Theorem > * d_find
The find attribute (may be NULL)
Definition: expr_value.h:88
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:91
virtual const Rational & getRational() const
Definition: expr_value.h:332
Op getOp() const
Get the Op from an Apply Expr.
Definition: expr_value.h:570
ExprClosure(ExprManager *em, int kind, const Expr &var, const Expr &body, ExprIndex idx=0)
Definition: expr_value.h:929
unsigned d_refcount
Reference counter for garbage collection.
Definition: expr_value.h:82
virtual bool isSymbol() const
Special named symbol.
Definition: expr_value.h:286
virtual void setRep(CDO< Theorem > *rep)
Definition: expr_value.h:481
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Definition: expr_value.cpp:210
long unsigned ExprIndex
Expression index type.
Definition: expr.h:87
MS C++ specific settings.
Definition: type.h:42
virtual bool isString() const
String expression tester.
Definition: expr_value.h:677
static Unsigned sizeWithChildren(const std::vector< Expr > &kids)
Definition: expr_value.cpp:322
virtual ~ExprBoundVar()
Definition: expr_value.h:886
Theorem d_simpCache
For caching calls to Simplify.
Definition: expr_value.h:106
virtual ~ExprSkolem()
Definition: expr_value.h:730
std::string d_name
Definition: expr_value.h:786
size_t d_hash
Cached hash value (initially 0)
Definition: expr_value.h:85
ExprClosure(ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, ExprIndex idx=0)
Definition: expr_value.h:933
virtual ~ExprString()
Definition: expr_value.h:687
bool isApply() const
Application of another expression.
Definition: expr_value.h:571
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:218
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Definition: expr_value.cpp:186
Expr d_quant
The quantified expression to skolemize.
Definition: expr_value.h:704
std::string toString(int base=10) const
virtual const Theorem & getTheorem() const
Definition: expr_value.h:405
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Definition: expr_value.cpp:174
int getKind() const
Get the kind of the expression.
Definition: expr_value.h:250
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.h:833
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
Definition: expr_value.h:827
size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:710
size_t hash() const
Caching hash function.
Definition: expr_value.h:155
virtual const Expr & getVar() const
Returns the original Boolean variable (for BoolVarExprValue)
Definition: expr_value.h:346
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Definition: expr_value.cpp:198
#define DebugAssert(cond, str)
Definition: debug.h:408
NotifyList * d_notifyList
The cached TCC of the expression (may be Null)
Definition: expr_value.h:103
std::string d_name
Definition: expr_value.h:863
bool operator==(const Expr &e1, const Expr &e2)
Definition: expr.h:1600
virtual bool isRational() const
Rational number expression tester.
Definition: expr_value.h:763
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:181
const std::vector< Expr > & d_children
Vector of children.
Definition: expr_value.h:493
bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Definition: expr_value.cpp:156
ExprNode(ExprManager *em, int kind, ExprIndex idx=0)
Constructor.
Definition: expr_value.h:456
virtual const std::vector< std::string > & getFields() const
Definition: expr_value.h:391
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:164
virtual unsigned arity() const
Default arity = 0.
Definition: expr_value.h:299
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:830
virtual bool isVar() const
Uninterpreted constants.
Definition: expr_value.h:797
virtual CDO< Theorem > * getRep() const
Definition: expr_value.h:307
virtual ~ExprApplyTmp()
Definition: expr_value.h:555
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.h:873
ExprRational(ExprManager *em, const Rational &r, ExprIndex idx=0)
Definition: expr_value.h:767
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:755
Definition: kinds.h:242
Unsigned computeSize() const
Use our static sizeWithChildren() for the member method.
Definition: expr_value.h:513
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
Definition: expr_manager.h:334
std::vector< std::vector< Expr > > d_manual_triggers
Manual triggers. // added by yeting.
Definition: expr_value.h:911
virtual bool isVar() const
Uninterpreted constants.
Definition: expr_value.h:282
virtual CDO< Theorem > * getRep() const
Definition: expr_value.h:479
unsigned d_simpCacheTag
For checking whether simplify cache is valid.
Definition: expr_value.h:109
virtual const ExprValue * getExprValue() const
Test whether the expression is a generic subclass.
Definition: expr_value.h:275
std::vector< Expr > d_vars
Bound variables.
Definition: expr_value.h:906
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
Definition: expr_value.h:339
ExprSkolem(ExprManager *em, int index, const Expr &exist, ExprIndex idx=0)
Definition: expr_value.h:727
virtual const std::vector< std::vector< Expr > > & getTriggers() const
Definition: expr_value.h:374
virtual int getTupleIndex() const
Definition: expr_value.h:401
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:205
CDO< Theorem > * d_sig
Definition: expr_value.h:423
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
ExprString(ExprManager *em, const std::string &s, ExprIndex idx=0)
Definition: expr_value.h:684
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:278
Application of functions and predicates.
Definition: expr.h:68
const std::vector< Expr > & getEmptyVector()
References to empty objects (used in ExprValue)
Definition: expr_manager.h:282
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:193
static size_t hash(const Rational &r)
Definition: expr_value.h:750
virtual const std::vector< Expr > & getKids() const
Get kids: by default, returns a ref to an empty vector.
Definition: expr_value.h:293
static std::hash< char * > s_charHash
Return child with greatest height.
Definition: expr_value.h:182
CDO< Theorem > * d_rep
Definition: expr_value.h:424
virtual bool isClosure() const
A LAMBDA-expression or a quantifier.
Definition: expr_value.h:288
int getBoundIndex() const
Definition: expr_value.h:707
virtual const std::string & getField() const
Definition: expr_value.h:396
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
virtual CDO< Theorem > * getSig() const
Special attributes for uninterpreted functions.
Definition: expr_value.h:302
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.h:794
size_t computeHash() const
Use our static hash() for the member method.
Definition: expr_value.h:541
const std::vector< Expr > & getKids() const
Return reference to children.
Definition: expr_value.h:439
ExprSymbol(ExprManager *em, int kind, const std::string &name, ExprIndex idx=0)
Definition: expr_value.h:842
void incRefcount()
Increment reference counter.
Definition: expr_value.h:142
virtual bool isApply() const
Application of another expression.
Definition: expr_value.h:284
virtual size_t getMMIndex() const
Tell ExprManager who we are.
Definition: expr_value.h:913
virtual ~ExprApply()
Definition: expr_value.h:585
ExprApplyTmp(ExprManager *em, const Op &op, const std::vector< Expr > &kids)
Definition: expr_value.h:550
unsigned arity() const
Return number of children.
Definition: expr_value.h:433
#define IF_DEBUG(code)
Definition: debug.h:406
#define PRIME
Definition: expr_value.h:50
MemoryManager * getMM(size_t MMIndex)
Return the memory manager (for the benefit of subclasses)
Definition: expr_value.h:195
virtual void setTriggers(const std::vector< std::vector< Expr > > &triggers)
Definition: expr_value.h:917
Expression Manager.
Definition: expr_manager.h:58
virtual ~ExprClosure()
Definition: expr_value.h:942
ExprVar(ExprManager *em, const std::string &name, ExprIndex idx=0)
Definition: expr_value.h:804
Unsigned getSize() const
Return DAG-size of Expr.
Definition: expr_value.h:162
virtual ~ExprRational()
Definition: expr_value.h:770
bool operator==(const ExprValue &ev2) const
Compare with another ExprValue.
Definition: expr_value.cpp:246
Definition: kinds.h:90
virtual Unsigned computeSize() const
Non-caching size function which actually computes the size.
Definition: expr_value.h:216
size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.h:713
virtual bool isString() const
String expression tester.
Definition: expr_value.h:278
void decRefcount()
Decrement reference counter.
Definition: expr_value.h:145
unsigned getFlag()
Return the current Expr flag counter.
Definition: expr_manager.h:213
virtual ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:151
static size_t hash(const Expr &e)
Definition: expr.h:992
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given memory manager.
Definition: expr_value.cpp:254
std::string d_name
Definition: expr_value.h:825
virtual int getBoundIndex() const
Definition: expr_value.h:386
ExprApply(ExprManager *em, const Op &op, ExprIndex idx=0)
Definition: expr_value.h:576
ExprValue(ExprManager *em, int kind, ExprIndex idx=0)
Constructor.
Definition: expr_value.h:223
Unsigned d_size
Size of dag rooted at this expression.
Definition: expr_value.h:115
virtual const std::string & getString() const
Definition: expr_value.h:326
std::string d_str
Definition: expr_value.h:663
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...
Definition: expr_value.h:901
ExprManager * d_em
Our expr. manager.
Definition: expr_value.h:132
virtual const std::vector< Expr > & getVars() const
Definition: expr_value.h:358
virtual const Rational & getRational() const
Definition: expr_value.h:747
size_t getMMIndex() const
Tell ExprManager who we are.
Definition: expr_value.h:429
unsigned d_flag
Which child has the largest height.
Definition: expr_value.h:124
size_t getMMIndex() const
Tell ExprManager who we are.
Definition: expr_value.h:498
bool isApply() const
Application of another expression.
Definition: expr_value.h:545
Unsigned computeSize() const
Use our static sizeWithChildren() for the member method.
Definition: expr_value.h:447
virtual ~ExprNodeTmp()
Destructor.
Definition: expr_value.h:526
static std::hash< long int > s_intHash
Definition: expr_value.h:183
const std::vector< Expr > & getKids() const
Return reference to children.
Definition: expr_value.h:505
std::string d_uid
Definition: expr_value.h:864
size_t getMMIndex() const
Tell ExprManager who we are.
Definition: expr_value.h:566
bool isKindRegistered(int kind)
Returns true if kind is built into CVC or has been registered via newKind.
Definition: expr_manager.h:392
static size_t hash(const std::string &str)
Definition: expr_value.h:666
virtual bool isVar() const
Uninterpreted constants.
Definition: expr_value.h:876
Definition of the API to expression package. See class Expr for details.
void gc(ExprValue *ev)
Garbage collect the ExprValue pointer.
virtual const Expr & getBody() const
Definition: expr_value.h:916
ExprBoundVar(ExprManager *em, const std::string &name, const std::string &uid, ExprIndex idx=0)
Definition: expr_value.h:882
virtual const Expr & getExistential() const
Definition: expr_value.h:381
virtual void setSig(CDO< Theorem > *sig)
Definition: expr_value.h:312
const Expr & getExistential() const
Definition: expr_value.h:706
virtual const std::vector< Expr > & getVars() const
Definition: expr_value.h:915
size_t getMMIndex() const
Tell ExprManager who we are.
Definition: expr_value.h:540
int d_kind
The kind of the expression. In particular, it determines which subclass of ExprValue is used to store...
Definition: expr_value.h:129
virtual const std::vector< std::vector< Expr > > & getTriggers() const
Definition: expr_value.h:918
int d_idx
Variable index in the quantified expression.
Definition: expr_value.h:705
Type d_type
The cached type of the expression (may be Null)
Definition: expr_value.h:94
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:671
static size_t hash(const int n)
Definition: expr_value.h:189
ExprClosure(ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &trigs, ExprIndex idx=0)
Definition: expr_value.h:937
The base class for holding the actual data in expressions.
Definition: expr_value.h:69
virtual size_t computeHash() const
Non-caching hash function which actually computes the hash.
Definition: expr_value.h:675
Definition: expr.cpp:35
ExprNode(ExprManager *em, int kind, const std::vector< Expr > &kids, ExprIndex idx=0)
Constructor.
Definition: expr_value.h:459
virtual const std::string & getUid() const
Definition: expr_value.h:320
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
Definition: expr_value.h:788
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:791
virtual ~ExprSymbol()
Definition: expr_value.h:846
virtual void setRep(CDO< Theorem > *rep)
Definition: expr_value.h:316
virtual void setTriggers(const std::vector< std::vector< Expr > > &triggers)
Definition: expr_value.h:370
virtual bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Definition: expr_value.cpp:144
virtual CDO< Theorem > * getSig() const
Special attributes for uninterpreted functions.
Definition: expr_value.h:478
virtual bool isClosure() const
A LAMBDA-expression or a quantifier.
Definition: expr_value.h:953
virtual const std::string & getString() const
Definition: expr_value.h:678
void setIndex(ExprIndex idx)
Set the ExprIndex.
Definition: expr_value.h:139
virtual bool isTheorem() const
Special Expr holding a theorem.
Definition: expr_value.h:290
bool operator==(const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses)
Definition: expr_value.cpp:269
virtual const Expr & getBody() const
Definition: expr_value.h:364
size_t computeHash() const
Use our static hash() for the member method.
Definition: expr_value.h:508
size_t computeHash() const
Use our static hash() for the member method.
Definition: expr_value.h:567
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:870