/*****************************************************************************/
/*!
 * \file expr_manager.h
 * \brief Expression manager API
 * 
 * Author: Sergey Berezin
 * 
 * Created: Wed Dec  4 14:20:56 2002
 *
 * <hr>
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

// Must be before #ifndef, since expr.h also includes this file (see
// comments in expr_value.h)
#ifndef _cvc3__expr_h_
#include "expr.h"
#endif

#ifndef _cvc3__include__expr_manager_h_
#define _cvc3__include__expr_manager_h_

#include "os.h"
#include "expr_map.h"

namespace CVC3 {
  // Command line flags
  class CLFlags;
  class PrettyPrinter;
  class MemoryManager;
  class ExprManagerNotifyObj;
  class TheoremManager;


///////////////////////////////////////////////////////////////////////////////
//! Expression Manager
/*!
  Class: ExprManager
  
  Author: Sergey Berezin
 
  Created: Wed Dec  4 14:26:35 2002

  Description: Global state of the Expr package for a particular
    instance of CVC3.  Each instance of the CVC3 library has
    its own expression manager, for thread-safety.
*/
///////////////////////////////////////////////////////////////////////////////

  class CVC_DLL ExprManager {
    friend class Expr;
    friend class ExprValue;
    friend class Op; // It wants to call rebuildExpr
    friend class HashEV; // Our own private class
    friend class Type;

    ContextManager* d_cm; //!< For backtracking attributes
    TheoremManager* d_tm; //!< Needed for Refl Theorems
    ExprManagerNotifyObj* d_notifyObj; //!< Notification on pop()
    ExprIndex d_index; //!< Index counter for Expr compare()
    unsigned d_flagCounter; //!< Counter for a generic Expr flag

    //! The database of registered kinds
    std::hash_map<int, std::string> d_kindMap;
    //! The set of kinds representing a type
    std::hash_set<int> d_typeKinds;
    //! Private class for hashing strings
    class HashString {
      std::hash<char*> h;
    public:
      size_t operator()(const std::string& s) const {
	return h(const_cast<char*>(s.c_str()));
      }
    };
    //! The reverse map of names to kinds
    std::hash_map<std::string, int, HashString> d_kindMapByName;
    /*! @brief The registered pretty-printer, a connector to
      theory-specific pretty-printers */
    PrettyPrinter *d_prettyPrinter;

    size_t hash(const ExprValue* ev) const;

    // Printing and other options 

    /*! @brief Print upto the given depth, replace the rest with
     "...".  -1==unlimited depth. */
    const int* d_printDepth;
    //! Whether to print with indentation
    const bool* d_withIndentation;
    //! Permanent indentation
    int d_indent;
    //! Transient indentation
    /*! Normally is the same as d_indent, but may temporarily be
      different for printing one single Expr */
    int d_indentTransient;
    //! Suggested line width for printing with indentation
    const int* d_lineWidth;
    //! Input language (printing)
    const std::string* d_inputLang;
    //! Output language (printing)
    const std::string* d_outputLang;
    //! Whether to print Expr's as DAGs
    const bool* d_dagPrinting;
    //! Which memory manager to use (copy the flag value and keep it the same)
    const std::string d_mmFlag;

    //! Private classe for d_exprSet
    class HashEV {
      ExprManager* d_em;
    public:
      HashEV(ExprManager* em): d_em(em) { }
      size_t operator()(ExprValue* ev) const { return d_em->hash(ev); }
    };
    //! Private class for d_exprSet
    class EqEV {
    public:
      bool operator()(const ExprValue* ev1, const ExprValue* ev2) const;
    };

    //! Hash set type for uniquifying expressions
    typedef std::hash_set<ExprValue*, HashEV, EqEV> ExprValueSet;
    //! Hash set for uniquifying expressions
    ExprValueSet d_exprSet;
    //! Array of memory managers for subclasses of ExprValue
    std::vector<MemoryManager*> d_mm;

    //! A hash function for hashing pointers
    std::hash<void*> d_pointerHash;
    
    //! Expr constants cached for fast access
    Expr d_bool;
    Expr d_false;
    Expr d_true;
    //! Empty vector of Expr to return by reference as empty vector of children
    std::vector<Expr> d_emptyVec;
    //! Null Expr to return by reference, for efficiency
    Expr d_nullExpr;

    void installExprValue(ExprValue* ev);

    //! Current value of the simplifier cache tag
    /*! The cached values of calls to Simplify are valid as long as
      their cache tag matches this tag.  Caches can then be
      invalidated by incrementing this tag. */
    unsigned d_simpCacheTagCurrent;

    //! Disable garbage collection
    /*! This flag disables the garbage collection.  Normally, it's set
      in the destructor, so that we can delete all remaining
      expressions without GC getting in the way. */
    bool d_disableGC;
    //! Postpone deleting garbage-collected expressions.
    /*! Useful during manipulation of context, especially at the time
     * of backtracking, since we may have objects with circular
     * dependencies (like find pointers).
     *
     * The postponed expressions will be deleted the next time the
     * garbage collector is called after this flag is cleared.
     */
    bool d_postponeGC;
    //! Vector of postponed garbage-collected expressions
    std::vector<ExprValue*> d_postponed;
    //! Rebuild cache
    ExprHashMap<Expr> d_rebuildCache;
    IF_DEBUG(bool d_inRebuild);

  public:
    //! Abstract class for computing expr type
    class TypeComputer {
    public:
      TypeComputer() {}
      virtual ~TypeComputer() {}
      //! Compute the type of e
      virtual void computeType(const Expr& e) = 0;
      //! Check that e is a valid Type expr
      virtual void checkType(const Expr& e) = 0;
    };
  private:
    //! Instance of TypeComputer: must be registered
    TypeComputer* d_typeComputer;

    /////////////////////////////////////////////////////////////////////////
    /*! \defgroup EM_Priv Private methods
     * \ingroup ExprPkg
     * @{
     */
    /////////////////////////////////////////////////////////////////////////

    //! Cached recursive descent.  Must be called only during rebuild()
    Expr rebuildRec(const Expr& e);

    //! Return either an existing or a new ExprValue matching ev
    ExprValue* newExprValue(ExprValue* ev);

    //! Return the current Expr flag counter
    unsigned getFlag() { return d_flagCounter; }
    //! Increment and return the Expr flag counter (this clears all the flags)
    unsigned nextFlag()
      { FatalAssert(++d_flagCounter, "flag overflow"); return d_flagCounter; }

    //! Compute the type of the Expr
    void computeType(const Expr& e);
    //! Check well-formedness of a type Expr
    void checkType(const Expr& e);

  public:
    //! Constructor
    ExprManager(ContextManager* cm, const CLFlags& flags);
    //! Destructor
    ~ExprManager();
    //! Free up all memory and delete all the expressions.
    /*!
     * No more expressions can be created after this point, only
     * destructors ~Expr() can be called.
     *
     * This method is needed to dis-entangle the mutual dependency of
     * ExprManager and ContextManager, when destructors of ExprValue
     * (sub)classes need to delete backtracking objects, and deleting
     * the ContextManager requires destruction of some remaining Exprs.
     */
    void clear();
    //! Check if the ExprManager is still active (clear() was not called)
    bool isActive();

    //! Garbage collect the ExprValue pointer 
    /*! \ingroup EM_Priv */
    void gc(ExprValue* ev);
    //! Postpone deletion of garbage-collected expressions.
    /*! \sa resumeGC() */
    void postponeGC() { d_postponeGC = true; }
    //! Resume deletion of garbage-collected expressions.
    /*! \sa postponeGC() */
    void resumeGC();

    /*! @brief Rebuild the Expr with this ExprManager if it belongs to
      another ExprManager */
    Expr rebuild(const Expr& e);

    //! Return the next Expr index
    /*! It should be used only by ExprValue() constructor */
    ExprIndex nextIndex() { return d_index++; }
    ExprIndex lastIndex() { return d_index - 1; }

    //! Clears the generic Expr flag in all Exprs
    void clearFlags() { nextFlag(); }

    // Core leaf exprs
    //! BOOLEAN Expr
    const Expr& boolExpr() { return d_bool; }
    //! FALSE Expr
    const Expr& falseExpr() { return d_false; }
    //! TRUE Expr
    const Expr& trueExpr() { return d_true; }
    //! References to empty objects (used in ExprValue)
    const std::vector<Expr>& getEmptyVector() { return d_emptyVec; }
    //! References to empty objects (used in ExprValue)
    const Expr& getNullExpr() { return d_nullExpr; }

    // Expr constructors

    //! Return either an existing or a new Expr matching ev
    Expr newExpr(ExprValue* ev) { return Expr(newExprValue(ev)); }

    Expr newLeafExpr(const Op& op);
    Expr newStringExpr(const std::string &s);
    Expr newRatExpr(const Rational& r);
    Expr newSkolemExpr(const Expr& e, int i);
    Expr newVarExpr(const std::string &s);
    Expr newSymbolExpr(const std::string &s, int kind);
    Expr newBoundVarExpr(const std::string &name, const std::string& uid);
    Expr newBoundVarExpr(const std::string &name, const std::string& uid,
                         const Type& type);
    Expr newBoundVarExpr(const Type& type);
    Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
                        const Expr& body);
    Expr newTheoremExpr(const Theorem& thm);

    // Vector of children constructors (vector may be empty)
    Expr andExpr(const std::vector <Expr>& children)
     { return Expr(AND, children, this); }
    Expr orExpr(const std::vector <Expr>& children)
     { return Expr(OR, children, this); }

    // Public methods

    //! Hash function for a single Expr
    size_t hash(const Expr& e) const;
    //! Fetch our ContextManager
    ContextManager* getCM() const { return d_cm; }
    //! Get the current context from our ContextManager
    Context* getCurrentContext() const { return d_cm->getCurrentContext(); }
    //! Get current scope level
    int scopelevel() { return d_cm->scopeLevel(); }

    //! Set the TheoremManager
    void setTM(TheoremManager* tm) { d_tm = tm; }
    //! Fetch the TheoremManager
    TheoremManager* getTM() const { return d_tm; }

    //! Return a MemoryManager for the given ExprValue type
    MemoryManager* getMM(size_t MMIndex) {
      DebugAssert(MMIndex < d_mm.size(), "ExprManager::getMM()");
      return d_mm[MMIndex];
    }
    //! Get the simplifier's cache tag
    unsigned getSimpCacheTag() const { return d_simpCacheTagCurrent; }
    //! Invalidate the simplifier's cache tag
    void invalidateSimpCache() { d_simpCacheTagCurrent++; }

    //! Register type computer
    void registerTypeComputer(TypeComputer* typeComputer)
      { d_typeComputer = typeComputer; }

    //! Get printing depth
    int printDepth() const { return *d_printDepth; }
    //! Whether to print with indentation
    bool withIndentation() const { return *d_withIndentation; }
    //! Suggested line width for printing with indentation
    int lineWidth() const { return *d_lineWidth; }
    //! Get initial indentation
    int indent() const { return d_indentTransient; }
    //! Set initial indentation.  Returns the previous permanent value.
    int indent(int n, bool permanent = false);
    //! Increment the current transient indentation by n
    /*! If the second argument is true, sets the result as permanent.
      \return previous permanent value. */
    int incIndent(int n, bool permanent = false);
    //! Set transient indentation to permanent
    void restoreIndent() { d_indentTransient = d_indent; }
    //! Get the input language for printing
    InputLanguage getInputLang() const;
    //! Get the output language for printing
    InputLanguage getOutputLang() const;
    //! Whether to print Expr's as DAGs
    bool dagPrinting() const { return *d_dagPrinting; }
    /*! @brief Return the pretty-printer if there is one; otherwise
       return NULL. */
    PrettyPrinter* getPrinter() const { return d_prettyPrinter; }
 
  /////////////////////////////////////////////////////////////////////////////
  // Kind registration                                                       //
  /////////////////////////////////////////////////////////////////////////////

    //! Register a new kind.
    /*! The kind may already be registered under the same name, but if
     *  the name is different, it's an error.
     * 
     * If the new kind is supposed to represent a type, set isType to true.
     */
    void newKind(int kind, const std::string &name, bool isType = false);
    //! Register the pretty-printer (can only do it if none registered)
    /*! The pointer is NOT owned by ExprManager. Delete it yourself.
     */
    void registerPrettyPrinter(PrettyPrinter& printer);
    //! Tell ExprManager that the printer is no longer valid
    void unregisterPrettyPrinter();
    /*! @brief Returns true if kind is built into CVC or has been registered
      via newKind. */
    bool isKindRegistered(int kind) { return d_kindMap.count(kind) > 0; }
    //! Check if a kind represents a type
    bool isTypeKind(int kind) { return d_typeKinds.count(kind) > 0; }

    /*! @brief Return the name associated with a kind.  The kind must
      already be registered. */
    const std::string& getKindName(int kind);
    //! Return a kind associated with a name.  Returns NULL_KIND if not found.
    int getKind(const std::string& name);
    //! Register a new subclass of ExprValue
    /*!
     * Takes the size (in bytes) of the new subclass and returns the
     * unique index of that subclass.  Subsequent calls to the
     * subclass's getMMIndex() must return that index.
     */
    size_t registerSubclass(size_t sizeOfSubclass);

  }; // end of class ExprManager


