CVC3  2.4.1
assumptions.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file assumptions.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Dec 10 00:37:49 GMT 2002
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 // CLASS: Assumptions
21 //
22 // AUTHOR: Sergey Berezin, 12/03/2002
23 //
24 // Abstract:
25 //
26 // Mathematically, the value of class Assumptions is a set of pairs
27 // 'u:A' on the LHS of the Theorem's sequent. Both u and A are Expr.
28 //
29 // Null assumptions is almost always treated as the empty set. The
30 // only exception: iterators cannot be constructed for Null.
31 //
32 // This interface should be used as little as possible by the users of
33 // Theorem class.
34 ///////////////////////////////////////////////////////////////////////////////
35 #ifndef _cvc3__expr_h_
36 #include "expr.h"
37 #endif
38 
39 #ifndef _cvc3__assumptions_h_
40 #define _cvc3__assumptions_h_
41 
42 #include "theorem.h"
43 
44 namespace CVC3 {
45 
46  class Assumptions {
47  private:
48  std::vector<Theorem> d_vector;
50 
51  private:
52  // Private constructor for internal use. Assumes v != NULL.
53  // Assumptions(AssumptionsValue *v);
54 
55  // helper function for []
56  const Theorem& findTheorem(const Expr& e) const;
57 
58  static bool findExpr(const Assumptions& a, const Expr& e,
59  std::vector<Theorem>& gamma);
60  static bool findExprs(const Assumptions& a, const std::vector<Expr>& es,
61  std::vector<Theorem>& gamma);
62 
63  void add(const std::vector<Theorem>& thms);
64 
65  public:
66  //! Default constructor: no value is created
68  //! Constructor from a vector of theorems
69  Assumptions(const std::vector<Theorem>& v);
70  //! Constructor for one theorem (common case)
71  Assumptions(const Theorem& t) { d_vector.push_back(t); }
72  //! Constructor for two theorems (common case)
73  Assumptions(const Theorem& t1, const Theorem& t2);
74 
75  // Destructor
77  // Copy constructor.
78  Assumptions(const Assumptions &assump) : d_vector(assump.d_vector) {}
79  // Assignment.
81  { d_vector = assump.d_vector; return *this; }
82 
83  static const Assumptions& emptyAssump() { return s_empty; }
84 
85  void add1(const Theorem& t) {
86  DebugAssert(d_vector.empty(), "expected empty vector");
87  d_vector.push_back(t);
88  }
89  void add(const Theorem& t);
90  void add(const Assumptions& a) { add(a.d_vector); }
91  // clear the set of assumptions
92  void clear() { d_vector.clear(); }
93  // get the size
94  unsigned size() const { return d_vector.size(); }
95  bool empty() const { return d_vector.empty(); }
96 
97  // needed by TheoremValue
99  DebugAssert(size() > 0, "Expected size > 0");
100  return d_vector[0];
101  }
102 
103  // Print functions
104  std::string toString() const;
105  void print() const;
106 
107  // Return Assumption associated with the expression. The
108  // value will be Null if the assumption is not in the set.
109  //
110  // NOTE: do not try to assign anything to the result, it won't work.
111  const Theorem& operator[](const Expr& e) const;
112 
113  // find only searches through current set of assumptions, will not recurse
114  const Theorem& find(const Expr& e) const;
115 
116  //! Iterator for the Assumptions: points to class Theorem.
117  /*! Cannot inherit from vector<Theorem>::const_iterator in gcc 2.96 */
118  class iterator : public std::iterator<std::input_iterator_tag,Theorem,ptrdiff_t> {
119  // Let's be friends
120  friend class Assumptions;
121  private:
122  std::vector<Theorem>::const_iterator d_it;
123 
124  iterator(const std::vector<Theorem>::const_iterator& i): d_it(i) { }
125  public:
126  //! Default constructor
127  iterator() { }
128  //! Destructor
129  ~iterator() { }
130  //! Equality
131  bool operator==(const iterator& i) const { return (d_it == i.d_it); }
132  //! Disequality
133  bool operator!=(const iterator& i) const { return (d_it != i.d_it); }
134  //! Dereference operator
135  const Theorem& operator*() const { return *d_it; }
136  //! Member dereference operator
137  const Theorem* operator->() const { return &(operator*()); }
138  //! Prefix increment
139  iterator& operator++() { ++d_it; return *this; }
140  //! Proxy class for postfix increment
141  class Proxy {
142  const Theorem* d_t;
143  public:
144  Proxy(const Theorem& t) : d_t(&t) { }
145  const Theorem& operator*() { return *d_t; }
146  };
147  //! Postfix increment
148  Proxy operator++(int) { return Proxy(*(d_it++)); }
149  };
150 
151  iterator begin() const { return iterator(d_vector.begin()); }
152  iterator end() const { return iterator(d_vector.end()); }
153 
154  // Merging assumptions
155  // friend Assumptions operator+(const Assumptions& a1, const Assumptions& a2);
156 
157  //! Returns all (recursive) assumptions except e
158  friend Assumptions operator-(const Assumptions& a, const Expr& e);
159  //! Returns all (recursive) assumptions except those in es
160  friend Assumptions operator-(const Assumptions& a,
161  const std::vector<Expr>& es);
162 
163  friend std::ostream& operator<<(std::ostream& os,
164  const Assumptions &assump);
165 
166  friend bool operator==(const Assumptions& a1, const Assumptions& a2)
167  { return a1.d_vector == a2.d_vector; }
168  friend bool operator!=(const Assumptions& a1, const Assumptions& a2)
169  { return a1.d_vector != a2.d_vector; }
170 
171  }; // end of class Assumptions
172 
173 } // end of namespace CVC3
174 
175 #endif
Assumptions()
Default constructor: no value is created.
Definition: assumptions.h:67
iterator(const std::vector< Theorem >::const_iterator &i)
Definition: assumptions.h:124
iterator & operator++()
Prefix increment.
Definition: assumptions.h:139
friend std::ostream & operator<<(std::ostream &os, const Assumptions &assump)
const Theorem & find(const Expr &e) const
static bool findExprs(const Assumptions &a, const std::vector< Expr > &es, std::vector< Theorem > &gamma)
Definition: assumptions.cpp:92
Data structure of expressions in CVC3.
Definition: expr.h:133
friend Assumptions operator-(const Assumptions &a, const Expr &e)
Returns all (recursive) assumptions except e.
unsigned size() const
Definition: assumptions.h:94
iterator()
Default constructor.
Definition: assumptions.h:127
void add(const std::vector< Theorem > &thms)
static Assumptions s_empty
Definition: assumptions.h:49
Assumptions(const Assumptions &assump)
Definition: assumptions.h:78
const Theorem & findTheorem(const Expr &e) const
Definition: assumptions.cpp:34
const Theorem & operator[](const Expr &e) const
const Theorem & operator*() const
Dereference operator.
Definition: assumptions.h:135
#define DebugAssert(cond, str)
Definition: debug.h:408
Proxy operator++(int)
Postfix increment.
Definition: assumptions.h:148
iterator end() const
Definition: assumptions.h:152
Assumptions & operator=(const Assumptions &assump)
Definition: assumptions.h:80
bool operator!=(const iterator &i) const
Disequality.
Definition: assumptions.h:133
void print() const
iterator begin() const
Definition: assumptions.h:151
bool operator==(const iterator &i) const
Equality.
Definition: assumptions.h:131
const Theorem * operator->() const
Member dereference operator.
Definition: assumptions.h:137
Assumptions(const Theorem &t)
Constructor for one theorem (common case)
Definition: assumptions.h:71
Proxy class for postfix increment.
Definition: assumptions.h:141
friend bool operator!=(const Assumptions &a1, const Assumptions &a2)
Definition: assumptions.h:168
friend bool operator==(const Assumptions &a1, const Assumptions &a2)
Definition: assumptions.h:166
std::vector< Theorem > d_vector
Definition: assumptions.h:48
Theorem & getFirst()
Definition: assumptions.h:98
Definition of the API to expression package. See class Expr for details.
void add1(const Theorem &t)
Definition: assumptions.h:85
bool empty() const
Definition: assumptions.h:95
Iterator for the Assumptions: points to class Theorem.
Definition: assumptions.h:118
std::vector< Theorem >::const_iterator d_it
Definition: assumptions.h:122
Definition: expr.cpp:35
void add(const Assumptions &a)
Definition: assumptions.h:90
std::string toString() const
static const Assumptions & emptyAssump()
Definition: assumptions.h:83
static bool findExpr(const Assumptions &a, const Expr &e, std::vector< Theorem > &gamma)
Definition: assumptions.cpp:58