CVC3  2.4.1
expr_manager.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr_manager.h
4  * \brief Expression manager API
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Wed Dec 4 14:20:56 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 // Must be before #ifndef, since expr.h also includes this file (see
23 // comments in expr_value.h)
24 #ifndef _cvc3__expr_h_
25 #include "expr.h"
26 #endif
27 
28 #ifndef _cvc3__include__expr_manager_h_
29 #define _cvc3__include__expr_manager_h_
30 
31 #include "os.h"
32 #include "expr_map.h"
33 #include <deque>
34 
35 namespace CVC3 {
36  // Command line flags
37  class CLFlags;
38  class PrettyPrinter;
39  class MemoryManager;
40  class ExprManagerNotifyObj;
41  class TheoremManager;
42 
43 ///////////////////////////////////////////////////////////////////////////////
44 //! Expression Manager
45 /*!
46  Class: ExprManager
47 
48  Author: Sergey Berezin
49 
50  Created: Wed Dec 4 14:26:35 2002
51 
52  Description: Global state of the Expr package for a particular
53  instance of CVC3. Each instance of the CVC3 library has
54  its own expression manager, for thread-safety.
55 */
56 ///////////////////////////////////////////////////////////////////////////////
57 
59  friend class Expr;
60  friend class ExprValue;
61  friend class Op; // It wants to call rebuildExpr
62  friend class HashEV; // Our own private class
63  friend class Type;
64 
65  ContextManager* d_cm; //!< For backtracking attributes
66  TheoremManager* d_tm; //!< Needed for Refl Theorems
67  ExprManagerNotifyObj* d_notifyObj; //!< Notification on pop()
68  ExprIndex d_index; //!< Index counter for Expr compare()
69  unsigned d_flagCounter; //!< Counter for a generic Expr flag
70 
71  //! The database of registered kinds
73  //! The set of kinds representing a type
75  //! Private class for hashing strings
76  class HashString {
78  public:
79  size_t operator()(const std::string& s) const {
80  return h(const_cast<char*>(s.c_str()));
81  }
82  };
83  //! The reverse map of names to kinds
85  /*! @brief The registered pretty-printer, a connector to
86  theory-specific pretty-printers */
88 
89  size_t hash(const ExprValue* ev) const;
90 
91  // Printing and other options
92 
93  /*! @brief Print upto the given depth, replace the rest with
94  "...". -1==unlimited depth. */
95  const int* d_printDepth;
96  //! Whether to print with indentation
97  const bool* d_withIndentation;
98  //! Permanent indentation
99  int d_indent;
100  //! Transient indentation
101  /*! Normally is the same as d_indent, but may temporarily be
102  different for printing one single Expr */
104  //! Suggested line width for printing with indentation
105  const int* d_lineWidth;
106  //! Input language (printing)
107  const std::string* d_inputLang;
108  //! Output language (printing)
109  const std::string* d_outputLang;
110  //! Whether to print Expr's as DAGs
111  const bool* d_dagPrinting;
112  //! Which memory manager to use (copy the flag value and keep it the same)
113  const std::string d_mmFlag;
114 
115  //! Private class for d_exprSet
116  class HashEV {
118  public:
119  HashEV(ExprManager* em): d_em(em) { }
120  size_t operator()(ExprValue* ev) const { return d_em->hash(ev); }
121  };
122  //! Private class for d_exprSet
123  class EqEV {
124  public:
125  bool operator()(const ExprValue* ev1, const ExprValue* ev2) const;
126  };
127 
128  //! Hash set type for uniquifying expressions
130  //! Hash set for uniquifying expressions
131  ExprValueSet d_exprSet;
132  //! Array of memory managers for subclasses of ExprValue
133  std::vector<MemoryManager*> d_mm;
134 
135  //! A hash function for hashing pointers
137 
138  //! Expr constants cached for fast access
142  //! Empty vector of Expr to return by reference as empty vector of children
143  std::vector<Expr> d_emptyVec;
144  //! Null Expr to return by reference, for efficiency
146 
147  void installExprValue(ExprValue* ev);
148 
149  //! Current value of the simplifier cache tag
150  /*! The cached values of calls to Simplify are valid as long as
151  their cache tag matches this tag. Caches can then be
152  invalidated by incrementing this tag. */
154 
155  //! Disable garbage collection
156  /*! This flag disables the garbage collection. Normally, it's set
157  in the destructor, so that we can delete all remaining
158  expressions without GC getting in the way. */
160  //! Postpone deleting garbage-collected expressions.
161  /*! Useful during manipulation of context, especially at the time
162  * of backtracking, since we may have objects with circular
163  * dependencies (like find pointers).
164  *
165  * The postponed expressions will be deleted the next time the
166  * garbage collector is called after this flag is cleared.
167  */
169  //! Vector of postponed garbage-collected expressions
170  std::vector<ExprValue*> d_postponed;
171 
172  //! Flag for whether GC is already running
173  bool d_inGC;
174  //! Queue of pending exprs to GC
175  std::deque<ExprValue*> d_pending;
176 
177  //! Rebuild cache
179  IF_DEBUG(bool d_inRebuild;)
180 
181  public:
182  //! Abstract class for computing expr type
183  class TypeComputer {
184  public:
186  virtual ~TypeComputer() {}
187  //! Compute the type of e
188  virtual void computeType(const Expr& e) = 0;
189  //! Check that e is a valid Type expr
190  virtual void checkType(const Expr& e) = 0;
191  //! Get information related to finiteness of a type
192  virtual Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
193  bool enumerate, bool computeSize) = 0;
194  };
195  private:
196  //! Instance of TypeComputer: must be registered
198 
199  /////////////////////////////////////////////////////////////////////////
200  /*! \defgroup EM_Priv Private methods
201  * \ingroup ExprPkg
202  * @{
203  */
204  /////////////////////////////////////////////////////////////////////////
205 
206  //! Cached recursive descent. Must be called only during rebuild()
207  Expr rebuildRec(const Expr& e);
208 
209  //! Return either an existing or a new ExprValue matching ev
210  ExprValue* newExprValue(ExprValue* ev);
211 
212  //! Return the current Expr flag counter
213  unsigned getFlag() { return d_flagCounter; }
214  //! Increment and return the Expr flag counter (this clears all the flags)
215  unsigned nextFlag()
216  { FatalAssert(++d_flagCounter, "flag overflow"); return d_flagCounter; }
217 
218  //! Compute the type of the Expr
219  void computeType(const Expr& e);
220  //! Check well-formedness of a type Expr
221  void checkType(const Expr& e);
222  //! Get information related to finiteness of a type
223  // 1. Returns Cardinality of the type (finite, infinite, or unknown)
224  // 2. If cardinality = finite and enumerate is true,
225  // sets e to the nth element of the type if it can
226  // sets e to NULL if n is out of bounds or if unable to compute nth element
227  // 3. If cardinality = finite and computeSize is true,
228  // sets n to the size of the type if it can
229  // sets n to 0 otherwise
230  Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
231  bool enumerate, bool computeSize);
232 
233  public:
234  //! Constructor
235  ExprManager(ContextManager* cm, const CLFlags& flags);
236  //! Destructor
237  ~ExprManager();
238  //! Free up all memory and delete all the expressions.
239  /*!
240  * No more expressions can be created after this point, only
241  * destructors ~Expr() can be called.
242  *
243  * This method is needed to dis-entangle the mutual dependency of
244  * ExprManager and ContextManager, when destructors of ExprValue
245  * (sub)classes need to delete backtracking objects, and deleting
246  * the ContextManager requires destruction of some remaining Exprs.
247  */
248  void clear();
249  //! Check if the ExprManager is still active (clear() was not called)
250  bool isActive();
251 
252  //! Garbage collect the ExprValue pointer
253  /*! \ingroup EM_Priv */
254  void gc(ExprValue* ev);
255  //! Postpone deletion of garbage-collected expressions.
256  /*! \sa resumeGC() */
257  void postponeGC() { d_postponeGC = true; }
258  //! Resume deletion of garbage-collected expressions.
259  /*! \sa postponeGC() */
260  void resumeGC();
261 
262  /*! @brief Rebuild the Expr with this ExprManager if it belongs to
263  another ExprManager */
264  Expr rebuild(const Expr& e);
265 
266  //! Return the next Expr index
267  /*! It should be used only by ExprValue() constructor */
268  ExprIndex nextIndex() { return d_index++; }
269  ExprIndex lastIndex() { return d_index - 1; }
270 
271  //! Clears the generic Expr flag in all Exprs
272  void clearFlags() { nextFlag(); }
273 
274  // Core leaf exprs
275  //! BOOLEAN Expr
276  const Expr& boolExpr() { return d_bool; }
277  //! FALSE Expr
278  const Expr& falseExpr() { return d_false; }
279  //! TRUE Expr
280  const Expr& trueExpr() { return d_true; }
281  //! References to empty objects (used in ExprValue)
282  const std::vector<Expr>& getEmptyVector() { return d_emptyVec; }
283  //! References to empty objects (used in ExprValue)
284  const Expr& getNullExpr() { return d_nullExpr; }
285 
286  // Expr constructors
287 
288  //! Return either an existing or a new Expr matching ev
289  Expr newExpr(ExprValue* ev) { return Expr(newExprValue(ev)); }
290 
291  Expr newLeafExpr(const Op& op);
292  Expr newStringExpr(const std::string &s);
293  Expr newRatExpr(const Rational& r);
294  Expr newSkolemExpr(const Expr& e, int i);
295  Expr newVarExpr(const std::string &s);
296  Expr newSymbolExpr(const std::string &s, int kind);
297  Expr newBoundVarExpr(const std::string &name, const std::string& uid);
298  Expr newBoundVarExpr(const std::string &name, const std::string& uid,
299  const Type& type);
300  Expr newBoundVarExpr(const Type& type);
301  Expr newClosureExpr(int kind, const Expr& var, const Expr& body);
302  Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
303  const Expr& body);
304  Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
305  const Expr& body, const Expr& trigger);
306  Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
307  const Expr& body, const std::vector<Expr>& triggers);
308  Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
309  const Expr& body, const std::vector<std::vector<Expr> >& triggers);
310 
311  // Vector of children constructors (vector may be empty)
312  Expr andExpr(const std::vector <Expr>& children)
313  { return Expr(AND, children, this); }
314  Expr orExpr(const std::vector <Expr>& children)
315  { return Expr(OR, children, this); }
316 
317  // Public methods
318 
319  //! Hash function for a single Expr
320  size_t hash(const Expr& e) const;
321  //! Fetch our ContextManager
322  ContextManager* getCM() const { return d_cm; }
323  //! Get the current context from our ContextManager
324  Context* getCurrentContext() const { return d_cm->getCurrentContext(); }
325  //! Get current scope level
326  int scopelevel() { return d_cm->scopeLevel(); }
327 
328  //! Set the TheoremManager
329  void setTM(TheoremManager* tm) { d_tm = tm; }
330  //! Fetch the TheoremManager
331  TheoremManager* getTM() const { return d_tm; }
332 
333  //! Return a MemoryManager for the given ExprValue type
334  MemoryManager* getMM(size_t MMIndex) {
335  DebugAssert(MMIndex < d_mm.size(), "ExprManager::getMM()");
336  return d_mm[MMIndex];
337  }
338  //! Get the simplifier's cache tag
339  unsigned getSimpCacheTag() const { return d_simpCacheTagCurrent; }
340  //! Invalidate the simplifier's cache tag
341  void invalidateSimpCache() { d_simpCacheTagCurrent++; }
342 
343  //! Register type computer
344  void registerTypeComputer(TypeComputer* typeComputer)
345  { d_typeComputer = typeComputer; }
346 
347  //! Get printing depth
348  int printDepth() const { return *d_printDepth; }
349  //! Whether to print with indentation
350  bool withIndentation() const { return *d_withIndentation; }
351  //! Suggested line width for printing with indentation
352  int lineWidth() const { return *d_lineWidth; }
353  //! Get initial indentation
354  int indent() const { return d_indentTransient; }
355  //! Set initial indentation. Returns the previous permanent value.
356  int indent(int n, bool permanent = false);
357  //! Increment the current transient indentation by n
358  /*! If the second argument is true, sets the result as permanent.
359  \return previous permanent value. */
360  int incIndent(int n, bool permanent = false);
361  //! Set transient indentation to permanent
362  void restoreIndent() { d_indentTransient = d_indent; }
363  //! Get the input language for printing
364  InputLanguage getInputLang() const;
365  //! Get the output language for printing
366  InputLanguage getOutputLang() const;
367  //! Whether to print Expr's as DAGs
368  bool dagPrinting() const { return *d_dagPrinting; }
369  /*! @brief Return the pretty-printer if there is one; otherwise
370  return NULL. */
371  PrettyPrinter* getPrinter() const { return d_prettyPrinter; }
372 
373  /////////////////////////////////////////////////////////////////////////////
374  // Kind registration //
375  /////////////////////////////////////////////////////////////////////////////
376 
377  //! Register a new kind.
378  /*! The kind may already be registered under the same name, but if
379  * the name is different, it's an error.
380  *
381  * If the new kind is supposed to represent a type, set isType to true.
382  */
383  void newKind(int kind, const std::string &name, bool isType = false);
384  //! Register the pretty-printer (can only do it if none registered)
385  /*! The pointer is NOT owned by ExprManager. Delete it yourself.
386  */
387  void registerPrettyPrinter(PrettyPrinter& printer);
388  //! Tell ExprManager that the printer is no longer valid
389  void unregisterPrettyPrinter();
390  /*! @brief Returns true if kind is built into CVC or has been registered
391  via newKind. */
392  bool isKindRegistered(int kind) { return d_kindMap.count(kind) > 0; }
393  //! Check if a kind represents a type
394  bool isTypeKind(int kind) { return d_typeKinds.count(kind) > 0; }
395 
396  /*! @brief Return the name associated with a kind. The kind must
397  already be registered. */
398  const std::string& getKindName(int kind);
399  //! Return a kind associated with a name. Returns NULL_KIND if not found.
400  int getKind(const std::string& name);
401  //! Register a new subclass of ExprValue
402  /*!
403  * Takes the size (in bytes) of the new subclass and returns the
404  * unique index of that subclass. Subsequent calls to the
405  * subclass's getMMIndex() must return that index.
406  */
407  size_t registerSubclass(size_t sizeOfSubclass);
408 
409  //! Calculate memory usage
410  unsigned long getMemory(int verbosity);
411 
412  }; // end of class ExprManager
413 
414 
415 /*****************************************************************************/
416 /*!
417  *\class ExprManagerNotifyObj
418  *\brief Notifies ExprManager before and after each pop()
419  *
420  * Author: Sergey Berezin
421  *
422  * Created: Tue Mar 1 12:29:14 2005
423  *
424  * Disables the deletion of Exprs during context restoration
425  * (backtracking). This solves the problem of circular dependencies,
426  * e.g. in find pointers.
427  */
428 /*****************************************************************************/
431  public:
432  //! Constructor
434  : ContextNotifyObj(cxt), d_em(em) { }
435 
436  void notifyPre(void);
437  void notify(void);
438  unsigned long getMemory(int verbosity) { return sizeof(ExprManagerNotifyObj); }
439  };
440 
441 
442 } // end of namespace CVC3
443 
444 // Include expr_value here for inline definitions
445 #include "expr_value.h"
446 
447 namespace CVC3 {
448 
449 inline size_t ExprManager::hash(const ExprValue* ev) const {
450  DebugAssert(ev!=NULL, "ExprManager::hash() called on a NULL ExprValue");
451  return ev->hash();
452 }
453 
455 {
456  if (op.getKind() != APPLY) {
457  ExprValue ev(this, op.getKind());
458  return newExpr(&ev);
459  }
460  else {
461  DebugAssert(op.getExpr().getEM() == this, "ExprManager mismatch");
462  std::vector<Expr> kids;
463  ExprApply ev(this, op, kids);
464  return newExpr(&ev);
465  }
466 }
467 
468 inline Expr ExprManager::newStringExpr(const std::string &s)
469  { ExprString ev(this, s); return newExpr(&ev); }
470 
472  { ExprRational ev(this, r); return newExpr(&ev); }
473 
474 inline Expr ExprManager::newSkolemExpr(const Expr& e, int i)
475  { DebugAssert(e.getEM() == this, "ExprManager mismatch");
476  ExprSkolem ev(this, i, e); return newExpr(&ev); }
477 
478 inline Expr ExprManager::newVarExpr(const std::string &s)
479  { ExprVar ev(this, s); return newExpr(&ev); }
480 
481 inline Expr ExprManager::newSymbolExpr(const std::string &s, int kind)
482  { ExprSymbol ev(this, kind, s); return newExpr(&ev); }
483 
484 inline Expr ExprManager::newBoundVarExpr(const std::string &name,
485  const std::string& uid)
486  { ExprBoundVar ev(this, name, uid); return newExpr(&ev); }
487 
488 inline Expr ExprManager::newBoundVarExpr(const std::string& name,
489  const std::string& uid,
490  const Type& type) {
491  Expr res = newBoundVarExpr(name, uid);
492  DebugAssert(type.getExpr().getKind() != ARROW,"");
493  DebugAssert(res.lookupType().isNull(),
494  "newBoundVarExpr: redefining a variable " + name);
495  res.setType(type);
496  return res;
497 }
498 
500  static int nextNum = 0;
501  std::string name("_cvc3_");
502  std::string uid = int2string(nextNum++);
503  return newBoundVarExpr(name, uid, type);
504 }
505 
507  const Expr& var,
508  const Expr& body)
509  { ExprClosure ev(this, kind, var, body); return newExpr(&ev); }
510 
512  const std::vector<Expr>& vars,
513  const Expr& body)
514  { ExprClosure ev(this, kind, vars, body); return newExpr(&ev); }
515 
517  const std::vector<Expr>& vars,
518  const Expr& body,
519  const std::vector<Expr>& triggers)
520  { ExprClosure ev(this, kind, vars, body);
521  Expr ret = newExpr(&ev); ret.setTriggers(triggers); return ret; }
522 
524  const std::vector<Expr>& vars,
525  const Expr& body,
526  const std::vector<std::vector<Expr> >& triggers)
527  { ExprClosure ev(this, kind, vars, body);
528  Expr ret = newExpr(&ev); ret.setTriggers(triggers); return ret; }
529 
531  const std::vector<Expr>& vars,
532  const Expr& body,
533  const Expr& trigger)
534  { ExprClosure ev(this, kind, vars, body);
535  Expr ret = newExpr(&ev); ret.setTrigger(trigger); return ret; }
536 
538  const ExprValue* ev2) const {
539  return (*ev1) == (*ev2);
540 }
541 
542 inline size_t ExprManager::hash(const Expr& e) const {
543  DebugAssert(!e.isNull(), "ExprManager::hash() called on a Null Expr");
544  return e.d_expr->hash();
545 }
546 
547 } // end of namespace CVC3
548 
549 #endif
550 
unsigned getSimpCacheTag() const
Get the simplifier's cache tag.
Definition: expr_manager.h:339
bool isNull() const
Definition: expr.h:1223
const Expr & getExpr() const
Definition: expr_op.h:84
std::vector< Expr > d_emptyVec
Empty vector of Expr to return by reference as empty vector of children.
Definition: expr_manager.h:143
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::deque< ExprValue * > d_pending
Queue of pending exprs to GC.
Definition: expr_manager.h:175
size_type count(const _Key &key) const
Definition: hash_map.h:217
Data structure of expressions in CVC3.
Definition: expr.h:133
int d_indent
Permanent indentation.
Definition: expr_manager.h:99
#define CVC_DLL
Definition: type.h:43
TypeComputer * d_typeComputer
Instance of TypeComputer: must be registered.
Definition: expr_manager.h:197
ExprManager * getEM() const
Definition: expr.h:1156
HashEV(ExprManager *em)
Definition: expr_manager.h:119
PrettyPrinter * d_prettyPrinter
The registered pretty-printer, a connector to theory-specific pretty-printers.
Definition: expr_manager.h:87
Expr d_nullExpr
Null Expr to return by reference, for efficiency.
Definition: expr_manager.h:145
const Expr & getNullExpr()
References to empty objects (used in ExprValue)
Definition: expr_manager.h:284
void postponeGC()
Postpone deletion of garbage-collected expressions.
Definition: expr_manager.h:257
std::hash< char * > h
Definition: expr_manager.h:77
size_t operator()(const std::string &s) const
Definition: expr_manager.h:79
size_type count(const _Key &key) const
Definition: hash_set.h:195
unsigned d_simpCacheTagCurrent
Current value of the simplifier cache tag.
Definition: expr_manager.h:153
std::vector< ExprValue * > d_postponed
Vector of postponed garbage-collected expressions.
Definition: expr_manager.h:170
Expr newSymbolExpr(const std::string &s, int kind)
Definition: expr_manager.h:481
const Expr & boolExpr()
BOOLEAN Expr.
Definition: expr_manager.h:276
int scopelevel()
Get current scope level.
Definition: expr_manager.h:326
void setTriggers(const std::vector< std::vector< Expr > > &triggers) const
Set the triggers for a closure Expr.
Definition: expr.h:1076
Private class for d_exprSet.
Definition: expr_manager.h:123
InputLanguage
Different input languages.
Definition: lang.h:30
void setTM(TheoremManager *tm)
Set the TheoremManager.
Definition: expr_manager.h:329
ContextManager * getCM() const
Fetch our ContextManager.
Definition: expr_manager.h:322
long unsigned ExprIndex
Expression index type.
Definition: expr.h:87
bool dagPrinting() const
Whether to print Expr's as DAGs.
Definition: expr_manager.h:368
MS C++ specific settings.
Definition: type.h:42
std::hash_set< ExprValue *, HashEV, EqEV > ExprValueSet
Hash set type for uniquifying expressions.
Definition: expr_manager.h:129
Expr orExpr(const std::vector< Expr > &children)
Definition: expr_manager.h:314
const std::string * d_inputLang
Input language (printing)
Definition: expr_manager.h:107
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
Definition: expr.h:1265
Notifies ExprManager before and after each pop()
Definition: expr_manager.h:429
bool d_postponeGC
Postpone deleting garbage-collected expressions.
Definition: expr_manager.h:168
const std::string * d_outputLang
Output language (printing)
Definition: expr_manager.h:109
Definition: kinds.h:51
size_t hash() const
Caching hash function.
Definition: expr_value.h:155
#define DebugAssert(cond, str)
Definition: debug.h:408
ExprHashMap< Expr > d_rebuildCache
Rebuild cache.
Definition: expr_manager.h:178
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Definition: expr_manager.h:506
ExprIndex d_index
Index counter for Expr compare()
Definition: expr_manager.h:68
void registerTypeComputer(TypeComputer *typeComputer)
Register type computer.
Definition: expr_manager.h:344
const int * d_lineWidth
Suggested line width for printing with indentation.
Definition: expr_manager.h:105
Context * getCurrentContext()
Definition: context.h:406
const bool * d_dagPrinting
Whether to print Expr's as DAGs.
Definition: expr_manager.h:111
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Definition: expr_manager.h:484
void setTrigger(const Expr &trigger) const
Definition: expr.h:1096
ContextManager * d_cm
For backtracking attributes.
Definition: expr_manager.h:65
const Expr & getExpr() const
Definition: type.h:52
std::hash_map< std::string, int, HashString > d_kindMapByName
The reverse map of names to kinds.
Definition: expr_manager.h:84
Expr newExpr(ExprValue *ev)
Return either an existing or a new Expr matching ev.
Definition: expr_manager.h:289
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
Definition: expr_manager.h:334
Expr newStringExpr(const std::string &s)
Definition: expr_manager.h:468
unsigned long getMemory(int verbosity)
Definition: expr_manager.h:438
std::hash_set< int > d_typeKinds
The set of kinds representing a type.
Definition: expr_manager.h:74
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
TheoremManager * getTM() const
Fetch the TheoremManager.
Definition: expr_manager.h:331
Abstract class for computing expr type.
Definition: expr_manager.h:183
const int * d_printDepth
Print upto the given depth, replace the rest with "...". -1==unlimited depth.
Definition: expr_manager.h:95
const std::vector< Expr > & getEmptyVector()
References to empty objects (used in ExprValue)
Definition: expr_manager.h:282
bool withIndentation() const
Whether to print with indentation.
Definition: expr_manager.h:350
Abstraction over different operating systems.
const Expr & falseExpr()
FALSE Expr.
Definition: expr_manager.h:278
bool isTypeKind(int kind)
Check if a kind represents a type.
Definition: expr_manager.h:394
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
Definition: kinds.h:68
int getKind() const
Definition: expr.h:1168
size_t hash(const ExprValue *ev) const
Definition: expr_manager.h:449
PrettyPrinter * getPrinter() const
Return the pretty-printer if there is one; otherwise return NULL.
Definition: expr_manager.h:371
std::string int2string(int n)
Definition: cvc_util.h:46
bool d_inGC
Flag for whether GC is already running.
Definition: expr_manager.h:173
bool isNull() const
Definition: type.h:59
int getKind() const
Definition: expr_op.h:82
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
unsigned d_flagCounter
Counter for a generic Expr flag.
Definition: expr_manager.h:69
#define IF_DEBUG(code)
Definition: debug.h:406
TheoremManager * d_tm
Needed for Refl Theorems.
Definition: expr_manager.h:66
void clearFlags()
Clears the generic Expr flag in all Exprs.
Definition: expr_manager.h:272
Expression Manager.
Definition: expr_manager.h:58
std::hash< void * > d_pointerHash
A hash function for hashing pointers.
Definition: expr_manager.h:136
size_t operator()(ExprValue *ev) const
Definition: expr_manager.h:120
Expr newRatExpr(const Rational &r)
Definition: expr_manager.h:471
void restoreIndent()
Set transient indentation to permanent.
Definition: expr_manager.h:362
Private class for d_exprSet.
Definition: expr_manager.h:116
Definition: kinds.h:90
Context * getCurrentContext() const
Get the current context from our ContextManager.
Definition: expr_manager.h:324
int indent() const
Get initial indentation.
Definition: expr_manager.h:354
std::hash_map< int, std::string > d_kindMap
The database of registered kinds.
Definition: expr_manager.h:72
unsigned getFlag()
Return the current Expr flag counter.
Definition: expr_manager.h:213
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...
Definition: expr_value.h:901
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
int printDepth() const
Get printing depth.
Definition: expr_manager.h:348
Expr andExpr(const std::vector< Expr > &children)
Definition: expr_manager.h:312
bool isKindRegistered(int kind)
Returns true if kind is built into CVC or has been registered via newKind.
Definition: expr_manager.h:392
Expr d_bool
Expr constants cached for fast access.
Definition: expr_manager.h:139
ExprManagerNotifyObj * d_notifyObj
Notification on pop()
Definition: expr_manager.h:67
const std::string d_mmFlag
Which memory manager to use (copy the flag value and keep it the same)
Definition: expr_manager.h:113
bool d_disableGC
Disable garbage collection.
Definition: expr_manager.h:159
Definition of the API to expression package. See class Expr for details.
Private class for hashing strings.
Definition: expr_manager.h:76
ExprIndex nextIndex()
Return the next Expr index.
Definition: expr_manager.h:268
Expr newVarExpr(const std::string &s)
Definition: expr_manager.h:478
const bool * d_withIndentation
Whether to print with indentation.
Definition: expr_manager.h:97
ExprManagerNotifyObj(ExprManager *em, Context *cxt)
Constructor.
Definition: expr_manager.h:433
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
Definition: expr_manager.h:341
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
int lineWidth() const
Suggested line width for printing with indentation.
Definition: expr_manager.h:352
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
Definition: expr.cpp:35
int d_indentTransient
Transient indentation.
Definition: expr_manager.h:103
ExprValueSet d_exprSet
Hash set for uniquifying expressions.
Definition: expr_manager.h:131
Definition: kinds.h:67
std::vector< MemoryManager * > d_mm
Array of memory managers for subclasses of ExprValue.
Definition: expr_manager.h:133
Abstract API to a pretty-printer for Expr.
unsigned nextFlag()
Increment and return the Expr flag counter (this clears all the flags)
Definition: expr_manager.h:215
bool operator()(const ExprValue *ev1, const ExprValue *ev2) const
Definition: expr_manager.h:537