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 namespace CVC3 {
00043 
00044   class Assumptions {
00045   private:
00046     std::vector<Theorem> d_vector;
00047     static Assumptions s_empty;
00048 
00049   private:
00050     // Private constructor for internal use.  Assumes v != NULL.
00051     //    Assumptions(AssumptionsValue *v);
00052 
00053     // helper function for []
00054     const Theorem& findTheorem(const Expr& e) const;
00055 
00056     static bool findExpr(const Assumptions& a, const Expr& e, 
00057        std::vector<Theorem>& gamma);
00058     static bool findExprs(const Assumptions& a, const std::vector<Expr>& es, 
00059         std::vector<Theorem>& gamma);
00060 
00061     void add(const std::vector<Theorem>& thms);
00062 
00063   public:
00064     //! Default constructor: no value is created
00065     Assumptions() { }
00066     //! Constructor from a vector of theorems
00067     Assumptions(const std::vector<Theorem>& v);
00068     //! Constructor for one theorem (common case)
00069     Assumptions(const Theorem& t) { d_vector.push_back(t); }
00070     //! Constructor for two theorems (common case)
00071     Assumptions(const Theorem& t1, const Theorem& t2);
00072 
00073     // Destructor
00074     ~Assumptions() {}
00075     // Copy constructor.
00076     Assumptions(const Assumptions &assump) : d_vector(assump.d_vector) {}
00077     // Assignment.
00078     Assumptions &operator=(const Assumptions &assump)
00079     { d_vector = assump.d_vector; return *this; }
00080 
00081     static const Assumptions& emptyAssump() { return s_empty; }
00082 
00083     void add1(const Theorem& t) {
00084       DebugAssert(d_vector.empty(), "expected empty vector");
00085       d_vector.push_back(t);
00086     }
00087     void add(const Theorem& t);
00088     void add(const Assumptions& a) { add(a.d_vector); }
00089     // clear the set of assumptions
00090     void clear() { d_vector.clear(); }
00091     // get the size
00092     unsigned size() const { return d_vector.size(); }
00093     bool empty() const { return d_vector.empty(); }
00094 
00095     // needed by TheoremValue
00096     Theorem& getFirst() {
00097       DebugAssert(size() > 0, "Expected size > 0");
00098       return d_vector[0];
00099     }
00100     
00101     // Print functions
00102     std::string toString() const;
00103     void print() const;
00104 
00105     // Return Assumption associated with the expression.  The
00106     // value will be Null if the assumption is not in the set.
00107     //
00108     // NOTE: do not try to assign anything to the result, it won't work.
00109     const Theorem& operator[](const Expr& e) const;
00110 
00111     // find only searches through current set of assumptions, will not recurse
00112     const Theorem& find(const Expr& e) const;
00113 
00114     //! Iterator for the Assumptions: points to class Theorem.
00115     /*! Cannot inherit from vector<Theorem>::const_iterator in gcc 2.96 */
00116     class iterator : public std::iterator<std::input_iterator_tag,Theorem,ptrdiff_t> {
00117       // Let's be friends
00118       friend class Assumptions;
00119     private:
00120       std::vector<Theorem>::const_iterator d_it;
00121 
00122       iterator(const std::vector<Theorem>::const_iterator& i): d_it(i) { }
00123     public:
00124       //! Default constructor
00125       iterator() { }
00126       //! Destructor
00127       ~iterator() { }
00128       //! Equality
00129       bool operator==(const iterator& i) const { return (d_it == i.d_it); }
00130       //! Disequality
00131       bool operator!=(const iterator& i) const { return (d_it != i.d_it); }
00132       //! Dereference operator
00133       const Theorem& operator*() const { return *d_it; }
00134       //! Member dereference operator
00135       const Theorem* operator->() const { return &(operator*()); }
00136       //! Prefix increment
00137       iterator& operator++() { ++d_it; return *this; }
00138       //! Proxy class for postfix increment
00139       class Proxy {
00140   const Theorem* d_t;
00141       public:
00142   Proxy(const Theorem& t) : d_t(&t) { }
00143   const Theorem& operator*() { return *d_t; }
00144       };
00145       //! Postfix increment
00146       Proxy operator++(int) { return Proxy(*(d_it++)); }
00147     };
00148 
00149     iterator begin() const { return iterator(d_vector.begin()); }
00150     iterator end() const { return iterator(d_vector.end()); }
00151 
00152     // Merging assumptions
00153     //    friend Assumptions operator+(const Assumptions& a1, const Assumptions& a2);
00154 
00155     //! Returns all (recursive) assumptions except e
00156     friend Assumptions operator-(const Assumptions& a, const Expr& e);
00157     //! Returns all (recursive) assumptions except those in es
00158     friend Assumptions operator-(const Assumptions& a,
00159                                  const std::vector<Expr>& es);
00160 
00161     friend std::ostream& operator<<(std::ostream& os,
00162                                     const Assumptions &assump);
00163 
00164     friend bool operator==(const Assumptions& a1, const Assumptions& a2)
00165     { return a1.d_vector == a2.d_vector; }
00166     friend bool operator!=(const Assumptions& a1, const Assumptions& a2)
00167     { return a1.d_vector != a2.d_vector; }
00168 
00169   }; // end of class Assumptions
00170 
00171 } // end of namespace CVC3
00172 
00173 #endif

Generated on Tue Jul 3 14:33:34 2007 for CVC3 by  doxygen 1.5.1