theorem_value.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theorem_value.h
 * 
 * Author: Sergey Berezin
 * 
 * Created: Dec 10 01:03:34 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: TheoremValue
//
// AUTHOR: Sergey Berezin, 07/05/02
//
// Abstract:
//
// A class representing a proven fact in CVC.  It stores the theorem
// as a CVC expression, and in the appropriate modes also the set of
// assumptions and the proof.
//
// The idea is to allow only a few trusted classes to create values of
// this class.  If all the critical computations in the decision
// procedures are done through the use of Theorems, then soundness of
// these decision procedures will rely only on the soundness of the
// methods in the trusted classes (the inference rules).
//
// Thus, proof checking can effectively be done at run-time on the
// fly.  Or the soundness may be potentially proven by static analysis
// and many run-time checks can then be optimized away.
//
// This theorem_value.h file should NOT be used by the decision
// procedures.  Use theorem.h instead.
//
////////////////////////////////////////////////////////////////////////

#ifndef _CVC_lite__theorem_value_h_
#define _CVC_lite__theorem_value_h_

#include "theorem.h"
#include "theorem_manager.h"

namespace CVCL {

  class TheoremValue
  {
    // These are the only classes that can create new TheoremValue classes
    friend class Theorem;
    friend class RWTheoremValue;
    friend class ReflexivityTheoremValue;

  protected:
    //! Theorem Manager
    TheoremManager* d_tm;

    //! The expression representing a theorem
    Expr d_thm;

    //! The assumptions for the theorem
    Assumptions d_assump;

    //! Proof of the theorem
    Proof d_proof;

    //! How many pointers to this theorem value
    int d_refcount : 16;

    //! Largest scope level of the assumptions
    int d_scopeLevel : 16;

    //! Temporary flag used during traversals
    unsigned d_flag;

    //! Temporary cache used during traversals
    int d_cachedValue : 29;

    bool d_isAssump : 1;
    bool d_expand : 1; //!< whether it should this be expanded in graph traversal
    bool d_clauselit : 1;  //!< whether it belongs to the conflict clause


  private:
    // Constructor.   
    /*!
     * NOTE: it is private; only friend classes can call it.
     *
     * If the assumptions refer to only one theorem, grab the
     * assumptions of that theorem instead.
     */
    TheoremValue(TheoremManager* tm, const Expr &thm,
                 const Assumptions& assump, const Proof& pf, 
                 bool isAssump, int scope = -1) :
      d_tm(tm), d_thm(thm), d_proof(pf), d_refcount(0),
      d_scopeLevel(0), d_flag(0), d_isAssump(isAssump) {
      DebugAssert(d_tm->isActive(), "TheoremValue()");
      if (isAssump) {
        if (scope == -1) d_scopeLevel = tm->getCM()->scopeLevel();
        else d_scopeLevel = scope;
      }
      else {
        d_assump = assump;
        d_assump.setConst(); // Make assumptions constant
        if (!d_assump.isNull() && !d_assump.empty()) {
          //TODO: this is probably inefficient
          const Assumptions::iterator iend = d_assump.end();
          for (Assumptions::iterator i = d_assump.begin(); 
               i != iend; ++i)
            if (i->getScope() > d_scopeLevel)
              d_scopeLevel = i->getScope();
        }
      }
    }
    // Disable copy constructor and assignment
    TheoremValue(const TheoremValue& t) {
      FatalAssert(false, "TheoremValue() copy constructor called");
    }
    TheoremValue& operator=(const TheoremValue& t) {
      FatalAssert(false, "TheoremValue assignment operator called");
      return *this;
    }

    bool isFlagged() const {
      return d_flag == d_tm->getFlag();
    }

    void clearAllFlags() {
      d_tm->clearAllFlags();
    }
    
    void setFlag() {
      d_flag = d_tm->getFlag();
    }

    void setCachedValue(int value) {
      d_cachedValue = value;
    }

    int getCachedValue() const {
      return d_cachedValue;
    }

    void setExpandFlag(bool val) {
      d_expand = val;
    }

    bool getExpandFlag() {
      return d_expand;
    }
    
    void setLitFlag(bool val) {
      d_clauselit = val;
    }

    bool getLitFlag() {
      return d_clauselit;
    }

    int getScope() {
      return d_scopeLevel;
    }

//     virtual bool isRewrite() const { return d_thm.isEq() || d_thm.isIff(); }
    virtual bool isRewrite() const { return false; }

    virtual const Expr& getExpr() const { return d_thm; }
    virtual const Expr& getLHS() const {
      //      TRACE("getExpr","TheoremValue::getLHS called (",d_thm,")");
      DebugAssert(isRewrite(),
                  "TheoremValue::getLHS() called on non-rewrite theorem:\n"
                  +toString());
      return d_thm[0];
    }
    virtual const Expr& getRHS() const {
      //      TRACE("getExpr","TheoremValue::getRHS called (",d_thm,")");
      DebugAssert(isRewrite(),
                  "TheoremValue::getRHS() called on non-rewrite theorem:\n"
                  +toString());
      return d_thm[1];
    }

