expr_manager.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_manager.h
00004  * \brief Expression manager API
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Wed Dec  4 14:20:56 2002
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 // Must be before #ifndef, since expr.h also includes this file (see
00023 // comments in expr_value.h)
00024 #ifndef _cvc3__expr_h_
00025 #include "expr.h"
00026 #endif
00027 
00028 #ifndef _cvc3__include__expr_manager_h_
00029 #define _cvc3__include__expr_manager_h_
00030 
00031 #include "os.h"
00032 #include "expr_map.h"
00033 
00034 namespace CVC3 {
00035   // Command line flags
00036   class CLFlags;
00037   class PrettyPrinter;
00038   class MemoryManager;
00039   class ExprManagerNotifyObj;
00040   class TheoremManager;
00041 
00042 
00043 ///////////////////////////////////////////////////////////////////////////////
00044 //! Expression Manager
00045 /*!
00046   Class: ExprManager
00047   
00048   Author: Sergey Berezin
00049  
00050   Created: Wed Dec  4 14:26:35 2002
00051 
00052   Description: Global state of the Expr package for a particular
00053     instance of CVC3.  Each instance of the CVC3 library has
00054     its own expression manager, for thread-safety.
00055 */
00056 ///////////////////////////////////////////////////////////////////////////////
00057 
00058   class CVC_DLL ExprManager {
00059     friend class Expr;
00060     friend class ExprValue;
00061     friend class Op; // It wants to call rebuildExpr
00062     friend class HashEV; // Our own private class
00063     friend class Type;
00064 
00065     ContextManager* d_cm; //!< For backtracking attributes
00066     TheoremManager* d_tm; //!< Needed for Refl Theorems
00067     ExprManagerNotifyObj* d_notifyObj; //!< Notification on pop()
00068     ExprIndex d_index; //!< Index counter for Expr compare()
00069     unsigned d_flagCounter; //!< Counter for a generic Expr flag
00070 
00071     //! The database of registered kinds
00072     std::hash_map<int, std::string> d_kindMap;
00073     //! The set of kinds representing a type
00074     std::hash_set<int> d_typeKinds;
00075     //! Private class for hashing strings
00076     class HashString {
00077       std::hash<char*> h;
00078     public:
00079       size_t operator()(const std::string& s) const {
00080   return h(const_cast<char*>(s.c_str()));
00081       }
00082     };
00083     //! The reverse map of names to kinds
00084     std::hash_map<std::string, int, HashString> d_kindMapByName;
00085     /*! @brief The registered pretty-printer, a connector to
00086       theory-specific pretty-printers */
00087     PrettyPrinter *d_prettyPrinter;
00088 
00089     size_t hash(const ExprValue* ev) const;
00090 
00091     // Printing and other options 
00092 
00093     /*! @brief Print upto the given depth, replace the rest with
00094      "...".  -1==unlimited depth. */
00095     const int* d_printDepth;
00096     //! Whether to print with indentation
00097     const bool* d_withIndentation;
00098     //! Permanent indentation
00099     int d_indent;
00100     //! Transient indentation
00101     /*! Normally is the same as d_indent, but may temporarily be
00102       different for printing one single Expr */
00103     int d_indentTransient;
00104     //! Suggested line width for printing with indentation
00105     const int* d_lineWidth;
00106     //! Input language (printing)
00107     const std::string* d_inputLang;
00108     //! Output language (printing)
00109     const std::string* d_outputLang;
00110     //! Whether to print Expr's as DAGs
00111     const bool* d_dagPrinting;
00112     //! Which memory manager to use (copy the flag value and keep it the same)
00113     const std::string d_mmFlag;
00114 
00115     //! Private classe for d_exprSet
00116     class HashEV {
00117       ExprManager* d_em;
00118     public:
00119       HashEV(ExprManager* em): d_em(em) { }
00120       size_t operator()(ExprValue* ev) const { return d_em->hash(ev); }
00121     };
00122     //! Private class for d_exprSet
00123     class EqEV {
00124     public:
00125       bool operator()(const ExprValue* ev1, const ExprValue* ev2) const;
00126     };
00127 
00128     //! Hash set type for uniquifying expressions
00129     typedef std::hash_set<ExprValue*, HashEV, EqEV> ExprValueSet;
00130     //! Hash set for uniquifying expressions
00131     ExprValueSet d_exprSet;
00132     //! Array of memory managers for subclasses of ExprValue
00133     std::vector<MemoryManager*> d_mm;
00134 
00135     //! A hash function for hashing pointers
00136     std::hash<void*> d_pointerHash;
00137     
00138     //! Expr constants cached for fast access
00139     Expr d_bool;
00140     Expr d_false;
00141     Expr d_true;
00142     //! Empty vector of Expr to return by reference as empty vector of children
00143     std::vector<Expr> d_emptyVec;
00144     //! Null Expr to return by reference, for efficiency
00145     Expr d_nullExpr;
00146 
00147     void installExprValue(ExprValue* ev);
00148 
00149     //! Current value of the simplifier cache tag
00150     /*! The cached values of calls to Simplify are valid as long as
00151       their cache tag matches this tag.  Caches can then be
00152       invalidated by incrementing this tag. */
00153     unsigned d_simpCacheTagCurrent;
00154 
00155     //! Disable garbage collection
00156     /*! This flag disables the garbage collection.  Normally, it's set
00157       in the destructor, so that we can delete all remaining
00158       expressions without GC getting in the way. */
00159     bool d_disableGC;
00160     //! Postpone deleting garbage-collected expressions.
00161     /*! Useful during manipulation of context, especially at the time
00162      * of backtracking, since we may have objects with circular
00163      * dependencies (like find pointers).
00164      *
00165      * The postponed expressions will be deleted the next time the
00166      * garbage collector is called after this flag is cleared.
00167      */
00168     bool d_postponeGC;
00169     //! Vector of postponed garbage-collected expressions
00170     std::vector<ExprValue*> d_postponed;
00171     //! Rebuild cache
00172     ExprHashMap<Expr> d_rebuildCache;
00173     IF_DEBUG(bool d_inRebuild);
00174 
00175   public:
00176     //! Abstract class for computing expr type
00177     class TypeComputer {
00178     public:
00179       TypeComputer() {}
00180       virtual ~TypeComputer() {}
00181       //! Compute the type of e
00182       virtual void computeType(const Expr& e) = 0;
00183       //! Check that e is a valid Type expr
00184       virtual void checkType(const Expr& e) = 0;
00185     };
00186   private:
00187     //! Instance of TypeComputer: must be registered
00188     TypeComputer* d_typeComputer;
00189 
00190     /////////////////////////////////////////////////////////////////////////
00191     /*! \defgroup EM_Priv Private methods
00192      * \ingroup ExprPkg
00193      * @{
00194      */
00195     /////////////////////////////////////////////////////////////////////////
00196 
00197     //! Cached recursive descent.  Must be called only during rebuild()
00198     Expr rebuildRec(const Expr& e);
00199 
00200     //! Return either an existing or a new ExprValue matching ev
00201     ExprValue* newExprValue(ExprValue* ev);
00202 
00203     //! Return the current Expr flag counter
00204     unsigned getFlag() { return d_flagCounter; }
00205     //! Increment and return the Expr flag counter (this clears all the flags)
00206     unsigned nextFlag()
00207       { FatalAssert(++d_flagCounter, "flag overflow"); return d_flagCounter; }
00208 
00209     //! Compute the type of the Expr
00210     void computeType(const Expr& e);
00211     //! Check well-formedness of a type Expr
00212     void checkType(const Expr& e);
00213 
00214   public:
00215     //! Constructor
00216     ExprManager(ContextManager* cm, const CLFlags& flags);
00217     //! Destructor
00218     ~ExprManager();
00219     //! Free up all memory and delete all the expressions.
00220     /*!
00221      * No more expressions can be created after this point, only
00222      * destructors ~Expr() can be called.
00223      *
00224      * This method is needed to dis-entangle the mutual dependency of
00225      * ExprManager and ContextManager, when destructors of ExprValue
00226      * (sub)classes need to delete backtracking objects, and deleting
00227      * the ContextManager requires destruction of some remaining Exprs.
00228      */
00229     void clear();
00230     //! Check if the ExprManager is still active (clear() was not called)
00231     bool isActive();
00232 
00233     //! Garbage collect the ExprValue pointer 
00234     /*! \ingroup EM_Priv */
00235     void gc(ExprValue* ev);
00236     //! Postpone deletion of garbage-collected expressions.
00237     /*! \sa resumeGC() */
00238     void postponeGC() { d_postponeGC = true; }
00239     //! Resume deletion of garbage-collected expressions.
00240     /*! \sa postponeGC() */
00241     void resumeGC();
00242 
00243     /*! @brief Rebuild the Expr with this ExprManager if it belongs to
00244       another ExprManager */
00245     Expr rebuild(const Expr& e);
00246 
00247     //! Return the next Expr index
00248     /*! It should be used only by ExprValue() constructor */
00249     ExprIndex nextIndex() { return d_index++; }
00250     ExprIndex lastIndex() { return d_index - 1; }
00251 
00252     //! Clears the generic Expr flag in all Exprs
00253     void clearFlags() { nextFlag(); }
00254 
00255     // Core leaf exprs
00256     //! BOOLEAN Expr
00257     const Expr& boolExpr() { return d_bool; }
00258     //! FALSE Expr
00259     const Expr& falseExpr() { return d_false; }
00260     //! TRUE Expr
00261     const Expr& trueExpr() { return d_true; }
00262     //! References to empty objects (used in ExprValue)
00263     const std::vector<Expr>& getEmptyVector() { return d_emptyVec; }
00264     //! References to empty objects (used in ExprValue)
00265     const Expr& getNullExpr() { return d_nullExpr; }
00266 
00267     // Expr constructors
00268 
00269     //! Return either an existing or a new Expr matching ev
00270     Expr newExpr(ExprValue* ev) { return Expr(newExprValue(ev)); }
00271 
00272     Expr newLeafExpr(const Op& op);
00273     Expr newStringExpr(const std::string &s);
00274     Expr newRatExpr(const Rational& r);
00275     Expr newSkolemExpr(const Expr& e, int i);
00276     Expr newVarExpr(const std::string &s);
00277     Expr newSymbolExpr(const std::string &s, int kind);
00278     Expr newBoundVarExpr(const std::string &name, const std::string& uid);
00279     Expr newBoundVarExpr(const std::string &name, const std::string& uid,
00280                          const Type& type);
00281     Expr newBoundVarExpr(const Type& type);
00282     Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00283                         const Expr& body);
00284     Expr newTheoremExpr(const Theorem& thm);
00285 
00286     // Vector of children constructors (vector may be empty)
00287     Expr andExpr(const std::vector <Expr>& children)
00288      { return Expr(AND, children, this); }
00289     Expr orExpr(const std::vector <Expr>& children)
00290      { return Expr(OR, children, this); }
00291 
00292     // Public methods
00293 
00294     //! Hash function for a single Expr
00295     size_t hash(const Expr& e) const;
00296     //! Fetch our ContextManager
00297     ContextManager* getCM() const { return d_cm; }
00298     //! Get the current context from our ContextManager
00299     Context* getCurrentContext() const { return d_cm->getCurrentContext(); }
00300     //! Get current scope level
00301     int scopelevel() { return d_cm->scopeLevel(); }
00302 
00303     //! Set the TheoremManager
00304     void setTM(TheoremManager* tm) { d_tm = tm; }
00305     //! Fetch the TheoremManager
00306     TheoremManager* getTM() const { return d_tm; }
00307 
00308     //! Return a MemoryManager for the given ExprValue type
00309     MemoryManager* getMM(size_t MMIndex) {
00310       DebugAssert(MMIndex < d_mm.size(), "ExprManager::getMM()");
00311       return d_mm[MMIndex];
00312     }
00313     //! Get the simplifier's cache tag
00314     unsigned getSimpCacheTag() const { return d_simpCacheTagCurrent; }
00315     //! Invalidate the simplifier's cache tag
00316     void invalidateSimpCache() { d_simpCacheTagCurrent++; }
00317 
00318     //! Register type computer
00319     void registerTypeComputer(TypeComputer* typeComputer)
00320       { d_typeComputer = typeComputer; }
00321 
00322     //! Get printing depth
00323     int printDepth() const { return *d_printDepth; }
00324     //! Whether to print with indentation
00325     bool withIndentation() const { return *d_withIndentation; }
00326     //! Suggested line width for printing with indentation
00327     int lineWidth() const { return *d_lineWidth; }
00328     //! Get initial indentation
00329     int indent() const { return d_indentTransient; }
00330     //! Set initial indentation.  Returns the previous permanent value.
00331     int indent(int n, bool permanent = false);
00332     //! Increment the current transient indentation by n
00333     /*! If the second argument is true, sets the result as permanent.
00334       \return previous permanent value. */
00335     int incIndent(int n, bool permanent = false);
00336     //! Set transient indentation to permanent
00337     void restoreIndent() { d_indentTransient = d_indent; }
00338     //! Get the input language for printing
00339     InputLanguage getInputLang() const;
00340     //! Get the output language for printing
00341     InputLanguage getOutputLang() const;
00342     //! Whether to print Expr's as DAGs
00343     bool dagPrinting() const { return *d_dagPrinting; }
00344     /*! @brief Return the pretty-printer if there is one; otherwise
00345        return NULL. */
00346     PrettyPrinter* getPrinter() const { return d_prettyPrinter; }
00347  
00348   /////////////////////////////////////////////////////////////////////////////
00349   // Kind registration                                                       //
00350   /////////////////////////////////////////////////////////////////////////////
00351 
00352     //! Register a new kind.
00353     /*! The kind may already be registered under the same name, but if
00354      *  the name is different, it's an error.
00355      * 
00356      * If the new kind is supposed to represent a type, set isType to true.
00357      */
00358     void newKind(int kind, const std::string &name, bool isType = false);
00359     //! Register the pretty-printer (can only do it if none registered)
00360     /*! The pointer is NOT owned by ExprManager. Delete it yourself.
00361      */
00362     void registerPrettyPrinter(PrettyPrinter& printer);
00363     //! Tell ExprManager that the printer is no longer valid
00364     void unregisterPrettyPrinter();
00365     /*! @brief Returns true if kind is built into CVC or has been registered
00366       via newKind. */
00367     bool isKindRegistered(int kind) { return d_kindMap.count(kind) > 0; }
00368     //! Check if a kind represents a type
00369     bool isTypeKind(int kind) { return d_typeKinds.count(kind) > 0; }
00370 
00371     /*! @brief Return the name associated with a kind.  The kind must
00372       already be registered. */
00373     const std::string& getKindName(int kind);
00374     //! Return a kind associated with a name.  Returns NULL_KIND if not found.
00375     int getKind(const std::string& name);
00376     //! Register a new subclass of ExprValue
00377     /*!
00378      * Takes the size (in bytes) of the new subclass and returns the
00379      * unique index of that subclass.  Subsequent calls to the
00380      * subclass's getMMIndex() must return that index.
00381      */
00382     size_t registerSubclass(size_t sizeOfSubclass);
00383 
00384   }; // end of class ExprManager
00385 
00386 
00387 /*****************************************************************************/
00388 /*!
00389  *\class ExprManagerNotifyObj
00390  *\brief Notifies ExprManager before and after each pop()
00391  *
00392  * Author: Sergey Berezin
00393  *
00394  * Created: Tue Mar  1 12:29:14 2005
00395  *
00396  * Disables the deletion of Exprs during context restoration
00397  * (backtracking).  This solves the problem of circular dependencies,
00398  * e.g. in find pointers.
00399  */
00400 /*****************************************************************************/
00401   class ExprManagerNotifyObj: public ContextNotifyObj {
00402     ExprManager* d_em;
00403   public:
00404     //! Constructor
00405     ExprManagerNotifyObj(ExprManager* em, Context* cxt)
00406       : ContextNotifyObj(cxt), d_em(em) { }
00407 
00408     void notifyPre(void);
00409     void notify(void);
00410   };
00411     
00412 
00413 } // end of namespace CVC3
00414 
00415 // Include expr_value here for inline definitions
00416 #include "expr_value.h"
00417 
00418 namespace CVC3 {
00419 
00420 inline Expr ExprManager::newLeafExpr(const Op& op)
00421 {
00422   if (op.getExpr().isNull()) {
00423     ExprValue ev(this, op.getKind());
00424     return newExpr(&ev);
00425   }
00426   else {
00427     DebugAssert(op.getExpr().getEM() == this, "ExprManager mismatch");
00428     std::vector<Expr> kids;
00429     ExprApply ev(this, op, kids);
00430     return newExpr(&ev);
00431   }
00432 }
00433 
00434 inline Expr ExprManager::newStringExpr(const std::string &s)
00435   { ExprString ev(this, s); return newExpr(&ev); }
00436 
00437 inline Expr ExprManager::newRatExpr(const Rational& r)
00438   { ExprRational ev(this, r); return newExpr(&ev); }
00439 
00440 inline Expr ExprManager::newSkolemExpr(const Expr& e, int i)
00441   { DebugAssert(e.getEM() == this, "ExprManager mismatch");
00442     ExprSkolem ev(this, i, e); return newExpr(&ev); }
00443 
00444 inline Expr ExprManager::newVarExpr(const std::string &s)
00445   { ExprVar ev(this, s); return newExpr(&ev); }
00446 
00447 inline Expr ExprManager::newSymbolExpr(const std::string &s, int kind)
00448   { ExprSymbol ev(this, kind, s); return newExpr(&ev); }
00449 
00450 inline Expr ExprManager::newBoundVarExpr(const std::string &name,
00451                                          const std::string& uid)
00452   { ExprBoundVar ev(this, name, uid); return newExpr(&ev); }
00453 
00454 inline Expr ExprManager::newBoundVarExpr(const std::string& name,
00455                                          const std::string& uid,
00456                                          const Type& type) {
00457   Expr res = newBoundVarExpr(name, uid);
00458   DebugAssert(type.getExpr().getKind() != ARROW,"");
00459   DebugAssert(res.lookupType().isNull(), 
00460               "newBoundVarExpr: redefining a variable " + name);
00461   res.setType(type);
00462   return res;
00463 }
00464 
00465 inline Expr ExprManager::newBoundVarExpr(const Type& type) {
00466   static int nextNum = 0;
00467   std::string name("_cvc3_");
00468   std::string uid =  int2string(nextNum++);
00469   return newBoundVarExpr(name, uid, type);
00470 }
00471 
00472 inline Expr ExprManager::newClosureExpr(int kind,
00473                                         const std::vector<Expr>& vars,
00474                                         const Expr& body)
00475   { ExprClosure ev(this, kind, vars, body); return newExpr(&ev); }
00476 
00477 inline Expr ExprManager::newTheoremExpr(const Theorem& thm)
00478   { ExprTheorem ev(this, thm); return newExpr(&ev); }
00479 
00480 inline size_t ExprManager::hash(const ExprValue* ev) const {
00481   DebugAssert(ev!=NULL, "ExprManager::hash() called on a NULL ExprValue");
00482   return ev->hash();
00483 }
00484 
00485 inline bool ExprManager::EqEV::operator()(const ExprValue* ev1,
00486                                           const ExprValue* ev2) const {
00487   return (*ev1) == (*ev2);
00488 }
00489 
00490 inline size_t ExprManager::hash(const Expr& e) const {
00491   DebugAssert(!e.isNull(), "ExprManager::hash() called on a Null Expr");
00492   return e.d_expr->hash();
00493 }
00494  
00495 } // end of namespace CVC3
00496 
00497 #endif
00498 

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1