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
58 class CVC_DLL ExprManager {
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
72 std::hash_map<int, std::string> d_kindMap;
73 //! The set of kinds representing a type
74 std::hash_set<int> d_typeKinds;
75 //! Private class for hashing strings
76 class HashString {
77 std::hash<char*> h;
78 public:
operator()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
84 std::hash_map<std::string, int, HashString> d_kindMapByName;
85 /*! @brief The registered pretty-printer, a connector to
86 theory-specific pretty-printers */
87 PrettyPrinter *d_prettyPrinter;
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 */
103 int d_indentTransient;
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 {
117 ExprManager* d_em;
118 public:
HashEV(ExprManager * em)119 HashEV(ExprManager* em): d_em(em) { }
operator()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
129 typedef std::hash_set<ExprValue*, HashEV, EqEV> ExprValueSet;
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
136 std::hash<void*> d_pointerHash;
137
138 //! Expr constants cached for fast access
139 Expr d_bool;
140 Expr d_false;
141 Expr d_true;
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
145 Expr d_nullExpr;
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. */
153 unsigned d_simpCacheTagCurrent;
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. */
159 bool d_disableGC;
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 */
168 bool d_postponeGC;
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
178 ExprHashMap<Expr> d_rebuildCache;
IF_DEBUG(bool d_inRebuild;)179 IF_DEBUG(bool d_inRebuild;)
180
181 public:
182 //! Abstract class for computing expr type
183 class TypeComputer {
184 public:
185 TypeComputer() {}
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
197 TypeComputer* d_typeComputer;
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
getFlag()213 unsigned getFlag() { return d_flagCounter; }
214 //! Increment and return the Expr flag counter (this clears all the flags)
nextFlag()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() */
postponeGC()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 */
nextIndex()268 ExprIndex nextIndex() { return d_index++; }
lastIndex()269 ExprIndex lastIndex() { return d_index - 1; }
270
271 //! Clears the generic Expr flag in all Exprs
clearFlags()272 void clearFlags() { nextFlag(); }
273
274 // Core leaf exprs
275 //! BOOLEAN Expr
boolExpr()276 const Expr& boolExpr() { return d_bool; }
277 //! FALSE Expr
falseExpr()278 const Expr& falseExpr() { return d_false; }
279 //! TRUE Expr
trueExpr()280 const Expr& trueExpr() { return d_true; }
281 //! References to empty objects (used in ExprValue)
getEmptyVector()282 const std::vector<Expr>& getEmptyVector() { return d_emptyVec; }
283 //! References to empty objects (used in ExprValue)
getNullExpr()284 const Expr& getNullExpr() { return d_nullExpr; }
285
286 // Expr constructors
287
288 //! Return either an existing or a new Expr matching ev
newExpr(ExprValue * 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)
andExpr(const std::vector<Expr> & children)312 Expr andExpr(const std::vector <Expr>& children)
313 { return Expr(AND, children, this); }
orExpr(const std::vector<Expr> & children)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
getCM()322 ContextManager* getCM() const { return d_cm; }
323 //! Get the current context from our ContextManager
getCurrentContext()324 Context* getCurrentContext() const { return d_cm->getCurrentContext(); }
325 //! Get current scope level
scopelevel()326 int scopelevel() { return d_cm->scopeLevel(); }
327
328 //! Set the TheoremManager
setTM(TheoremManager * tm)329 void setTM(TheoremManager* tm) { d_tm = tm; }
330 //! Fetch the TheoremManager
getTM()331 TheoremManager* getTM() const { return d_tm; }
332
333 //! Return a MemoryManager for the given ExprValue type
getMM(size_t MMIndex)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
getSimpCacheTag()339 unsigned getSimpCacheTag() const { return d_simpCacheTagCurrent; }
340 //! Invalidate the simplifier's cache tag
invalidateSimpCache()341 void invalidateSimpCache() { d_simpCacheTagCurrent++; }
342
343 //! Register type computer
registerTypeComputer(TypeComputer * typeComputer)344 void registerTypeComputer(TypeComputer* typeComputer)
345 { d_typeComputer = typeComputer; }
346
347 //! Get printing depth
printDepth()348 int printDepth() const { return *d_printDepth; }
349 //! Whether to print with indentation
withIndentation()350 bool withIndentation() const { return *d_withIndentation; }
351 //! Suggested line width for printing with indentation
lineWidth()352 int lineWidth() const { return *d_lineWidth; }
353 //! Get initial indentation
indent()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
restoreIndent()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
dagPrinting()368 bool dagPrinting() const { return *d_dagPrinting; }
369 /*! @brief Return the pretty-printer if there is one; otherwise
370 return NULL. */
getPrinter()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. */
isKindRegistered(int kind)392 bool isKindRegistered(int kind) { return d_kindMap.count(kind) > 0; }
393 //! Check if a kind represents a type
isTypeKind(int kind)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 /*****************************************************************************/
429 class ExprManagerNotifyObj: public ContextNotifyObj {
430 ExprManager* d_em;
431 public:
432 //! Constructor
ExprManagerNotifyObj(ExprManager * em,Context * cxt)433 ExprManagerNotifyObj(ExprManager* em, Context* cxt)
434 : ContextNotifyObj(cxt), d_em(em) { }
435
436 void notifyPre(void);
437 void notify(void);
getMemory(int verbosity)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
hash(const ExprValue * ev)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
newLeafExpr(const Op & op)454 inline Expr ExprManager::newLeafExpr(const Op& op)
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
newStringExpr(const std::string & s)468 inline Expr ExprManager::newStringExpr(const std::string &s)
469 { ExprString ev(this, s); return newExpr(&ev); }
470
newRatExpr(const Rational & r)471 inline Expr ExprManager::newRatExpr(const Rational& r)
472 { ExprRational ev(this, r); return newExpr(&ev); }
473
newSkolemExpr(const Expr & e,int i)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
newVarExpr(const std::string & s)478 inline Expr ExprManager::newVarExpr(const std::string &s)
479 { ExprVar ev(this, s); return newExpr(&ev); }
480
newSymbolExpr(const std::string & s,int kind)481 inline Expr ExprManager::newSymbolExpr(const std::string &s, int kind)
482 { ExprSymbol ev(this, kind, s); return newExpr(&ev); }
483
newBoundVarExpr(const std::string & name,const std::string & uid)484 inline Expr ExprManager::newBoundVarExpr(const std::string &name,
485 const std::string& uid)
486 { ExprBoundVar ev(this, name, uid); return newExpr(&ev); }
487
newBoundVarExpr(const std::string & name,const std::string & uid,const Type & type)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
newBoundVarExpr(const Type & type)499 inline Expr ExprManager::newBoundVarExpr(const Type& type) {
500 static int nextNum = 0;
501 std::string name("_cvc3_");
502 std::string uid = int2string(nextNum++);
503 return newBoundVarExpr(name, uid, type);
504 }
505
newClosureExpr(int kind,const Expr & var,const Expr & body)506 inline Expr ExprManager::newClosureExpr(int kind,
507 const Expr& var,
508 const Expr& body)
509 { ExprClosure ev(this, kind, var, body); return newExpr(&ev); }
510
newClosureExpr(int kind,const std::vector<Expr> & vars,const Expr & body)511 inline Expr ExprManager::newClosureExpr(int kind,
512 const std::vector<Expr>& vars,
513 const Expr& body)
514 { ExprClosure ev(this, kind, vars, body); return newExpr(&ev); }
515
newClosureExpr(int kind,const std::vector<Expr> & vars,const Expr & body,const std::vector<Expr> & triggers)516 inline Expr ExprManager::newClosureExpr(int kind,
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
newClosureExpr(int kind,const std::vector<Expr> & vars,const Expr & body,const std::vector<std::vector<Expr>> & triggers)523 inline Expr ExprManager::newClosureExpr(int kind,
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
newClosureExpr(int kind,const std::vector<Expr> & vars,const Expr & body,const Expr & trigger)530 inline Expr ExprManager::newClosureExpr(int kind,
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
operator()537 inline bool ExprManager::EqEV::operator()(const ExprValue* ev1,
538 const ExprValue* ev2) const {
539 return (*ev1) == (*ev2);
540 }
541
hash(const Expr & e)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
551