CVC3  2.4.1
expr.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr.h
4  * \brief Definition of the API to expression package. See class Expr for details.
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Tue Nov 26 00:27:40 2002
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__expr_h_
23 #define _cvc3__expr_h_
24 
25 #include <stdlib.h>
26 #include <sstream>
27 #include <set>
28 #include <functional>
29 #include <iterator>
30 #include <map>
31 
32 #include "os.h"
33 #include "compat_hash_map.h"
34 #include "compat_hash_set.h"
35 #include "rational.h"
36 #include "kinds.h"
37 #include "cdo.h"
38 #include "cdflags.h"
39 #include "lang.h"
40 #include "memory_manager.h"
41 
42 class CInterface;
43 
44 namespace CVC3 {
45 
46  class NotifyList;
47  class Theory;
48  class Op;
49  class Type;
50  class Theorem;
51 
52  template<class Data>
53  class ExprHashMap;
54 
55  class ExprManager;
56  // Internal data-holding classes
57  class ExprValue;
58  class ExprNode;
59  // Printing
60  class ExprStream;
61 
62  //! Type ID of each ExprValue subclass.
63  /*! It is defined in expr.h, so that ExprManager can use it before loading
64  expr_value.h */
65  typedef enum {
68  EXPR_APPLY, //!< Application of functions and predicates
76  EXPR_VALUE_TYPE_LAST // The end of list; don't assign it to any subclass
77  } ExprValueType;
78 
79  //! Enum for cardinality of types
80  typedef enum {
84  } Cardinality;
85 
86  //! Expression index type
87  typedef long unsigned ExprIndex;
88 
89  /**************************************************************************/
90  /*! \defgroup ExprPkg Expression Package
91  * \ingroup BuildingBlocks
92  */
93  /**************************************************************************/
94  /*! \defgroup Expr_SmartPointer Smart Pointer Functionality in Expr
95  * \ingroup ExprPkg
96  */
97  /**************************************************************************/
98 
99  /**************************************************************************/
100  //! Data structure of expressions in CVC3
101  /*! \ingroup ExprPkg
102  * Class: Expr <br>
103  * Author: Clark Barrett <br>
104  * Created: Mon Nov 25 15:29:37 2002
105  *
106  * This class is the main data structure for expressions that all
107  * other components should use. It is actually a <em>smart
108  * pointer</em> to the actual data holding class ExprValue and its
109  * subclasses.
110  *
111  * Expressions are represented as DAGs with maximal sharing of
112  * subexpressions. Therefore, testing for equality is a constant time
113  * operation (simply compare the pointers).
114  *
115  * Unused expressions are automatically garbage-collected. The use is
116  * determined by a reference counting mechanism. In particular, this
117  * means that if there is a circular dependency among expressions
118  * (e.g. an attribute points back to the expression itself), these
119  * expressions will not be garbage-collected, even if no one else is
120  * using them.
121  *
122  * The most frequently used operations are getKind() (determining the
123  * kind of the top level node of the expression), arity() (how many
124  * children an Expr has), operator[]() for accessing a child, and
125  * various testers and methods for constructing new expressions.
126  *
127  * In addition, a total ordering operator<() is provided. It is
128  * guaranteed to remain the same for the lifetime of the expressions
129  * (it may change, however, if the expression is garbage-collected and
130  * reborn).
131  */
132  /**************************************************************************/
133 class CVC_DLL Expr {
134  friend class ExprHasher;
135  friend class ExprManager;
136  friend class Op;
137  friend class ExprValue;
138  friend class ExprNode;
139  friend class ExprClosure;
140  friend class ::CInterface;
141  friend class Theorem;
142 
143  /*! \addtogroup ExprPkg
144  * @{
145  */
146  //! bit-masks for static flags
147  typedef enum {
148  //! Whether is valid TYPE expr
149  VALID_TYPE = 0x1,
150  //! Whether IS_ATOMIC flag is valid (initialized)
151  VALID_IS_ATOMIC = 0x2,
152  //! Whether the expression is an atomic term or formula
153  IS_ATOMIC = 0x4,
154  //! Expression is the result of a "normal" (idempotent) rewrite
155  REWRITE_NORMAL = 0x8,
156  //! Finite type
157  IS_FINITE = 0x400,
158  //! Well-founded (used in datatypes)
159  WELL_FOUNDED = 0x800,
160  //! Compute transitive closure (for binary uninterpreted predicates)
161  COMPUTE_TRANS_CLOSURE = 0x1000,
162  //! Whether expr contains a bounded variable (for quantifier instantiation)
163  CONTAINS_BOUND_VAR = 0x00020000,
164  //! Whether expr uses CC algorithm that relies on not simplifying an expr that has a find
165  USES_CC = 0x00080000,
166  //! Whether TERMINALS_CONST flag is valid (initialized)
167  VALID_TERMINALS_CONST = 0x00100000,
168  //! Whether expr contains only numerical constants at all possible ite terminals
169  TERMINALS_CONST = 0x00200000
170  } StaticFlagsEnum;
171 
172  //! bit-masks for dynamic flags
173  // TODO: Registered flags instead of hard-wired
174  typedef enum {
175  //! Whether expr has been added as an implied literal
176  IMPLIED_LITERAL = 0x10,
177  IS_USER_ASSUMPTION = 0x20,
178  IS_INT_ASSUMPTION = 0x40,
179  IS_JUSTIFIED = 0x80,
180  IS_TRANSLATED = 0x100,
181  IS_USER_REGISTERED_ATOM = 0x200,
182  IS_SELECTED = 0x2000,
183  IS_STORED_PREDICATE = 0x4000,
184  IS_REGISTERED_ATOM = 0x8000,
185  IN_USER_ASSUMPTION = 0x00010000,
186  //! Whether expr is normalized (in array theory)
187  NOT_ARRAY_NORMALIZED = 0x00040000
188  } DynamicFlagsEnum;
189 
190  //! Convenient null expr
191  static Expr s_null;
192 
193  /////////////////////////////////////////////////////////////////////////////
194  // Private Dynamic Data //
195  /////////////////////////////////////////////////////////////////////////////
196  //! The value. This is the only data member in this class.
198 
199  /////////////////////////////////////////////////////////////////////////////
200  // Private methods //
201  /////////////////////////////////////////////////////////////////////////////
202 
203  //! Private constructor, simply wraps around the pointer
204  Expr(ExprValue* expr);
205 
206  Expr recursiveSubst(const ExprHashMap<Expr>& subst,
207  ExprHashMap<Expr>& visited) const;
208 
209  Expr recursiveQuantSubst(const ExprHashMap<Expr>& subst,
210  ExprHashMap<Expr>& visited) const;
211 
212  std::vector<std::vector<Expr> > substTriggers(const ExprHashMap<Expr> & subst,
213  ExprHashMap<Expr> & visited) const;
214 public:
215  /////////////////////////////////////////////////////////////////////////////
216  // Public Classes and Types //
217  /////////////////////////////////////////////////////////////////////////////
218 
219  /////////////////////////////////////////////////////////////////////////////
220  /*!
221  * Class: Expr::iterator
222  * Author: Sergey Berezin
223  * Created: Fri Dec 6 15:38:51 2002
224  * Description: STL-like iterator API to the Expr's children.
225  * IMPORTANT: the iterator will not be valid after the originating
226  * expression is destroyed.
227  */
228  /////////////////////////////////////////////////////////////////////////////
230  : public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
231  {
232  friend class Expr;
233  private:
234  std::vector<Expr>::const_iterator d_it;
235  // Private constructors (used by Expr only)
236  //
237  //! Construct an iterator out of the vector's iterator
238  iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
239  // Public methods
240  public:
241  //! Default constructor
242  iterator() { }
243  // Copy constructor and operator= are defined by C++, that's good enough
244 
245  //! Equality
246  bool operator==(const iterator& i) const {
247  return d_it == i.d_it;
248  }
249  //! Disequality
250  bool operator!=(const iterator& i) const { return !(*this == i); }
251  //! Dereference operator
252  const Expr& operator*() const { return *d_it; }
253  //! Dereference and member access
254  const Expr* operator->() const { return &(operator*()); }
255  //! Prefix increment
257  ++d_it;
258  return *this;
259  }
260  /*! @brief Postfix increment requires a Proxy object to hold the
261  * intermediate value for dereferencing */
262  class Proxy {
263  const Expr* d_e;
264  public:
265  Proxy(const Expr& e) : d_e(&e) { }
266  Expr operator*() { return *d_e; }
267  };
268  //! Postfix increment
269  /*! \return Proxy with the old Expr.
270  *
271  * Now, an expression like *i++ will return the current *i, and
272  * then advance the iterator. However, don't try to use Proxy for
273  * anything else.
274  */
276  Proxy e(*(*this));
277  ++(*this);
278  return e;
279  }
280  }; // end of class Expr::iterator
281 
282  /////////////////////////////////////////////////////////////////////////////
283  // Constructors //
284  /////////////////////////////////////////////////////////////////////////////
285 
286  //! Default constructor creates the Null Expr
287  Expr(): d_expr(NULL) {}
288 
289  /*! @brief Copy constructor and assignment (copy the pointer and take care
290  of the refcount) */
291  Expr(const Expr& e);
292  //! Assignment operator: take care of the refcounting and GC
293  Expr& operator=(const Expr& e);
294 
295  // These constructors grab the ExprManager from the Op or the first
296  // child. The operator and all children must belong to the same
297  // ExprManager.
298  Expr(const Op& op, const Expr& child);
299  Expr(const Op& op, const Expr& child0, const Expr& child1);
300  Expr(const Op& op, const Expr& child0, const Expr& child1,
301  const Expr& child2);
302  Expr(const Op& op, const Expr& child0, const Expr& child1,
303  const Expr& child2, const Expr& child3);
304  Expr(const Op& op, const std::vector<Expr>& children,
305  ExprManager* em = NULL);
306 
307  //! Destructor
308  ~Expr();
309 
310  // Compound expression constructors
311  Expr eqExpr(const Expr& right) const;
312  Expr notExpr() const;
313  Expr negate() const; // avoid double-negatives
314  Expr andExpr(const Expr& right) const;
315  Expr orExpr(const Expr& right) const;
316  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
317  Expr iffExpr(const Expr& right) const;
318  Expr impExpr(const Expr& right) const;
319  Expr xorExpr(const Expr& right) const;
320  //! Create a Skolem constant for the i'th variable of an existential (*this)
321  Expr skolemExpr(int i) const;
322  //! Create a Boolean variable out of the expression
323  // Expr boolVarExpr() const;
324  //! Rebuild Expr with a new ExprManager
325  Expr rebuild(ExprManager* em) const;
326 // Expr newForall(const Expr& e);
327 // Expr newExists(const Expr& e);
328  Expr substExpr(const std::vector<Expr>& oldTerms,
329  const std::vector<Expr>& newTerms) const;
330  Expr substExpr(const ExprHashMap<Expr>& oldToNew) const;
331 
332 // by yeting, a special subst function for TheoryQuant
333  Expr substExprQuant(const std::vector<Expr>& oldTerms,
334  const std::vector<Expr>& newTerms) const;
335  Expr substExprQuant(const ExprHashMap<Expr>& oldToNew) const;
336 
337  Expr operator!() const { return notExpr(); }
338  Expr operator&&(const Expr& right) const { return andExpr(right); }
339  Expr operator||(const Expr& right) const { return orExpr(right); }
340 
341  /////////////////////////////////////////////////////////////////////////////
342  // Public Static Methods //
343  /////////////////////////////////////////////////////////////////////////////
344 
345  static size_t hash(const Expr& e);
346 
347  /////////////////////////////////////////////////////////////////////////////
348  // Read-only (const) methods //
349  /////////////////////////////////////////////////////////////////////////////
350 
351  size_t hash() const;
352 
353  // Core expression testers
354 
355  bool isFalse() const { return getKind() == FALSE_EXPR; }
356  bool isTrue() const { return getKind() == TRUE_EXPR; }
357  bool isBoolConst() const { return isFalse() || isTrue(); }
358  bool isVar() const;
359  bool isBoundVar() const { return getKind() == BOUND_VAR; }
360  bool isString() const;
361  bool isClosure() const;
362  bool isQuantifier() const;
363  bool isLambda() const;
364  bool isApply() const;
365  bool isSymbol() const;
366  bool isTheorem() const;
367 
368  bool isConstant() const { return getOpKind() <= MAX_CONST; }
369 
370  bool isRawList() const {return getKind() == RAW_LIST;}
371 
372  //! Expr represents a type
373  bool isType() const;
374  /*
375  bool isRecord() const;
376  bool isRecordAccess() const;
377  bool isTupleAccess() const;
378  */
379  //! Provide access to ExprValue for client subclasses of ExprValue *only*
380  /*@ Calling getExprValue on an Expr with a built-in ExprValue class will
381  * cause an error */
382  const ExprValue* getExprValue() const;
383 
384  //! Test if e is a term (as opposed to a predicate/formula)
385  bool isTerm() const;
386  //! Test if e is atomic
387  /*! An atomic expression is TRUE or FALSE or one that does not
388  * contain a formula (including not being a formula itself).
389  * \sa isAtomicFormula */
390  bool isAtomic() const;
391  //! Test if e is an atomic formula
392  /*! An atomic formula is TRUE or FALSE or an application of a predicate
393  (possibly 0-ary) which does not properly contain any formula. For
394  instance, the formula "x = IF f THEN y ELSE z ENDIF" is not an atomic
395  formula, since it contains the condition "f", which is a formula. */
396  bool isAtomicFormula() const;
397  //! An abstract atomic formua is an atomic formula or a quantified formula
398  bool isAbsAtomicFormula() const
399  { return isQuantifier() || isAtomicFormula(); }
400  //! Test if e is a literal
401  /*! A literal is an atomic formula, or its negation.
402  \sa isAtomicFormula */
403  bool isLiteral() const
404  { return (isAtomicFormula() || (isNot() && (*this)[0].isAtomicFormula())); }
405  //! Test if e is an abstract literal
406  bool isAbsLiteral() const
407  { return (isAbsAtomicFormula() || (isNot() && (*this)[0].isAbsAtomicFormula())); }
408  //! A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool)
409  bool isBoolConnective() const;
410  //! True iff expr is not a Bool connective
411  bool isPropAtom() const { return !isTerm() && !isBoolConnective(); }
412  //! PropAtom or negation of PropAtom
413  bool isPropLiteral() const
414  { return (isNot() && (*this)[0].isPropAtom()) || isPropAtom(); }
415  //! Return whether Expr contains a non-bool type ITE as a sub-term
416  bool containsTermITE() const;
417 
418 
419  bool isEq() const { return getKind() == EQ; }
420  bool isNot() const { return getKind() == NOT; }
421  bool isAnd() const { return getKind() == AND; }
422  bool isOr() const { return getKind() == OR; }
423  bool isITE() const { return getKind() == ITE; }
424  bool isIff() const { return getKind() == IFF; }
425  bool isImpl() const { return getKind() == IMPLIES; }
426  bool isXor() const { return getKind() == XOR;}
427 
428  bool isForall() const { return getKind() == FORALL; }
429  bool isExists() const { return getKind() == EXISTS; }
430 
431  bool isRational() const { return getKind() == RATIONAL_EXPR; }
432  bool isSkolem() const { return getKind() == SKOLEM_VAR;}
433 
434  // Leaf accessors - these functions must only be called one expressions of
435  // the appropriate kind.
436 
437  // For UCONST and BOUND_VAR Expr's
438  const std::string& getName() const;
439  //! For BOUND_VAR, get the UID
440  const std::string& getUid() const;
441 
442  // For STRING_EXPR's
443  const std::string& getString() const;
444  //! Get bound variables from a closure Expr
445  const std::vector<Expr>& getVars() const;
446  //! Get the existential axiom expression for skolem constant
447  const Expr& getExistential() const;
448  //! Get the index of the bound var that skolem constant comes from
449  int getBoundIndex() const;
450 
451  //! Get the body of the closure Expr
452  const Expr& getBody() const;
453 
454  //! Set the triggers for a closure Expr
455  void setTriggers(const std::vector<std::vector<Expr> >& triggers) const;
456  void setTriggers(const std::vector<Expr>& triggers) const;
457  void setTrigger(const Expr& trigger) const;
458  void setMultiTrigger(const std::vector<Expr>& multiTrigger) const;
459 
460  //! Get the manual triggers of the closure Expr
461  const std::vector<std::vector<Expr> >& getTriggers() const; //by yeting
462 
463  //! Get the Rational value out of RATIONAL_EXPR
464  const Rational& getRational() const;
465  //! Get theorem from THEOREM_EXPR
466  const Theorem& getTheorem() const;
467 
468  // Get the expression manager. The expression must be non-null.
469  ExprManager *getEM() const;
470 
471  // Return a ref to the vector of children.
472  const std::vector<Expr>& getKids() const;
473 
474  // Get the kind of this expr.
475  int getKind() const;
476 
477  // Get the index field
478  ExprIndex getIndex() const;
479 
480  // True if this is the most recently created expression
481  bool hasLastIndex() const;
482 
483  //! Make the expr into an operator
484  Op mkOp() const;
485 
486  //! Get operator from expression
487  Op getOp() const;
488 
489  //! Get expression of operator (for APPLY Exprs only)
490  Expr getOpExpr() const;
491 
492  //! Get kind of operator (for APPLY Exprs only)
493  int getOpKind() const;
494 
495  // Return the number of children. Note, that an application of a
496  // user-defined function has the arity of that function (the number
497  // of arguments), and the function name itself is part of the
498  // operator.
499  int arity() const;
500 
501  // Return the ith child. As with arity, it's also the ith argument
502  // in function application.
503  const Expr& operator[](int i) const;
504 
505  //! Remove leading NOT if any
506  const Expr& unnegate() const { return isNot() ? (*this)[0] : *this; }
507 
508  //! Begin iterator
509  iterator begin() const;
510 
511  //! End iterator
512  iterator end() const;
513 
514  // Check if Expr is Null
515  bool isNull() const;
516 
517  // Check if Expr is not Null
518  bool isInitialized() const { return d_expr != NULL; }
519  //! Get the memory manager index (it uniquely identifies the subclass)
520  size_t getMMIndex() const;
521 
522  // Attributes
523 
524  // True if the find attribute has been set to something other than NULL.
525  bool hasFind() const;
526 
527  // Return the attached find attribute for the expr. Note that this
528  // must be called repeatedly to get the root of the union-find tree.
529  // Should only be called if hasFind is true.
530  const Theorem& getFind() const;
531  int getFindLevel() const;
532  const Theorem& getEqNext() const;
533 
534  // Return the notify list
535  NotifyList* getNotify() const;
536 
537  //! Get the type. Recursively compute if necessary
538  Type getType() const;
539  //! Look up the current type. Do not recursively compute (i.e. may be NULL)
540  Type lookupType() const;
541  //! Return cardinality of type
542  Cardinality typeCard() const;
543  //! Return nth (starting with 0) element in a finite type
544  /*! Returns NULL Expr if unable to compute nth element
545  */
546  Expr typeEnumerateFinite(Unsigned n) const;
547  //! Return size of a finite type; returns 0 if size cannot be determined
548  Unsigned typeSizeFinite() const;
549 
550  /*! @brief Return true if there is a valid cached value for calling
551  simplify on this Expr. */
552  bool validSimpCache() const;
553 
554  // Get the cached Simplify of this Expr.
555  const Theorem& getSimpCache() const;
556 
557  // Return true if valid type flag is set for Expr
558  bool isValidType() const;
559 
560  // Return true if there is a valid flag for whether Expr is atomic
561  bool validIsAtomicFlag() const;
562 
563  // Return true if there is a valid flag for whether terminals are const
564  bool validTerminalsConstFlag() const;
565 
566  // Get the isAtomic flag
567  bool getIsAtomicFlag() const;
568 
569  // Get the TerminalsConst flag
570  bool getTerminalsConstFlag() const;
571 
572  // Get the RewriteNormal flag
573  bool isRewriteNormal() const;
574 
575  // Get the isFinite flag
576  bool isFinite() const;
577 
578  // Get the WellFounded flag
579  bool isWellFounded() const;
580 
581  // Get the ComputeTransClosure flag
582  bool computeTransClosure() const;
583 
584  // Get the ContainsBoundVar flag
585  bool containsBoundVar() const;
586 
587  // Get the usesCC flag
588  bool usesCC() const;
589 
590  // Get the notArrayNormalized flag
591  bool notArrayNormalized() const;
592 
593  // Get the ImpliedLiteral flag
594  bool isImpliedLiteral() const;
595 
596  // Get the UserAssumption flag
597  bool isUserAssumption() const;
598 
599  // Get the inUserAssumption flag
600  bool inUserAssumption() const;
601 
602  // Get the IntAssumption flag
603  bool isIntAssumption() const;
604 
605  // Get the Justified flag
606  bool isJustified() const;
607 
608  // Get the Translated flag
609  bool isTranslated() const;
610 
611  // Get the UserRegisteredAtom flag
612  bool isUserRegisteredAtom() const;
613 
614  // Get the RegisteredAtom flag
615  bool isRegisteredAtom() const;
616 
617  // Get the Selected flag
618  bool isSelected() const;
619 
620  // Get the Stored Predicate flag
621  bool isStoredPredicate() const;
622 
623  //! Check if the generic flag is set
624  bool getFlag() const;
625  //! Set the generic flag
626  void setFlag() const;
627  //! Clear the generic flag in all Exprs
628  void clearFlags() const;
629 
630  // Printing functions
631 
632  //! Print the expression to a string
633  std::string toString() const;
634  //! Print the expression to a string using the given output language
635  std::string toString(InputLanguage lang) const;
636  //! Print the expression in the specified format
637  void print(InputLanguage lang, bool dagify = true) const;
638 
639  //! Print the expression as AST (lisp-like format)
640  void print() const { print(AST_LANG); }
641  //! Print the expression as AST without dagifying
642  void printnodag() const;
643 
644  //! Pretty-print the expression
645  void pprint() const;
646  //! Pretty-print without dagifying
647  void pprintnodag() const;
648 
649  //! Print a leaf node
650  /*@ The top node is pretty-printed if it is a basic leaf type;
651  * otherwise, just the kind is printed. Should only be called on expressions
652  * with no children. */
653  ExprStream& print(ExprStream& os) const;
654  //! Print the top node and then recurse through the children */
655  /*@ The top node is printed as an AST with all the information, including
656  * "hidden" Exprs that are part of the ExprValue */
657  ExprStream& printAST(ExprStream& os) const;
658  //! Set initial indentation to n.
659  /*! The indentation will be reset to default unless the second
660  argument is true.
661  \return reference to itself, so one can write `os << e.indent(5)'
662  */
663  Expr& indent(int n, bool permanent = false);
664 
665  /////////////////////////////////////////////////////////////////////////////
666  // Other Public methods //
667  /////////////////////////////////////////////////////////////////////////////
668 
669  // Attributes
670 
671  //! Set the find attribute to e
672  void setFind(const Theorem& e) const;
673 
674  //! Set the eqNext attribute to e
675  void setEqNext(const Theorem& e) const;
676 
677  //! Add (e,i) to the notify list of this expression
678  void addToNotify(Theory* i, const Expr& e) const;
679 
680  //! Set the cached type
681  void setType(const Type& t) const;
682 
683  // Cache the result of a call to Simplify on this Expr
684  void setSimpCache(const Theorem& e) const;
685 
686  // Set the valid type flag for this Expr
687  void setValidType() const;
688 
689  // Set the isAtomicFlag for this Expr
690  void setIsAtomicFlag(bool value) const;
691 
692  // Set the TerminalsConst flag for this Expr
693  void setTerminalsConstFlag(bool value) const;
694 
695  // Set or clear the RewriteNormal flag
696  void setRewriteNormal() const;
697  void clearRewriteNormal() const;
698 
699  // Set the isFinite flag
700  void setFinite() const;
701 
702  // Set the WellFounded flag
703  void setWellFounded() const;
704 
705  // Set the ComputeTransClosure flag
706  void setComputeTransClosure() const;
707 
708  // Set the ContainsBoundVar flag
709  void setContainsBoundVar() const;
710 
711  // Set the UsesCC flag
712  void setUsesCC() const;
713 
714  // Set the notArrayNormalized flag
715  void setNotArrayNormalized() const;
716 
717  // Set the impliedLiteral flag for this Expr
718  void setImpliedLiteral() const;
719 
720  // Set the user assumption flag for this Expr
721  void setUserAssumption(int scope = -1) const;
722 
723  // Set the in user assumption flag for this Expr
724  void setInUserAssumption(int scope = -1) const;
725 
726  // Set the internal assumption flag for this Expr
727  void setIntAssumption() const;
728 
729  // Set the justified flag for this Expr
730  void setJustified() const;
731 
732  //! Set the translated flag for this Expr
733  void setTranslated(int scope = -1) const;
734 
735  //! Set the UserRegisteredAtom flag for this Expr
736  void setUserRegisteredAtom() const;
737 
738  //! Set the RegisteredAtom flag for this Expr
739  void setRegisteredAtom() const;
740 
741  //! Set the Selected flag for this Expr
742  void setSelected() const;
743 
744  //! Set the Stored Predicate flag for this Expr
745  void setStoredPredicate() const;
746 
747  //! Check if the current Expr (*this) is a subexpression of e
748  bool subExprOf(const Expr& e) const;
749  // Returns the maximum number of Boolean expressions on a path from
750  // this to a leaf, including this.
751 
752  inline Unsigned getSize() const;
753 
754 // inline int getHeight() const;
755 
756 // // Returns the index of the highest kid.
757 // inline int getHighestKid() const;
758 
759 // // Gets/sets an expression that this expression was simplified from
760 // // (see newRWTheorem). This is the equivalent of SVC's Sigx.
761 // inline bool hasSimpFrom() const;
762 // inline const Expr& getSimpFrom() const;
763 // inline void setSimpFrom(const Expr& simpFrom);
764 
765  // Attributes for uninterpreted function symbols.
766  bool hasSig() const;
767  bool hasRep() const;
768  const Theorem& getSig() const;
769  const Theorem& getRep() const;
770  void setSig(const Theorem& e) const;
771  void setRep(const Theorem& e) const;
772 
773  /////////////////////////////////////////////////////////////////////////////
774  // Friend methods //
775  /////////////////////////////////////////////////////////////////////////////
776 
777  friend CVC_DLL std::ostream& operator<<(std::ostream& os, const Expr& e);
778 
779  // The master method which defines some fixed total ordering on all
780  // Exprs. If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1
781  // respectively. A Null expr is always "smaller" than any other
782  // expr, but is equal to itself.
783  friend int compare(const Expr& e1, const Expr& e2);
784 
785  friend bool operator==(const Expr& e1, const Expr& e2);
786  friend bool operator!=(const Expr& e1, const Expr& e2);
787 
788  friend bool operator<(const Expr& e1, const Expr& e2);
789  friend bool operator<=(const Expr& e1, const Expr& e2);
790  friend bool operator>(const Expr& e1, const Expr& e2);
791  friend bool operator>=(const Expr& e1, const Expr& e2);
792 
793  /*!@}*/ // end of group Expr
794 
795 }; // end of class Expr
796 
797 } // end of namespace CVC3
798 
799 // Include expr_value.h here. We cannot include it earlier, since it
800 // needs the definition of class Expr. See comments in expr_value.h.
801 #ifndef DOXYGEN
802 #include "expr_op.h"
803 #include "expr_manager.h"
804 #endif
805 namespace CVC3 {
806 
807 inline Expr::Expr(ExprValue* expr) : d_expr(expr) { d_expr->incRefcount(); }
808 
809 inline Expr::Expr(const Expr& e) : d_expr(e.d_expr) {
810  if (d_expr != NULL) d_expr->incRefcount();
811 }
812 
813 inline Expr& Expr::operator=(const Expr& e) {
814  if(&e == this) return *this; // Self-assignment
815  ExprValue* tmp = e.d_expr;
816  if(tmp == d_expr) return *this;
817  if (tmp == NULL) {
818  d_expr->decRefcount();
819  }
820  else {
821  tmp->incRefcount();
822  if(d_expr != NULL) {
823  d_expr->decRefcount();
824  }
825  }
826  d_expr = tmp;
827  return *this;
828 }
829 
830 inline Expr::Expr(const Op& op, const Expr& child) {
831  ExprManager* em = child.getEM();
832  if (op.getKind() != APPLY) {
833  ExprNode ev(em, op.getKind());
834  std::vector<Expr>& kids = ev.getKids1();
835  kids.push_back(child);
836  d_expr = em->newExprValue(&ev);
837  } else {
838  ExprApply ev(em, op);
839  std::vector<Expr>& kids = ev.getKids1();
840  kids.push_back(child);
841  d_expr = em->newExprValue(&ev);
842  }
843  d_expr->incRefcount();
844 }
845 
846 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1) {
847  ExprManager* em = child0.getEM();
848  if (op.getKind() != APPLY) {
849  ExprNode ev(em, op.getKind());
850  std::vector<Expr>& kids = ev.getKids1();
851  kids.push_back(child0);
852  kids.push_back(child1);
853  d_expr = em->newExprValue(&ev);
854  } else {
855  ExprApply ev(em, op);
856  std::vector<Expr>& kids = ev.getKids1();
857  kids.push_back(child0);
858  kids.push_back(child1);
859  d_expr = em->newExprValue(&ev);
860  }
861  d_expr->incRefcount();
862 }
863 
864 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
865  const Expr& child2) {
866  ExprManager* em = child0.getEM();
867  if (op.getKind() != APPLY) {
868  ExprNode ev(em, op.getKind());
869  std::vector<Expr>& kids = ev.getKids1();
870  kids.push_back(child0);
871  kids.push_back(child1);
872  kids.push_back(child2);
873  d_expr = em->newExprValue(&ev);
874  } else {
875  ExprApply ev(em, op);
876  std::vector<Expr>& kids = ev.getKids1();
877  kids.push_back(child0);
878  kids.push_back(child1);
879  kids.push_back(child2);
880  d_expr = em->newExprValue(&ev);
881  }
882  d_expr->incRefcount();
883 }
884 
885 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
886  const Expr& child2, const Expr& child3) {
887  ExprManager* em = child0.getEM();
888  if (op.getKind() != APPLY) {
889  ExprNode ev(em, op.getKind());
890  std::vector<Expr>& kids = ev.getKids1();
891  kids.push_back(child0);
892  kids.push_back(child1);
893  kids.push_back(child2);
894  kids.push_back(child3);
895  d_expr = em->newExprValue(&ev);
896  } else {
897  ExprApply ev(em, op);
898  std::vector<Expr>& kids = ev.getKids1();
899  kids.push_back(child0);
900  kids.push_back(child1);
901  kids.push_back(child2);
902  kids.push_back(child3);
903  d_expr = em->newExprValue(&ev);
904  }
905  d_expr->incRefcount();
906 }
907 
908 inline Expr::Expr(const Op& op, const std::vector<Expr>& children,
909  ExprManager* em) {
910  if (em == NULL) {
911  if (op.getKind() == APPLY) em = op.getExpr().getEM();
912  else {
913  DebugAssert(children.size() > 0,
914  "Expr::Expr(Op, children): op's EM is NULL and "
915  "no children given");
916  em = children[0].getEM();
917  }
918  }
919  if (op.getKind() != APPLY) {
920  ExprNodeTmp ev(em, op.getKind(), children);
921  d_expr = em->newExprValue(&ev);
922  } else {
923  ExprApplyTmp ev(em, op, children);
924  d_expr = em->newExprValue(&ev);
925  }
926  d_expr->incRefcount();
927 }
928 
929 inline Expr Expr::eqExpr(const Expr& right) const {
930  return Expr(EQ, *this, right);
931 }
932 
933 inline Expr Expr::notExpr() const {
934  return Expr(NOT, *this);
935 }
936 
937 inline Expr Expr::negate() const {
938  return isNot() ? (*this)[0] : this->notExpr();
939 }
940 
941 inline Expr Expr::andExpr(const Expr& right) const {
942  return Expr(AND, *this, right);
943 }
944 
945 inline Expr andExpr(const std::vector <Expr>& children) {
946  DebugAssert(children.size()>0 && !children[0].isNull(),
947  "Expr::andExpr(kids)");
948  return Expr(AND, children);
949 }
950 
951 inline Expr Expr::orExpr(const Expr& right) const {
952  return Expr(OR, *this, right);
953 }
954 
955 inline Expr orExpr(const std::vector <Expr>& children) {
956  DebugAssert(children.size()>0 && !children[0].isNull(),
957  "Expr::andExpr(kids)");
958  return Expr(OR, children);
959 }
960 
961 inline Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
962  return Expr(ITE, *this, thenpart, elsepart);
963 }
964 
965 inline Expr Expr::iffExpr(const Expr& right) const {
966  return Expr(IFF, *this, right);
967 }
968 
969 inline Expr Expr::impExpr(const Expr& right) const {
970  return Expr(IMPLIES, *this, right);
971 }
972 
973 inline Expr Expr::xorExpr(const Expr& right) const {
974  return Expr(XOR, *this, right);
975 }
976 
977 inline Expr Expr::skolemExpr(int i) const {
978  return getEM()->newSkolemExpr(*this, i);
979 }
980 
981 inline Expr Expr::rebuild(ExprManager* em) const {
982  return em->rebuild(*this);
983 }
984 
985 inline Expr::~Expr() {
986  if(d_expr != NULL) {
987  IF_DEBUG(FatalAssert(d_expr->d_refcount > 0, "Mis-handled the ref. counting");)
988  if (--(d_expr->d_refcount) == 0) d_expr->d_em->gc(d_expr);
989  }
990 }
991 
992 inline size_t Expr::hash(const Expr& e) { return e.getEM()->hash(e); }
993 
994 /////////////////////////////////////////////////////////////////////////////
995 // Read-only (const) methods //
996 /////////////////////////////////////////////////////////////////////////////
997 
998 inline size_t Expr::hash() const { return getEM()->hash(*this); }
999 
1000 inline const ExprValue* Expr::getExprValue() const
1001  { return d_expr->getExprValue(); }
1002 
1003 // Core Expression Testers
1004 
1005 inline bool Expr::isVar() const { return d_expr->isVar(); }
1006 inline bool Expr::isString() const { return d_expr->isString(); }
1007 inline bool Expr::isClosure() const { return d_expr->isClosure(); }
1008 inline bool Expr::isQuantifier() const {
1009  return (isClosure() && (getKind() == FORALL || getKind() == EXISTS));
1010 }
1011 inline bool Expr::isLambda() const {
1012  return (isClosure() && getKind() == LAMBDA);
1013 }
1014 inline bool Expr::isApply() const
1015 { DebugAssert((getKind() != APPLY || d_expr->isApply()) &&
1016  (!d_expr->isApply() || getKind() == APPLY), "APPLY mismatch");
1017  return getKind() == APPLY; }
1018 inline bool Expr::isSymbol() const { return d_expr->isSymbol(); }
1019 inline bool Expr::isTheorem() const { return d_expr->isTheorem(); }
1020 inline bool Expr::isType() const { return getEM()->isTypeKind(getOpKind()); }
1021 inline bool Expr::isTerm() const { return !getType().isBool(); }
1022 inline bool Expr::isBoolConnective() const {
1023  if (!getType().isBool()) return false;
1024  switch (getKind()) {
1025  case NOT: case AND: case OR: case IMPLIES: case IFF: case XOR: case ITE:
1026  return true; }
1027  return false;
1028 }
1029 
1030 inline Unsigned Expr::getSize() const {
1031  if (d_expr->d_size == 0) {
1032  clearFlags();
1033  const_cast<ExprValue*>(d_expr)->d_size = d_expr->getSize();
1034  }
1035  return d_expr->d_size;
1036 }
1037 
1038  //inline int Expr::getHeight() const { return d_expr->getHeight(); }
1039  //inline int Expr::getHighestKid() const { return d_expr->getHighestKid(); }
1040 
1041  //inline bool Expr::hasSimpFrom() const
1042 // { return !d_expr->getSimpFrom().isNull(); }
1043 // inline const Expr& Expr::getSimpFrom() const
1044 // { return hasSimpFrom() ? d_expr->getSimpFrom() : *this; }
1045 // inline void Expr::setSimpFrom(const Expr& simpFrom)
1046 // { d_expr->setSimpFrom(simpFrom); }
1047 
1048 // Leaf accessors
1049 
1050 inline const std::string& Expr::getName() const {
1051  DebugAssert(!isNull(), "Expr::getName() on Null expr");
1052  return d_expr->getName();
1053 }
1054 
1055 inline const std::string& Expr::getString() const {
1057  "CVC3::Expr::getString(): not a string Expr:\n "
1058  + toString(AST_LANG));
1059  return d_expr->getString();
1060 }
1061 
1062 inline const std::vector<Expr>& Expr::getVars() const {
1064  "CVC3::Expr::getVars(): not a closure Expr:\n "
1065  + toString(AST_LANG));
1066  return d_expr->getVars();
1067 }
1068 
1069 inline const Expr& Expr::getBody() const {
1071  "CVC3::Expr::getBody(): not a closure Expr:\n "
1072  + toString(AST_LANG));
1073  return d_expr->getBody();
1074 }
1075 
1076  inline void Expr::setTriggers(const std::vector< std::vector<Expr> >& triggers) const {
1078  "CVC3::Expr::setTriggers(): not a closure Expr:\n "
1079  + toString(AST_LANG));
1080  d_expr->setTriggers(triggers);
1081 }
1082 
1083 inline void Expr::setTriggers(const std::vector<Expr>& triggers) const {
1085  "CVC3::Expr::setTriggers(): not a closure Expr:\n "
1086  + toString(AST_LANG));
1087  std::vector<std::vector<Expr> > patternvv;
1088  for(std::vector<Expr>::const_iterator i = triggers.begin(); i != triggers.end(); ++i ) {
1089  std::vector<Expr> patternv;
1090  patternv.push_back(*i);
1091  patternvv.push_back(patternv);
1092  }
1093  d_expr->setTriggers(patternvv);
1094  }
1095 
1096 inline void Expr::setTrigger(const Expr& trigger) const {
1098  "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1099  + toString(AST_LANG));
1100  std::vector<std::vector<Expr> > patternvv;
1101  std::vector<Expr> patternv;
1102  patternv.push_back(trigger);
1103  patternvv.push_back(patternv);
1104  setTriggers(patternvv);
1105 }
1106 
1107 inline void Expr::setMultiTrigger(const std::vector<Expr>& multiTrigger) const {
1109  "CVC3::Expr::setTrigger(): not a closure Expr:\n "
1110  + toString(AST_LANG));
1111  std::vector<std::vector<Expr> > patternvv;
1112  patternvv.push_back(multiTrigger);
1113  setTriggers(patternvv);
1114 }
1115 
1116  inline const std::vector<std::vector<Expr> >& Expr::getTriggers() const { //by yeting
1118  "CVC3::Expr::getTrigs(): not a closure Expr:\n "
1119  + toString(AST_LANG));
1120  return d_expr->getTriggers();
1121 }
1122 
1123 inline const Expr& Expr::getExistential() const {
1125  "CVC3::Expr::getExistential() not a skolem variable");
1126  return d_expr->getExistential();
1127 }
1128 inline int Expr::getBoundIndex() const {
1130  "CVC3::Expr::getBoundIndex() not a skolem variable");
1131  return d_expr->getBoundIndex();
1132 }
1133 
1134 
1135 inline const Rational& Expr::getRational() const {
1137  "CVC3::Expr::getRational(): not a rational Expr:\n "
1138  + toString(AST_LANG));
1139  return d_expr->getRational();
1140 }
1141 
1142 inline const Theorem& Expr::getTheorem() const {
1144  "CVC3::Expr::getTheorem(): not a Theorem Expr:\n "
1145  + toString(AST_LANG));
1146  return d_expr->getTheorem();
1147 }
1148 
1149 inline const std::string& Expr::getUid() const {
1151  "CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n "
1152  + toString(AST_LANG));
1153  return d_expr->getUid();
1154 }
1155 
1156 inline ExprManager* Expr::getEM() const {
1157  DebugAssert(d_expr != NULL,
1158  "CVC3::Expr:getEM: on Null Expr (not initialized)");
1159  return d_expr->d_em;
1160 }
1161 
1162 inline const std::vector<Expr>& Expr::getKids() const {
1163  DebugAssert(d_expr != NULL, "Expr::getKids on Null Expr");
1164  if(isNull()) return getEM()->getEmptyVector();
1165  else return d_expr->getKids();
1166 }
1167 
1168 inline int Expr::getKind() const {
1169  if(d_expr == NULL) return NULL_KIND; // FIXME: invent a better Null kind
1170  return d_expr->d_kind;
1171  }
1172 
1173 inline ExprIndex Expr::getIndex() const { return d_expr->d_index; }
1174 
1175 inline bool Expr::hasLastIndex() const
1176 { return d_expr->d_em->lastIndex() == getIndex(); }
1177 
1178 inline Op Expr::mkOp() const {
1179  DebugAssert(!isNull(), "Expr::mkOp() on Null expr");
1180  return Op(*this);
1181 }
1182 
1183 inline Op Expr::getOp() const {
1184  DebugAssert(!isNull(), "Expr::getOp() on Null expr");
1185  if (isApply()) return d_expr->getOp();
1186  DebugAssert(arity() > 0,
1187  "Expr::getOp() called on non-apply expr with no children");
1188  return Op(getKind());
1189 }
1190 
1191 inline Expr Expr::getOpExpr() const {
1192  DebugAssert(isApply(), "getOpExpr() called on non-apply");
1193  return getOp().getExpr();
1194 }
1195 
1196 inline int Expr::getOpKind() const {
1197  if (!isApply()) return getKind();
1198  return getOp().getExpr().getKind();
1199 }
1200 
1201 inline int Expr::arity() const {
1202  if(isNull()) return 0;
1203  else return d_expr->arity();
1204 }
1205 
1206 inline const Expr& Expr::operator[](int i) const {
1207  DebugAssert(i < arity(), "out of bounds access");
1208  return (d_expr->getKids())[i];
1209 }
1210 
1211 inline Expr::iterator Expr::begin() const {
1212  if (isNull() || d_expr->arity() == 0)
1213  return Expr::iterator(getEM()->getEmptyVector().begin());
1214  else return Expr::iterator(d_expr->getKids().begin());
1215 }
1216 
1217 inline Expr::iterator Expr::end() const {
1218  if (isNull() || d_expr->arity() == 0)
1219  return Expr::iterator(getEM()->getEmptyVector().end());
1220  else return Expr::iterator(d_expr->getKids().end());
1221 }
1222 
1223 inline bool Expr::isNull() const {
1224  return (d_expr == NULL) || (d_expr->d_kind == NULL_KIND);
1225 }
1226 
1227 inline size_t Expr::getMMIndex() const {
1228  DebugAssert(!isNull(), "Expr::getMMIndex()");
1229  return d_expr->getMMIndex();
1230 }
1231 
1232 inline bool Expr::hasFind() const {
1233  DebugAssert(!isNull(), "hasFind called on NULL Expr");
1234  return (d_expr->d_find && !(d_expr->d_find->get().isNull()));
1235 }
1236 
1237 inline const Theorem& Expr::getFind() const {
1238  DebugAssert(hasFind(), "Should only be called if find is valid");
1239  return d_expr->d_find->get();
1240 }
1241 
1242 inline int Expr::getFindLevel() const {
1243  DebugAssert(hasFind(), "Should only be called if find is valid");
1244  return d_expr->d_find->level();
1245 }
1246 
1247 inline const Theorem& Expr::getEqNext() const {
1248  DebugAssert(!isNull(), "getEqNext called on NULL Expr");
1249  DebugAssert(hasFind(), "Should only be called if find is valid");
1250  DebugAssert(d_expr->d_eqNext, "getEqNext: d_eqNext is NULL");
1251  return d_expr->d_eqNext->get();
1252 }
1253 
1254 inline NotifyList* Expr::getNotify() const {
1255  if(isNull()) return NULL;
1256  else return d_expr->d_notifyList;
1257 }
1258 
1259 inline Type Expr::getType() const {
1260  if (isNull()) return s_null;
1261  if (d_expr->d_type.isNull()) getEM()->computeType(*this);
1262  return d_expr->d_type;
1263 }
1264 
1265 inline Type Expr::lookupType() const {
1266  if (isNull()) return s_null;
1267  return d_expr->d_type;
1268 }
1269 
1270 inline Cardinality Expr::typeCard() const {
1271  DebugAssert(!isNull(), "typeCard called on NULL Expr");
1272  Expr e(*this);
1273  Unsigned n;
1274  return getEM()->finiteTypeInfo(e, n, false, false);
1275 }
1276 
1278  DebugAssert(!isNull(), "typeEnumerateFinite called on NULL Expr");
1279  Expr e(*this);
1280  Cardinality card = getEM()->finiteTypeInfo(e, n, true, false);
1281  if (card != CARD_FINITE) e = Expr();
1282  return e;
1283 }
1284 
1286  DebugAssert(!isNull(), "typeCard called on NULL Expr");
1287  Expr e(*this);
1288  Unsigned n;
1289  Cardinality card = getEM()->finiteTypeInfo(e, n, false, true);
1290  if (card != CARD_FINITE) n = 0;
1291  return n;
1292 }
1293 
1294 inline bool Expr::validSimpCache() const {
1295  return d_expr->d_simpCacheTag == getEM()->getSimpCacheTag();
1296 }
1297 
1298 inline const Theorem& Expr::getSimpCache() const {
1299  return d_expr->d_simpCache;
1300 }
1301 
1302 inline bool Expr::isValidType() const {
1304 }
1305 
1306 inline bool Expr::validIsAtomicFlag() const {
1308 }
1309 
1310 inline bool Expr::validTerminalsConstFlag() const {
1312 }
1313 
1314 inline bool Expr::getIsAtomicFlag() const {
1316 }
1317 
1318 inline bool Expr::getTerminalsConstFlag() const {
1320 }
1321 
1322 inline bool Expr::isRewriteNormal() const {
1324 }
1325 
1326 inline bool Expr::isFinite() const {
1328 }
1329 
1330 inline bool Expr::isWellFounded() const {
1332 }
1333 
1334 inline bool Expr::computeTransClosure() const {
1336 }
1337 
1338 inline bool Expr::containsBoundVar() const {
1340 }
1341 
1342 inline bool Expr::usesCC() const {
1343  return d_expr->d_dynamicFlags.get(USES_CC);
1344 }
1345 
1346 inline bool Expr::notArrayNormalized() const {
1348 }
1349 
1350 inline bool Expr::isImpliedLiteral() const {
1352 }
1353 
1354 inline bool Expr::isUserAssumption() const {
1356 }
1357 
1358 inline bool Expr::inUserAssumption() const {
1360 }
1361 
1362 inline bool Expr::isIntAssumption() const {
1364 }
1365 
1366 inline bool Expr::isJustified() const {
1368 }
1369 
1370 inline bool Expr::isTranslated() const {
1372 }
1373 
1374 inline bool Expr::isUserRegisteredAtom() const {
1376 }
1377 
1378 inline bool Expr::isRegisteredAtom() const {
1380 }
1381 
1382 inline bool Expr::isSelected() const {
1384 }
1385 
1386 inline bool Expr::isStoredPredicate() const {
1388 }
1389 
1390 inline bool Expr::getFlag() const {
1391  DebugAssert(!isNull(), "Expr::getFlag() on Null Expr");
1392  return (d_expr->d_flag == getEM()->getFlag());
1393 }
1394 
1395 inline void Expr::setFlag() const {
1396  DebugAssert(!isNull(), "Expr::setFlag() on Null Expr");
1397  d_expr->d_flag = getEM()->getFlag();
1398 }
1399 
1400 inline void Expr::clearFlags() const {
1401  DebugAssert(!isNull(), "Expr::clearFlags() on Null Expr");
1402  getEM()->clearFlags();
1403 }
1404 
1405 inline void Expr::setFind(const Theorem& e) const {
1406  DebugAssert(!isNull(), "Expr::setFind() on Null expr");
1407  DebugAssert(e.getLHS() == *this, "bad call to setFind");
1408  if (d_expr->d_find) d_expr->d_find->set(e);
1409  else {
1410  CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1411  d_expr->d_find = tmp;
1412  IF_DEBUG(tmp->setName("CDO[Expr.find]");)
1413  }
1414 }
1415 
1416 inline void Expr::setEqNext(const Theorem& e) const {
1417  DebugAssert(!isNull(), "Expr::setEqNext() on Null expr");
1418  DebugAssert(e.getLHS() == *this, "bad call to setEqNext");
1419  if (d_expr->d_eqNext) d_expr->d_eqNext->set(e);
1420  else {
1421  CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1422  d_expr->d_eqNext = tmp;
1423  IF_DEBUG(tmp->setName("CDO[Expr.eqNext]");)
1424  }
1425 }
1426 
1427 inline void Expr::setType(const Type& t) const {
1428  DebugAssert(!isNull(), "Expr::setType() on Null expr");
1429  d_expr->d_type = t;
1430 }
1431 
1432 inline void Expr::setSimpCache(const Theorem& e) const {
1433  DebugAssert(!isNull(), "Expr::setSimpCache() on Null expr");
1434  d_expr->d_simpCache = e;
1436 }
1437 
1438 inline void Expr::setValidType() const {
1439  DebugAssert(!isNull(), "Expr::setValidType() on Null expr");
1441 }
1442 
1443 inline void Expr::setIsAtomicFlag(bool value) const {
1444  DebugAssert(!isNull(), "Expr::setIsAtomicFlag() on Null expr");
1446  if (value) d_expr->d_dynamicFlags.set(IS_ATOMIC, 0);
1448 }
1449 
1450 inline void Expr::setTerminalsConstFlag(bool value) const {
1451  DebugAssert(!isNull(), "Expr::setTerminalsConstFlag() on Null expr");
1453  if (value) d_expr->d_dynamicFlags.set(TERMINALS_CONST, 0);
1455 }
1456 
1457 inline void Expr::setRewriteNormal() const {
1458  DebugAssert(!isNull(), "Expr::setRewriteNormal() on Null expr");
1459  TRACE("setRewriteNormal", "setRewriteNormal(", *this, ")");
1461 }
1462 
1463 inline void Expr::setFinite() const {
1464  DebugAssert(!isNull(), "Expr::setFinite() on Null expr");
1466 }
1467 
1468 inline void Expr::setWellFounded() const {
1469  DebugAssert(!isNull(), "Expr::setWellFounded() on Null expr");
1471 }
1472 
1473 inline void Expr::setComputeTransClosure() const {
1474  DebugAssert(!isNull(), "Expr::setComputeTransClosure() on Null expr");
1476 }
1477 
1478 inline void Expr::setContainsBoundVar() const {
1479  DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
1481 }
1482 
1483 inline void Expr::setUsesCC() const {
1484  DebugAssert(!isNull(), "Expr::setUsesCC() on Null expr");
1486 }
1487 
1488 inline void Expr::setNotArrayNormalized() const {
1489  DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
1491 }
1492 
1493 inline void Expr::setImpliedLiteral() const {
1494  DebugAssert(!isNull(), "Expr::setImpliedLiteral() on Null expr");
1496 }
1497 
1498 inline void Expr::setUserAssumption(int scope) const {
1499  DebugAssert(!isNull(), "Expr::setUserAssumption() on Null expr");
1501 }
1502 
1503 inline void Expr::setInUserAssumption(int scope) const {
1504  DebugAssert(!isNull(), "Expr::setInUserAssumption() on Null expr");
1506 }
1507 
1508 inline void Expr::setIntAssumption() const {
1509  DebugAssert(!isNull(), "Expr::setIntAssumption() on Null expr");
1511 }
1512 
1513 inline void Expr::setJustified() const {
1514  DebugAssert(!isNull(), "Expr::setJustified() on Null expr");
1516 }
1517 
1518 inline void Expr::setTranslated(int scope) const {
1519  DebugAssert(!isNull(), "Expr::setTranslated() on Null expr");
1521 }
1522 
1523 inline void Expr::setUserRegisteredAtom() const {
1524  DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
1526 }
1527 
1528 inline void Expr::setRegisteredAtom() const {
1529  DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
1531 }
1532 
1533 inline void Expr::setSelected() const {
1534  DebugAssert(!isNull(), "Expr::setSelected() on Null expr");
1536 }
1537 
1538 inline void Expr::setStoredPredicate() const {
1539  DebugAssert(!isNull(), "Expr::setStoredPredicate() on Null expr");
1541 }
1542 
1543 inline void Expr::clearRewriteNormal() const {
1544  DebugAssert(!isNull(), "Expr::clearRewriteNormal() on Null expr");
1546 }
1547 
1548 inline bool Expr::hasSig() const {
1549  return (!isNull()
1550  && d_expr->getSig() != NULL
1551  && !(d_expr->getSig()->get().isNull()));
1552 }
1553 
1554 inline bool Expr::hasRep() const {
1555  return (!isNull()
1556  && d_expr->getRep() != NULL
1557  && !(d_expr->getRep()->get().isNull()));
1558 }
1559 
1560 inline const Theorem& Expr::getSig() const {
1561  static Theorem nullThm;
1562  DebugAssert(!isNull(), "Expr::getSig() on Null expr");
1563  if(d_expr->getSig() != NULL)
1564  return d_expr->getSig()->get();
1565  else
1566  return nullThm;
1567 }
1568 
1569 inline const Theorem& Expr::getRep() const {
1570  static Theorem nullThm;
1571  DebugAssert(!isNull(), "Expr::getRep() on Null expr");
1572  if(d_expr->getRep() != NULL)
1573  return d_expr->getRep()->get();
1574  else
1575  return nullThm;
1576 }
1577 
1578 inline void Expr::setSig(const Theorem& e) const {
1579  DebugAssert(!isNull(), "Expr::setSig() on Null expr");
1580  CDO<Theorem>* sig = d_expr->getSig();
1581  if(sig != NULL) sig->set(e);
1582  else {
1583  CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1584  d_expr->setSig(tmp);
1585  IF_DEBUG(tmp->setName("CDO[Expr.sig] in "+toString());)
1586  }
1587 }
1588 
1589 inline void Expr::setRep(const Theorem& e) const {
1590  DebugAssert(!isNull(), "Expr::setRep() on Null expr");
1591  CDO<Theorem>* rep = d_expr->getRep();
1592  if(rep != NULL) rep->set(e);
1593  else {
1594  CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
1595  d_expr->setRep(tmp);
1596  IF_DEBUG(tmp->setName("CDO[Expr.rep] in "+toString());)
1597  }
1598 }
1599 
1600 inline bool operator==(const Expr& e1, const Expr& e2) {
1601  // Comparing pointers (equal expressions are always shared)
1602  return e1.d_expr == e2.d_expr;
1603 }
1604 
1605 inline bool operator!=(const Expr& e1, const Expr& e2)
1606  { return !(e1 == e2); }
1607 
1608 // compare() is defined in expr.cpp
1609 
1610 inline bool operator<(const Expr& e1, const Expr& e2)
1611  { return compare(e1,e2) < 0; }
1612 inline bool operator<=(const Expr& e1, const Expr& e2)
1613  { return compare(e1,e2) <= 0; }
1614 inline bool operator>(const Expr& e1, const Expr& e2)
1615  { return compare(e1,e2) > 0; }
1616 inline bool operator>=(const Expr& e1, const Expr& e2)
1617  { return compare(e1,e2) >= 0; }
1618 
1619 } // end of namespace CVC3
1620 
1621 #endif
Class Op representing the Expr's operator.
unsigned getSimpCacheTag() const
Get the simplifier's cache tag.
Definition: expr_manager.h:339
bool isBoundVar() const
Definition: expr.h:359
CDFlags d_dynamicFlags
context-dependent bit-vector for flags that are context-dependent
Definition: expr_value.h:112
Expr operator||(const Expr &right) const
Definition: expr.h:339
int arity() const
Definition: expr.h:1201
bool isIff() const
Definition: expr.h:424
bool isNull() const
Definition: expr.h:1223
void computeType(const Expr &e)
Compute the type of the Expr.
const Expr & getExpr() const
Definition: expr_op.h:84
iterator begin() const
Begin iterator.
Definition: expr.h:1211
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
bool isEq() const
Definition: expr.h:419
size_t getMMIndex() const
Get the memory manager index (it uniquely identifies the subclass)
Definition: expr.h:1227
bool getTerminalsConstFlag() const
Definition: expr.h:1318
Expr newSkolemExpr(const Expr &e, int i)
Definition: expr_manager.h:474
ExprIndex lastIndex()
Definition: expr_manager.h:269
ExprValue * d_expr
The value. This is the only data member in this class.
Definition: expr.h:197
std::vector< Expr > & getKids1()
Return reference to children.
Definition: expr_value.h:436
void setRewriteNormal() const
Definition: expr.h:1457
void setFlag() const
Set the generic flag.
Definition: expr.h:1395
Data structure of expressions in CVC3.
Definition: expr.h:133
const Theorem & getFind() const
Definition: expr.h:1237
ExprIndex d_index
Unique expression id.
Definition: expr_value.h:79
#define CVC_DLL
Definition: type.h:43
ExprManager * getEM() const
Definition: expr.h:1156
void setFinite() const
Definition: expr.h:1463
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
size_t hash() const
Definition: expr.h:998
friend bool operator>=(const Expr &e1, const Expr &e2)
Definition: expr.h:1616
virtual Op getOp() const
Get the Op from an Apply Expr.
Definition: expr_value.h:353
bool isTrue() const
Definition: expr.h:356
bool isRational() const
Definition: expr.h:431
void set(unsigned mask, int scope=-1)
Definition: cdflags.h:57
bool isLiteral() const
Test if e is a literal.
Definition: expr.h:403
iterator & operator++()
Prefix increment.
Definition: expr.h:256
Compute transitive closure (for binary uninterpreted predicates)
Definition: expr.h:161
static Expr s_null
Convenient null expr.
Definition: expr.h:191
bool notArrayNormalized() const
Definition: expr.h:1346
void setStoredPredicate() const
Set the Stored Predicate flag for this Expr.
Definition: expr.h:1538
ExprValue * newExprValue(ExprValue *ev)
Return either an existing or a new ExprValue matching ev.
bool operator<=(const Expr &e1, const Expr &e2)
Definition: expr.h:1612
bool isImpl() const
Definition: expr.h:425
const Expr * operator->() const
Dereference and member access.
Definition: expr.h:254
int compare(const Expr &e1, const Expr &e2)
Definition: expr.cpp:597
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:263
Definition: cdo.h:39
CDO< Theorem > * d_find
The find attribute (may be NULL)
Definition: expr_value.h:88
bool isInitialized() const
Definition: expr.h:518
bool isSkolem() const
Definition: expr.h:432
bool isITE() const
Definition: expr.h:423
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
void clearFlags() const
Clear the generic flag in all Exprs.
Definition: expr.h:1400
virtual const Rational & getRational() const
Definition: expr_value.h:332
void set(const T &data, int scope=-1)
Definition: cdo.h:63
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
bool isStoredPredicate() const
Definition: expr.h:1386
Definition: kinds.h:84
void setTriggers(const std::vector< std::vector< Expr > > &triggers) const
Set the triggers for a closure Expr.
Definition: expr.h:1076
Cardinality typeCard() const
Return cardinality of type.
Definition: expr.h:1270
bool isFalse() const
Definition: expr.h:355
InputLanguage
Different input languages.
Definition: lang.h:30
Proxy(const Expr &e)
Definition: expr.h:265
bool isImpliedLiteral() const
Definition: expr.h:1350
void setFind(const Theorem &e) const
Set the find attribute to e.
Definition: expr.h:1405
void setIsAtomicFlag(bool value) const
Definition: expr.h:1443
bool computeTransClosure() const
Definition: expr.h:1334
long unsigned ExprIndex
Expression index type.
Definition: expr.h:87
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
Whether expr contains a bounded variable (for quantifier instantiation)
Definition: expr.h:163
bool isPropAtom() const
True iff expr is not a Bool connective.
Definition: expr.h:411
int getFindLevel() const
Definition: expr.h:1242
Expr()
Default constructor creates the Null Expr.
Definition: expr.h:287
bool isTranslated() const
Definition: expr.h:1370
Definition: kinds.h:85
Theorem d_simpCache
For caching calls to Simplify.
Definition: expr_value.h:106
friend int compare(const Expr &e1, const Expr &e2)
Definition: expr.cpp:597
Expr operator&&(const Expr &right) const
Definition: expr.h:338
Expr operator!() const
Definition: expr.h:337
Definition: kinds.h:66
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
Definition: expr.h:1265
const Expr * d_e
Definition: expr.h:263
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
bool isBool() const
Definition: type.h:60
virtual const Theorem & getTheorem() const
Definition: expr_value.h:405
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
Definition: expr.h:398
Whether IS_ATOMIC flag is valid (initialized)
Definition: expr.h:151
void setUserAssumption(int scope=-1) const
Definition: expr.h:1498
#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
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Definition: expr.h:1021
bool inUserAssumption() const
Definition: expr.h:1358
bool isValidType() const
Definition: expr.h:1302
bool isType() const
Expr represents a type.
Definition: expr.h:1020
bool operator==(const Expr &e1, const Expr &e2)
Definition: expr.h:1600
Definition of input and output languages to CVC3.
bool hasFind() const
Definition: expr.h:1232
void setRep(const Theorem &e) const
Definition: expr.h:1589
void setSig(const Theorem &e) const
Definition: expr.h:1578
bool operator>(const Expr &e1, const Expr &e2)
Definition: expr.h:1614
const Expr & getExistential() const
Get the existential axiom expression for skolem constant.
Definition: expr.h:1123
friend bool operator<=(const Expr &e1, const Expr &e2)
Definition: expr.h:1612
const std::vector< std::vector< Expr > > & getTriggers() const
Get the manual triggers of the closure Expr.
Definition: expr.h:1116
bool isOr() const
Definition: expr.h:422
bool get(unsigned mask) const
Definition: cdflags.h:59
friend bool operator!=(const Expr &e1, const Expr &e2)
Definition: expr.h:1605
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
void setUsesCC() const
Definition: expr.h:1483
Expr andExpr(const Expr &right) const
Definition: expr.h:941
Whether is valid TYPE expr.
Definition: expr.h:149
virtual unsigned arity() const
Default arity = 0.
Definition: expr_value.h:299
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
virtual CDO< Theorem > * getRep() const
Definition: expr_value.h:307
bool validIsAtomicFlag() const
Definition: expr.h:1306
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
void setValidType() const
Definition: expr.h:1438
Expr impExpr(const Expr &right) const
Definition: expr.h:969
void setTrigger(const Expr &trigger) const
Definition: expr.h:1096
Context Dependent Vector of Flags.
bool isWellFounded() const
Definition: expr.h:1330
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
bool isNot() const
Definition: expr.h:420
bool isClosure() const
Definition: expr.h:1007
bool isExists() const
Definition: expr.h:429
bool isRawList() const
Definition: expr.h:370
virtual bool isVar() const
Uninterpreted constants.
Definition: expr_value.h:282
ExprValueType
Type ID of each ExprValue subclass.
Definition: expr.h:65
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
bool isXor() const
Definition: expr.h:426
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
Definition: expr_value.h:339
virtual const std::vector< std::vector< Expr > > & getTriggers() const
Definition: expr_value.h:374
Definition: kinds.h:44
Expr operator*(const Expr &left, const Expr &right)
Definition: theory_arith.h:236
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
Unsigned typeSizeFinite() const
Return size of a finite type; returns 0 if size cannot be determined.
Definition: expr.h:1285
Application of functions and predicates.
Definition: expr.h:68
bool isBoolConnective() const
A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool)
Definition: expr.h:1022
bool isString() const
Definition: expr.h:1006
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
const std::vector< Expr > & getEmptyVector()
References to empty objects (used in ExprValue)
Definition: expr_manager.h:282
const Expr & operator*() const
Dereference operator.
Definition: expr.h:252
Expr rebuild(ExprManager *em) const
Create a Boolean variable out of the expression.
Definition: expr.h:981
bool isSelected() const
Definition: expr.h:1382
const Theorem & getTheorem() const
Get theorem from THEOREM_EXPR.
Definition: expr.h:1142
virtual const std::vector< Expr > & getKids() const
Get kids: by default, returns a ref to an empty vector.
Definition: expr_value.h:293
Expr skolemExpr(int i) const
Create a Skolem constant for the i'th variable of an existential (*this)
Definition: expr.h:977
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
const Theorem & getSig() const
Definition: expr.h:1560
bool hasLastIndex() const
Definition: expr.h:1175
void setImpliedLiteral() const
Definition: expr.h:1493
bool validSimpCache() const
Return true if there is a valid cached value for calling simplify on this Expr.
Definition: expr.h:1294
bool getIsAtomicFlag() const
Definition: expr.h:1314
Whether TERMINALS_CONST flag is valid (initialized)
Definition: expr.h:167
Expr typeEnumerateFinite(Unsigned n) const
Return nth (starting with 0) element in a finite type.
Definition: expr.h:1277
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
const Theorem & getEqNext() const
Definition: expr.h:1247
Abstraction over different operating systems.
const Theorem & getSimpCache() const
Definition: expr.h:1298
const Theorem & getRep() const
Definition: expr.h:1569
virtual bool isClosure() const
A LAMBDA-expression or a quantifier.
Definition: expr_value.h:288
Proxy operator++(int)
Postfix increment.
Definition: expr.h:275
bool isTypeKind(int kind)
Check if a kind represents a type.
Definition: expr_manager.h:394
Expr negate() const
Definition: expr.h:937
Definition: kinds.h:68
bool isBoolConst() const
Definition: expr.h:357
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
size_t hash(const ExprValue *ev) const
Definition: expr_manager.h:449
const Expr & unnegate() const
Remove leading NOT if any.
Definition: expr.h:506
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
void clearRewriteNormal() const
Definition: expr.h:1543
virtual CDO< Theorem > * getSig() const
Special attributes for uninterpreted functions.
Definition: expr_value.h:302
bool isNull() const
Definition: type.h:59
void incRefcount()
Increment reference counter.
Definition: expr_value.h:142
virtual bool isApply() const
Application of another expression.
Definition: expr_value.h:284
Whether the expression is an atomic term or formula.
Definition: expr.h:153
void setRegisteredAtom() const
Set the RegisteredAtom flag for this Expr.
Definition: expr.h:1528
Expression manager API.
int getKind() const
Definition: expr_op.h:82
~Expr()
Destructor.
Definition: expr.h:985
bool operator==(const iterator &i) const
Equality.
Definition: expr.h:246
#define IF_DEBUG(code)
Definition: debug.h:406
Expr & operator=(const Expr &e)
Assignment operator: take care of the refcounting and GC.
Definition: expr.h:813
void clearFlags()
Clears the generic Expr flag in all Exprs.
Definition: expr_manager.h:272
Expression Manager.
Definition: expr_manager.h:58
Expr notExpr() const
Definition: expr.h:933
Definition: kinds.h:71
bool operator<(const Expr &e1, const Expr &e2)
Definition: expr.h:1610
bool usesCC() const
Definition: expr.h:1342
Unsigned getSize() const
Return DAG-size of Expr.
Definition: expr_value.h:162
friend class Op
Definition: expr.h:136
void setSimpCache(const Theorem &e) const
Definition: expr.h:1432
void setInUserAssumption(int scope=-1) const
Definition: expr.h:1503
void setUserRegisteredAtom() const
Set the UserRegisteredAtom flag for this Expr.
Definition: expr.h:1523
bool isForall() const
Definition: expr.h:428
bool isApply() const
Definition: expr.h:1014
NotifyList * getNotify() const
Definition: expr.h:1254
bool getFlag() const
Check if the generic flag is set.
Definition: expr.h:1390
bool isUserRegisteredAtom() const
Definition: expr.h:1374
Expr orExpr(const Expr &right) const
Definition: expr.h:951
Definition: kinds.h:90
bool isPropLiteral() const
PropAtom or negation of PropAtom.
Definition: expr.h:413
Definition: kinds.h:69
Expression is the result of a "normal" (idempotent) rewrite.
Definition: expr.h:155
virtual bool isString() const
String expression tester.
Definition: expr_value.h:278
const std::string & getName() const
Definition: expr.h:1050
const ExprValue * getExprValue() const
Provide access to ExprValue for client subclasses of ExprValue only
Definition: expr.h:1000
void setTranslated(int scope=-1) const
Set the translated flag for this Expr.
Definition: expr.h:1518
Context * getCurrentContext() const
Get the current context from our ContextManager.
Definition: expr_manager.h:324
void decRefcount()
Decrement reference counter.
Definition: expr_value.h:145
int getBoundIndex() const
Get the index of the bound var that skolem constant comes from.
Definition: expr.h:1128
Well-founded (used in datatypes)
Definition: expr.h:159
Whether expr has been added as an implied literal.
Definition: expr.h:176
unsigned getFlag()
Return the current Expr flag counter.
Definition: expr_manager.h:213
virtual int getBoundIndex() const
Definition: expr_value.h:386
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
bool operator>=(const Expr &e1, const Expr &e2)
Definition: expr.h:1616
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
bool isRegisteredAtom() const
Definition: expr.h:1378
virtual const std::vector< Expr > & getVars() const
Definition: expr_value.h:358
bool isFinite() const
Definition: expr.h:1326
void setSelected() const
Set the Selected flag for this Expr.
Definition: expr.h:1533
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
static int right(int i)
Definition: minisat_heap.h:54
void setTerminalsConstFlag(bool value) const
Definition: expr.h:1450
unsigned d_flag
Which child has the largest height.
Definition: expr_value.h:124
void print() const
Print the expression as AST (lisp-like format)
Definition: expr.h:640
iterator(std::vector< Expr >::const_iterator it)
Construct an iterator out of the vector's iterator.
Definition: expr.h:238
bool isQuantifier() const
Definition: expr.h:1008
bool isSymbol() const
Definition: expr.h:1018
bool isVar() const
Definition: expr.h:1005
Whether expr contains only numerical constants at all possible ite terminals.
Definition: expr.h:169
bool isUserAssumption() const
Definition: expr.h:1354
bool operator!=(const Expr &e1, const Expr &e2)
Definition: expr.h:1605
bool isAbsLiteral() const
Test if e is an abstract literal.
Definition: expr.h:406
bool isIntAssumption() const
Definition: expr.h:1362
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
Expr xorExpr(const Expr &right) const
Definition: expr.h:973
bool containsBoundVar() const
Definition: expr.h:1338
void gc(ExprValue *ev)
Garbage collect the ExprValue pointer.
Whether expr uses CC algorithm that relies on not simplifying an expr that has a find.
Definition: expr.h:165
Expr rebuild(const Expr &e)
Rebuild the Expr with this ExprManager if it belongs to another ExprManager.
virtual const Expr & getExistential() const
Definition: expr_value.h:381
virtual void setSig(CDO< Theorem > *sig)
Definition: expr_value.h:312
bool isTheorem() const
Definition: expr.h:1019
Op mkOp() const
Make the expr into an operator.
Definition: expr.h:1178
const Expr & getLHS() const
Definition: theorem.cpp:240
bool isConstant() const
Definition: expr.h:368
void setEqNext(const Theorem &e) const
Set the eqNext attribute to e.
Definition: expr.h:1416
void setMultiTrigger(const std::vector< Expr > &multiTrigger) const
Definition: expr.h:1107
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
Unsigned getSize() const
Definition: expr.h:1030
bool isJustified() const
Definition: expr.h:1366
bool isRewriteNormal() const
Definition: expr.h:1322
Type d_type
The cached type of the expression (may be Null)
Definition: expr_value.h:94
Definition: kinds.h:81
void setIntAssumption() const
Definition: expr.h:1508
Definition: kinds.h:61
void setWellFounded() const
Definition: expr.h:1468
The base class for holding the actual data in expressions.
Definition: expr_value.h:69
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
bool validTerminalsConstFlag() const
Definition: expr.h:1310
ExprIndex getIndex() const
Definition: expr.h:1173
const std::string & getString() const
Definition: expr.h:1055
bool operator!=(const iterator &i) const
Disequality.
Definition: expr.h:250
Definition: expr.cpp:35
Postfix increment requires a Proxy object to hold the intermediate value for dereferencing.
Definition: expr.h:262
Definition: kinds.h:99
bool hasRep() const
Definition: expr.h:1554
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
virtual const std::string & getUid() const
Definition: expr_value.h:320
bool isLambda() const
Definition: expr.h:1011
void setNotArrayNormalized() const
Definition: expr.h:1488
Definition: kinds.h:229
friend bool operator>(const Expr &e1, const Expr &e2)
Definition: expr.h:1614
void setContainsBoundVar() const
Definition: expr.h:1478
const Expr & operator[](int i) const
Definition: expr.h:1206
void setJustified() const
Definition: expr.h:1513
std::vector< Expr >::const_iterator d_it
Definition: expr.h:234
void setComputeTransClosure() const
Definition: expr.h:1473
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
friend bool operator<(const Expr &e1, const Expr &e2)
Definition: expr.h:1610
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
iterator()
Default constructor.
Definition: expr.h:242
Definition: kinds.h:67
bool hasSig() const
Definition: expr.h:1548
void clear(unsigned mask, int scope=-1)
Definition: cdflags.h:58
Whether expr is normalized (in array theory)
Definition: expr.h:187
virtual bool isTheorem() const
Special Expr holding a theorem.
Definition: expr_value.h:290
Definition: kinds.h:70
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Get information related to finiteness of a type.
virtual const Expr & getBody() const
Definition: expr_value.h:364
Finite type.
Definition: expr.h:157
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421
const std::string & getUid() const
For BOUND_VAR, get the UID.
Definition: expr.h:1149