CVC3

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 #include <deque>
00034 
00035 namespace CVC3 {
00036   // Command line flags
00037   class CLFlags;
00038   class PrettyPrinter;
00039   class MemoryManager;
00040   class ExprManagerNotifyObj;
00041   class TheoremManager;
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 class 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 
00172     //! Flag for whether GC is already running
00173     bool d_inGC;
00174     //! Queue of pending exprs to GC
00175     std::deque<ExprValue*> d_pending;
00176 
00177     //! Rebuild cache
00178     ExprHashMap<Expr> d_rebuildCache;
00179     IF_DEBUG(bool d_inRebuild;)
00180 
00181   public:
00182     //! Abstract class for computing expr type
00183     class TypeComputer {
00184     public:
00185       TypeComputer() {}
00186       virtual ~TypeComputer() {}
00187       //! Compute the type of e
00188       virtual void computeType(const Expr& e) = 0;
00189       //! Check that e is a valid Type expr
00190       virtual void checkType(const Expr& e) = 0;
00191       //! Get information related to finiteness of a type
00192       virtual Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00193                                          bool enumerate, bool computeSize) = 0;
00194     };
00195   private:
00196     //! Instance of TypeComputer: must be registered
00197     TypeComputer* d_typeComputer;
00198 
00199     /////////////////////////////////////////////////////////////////////////
00200     /*! \defgroup EM_Priv Private methods
00201      * \ingroup ExprPkg
00202      * @{
00203      */
00204     /////////////////////////////////////////////////////////////////////////
00205 
00206     //! Cached recursive descent.  Must be called only during rebuild()
00207     Expr rebuildRec(const Expr& e);
00208 
00209     //! Return either an existing or a new ExprValue matching ev
00210     ExprValue* newExprValue(ExprValue* ev);
00211 
00212     //! Return the current Expr flag counter
00213     unsigned getFlag() { return d_flagCounter; }
00214     //! Increment and return the Expr flag counter (this clears all the flags)
00215     unsigned nextFlag()
00216       { FatalAssert(++d_flagCounter, "flag overflow"); return d_flagCounter; }
00217 
00218     //! Compute the type of the Expr
00219     void computeType(const Expr& e);
00220     //! Check well-formedness of a type Expr
00221     void checkType(const Expr& e);
00222     //! Get information related to finiteness of a type
00223     // 1. Returns Cardinality of the type (finite, infinite, or unknown)
00224     // 2. If cardinality = finite and enumerate is true,
00225     //    sets e to the nth element of the type if it can
00226     //    sets e to NULL if n is out of bounds or if unable to compute nth element
00227     // 3. If cardinality = finite and computeSize is true,
00228     //    sets n to the size of the type if it can
00229     //    sets n to 0 otherwise
00230     Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00231                                bool enumerate, bool computeSize);
00232 
00233   public:
00234     //! Constructor
00235     ExprManager(ContextManager* cm, const CLFlags& flags);
00236     //! Destructor
00237     ~ExprManager();
00238     //! Free up all memory and delete all the expressions.
00239     /*!
00240      * No more expressions can be created after this point, only
00241      * destructors ~Expr() can be called.
00242      *
00243      * This method is needed to dis-entangle the mutual dependency of
00244      * ExprManager and ContextManager, when destructors of ExprValue
00245      * (sub)classes need to delete backtracking objects, and deleting
00246      * the ContextManager requires destruction of some remaining Exprs.
00247      */
00248     void clear();
00249     //! Check if the ExprManager is still active (clear() was not called)
00250     bool isActive();
00251 
00252     //! Garbage collect the ExprValue pointer 
00253     /*! \ingroup EM_Priv */
00254     void gc(ExprValue* ev);
00255     //! Postpone deletion of garbage-collected expressions.
00256     /*! \sa resumeGC() */
00257     void postponeGC() { d_postponeGC = true; }
00258     //! Resume deletion of garbage-collected expressions.
00259     /*! \sa postponeGC() */
00260     void resumeGC();
00261 
00262     /*! @brief Rebuild the Expr with this ExprManager if it belongs to
00263       another ExprManager */
00264     Expr rebuild(const Expr& e);
00265 
00266     //! Return the next Expr index
00267     /*! It should be used only by ExprValue() constructor */
00268     ExprIndex nextIndex() { return d_index++; }
00269     ExprIndex lastIndex() { return d_index - 1; }
00270 
00271     //! Clears the generic Expr flag in all Exprs
00272     void clearFlags() { nextFlag(); }
00273 
00274     // Core leaf exprs
00275     //! BOOLEAN Expr
00276     const Expr& boolExpr() { return d_bool; }
00277     //! FALSE Expr
00278     const Expr& falseExpr() { return d_false; }
00279     //! TRUE Expr
00280     const Expr& trueExpr() { return d_true; }
00281     //! References to empty objects (used in ExprValue)
00282     const std::vector<Expr>& getEmptyVector() { return d_emptyVec; }
00283     //! References to empty objects (used in ExprValue)
00284     const Expr& getNullExpr() { return d_nullExpr; }
00285 
00286     // Expr constructors
00287 
00288     //! Return either an existing or a new Expr matching ev
00289     Expr newExpr(ExprValue* ev) { return Expr(newExprValue(ev)); }
00290 
00291     Expr newLeafExpr(const Op& op);
00292     Expr newStringExpr(const std::string &s);
00293     Expr newRatExpr(const Rational& r);
00294     Expr newSkolemExpr(const Expr& e, int i);
00295     Expr newVarExpr(const std::string &s);
00296     Expr newSymbolExpr(const std::string &s, int kind);
00297     Expr newBoundVarExpr(const std::string &name, const std::string& uid);
00298     Expr newBoundVarExpr(const std::string &name, const std::string& uid,
00299                          const Type& type);
00300     Expr newBoundVarExpr(const Type& type);
00301     Expr newClosureExpr(int kind, const Expr& var, const Expr& body);
00302     Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00303                         const Expr& body);
00304     Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00305                         const Expr& body, const Expr& trigger);
00306     Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00307                         const Expr& body, const std::vector<Expr>& triggers);
00308     Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00309                         const Expr& body, const std::vector<std::vector<Expr> >& triggers);
00310 
00311     // Vector of children constructors (vector may be empty)
00312     Expr andExpr(const std::vector <Expr>& children)
00313      { return Expr(AND, children, this); }
00314     Expr orExpr(const std::vector <Expr>& children)
00315      { return Expr(OR, children, this); }
00316 
00317     // Public methods
00318 
00319     //! Hash function for a single Expr
00320     size_t hash(const Expr& e) const;
00321     //! Fetch our ContextManager
00322     ContextManager* getCM() const { return d_cm; }
00323     //! Get the current context from our ContextManager
00324     Context* getCurrentContext() const { return d_cm->getCurrentContext(); }
00325     //! Get current scope level
00326     int scopelevel() { return d_cm->scopeLevel(); }
00327 
00328     //! Set the TheoremManager
00329     void setTM(TheoremManager* tm) { d_tm = tm; }
00330     //! Fetch the TheoremManager
00331     TheoremManager* getTM() const { return d_tm; }
00332 
00333     //! Return a MemoryManager for the given ExprValue type
00334     MemoryManager* getMM(size_t MMIndex) {
00335       DebugAssert(MMIndex < d_mm.size(), "ExprManager::getMM()");
00336       return d_mm[MMIndex];
00337     }
00338     //! Get the simplifier's cache tag
00339     unsigned getSimpCacheTag() const { return d_simpCacheTagCurrent; }
00340     //! Invalidate the simplifier's cache tag
00341     void invalidateSimpCache() { d_simpCacheTagCurrent++; }
00342 
00343     //! Register type computer
00344     void registerTypeComputer(TypeComputer* typeComputer)
00345       { d_typeComputer = typeComputer; }
00346 
00347     //! Get printing depth
00348     int printDepth() const { return *d_printDepth; }
00349     //! Whether to print with indentation
00350     bool withIndentation() const { return *d_withIndentation; }
00351     //! Suggested line width for printing with indentation
00352     int lineWidth() const { return *d_lineWidth; }
00353     //! Get initial indentation
00354     int indent() const { return d_indentTransient; }
00355     //! Set initial indentation.  Returns the previous permanent value.
00356     int indent(int n, bool permanent = false);
00357     //! Increment the current transient indentation by n
00358     /*! If the second argument is true, sets the result as permanent.
00359       \return previous permanent value. */
00360     int incIndent(int n, bool permanent = false);
00361     //! Set transient indentation to permanent
00362     void restoreIndent() { d_indentTransient = d_indent; }
00363     //! Get the input language for printing
00364     InputLanguage getInputLang() const;
00365     //! Get the output language for printing
00366     InputLanguage getOutputLang() const;
00367     //! Whether to print Expr's as DAGs
00368     bool dagPrinting() const { return *d_dagPrinting; }
00369     /*! @brief Return the pretty-printer if there is one; otherwise
00370        return NULL. */
00371     PrettyPrinter* getPrinter() const { return d_prettyPrinter; }
00372  
00373   /////////////////////////////////////////////////////////////////////////////
00374   // Kind registration                                                       //
00375   /////////////////////////////////////////////////////////////////////////////
00376 
00377     //! Register a new kind.
00378     /*! The kind may already be registered under the same name, but if
00379      *  the name is different, it's an error.
00380      * 
00381      * If the new kind is supposed to represent a type, set isType to true.
00382      */
00383     void newKind(int kind, const std::string &name, bool isType = false);
00384     //! Register the pretty-printer (can only do it if none registered)
00385     /*! The pointer is NOT owned by ExprManager. Delete it yourself.
00386      */
00387     void registerPrettyPrinter(PrettyPrinter& printer);
00388     //! Tell ExprManager that the printer is no longer valid
00389     void unregisterPrettyPrinter();
00390     /*! @brief Returns true if kind is built into CVC or has been registered
00391       via newKind. */
00392     bool isKindRegistered(int kind) { return d_kindMap.count(kind) > 0; }
00393     //! Check if a kind represents a type
00394     bool isTypeKind(int kind) { return d_typeKinds.count(kind) > 0; }
00395 
00396     /*! @brief Return the name associated with a kind.  The kind must
00397       already be registered. */
00398     const std::string& getKindName(int kind);
00399     //! Return a kind associated with a name.  Returns NULL_KIND if not found.
00400     int getKind(const std::string& name);
00401     //! Register a new subclass of ExprValue
00402     /*!
00403      * Takes the size (in bytes) of the new subclass and returns the
00404      * unique index of that subclass.  Subsequent calls to the
00405      * subclass's getMMIndex() must return that index.
00406      */
00407     size_t registerSubclass(size_t sizeOfSubclass);
00408 
00409     //! Calculate memory usage
00410     unsigned long getMemory(int verbosity);
00411 
00412   }; // end of class ExprManager
00413 
00414 
00415 /*****************************************************************************/
00416 /*!
00417  *\class ExprManagerNotifyObj
00418  *\brief Notifies ExprManager before and after each pop()
00419  *
00420  * Author: Sergey Berezin
00421  *
00422  * Created: Tue Mar  1 12:29:14 2005
00423  *
00424  * Disables the deletion of Exprs during context restoration
00425  * (backtracking).  This solves the problem of circular dependencies,
00426  * e.g. in find pointers.
00427  */
00428 /*****************************************************************************/
00429   class ExprManagerNotifyObj: public ContextNotifyObj {
00430     ExprManager* d_em;
00431   public:
00432     //! Constructor
00433     ExprManagerNotifyObj(ExprManager* em, Context* cxt)
00434       : ContextNotifyObj(cxt), d_em(em) { }
00435 
00436     void notifyPre(void);
00437     void notify(void);
00438     unsigned long getMemory(int verbosity) { return sizeof(ExprManagerNotifyObj); }
00439   };
00440     
00441 
00442 } // end of namespace CVC3
00443 
00444 // Include expr_value here for inline definitions
00445 #include "expr_value.h"
00446 
00447 namespace CVC3 {
00448 
00449 inline size_t ExprManager::hash(const ExprValue* ev) const {
00450   DebugAssert(ev!=NULL, "ExprManager::hash() called on a NULL ExprValue");
00451   return ev->hash();
00452 }
00453 
00454 inline Expr ExprManager::newLeafExpr(const Op& op)
00455 {
00456   if (op.getKind() != APPLY) {
00457     ExprValue ev(this, op.getKind());
00458     return newExpr(&ev);
00459   }
00460   else {
00461     DebugAssert(op.getExpr().getEM() == this, "ExprManager mismatch");
00462     std::vector<Expr> kids;
00463     ExprApply ev(this, op, kids);
00464     return newExpr(&ev);
00465   }
00466 }
00467 
00468 inline Expr ExprManager::newStringExpr(const std::string &s)
00469   { ExprString ev(this, s); return newExpr(&ev); }
00470 
00471 inline Expr ExprManager::newRatExpr(const Rational& r)
00472   { ExprRational ev(this, r); return newExpr(&ev); }
00473 
00474 inline Expr ExprManager::newSkolemExpr(const Expr& e, int i)
00475   { DebugAssert(e.getEM() == this, "ExprManager mismatch");
00476     ExprSkolem ev(this, i, e); return newExpr(&ev); }
00477 
00478 inline Expr ExprManager::newVarExpr(const std::string &s)
00479   { ExprVar ev(this, s); return newExpr(&ev); }
00480 
00481 inline Expr ExprManager::newSymbolExpr(const std::string &s, int kind)
00482   { ExprSymbol ev(this, kind, s); return newExpr(&ev); }
00483 
00484 inline Expr ExprManager::newBoundVarExpr(const std::string &name,
00485                                          const std::string& uid)
00486   { ExprBoundVar ev(this, name, uid); return newExpr(&ev); }
00487 
00488 inline Expr ExprManager::newBoundVarExpr(const std::string& name,
00489                                          const std::string& uid,
00490                                          const Type& type) {
00491   Expr res = newBoundVarExpr(name, uid);
00492   DebugAssert(type.getExpr().getKind() != ARROW,"");
00493   DebugAssert(res.lookupType().isNull(), 
00494               "newBoundVarExpr: redefining a variable " + name);
00495   res.setType(type);
00496   return res;
00497 }
00498 
00499 inline Expr ExprManager::newBoundVarExpr(const Type& type) {
00500   static int nextNum = 0;
00501   std::string name("_cvc3_");
00502   std::string uid =  int2string(nextNum++);
00503   return newBoundVarExpr(name, uid, type);
00504 }
00505 
00506 inline Expr ExprManager::newClosureExpr(int kind,
00507                                         const Expr& var,
00508                                         const Expr& body)
00509   { ExprClosure ev(this, kind, var, body); return newExpr(&ev); }
00510 
00511 inline Expr ExprManager::newClosureExpr(int kind,
00512                                         const std::vector<Expr>& vars,
00513                                         const Expr& body)
00514   { ExprClosure ev(this, kind, vars, body); return newExpr(&ev); }
00515 
00516 inline Expr ExprManager::newClosureExpr(int kind,
00517                                         const std::vector<Expr>& vars,
00518                                         const Expr& body,
00519                                         const std::vector<Expr>& triggers)
00520   { ExprClosure ev(this, kind, vars, body);
00521     Expr ret = newExpr(&ev); ret.setTriggers(triggers); return ret; }
00522 
00523 inline Expr ExprManager::newClosureExpr(int kind,
00524                                         const std::vector<Expr>& vars,
00525                                         const Expr& body,
00526                                         const std::vector<std::vector<Expr> >& triggers)
00527   { ExprClosure ev(this, kind, vars, body);
00528     Expr ret = newExpr(&ev); ret.setTriggers(triggers); return ret; }
00529 
00530 inline Expr ExprManager::newClosureExpr(int kind,
00531                                         const std::vector<Expr>& vars,
00532                                         const Expr& body,
00533                                         const Expr& trigger)
00534   { ExprClosure ev(this, kind, vars, body);
00535     Expr ret = newExpr(&ev); ret.setTrigger(trigger); return ret; }
00536 
00537 inline bool ExprManager::EqEV::operator()(const ExprValue* ev1,
00538                                           const ExprValue* ev2) const {
00539   return (*ev1) == (*ev2);
00540 }
00541 
00542 inline size_t ExprManager::hash(const Expr& e) const {
00543   DebugAssert(!e.isNull(), "ExprManager::hash() called on a Null Expr");
00544   return e.d_expr->hash();
00545 }
00546  
00547 } // end of namespace CVC3
00548 
00549 #endif
00550