CVC3

expr_op.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_op.h
00004  * \brief Class Op representing the Expr's operator.
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Fri Feb  7 15:14:42 2003
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 // expr.h Has to be included outside of #ifndef, since it sources us
00023 // recursively (read comments in expr_value.h).
00024 #ifndef _cvc3__expr_h_
00025 #include "expr.h"
00026 #endif
00027 
00028 #ifndef _cvc3__expr_op_h_
00029 #define _cvc3__expr_op_h_
00030 
00031 namespace CVC3 {
00032 
00033   class ExprManager;
00034 
00035 ///////////////////////////////////////////////////////////////////////////////
00036 //                                                                           //
00037 // Class: Op                     //
00038 // Author: Clark Barrett                                                     //
00039 // Created: Wed Nov 27 15:50:38 2002               //
00040 // Description: Encapsulates all possible Expr operators (including UFUNC)   //
00041 //              and allows switching on the kind.                            //
00042 //              Kinds should be registered with ExprManager.                 //
00043 // 
00044 // Technically, class Op is not part of Expr; it is provided as an
00045 // abstraction for the user.  So, building an Expr from an Op is less
00046 // efficient than building the same Expr directly from the kind.
00047 ///////////////////////////////////////////////////////////////////////////////
00048 class Op {
00049   friend class Expr;
00050   friend class ExprApply;
00051   friend class ExprApplyTmp;
00052   friend class ::CInterface;
00053 
00054   int d_kind;
00055   Expr d_expr;
00056 
00057   // Disallow silent conversion of expr to op
00058   //! Constructor for operators
00059   Op(const Expr& e): d_kind(APPLY), d_expr(e) { }
00060 
00061 public:
00062 /////////////////////////////////////////////////////////////////////////
00063 // Public methods
00064 /////////////////////////////////////////////////////////////////////////
00065 
00066   Op() : d_kind(NULL_KIND) { }
00067   // Construct an operator from a kind.
00068   Op(int kind) : d_kind(kind), d_expr()
00069     { DebugAssert(kind != APPLY, "APPLY cannot be an operator on its own"); }
00070   // Copy constructor
00071   Op(const Op& op): d_kind(op.d_kind), d_expr(op.d_expr) { }
00072   // A constructor that rebuilds the Op for the given ExprManager
00073   Op(ExprManager* em, const Op& op);
00074   // Destructor (does nothing)
00075   ~Op() { }
00076   // Assignment operator
00077   Op& operator=(const Op& op);
00078 
00079   // Check if Op is NULL
00080   bool isNull() const { return d_kind == NULL_KIND; }
00081   // Return the kind of the operator
00082   int getKind() const { return d_kind; }
00083   // Return the expr associated with this operator if applicable.
00084   const Expr& getExpr() const
00085     { DebugAssert(d_kind == APPLY, "Expected APPLY"); return d_expr; }
00086 
00087   // Printing functions.
00088 
00089   std::string toString() const;
00090   friend std::ostream& operator<<(std::ostream& os, const Op& op) {
00091     return os << "Op(" << op.d_kind << " " << op.d_expr << ")";
00092   }
00093   friend bool operator==(const Op& op1, const Op& op2) {
00094     return op1.d_kind == op2.d_kind && op1.d_expr == op2.d_expr;
00095   }
00096 
00097 }; // end of class Op
00098 
00099 
00100 } // end of namespace CVC3
00101 
00102 #endif