    const Assumptions& getAssumptionsRef() const { return d_assump; }

    bool isAssump() const { return d_isAssump; }
    const Proof& getProof() { return d_proof; }

  public:
    // Destructor
    virtual ~TheoremValue() { 
      DebugAssert(d_refcount == 0,
                  "Thm::TheoremValue::~TheoremValue(): refcount != 0.");
    }

    std::string toString() const {
      return d_assump.toString() + " |- " + getExpr().toString();
    }

    // Memory management
    virtual MemoryManager* getMM() { return d_tm->getMM(); }

    void* operator new(size_t size, MemoryManager* mm) {
      return mm->newData(size);
    }

    void operator delete(void* d) { }

  }; // end of class TheoremValue

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: RWTheoremValue                                                     //
// Author: Clark Barrett                                                     //
// Created: Fri May  2 12:51:55 2003                                         //
// Description: A special subclass for theorems of the form A |- t=t' or     //
//              A |- phi iff phi'.  The actual Expr is only created on       //
//              demand.  The idea is that getLHS and getRHS should be used   //
//              whenever possible, avoiding creating unnecessary Expr's.     //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
  class RWTheoremValue :public TheoremValue
  {
    friend class Theorem;

  protected:
    // d_thm in the base class contains the full expression, which is
    // only constructed on demand.
    Expr d_lhs;
    Expr d_rhs;

  private:
    // Constructor.   NOTE: it is private; only friend classes can call it.
    RWTheoremValue(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
                   const Assumptions& assump, const Proof& pf, bool isAssump,
                   int scope = -1)
      : TheoremValue(tm, Expr(), assump, pf, isAssump, scope),
        d_lhs(lhs), d_rhs(rhs) { }

    // Sometimes we have the full expression already created
    RWTheoremValue(TheoremManager* tm, const Expr& thm,
                   const Assumptions& assump, const Proof& pf, bool isAssump,
                   int scope = -1)
      : TheoremValue(tm, thm, assump, pf, isAssump, scope),
        d_lhs(thm[0]), d_rhs(thm[1]) { }

    const Expr& getExpr() const {
      if (d_thm.isNull()) {
        bool isBool = d_lhs.getType().isBool();
        // have to fake out the const qualifier
        Expr* pexpr = const_cast<Expr*>(&d_thm);
        *pexpr = isBool ? d_lhs.iffExpr(d_rhs) : d_lhs.eqExpr(d_rhs);
        //      TRACE("getExpr", "getExpr called on RWTheorem (", d_thm, ")");
      }
      return d_thm;
    }

    const Expr& getLHS() const { return d_lhs; }
    const Expr& getRHS() const { return d_rhs; }

  public:
    // Destructor
    ~RWTheoremValue() {}

    bool isRewrite() const { return true; }

    // Memory management
    MemoryManager* getMM() { return d_tm->getRWMM(); }

    void* operator new(size_t size, MemoryManager* mm) {
      return mm->newData(size);
    }

    void operator delete(void* d) { }

  }; // end of class RWTheoremValue

  //! A special subclass for reflexivity theorems: e = e and e <=> e
  /*! Such theorems are created extremely often, and do not contain
   * any useful information other than the expression itself.
   */
  class ReflexivityTheoremValue: public TheoremValue {
    friend class Theorem;
  private:
    // The expression 'e' in e = e or e <=> e
    Expr d_expr;
    // We do not take assumptions, only the proof object
    ReflexivityTheoremValue(TheoremManager* tm, const Expr& e, const Proof& pf)
      : TheoremValue(tm, Expr(), Assumptions(), pf, false), d_expr(e) { }

    ~ReflexivityTheoremValue() { }

    bool isRewrite() const { return true; }
    const Expr& getLHS() const { return d_expr; }
    const Expr& getRHS() const { return d_expr; }

    const Expr& getExpr() const {
      if (d_thm.isNull()) {
        bool isBool = d_expr.getType().isBool();
        // have to fake out the const qualifier
        Expr* pexpr = const_cast<Expr*>(&d_thm);
        *pexpr = isBool ? d_expr.iffExpr(d_expr) : d_expr.eqExpr(d_expr);
      }
      return d_thm;
    }

    // Memory management
    MemoryManager* getMM() { return d_tm->getReflMM(); }

    void* operator new(size_t size, MemoryManager* mm) {
      return mm->newData(size);
    }

    void operator delete(void* d) { }

  }; // end of class ReflexivityTheoremValue

}; // end of namespace CVCL

#endif

---