/*****************************************************************************/
/*!
 *\class ExprManagerNotifyObj
 *\brief Notifies ExprManager before and after each pop()
 *
 * Author: Sergey Berezin
 *
 * Created: Tue Mar  1 12:29:14 2005
 *
 * Disables the deletion of Exprs during context restoration
 * (backtracking).  This solves the problem of circular dependencies,
 * e.g. in find pointers.
 */
/*****************************************************************************/
  class ExprManagerNotifyObj: public ContextNotifyObj {
    ExprManager* d_em;
  public:
    //! Constructor
    ExprManagerNotifyObj(ExprManager* em, Context* cxt)
      : ContextNotifyObj(cxt), d_em(em) { }

    void notifyPre(void);
    void notify(void);
  };
    

} // end of namespace CVC3

// Include expr_value here for inline definitions
#include "expr_value.h"

namespace CVC3 {

inline Expr ExprManager::newLeafExpr(const Op& op)
{
  if (op.getExpr().isNull()) {
    ExprValue ev(this, op.getKind());
    return newExpr(&ev);
  }
  else {
    DebugAssert(op.getExpr().getEM() == this, "ExprManager mismatch");
    std::vector<Expr> kids;
    ExprApply ev(this, op, kids);
    return newExpr(&ev);
  }
}

inline Expr ExprManager::newStringExpr(const std::string &s)
  { ExprString ev(this, s); return newExpr(&ev); }

inline Expr ExprManager::newRatExpr(const Rational& r)
  { ExprRational ev(this, r); return newExpr(&ev); }

inline Expr ExprManager::newSkolemExpr(const Expr& e, int i)
  { DebugAssert(e.getEM() == this, "ExprManager mismatch");
    ExprSkolem ev(this, i, e); return newExpr(&ev); }

inline Expr ExprManager::newVarExpr(const std::string &s)
  { ExprVar ev(this, s); return newExpr(&ev); }

inline Expr ExprManager::newSymbolExpr(const std::string &s, int kind)
  { ExprSymbol ev(this, kind, s); return newExpr(&ev); }

inline Expr ExprManager::newBoundVarExpr(const std::string &name,
                                         const std::string& uid)
  { ExprBoundVar ev(this, name, uid); return newExpr(&ev); }

inline Expr ExprManager::newBoundVarExpr(const std::string& name,
                                         const std::string& uid,
                                         const Type& type) {
  Expr res = newBoundVarExpr(name, uid);
  DebugAssert(type.getExpr().getKind() != ARROW,"");
  DebugAssert(res.lookupType().isNull(), 
              "newBoundVarExpr: redefining a variable " + name);
  res.setType(type);
  return res;
}

inline Expr ExprManager::newBoundVarExpr(const Type& type) {
  static int nextNum = 0;
  std::string name("_cvc3_");
  std::string uid =  int2string(nextNum++);
  return newBoundVarExpr(name, uid, type);
}

inline Expr ExprManager::newClosureExpr(int kind,
                                        const std::vector<Expr>& vars,
                                        const Expr& body)
  { ExprClosure ev(this, kind, vars, body); return newExpr(&ev); }

inline Expr ExprManager::newTheoremExpr(const Theorem& thm)
  { ExprTheorem ev(this, thm); return newExpr(&ev); }

inline size_t ExprManager::hash(const ExprValue* ev) const {
  DebugAssert(ev!=NULL, "ExprManager::hash() called on a NULL ExprValue");
  return ev->hash();
}

inline bool ExprManager::EqEV::operator()(const ExprValue* ev1,
                                          const ExprValue* ev2) const {
  return (*ev1) == (*ev2);
}

inline size_t ExprManager::hash(const Expr& e) const {
  DebugAssert(!e.isNull(), "ExprManager::hash() called on a Null Expr");
  return e.d_expr->hash();
}
 
} // end of namespace CVC3

#endif