CVC3

assumptions.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file assumptions.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Dec 10 00:37:49 GMT 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // CLASS: Assumptions
00021 //
00022 // AUTHOR: Sergey Berezin, 12/03/2002
00023 //
00024 // Abstract:
00025 //
00026 // Mathematically, the value of class Assumptions is a set of pairs
00027 // 'u:A' on the LHS of the Theorem's sequent.  Both u and A are Expr.
00028 //
00029 // Null assumptions is almost always treated as the empty set.  The
00030 // only exception: iterators cannot be constructed for Null.
00031 //
00032 // This interface should be used as little as possible by the users of
00033 // Theorem class.
00034 ///////////////////////////////////////////////////////////////////////////////
00035 #ifndef _cvc3__expr_h_
00036 #include "expr.h"
00037 #endif
00038 
00039 #ifndef _cvc3__assumptions_h_
00040 #define _cvc3__assumptions_h_
00041 
00042 #include "theorem.h"
00043 
00044 namespace CVC3 {
00045 
00046   class Assumptions {
00047   private:
00048     std::vector<Theorem> d_vector;
00049     static Assumptions s_empty;
00050 
00051   private:
00052     // Private constructor for internal use.  Assumes v != NULL.
00053     //    Assumptions(AssumptionsValue *v);
00054 
00055     // helper function for []
00056     const Theorem& findTheorem(const Expr& e) const;
00057 
00058     static bool findExpr(const Assumptions& a, const Expr& e, 
00059        std::vector<Theorem>& gamma);
00060     static bool findExprs(const Assumptions& a, const std::vector<Expr>& es, 
00061         std::vector<Theorem>& gamma);
00062 
00063     void add(const std::vector<Theorem>& thms);
00064 
00065   public:
00066     //! Default constructor: no value is created
00067     Assumptions() { }
00068     //! Constructor from a vector of theorems
00069     Assumptions(const std::vector<Theorem>& v);
00070     //! Constructor for one theorem (common case)
00071     Assumptions(const Theorem& t) { d_vector.push_back(t); }
00072     //! Constructor for two theorems (common case)
00073     Assumptions(const Theorem& t1, const Theorem& t2);
00074 
00075     // Destructor
00076     ~Assumptions() {}
00077     // Copy constructor.
00078     Assumptions(const Assumptions &assump) : d_vector(assump.d_vector) {}
00079     // Assignment.
00080     Assumptions &operator=(const Assumptions &assump)
00081     { d_vector = assump.d_vector; return *this; }
00082 
00083     static const Assumptions& emptyAssump() { return s_empty; }
00084 
00085     void add1(const Theorem& t) {
00086       DebugAssert(d_vector.empty(), "expected empty vector");
00087       d_vector.push_back(t);
00088     }
00089     void add(const Theorem& t);
00090     void add(const Assumptions& a) { add(a.d_vector); }
00091     // clear the set of assumptions
00092     void clear() { d_vector.clear(); }
00093     // get the size
00094     unsigned size() const { return d_vector.size(); }
00095     bool empty() const { return d_vector.empty(); }
00096 
00097     // needed by TheoremValue
00098     Theorem& getFirst() {
00099       DebugAssert(size() > 0, "Expected size > 0");
00100       return d_vector[0];
00101     }
00102     
00103     // Print functions
00104     std::string toString() const;
00105     void print() const;
00106 
00107     // Return Assumption associated with the expression.  The
00108     // value will be Null if the assumption is not in the set.
00109     //
00110     // NOTE: do not try to assign anything to the result, it won't work.
00111     const Theorem& operator[](const Expr& e) const;
00112 
00113     // find only searches through current set of assumptions, will not recurse
00114     const Theorem& find(const Expr& e) const;
00115 
00116     //! Iterator for the Assumptions: points to class Theorem.
00117     /*! Cannot inherit from vector<Theorem>::const_iterator in gcc 2.96 */
00118     class iterator : public std::iterator<std::input_iterator_tag,Theorem,ptrdiff_t> {
00119       // Let's be friends
00120       friend class Assumptions;
00121     private:
00122       std::vector<Theorem>::const_iterator d_it;
00123 
00124       iterator(const std::vector<Theorem>::const_iterator& i): d_it(i) { }
00125     public:
00126       //! Default constructor
00127       iterator() { }
00128       //! Destructor
00129       ~iterator() { }
00130       //! Equality
00131       bool operator==(const iterator& i) const { return (d_it == i.d_it); }
00132       //! Disequality
00133       bool operator!=(const iterator& i) const { return (d_it != i.d_it); }
00134       //! Dereference operator
00135       const Theorem& operator*() const { return *d_it; }
00136       //! Member dereference operator
00137       const Theorem* operator->() const { return &(operator*()); }
00138       //! Prefix increment
00139       iterator& operator++() { ++d_it; return *this; }
00140       //! Proxy class for postfix increment
00141       class Proxy {
00142   const Theorem* d_t;
00143       public:
00144   Proxy(const Theorem& t) : d_t(&t) { }
00145   const Theorem& operator*() { return *d_t; }
00146       };
00147       //! Postfix increment
00148       Proxy operator++(int) { return Proxy(*(d_it++)); }
00149     };
00150 
00151     iterator begin() const { return iterator(d_vector.begin()); }
00152     iterator end() const { return iterator(d_vector.end()); }
00153 
00154     // Merging assumptions
00155     //    friend Assumptions operator+(const Assumptions& a1, const Assumptions& a2);
00156 
00157     //! Returns all (recursive) assumptions except e
00158     friend Assumptions operator-(const Assumptions& a, const Expr& e);
00159     //! Returns all (recursive) assumptions except those in es
00160     friend Assumptions operator-(const Assumptions& a,
00161                                  const std::vector<Expr>& es);
00162 
00163     friend std::ostream& operator<<(std::ostream& os,
00164                                     const Assumptions &assump);
00165 
00166     friend bool operator==(const Assumptions& a1, const Assumptions& a2)
00167     { return a1.d_vector == a2.d_vector; }
00168     friend bool operator!=(const Assumptions& a1, const Assumptions& a2)
00169     { return a1.d_vector != a2.d_vector; }
00170 
00171   }; // end of class Assumptions
00172 
00173 } // end of namespace CVC3
00174 
00175 #endif