CVC3  2.4.1
notifylist.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file notifylist.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Mon Jan 20 13:52:19 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__notifylist_h_
22 #define _cvc3__include__notifylist_h_
23 
24 #include "expr.h"
25 #include "cdlist.h"
26 
27 namespace CVC3 {
28 
29  class Theory;
30 
31 class NotifyList {
34 
35 public:
37  IF_DEBUG(d_elist.setName("CDList[NotifyList]");)
38  }
39  unsigned size() const { return d_tlist.size(); }
40  void add(Theory* t, const Expr& e) { d_tlist.push_back(t); d_elist.push_back(e); }
41  Theory* getTheory(int i) const { return d_tlist[i]; }
42  Expr getExpr(int i) const { return d_elist[i]; }
43 };
44 
45 }
46 
47 #endif
Data structure of expressions in CVC3.
Definition: expr.h:133
NotifyList(Context *c)
Definition: notifylist.h:36
unsigned size() const
Definition: notifylist.h:39
Base class for theories.
Definition: theory.h:64
Expr getExpr(int i) const
Definition: notifylist.h:42
Theory * getTheory(int i) const
Definition: notifylist.h:41
T & push_back(const T &data, int scope=-1)
Definition: cdlist.h:66
void add(Theory *t, const Expr &e)
Definition: notifylist.h:40
#define IF_DEBUG(code)
Definition: debug.h:406
Definition of the API to expression package. See class Expr for details.
CDList< Expr > d_elist
Definition: notifylist.h:33
CDList< Theory * > d_tlist
Definition: notifylist.h:32