assumptions_value.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file assumptions_value.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>
 * 
 */
/*****************************************************************************/

#ifndef _CVC_lite__assumptions_value_h_
#define _CVC_lite__assumptions_value_h_

#include "theorem.h"

namespace CVCL {

  class AssumptionsValue;

  class AVHash {
    std::hash<size_t> h;
  public:
    AVHash() {
      IF_DEBUG(if(sizeof(void*) != sizeof(size_t)) {
        debugger.flag("WARNING: sizeof(void*) != sizeof(size_t)")++;
      });
    }
    size_t operator()(const AssumptionsValue* p) const { return h((size_t)p); }
  };

  class AssumptionsValue {
    friend class Assumptions;
  private:
    int d_refcount;
    // When this flag is set, the set of assumptions cannot be changed
    bool d_const;
    std::vector<Theorem> d_vector;

  private:
    //! Constructor
    AssumptionsValue(int refcount=0): d_refcount(refcount), d_const(false) { }
    //! Copy constructor: reset d_const flag and refcount
    AssumptionsValue(const AssumptionsValue& a)
      : d_refcount(0), d_const(false), d_vector(a.d_vector) { }
    /*!
     * Creates the set of assumptions from a vector of theorems.  Theorems that
     * do not have premises are not included, since they are valid without any
     * context and thus do not add any information in the assumption tracking.
     */
    AssumptionsValue(const std::vector<Theorem>& v);
    //! Constructor from two theorems (optimized for common case)
    AssumptionsValue(const Theorem& t1, const Theorem& t2);
  
    static void mergeVectors(const std::vector<Theorem>& v1,
                             const std::vector<Theorem>& v2,
                             std::vector<Theorem>& v);

    // Add a new assumption.  If label is not supplied, generate new one.
    void add(const Theorem& t);
    // Add a whole set of assumptions
    void add(const AssumptionsValue& a);
    // Return the assumption for the given formula.  It may be Null if
    // the assumption is not in the set.
    // find only searches through current set of assumptions, will not recurse
    const Theorem& find(const Expr& e) const;

  public:
    std::string toString() const;

    friend std::ostream& operator<<(std::ostream& os,
                                    const AssumptionsValue &assump);
      
    friend bool operator==(const AssumptionsValue& a1, const AssumptionsValue& a2);
    friend bool operator!=(const AssumptionsValue& a1, const AssumptionsValue& a2);

  }; // end of class AssumptionsValue

  // comparison operators
  inline bool operator==(const AssumptionsValue& a1, const AssumptionsValue& a2) {
    return (a1.d_vector == a2.d_vector);
  }

  inline bool operator!=(const AssumptionsValue& a1, const AssumptionsValue& a2) { 
    return !(a1.d_vector == a2.d_vector);
  }

} // end of namespace CVCL

#endif

---