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: AssumptionsValue
//
// 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.
///////////////////////////////////////////////////////////////////////////////

#include "expr.h"

#ifndef _CVC_lite__assumptions_h_
#define _CVC_lite__assumptions_h_

#include <iostream>
#include <functional>
#include <iterator>
#include <vector>
// #include "theorem.h"
// #include "proof.h"
// #include "assumptions_value.h"

namespace CVCL {

  //class Theorem;
  class AssumptionsValue;
  class AVHash;

  class Assumptions {
  private:
    AssumptionsValue *d_val;
    // Private constructors for internal use.  Assumes v != NULL.
    Assumptions(AssumptionsValue *v);

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

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


  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);

    // Desctructor
    ~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);
//     void add(const Expr &e);
//     void add(const Expr& e, int level);
//     void add(const Expr& e, int level, const Proof& label);
    // Remove the assumption A from the set.  'A' does not have to be
    // in the set.
    // Note, that even if the set becomes empty, the value remains non-Null.
    //void erase(const Expr &e); // TODO: remove or change to remove parent?
    // Similarly, erase a set of assumptions at once
    //void erase(const Theorem &t);
    //void erase(const Assumptions& a);
    // 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;

    // clear the set of assumptions
    void clear();

    // get the size
    int size() 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);
    }

//     size_t size()  const { return (d_val)? d_val->d_map.size() : 0; }
    bool empty() const;

    // Check / set the flag indicating that the value is constant
    bool isConst() const;
    void setConst();

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

    friend Assumptions operator-(const Assumptions& a1,
                                 const Assumptions& a2);

    // returns all assumptions except e or es
    // functions will do recursive graph traversal
    friend Assumptions operator-(const Assumptions& a,
                                  const Expr& e);
    friend Assumptions operator-(const Assumptions& a,
                                 const std::vector<Expr>& es);

    // Print functions
    std::string toString() const;

    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);

    void print() const;
  }; // end of class Assumptions

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

  // comparison operators
  inline bool operator==(const Assumptions& a1, const Assumptions& a2) {
    if (a1.d_val == a2.d_val) return true;
    if (a1.d_val == NULL || a2.d_val == NULL) return false;
    return (*a1.d_val == *a2.d_val);
  }

  inline bool operator!=(const Assumptions& a1, const Assumptions& a2) { 
    if (a1.d_val == a2.d_val) return false;
    if (a1.d_val == NULL || a2.d_val == NULL) return true;
    return (*a1.d_val != *a2.d_val);
  }

} // end of namespace CVCL

#endif

---