assumptions.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file assumptions.h
 * 
 * Author: Sergey Berezin
 * 
 * Created: Dec 10 00:37:49 GMT 2002
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/
// CLASS: Assumptions
//
// AUTHOR: Sergey Berezin, 12/03/2002
//
// Abstract:
//
// Mathematically, the value of class Assumptions is a set of pairs
// 'u:A' on the LHS of the Theorem's sequent.  Both u and A are Expr.
//
// Null assumptions is almost always treated as the empty set.  The
// only exception: iterators cannot be constructed for Null.
//
// This interface should be used as little as possible by the users of
// Theorem class.
///////////////////////////////////////////////////////////////////////////////
#ifndef _CVC_lite__expr_h_
#include "expr.h"
#endif

#ifndef _CVC_lite__assumptions_h_
#define _CVC_lite__assumptions_h_

namespace CVCL {

  //class Theorem;
  class AssumptionsValue;
  class AVHash;

  class Assumptions {
  private:
    AssumptionsValue *d_val;

  private:
    // Private constructor for internal use.  Assumes v != NULL.
    Assumptions(AssumptionsValue *v);

    // helper function for []
    const Theorem& findTheorem(const Expr& e) const; 

    static bool findExpr(const Assumptions& a, const Expr& e, 
                         std::vector<Theorem>& gamma);
    static bool findExprs(const Assumptions& a, const std::vector<Expr>& es, 
                          std::vector<Theorem>& gamma);

  public:
    //! Default constructor: no value is created
    Assumptions() : d_val(NULL) { }
    //! Constructor from a vector of theorems
    Assumptions(const std::vector<Theorem>& v);
    //! Constructor for one theorem (common case)
    Assumptions(const Theorem& t);
    //! Constructor for two theorems (common case)
    Assumptions(const Theorem& t1, const Theorem& t2);

    // Destructor
    ~Assumptions();
    // Copy constructor.  IMPORTANT: it does NOT create a clean copy
    // of the set, but only copies the pointer.  Modifying the copy
    // will modify the original value!  Use copy() for cloning.
    Assumptions(const Assumptions &assump);
    // Assignment.
    Assumptions &operator=(const Assumptions &assump);

    bool isNull() const { return d_val == NULL; }
    // If we are Null, create a new empty AssumptionsValue.  Otherwise
    // do nothing.
    void init();
    // Create a clean copy of Assumptions, completely independent of
    // the original one
    Assumptions copy() const;
    // Add a new assumption.  If label is not supplied, generate a new one.
    // If we are Null, the initialization happens.
    void add(const Theorem& t);
    void add(const Assumptions& a);
    // clear the set of assumptions
    void clear();
    // get the size
    int size() const;
    bool empty() const;
    // Check / set the flag indicating that the value is constant
    bool isConst() const;
    void setConst();
    
    // Print functions
    std::string toString() const;
    void print() const;

    // Return Assumption associated with the expression.  The
    // value will be Null if the assumption is not in the set.
    //
    // NOTE: do not try to assign anything to the result, it won't work.
    const Theorem& operator[](const Expr& e) const;

    // find only searches through current set of assumptions, will not recurse
    const Theorem& find(const Expr& e) const;

    //! Iterator for the Assumptions: points to class Theorem.
    /*! Cannot inherit from vector<Theorem>::const_iterator in gcc 2.96 */
    class iterator : public std::iterator<std::input_iterator_tag,Theorem,ptrdiff_t> {
      // Let's be friends
      friend class Assumptions;
    private:
      std::vector<Theorem>::const_iterator d_it;

      iterator(const std::vector<Theorem>::const_iterator& i): d_it(i) { }
    public:
      //! Default constructor
      iterator() { }
      //! Destructor
      ~iterator() { }
      //! Equality
      bool operator==(const iterator& i) const { return (d_it == i.d_it); }
      //! Disequality
      bool operator!=(const iterator& i) const { return (d_it != i.d_it); }
      //! Dereference operator
      const Theorem& operator*() const { return *d_it; }
      //! Member dereference operator
      const Theorem* operator->() const { return &(operator*()); }
      //! Prefix increment
      iterator& operator++();
      //! Proxy class for postfix increment
      class Proxy {
        const Theorem* d_t;
      public:
        Proxy(const Theorem& t) : d_t(&t) { }
        const Theorem& operator*() { return *d_t; }
      };
      //! Postfix increment
      Proxy operator++(int);
    };

    iterator begin() const;
    iterator end() const;

    // Adding from iterators
    void add(const iterator& it) { add(*it); }

    // Merging assumptions
    //    friend Assumptions operator+(const Assumptions& a1, const Assumptions& a2);

    //! Returns all (recursive) assumptions except e
    friend Assumptions operator-(const Assumptions& a, const Expr& e);
    //! Returns all (recursive) assumptions except those in es
    friend Assumptions operator-(const Assumptions& a,
                                 const std::vector<Expr>& es);

    friend std::ostream& operator<<(std::ostream& os,
                                    const Assumptions &assump);

    friend bool operator==(const Assumptions& a1, const Assumptions& a2);
    friend bool operator!=(const Assumptions& a1, const Assumptions& a2);

  }; // end of class Assumptions

} // end of namespace CVCL

#endif

---