CVC3  2.4.1
expr_op.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr_op.h
4  * \brief Class Op representing the Expr's operator.
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Fri Feb 7 15:14:42 2003
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 // expr.h Has to be included outside of #ifndef, since it sources us
23 // recursively (read comments in expr_value.h).
24 #ifndef _cvc3__expr_h_
25 #include "expr.h"
26 #endif
27 
28 #ifndef _cvc3__expr_op_h_
29 #define _cvc3__expr_op_h_
30 
31 namespace CVC3 {
32 
33  class ExprManager;
34 
35 ///////////////////////////////////////////////////////////////////////////////
36 // //
37 // Class: Op //
38 // Author: Clark Barrett //
39 // Created: Wed Nov 27 15:50:38 2002 //
40 // Description: Encapsulates all possible Expr operators (including UFUNC) //
41 // and allows switching on the kind. //
42 // Kinds should be registered with ExprManager. //
43 //
44 // Technically, class Op is not part of Expr; it is provided as an
45 // abstraction for the user. So, building an Expr from an Op is less
46 // efficient than building the same Expr directly from the kind.
47 ///////////////////////////////////////////////////////////////////////////////
48 class Op {
49  friend class Expr;
50  friend class ExprApply;
51  friend class ExprApplyTmp;
52  friend class ::CInterface;
53 
54  int d_kind;
56 
57  // Disallow silent conversion of expr to op
58  //! Constructor for operators
59  Op(const Expr& e): d_kind(APPLY), d_expr(e) { }
60 
61 public:
62 /////////////////////////////////////////////////////////////////////////
63 // Public methods
64 /////////////////////////////////////////////////////////////////////////
65 
66  Op() : d_kind(NULL_KIND) { }
67  // Construct an operator from a kind.
68  Op(int kind) : d_kind(kind), d_expr()
69  { DebugAssert(kind != APPLY, "APPLY cannot be an operator on its own"); }
70  // Copy constructor
71  Op(const Op& op): d_kind(op.d_kind), d_expr(op.d_expr) { }
72  // A constructor that rebuilds the Op for the given ExprManager
73  Op(ExprManager* em, const Op& op);
74  // Destructor (does nothing)
75  ~Op() { }
76  // Assignment operator
77  Op& operator=(const Op& op);
78 
79  // Check if Op is NULL
80  bool isNull() const { return d_kind == NULL_KIND; }
81  // Return the kind of the operator
82  int getKind() const { return d_kind; }
83  // Return the expr associated with this operator if applicable.
84  const Expr& getExpr() const
85  { DebugAssert(d_kind == APPLY, "Expected APPLY"); return d_expr; }
86 
87  // Printing functions.
88 
89  std::string toString() const;
90  friend std::ostream& operator<<(std::ostream& os, const Op& op) {
91  return os << "Op(" << op.d_kind << " " << op.d_expr << ")";
92  }
93  friend bool operator==(const Op& op1, const Op& op2) {
94  return op1.d_kind == op2.d_kind && op1.d_expr == op2.d_expr;
95  }
96 
97 }; // end of class Op
98 
99 
100 } // end of namespace CVC3
101 
102 #endif
Op()
Definition: expr_op.h:66
const Expr & getExpr() const
Definition: expr_op.h:84
Op(const Expr &e)
Constructor for operators.
Definition: expr_op.h:59
Data structure of expressions in CVC3.
Definition: expr.h:133
friend bool operator==(const Op &op1, const Op &op2)
Definition: expr_op.h:93
#define DebugAssert(cond, str)
Definition: debug.h:408
Op(int kind)
Definition: expr_op.h:68
Expr d_expr
Definition: expr_op.h:55
Op(const Op &op)
Definition: expr_op.h:71
Op & operator=(const Op &op)
Definition: expr_op.cpp:31
int getKind() const
Definition: expr_op.h:82
std::string toString() const
Definition: expr_op.cpp:38
Expression Manager.
Definition: expr_manager.h:58
Definition: kinds.h:90
Definition of the API to expression package. See class Expr for details.
bool isNull() const
Definition: expr_op.h:80
friend std::ostream & operator<<(std::ostream &os, const Op &op)
Definition: expr_op.h:90
~Op()
Definition: expr_op.h:75
int d_kind
Definition: expr_op.h:54