theorem.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theorem.cpp
 * 
 * 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: Theorem
//
// AUTHOR: Sergey Berezin, 07/05/02
//
// See theorem.h file for more information.
///////////////////////////////////////////////////////////////////////////////

#include "theorem.h"
#include "theorem_value.h"
#include "command_line_flags.h"

namespace CVCL {
  using namespace std;

  //! Compare Theorems by their expressions.  Return -1, 0, or 1.
  /*!
   *  This is an arbitrary total ordering on Theorems.  For
   *  simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to
   *  be smaller than other theorems.
   */
  /*
  int compare(const Theorem& t1, const Theorem& t2) {
    return compare(t1.getExpr(), t2.getExpr());
  }
  */
  int compare(const Theorem& t1, const Theorem& t2) {
    if(t1.d_thm == t2.d_thm) return 0;
    if(t1.isNull()) return -1; // Null Theorem is less than other theorems
    if(t2.isNull()) return 1;

    bool rw1(t1.isRewrite()), rw2(t2.isRewrite());

    if(!rw2) return compare(t1, t2.getExpr());
    else if(!rw1) return -compare(t2, t1.getExpr());
    else {
      int res(compare(t1.getLHS(), t2.getLHS()));
      if(res==0) res = compare(t1.getRHS(), t2.getRHS());
      return res;
    }
  }
  /*
  int compare(const Theorem& t1, const Expr& e2) {
    return compare(t1.getExpr(), e2);
  }
  */
  int compare(const Theorem& t1, const Expr& e2) {
    bool rw1(t1.isRewrite()), rw2(e2.isEq() || e2.isIff());
    if(!rw1) {
      const Expr& e1 = t1.getExpr();
      rw1 = (e1.isEq() || e1.isIff());
    }
    if(rw1) {
      if(rw2) {
        int res(compare(t1.getLHS(), e2[0]));
        if(res==0) res = compare(t1.getRHS(), e2[1]);
        return res;
      } else return -1;
    } else {
      if(rw2) return 1;
      else return compare(t1.getExpr(), e2);
    }
  }
  
  int compareByPtr(const Theorem& t1, const Theorem& t2) {
    if(t1.d_thm == t2.d_thm) return 0;
    else if(t1.d_thm < t2.d_thm) return -1;
    else return 1;
  }

  // Assignment operator
  Theorem& Theorem::operator=(const Theorem& th) {
    // Handle self-assignment
    if(this == &th) return *this;
    IF_DEBUG(bool notNull(!isNull() || !th.isNull());
             if(notNull)
             TRACE("theorem", "Theorem::operator=(",
                   *this, " := "+th.toString()+") {"));
    DebugAssert(isNull() || d_thm->d_refcount > 0,
                "Theorem::operator=: OLD refcount = "
                + int2string(d_thm->d_refcount));

    IF_DEBUG(if((!isNull()) && d_thm->d_refcount == 1)
             TRACE("theorem", "Delete ", *this, ""));
    if((!isNull()) && --(d_thm->d_refcount) == 0) {
      MemoryManager* mm = d_thm->getMM();
      delete d_thm;
      mm->deleteData(d_thm);
    }
    d_thm = th.d_thm;
    DebugAssert(isNull() || d_thm->d_refcount > 0,
                "Theorem::operator=: NEW refcount = "
                 + int2string(d_thm->d_refcount)
                 + " in " + this->toString());
    if (d_thm) ++(d_thm->d_refcount);
    IF_DEBUG(if(notNull)
             TRACE("theorem", "Theorem::operator= => ", *this," }"));
    return *this;
  }

  // Constructors
  Theorem::Theorem(TheoremManager* tm, const Expr &thm,
                   const Assumptions& assump, const Proof& pf, 
                   bool isAssump, int scope) {
    if(thm.isEq() || thm.isIff())
      d_thm = new(tm->getRWMM()) RWTheoremValue(tm, thm, assump, pf, isAssump, scope);
    else
      d_thm = new(tm->getMM()) TheoremValue(tm, thm, assump, pf, isAssump, scope);
    d_thm->d_refcount++;
    TRACE("theorem", "Theorem(e) => ", *this, "");
    DebugAssert(!withProof() || !pf.isNull(),
                "Null proof in theorem:\n"+toString());
  }

  Theorem::Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
                   const Assumptions& assump, const Proof& pf, bool isAssump,
                   int scope) {
    d_thm = new(tm->getRWMM())
      RWTheoremValue(tm, lhs, rhs, assump, pf, isAssump, scope);
    d_thm->d_refcount++;

    // record that rhs was simplified from lhs, provided that both are
    // atomic and rhs is a fresh expression, following SVC. We try to
    // approximate this by seeing if the rhs was the last created
    // expression (i.e. it has the last index handed out by the
    // expression manager), but that's not reliable since the
    // expressions may have been created in a different order than
    // they are passed into Theorem().

    if (rhs.hasLastIndex() // FIXME: is this OK to comment out?
        // && tm->getVCL()->theoryCore()->isAtomicFormula(rhs)
        // && tm->getVCL()->theoryCore()->isAtomicFormula(lhs)
        )
      ((Expr &)rhs).setSimpFrom(lhs.hasSimpFrom() ?
                                lhs.getSimpFrom() :
                                lhs);
    TRACE("theorem", "Theorem(lhs,rhs) => ", *this, "");
    DebugAssert(!withProof() || !pf.isNull(),
                "Null proof in theorem:\n"+toString());
  }


  Theorem::Theorem(TheoremManager* tm, const Expr& e, const Proof& pf) {
    d_thm = new(tm->getReflMM()) ReflexivityTheoremValue(tm, e, pf);
    d_thm->d_refcount++;
    TRACE("theorem", "Theorem(e=e) => ", *this, "");    
    DebugAssert(!withProof() || !pf.isNull(),
                "Null proof in theorem:\n"+toString());
  }


  // Copy constructor
  Theorem::Theorem(const Theorem &th) : d_thm(th.d_thm) {
    if(!isNull()) {
      DebugAssert(d_thm->d_refcount > 0,
                  "Theorem(const Theorem&): refcount = "
                  + int2string(d_thm->d_refcount));
      d_thm->d_refcount++;
      TRACE("theorem", "Theorem(Theorem&) => ", *this, "");
    }
  }

  // Destructor
  Theorem::~Theorem() {
    if(!isNull()) {
      TRACE("theorem", "~Theorem(", *this, ") {");
      DebugAssert(d_thm->d_refcount > 0,
                  "~Theorem(): refcount = "
                  + int2string(d_thm->d_refcount));
      if((--d_thm->d_refcount) == 0) {
        TRACE_MSG("theorem", "~Theorem(): deleting");
        MemoryManager* mm = d_thm->getMM();
        delete d_thm;
        mm->deleteData(d_thm);
      }
      TRACE_MSG("theorem", "~Theorem() => }");
    }
  }

  void Theorem::printx() const { getExpr().print(); }

  void Theorem::print() const { cout << toString() << endl; }

  // Test if we are running in a proof production mode and with assumptions
  bool Theorem::withProof() const {
    return d_thm->d_tm->withProof();
  }
  bool Theorem::withAssumptions() const {
    return d_thm->d_tm->withAssumptions();
  }
  
  bool Theorem::isRewrite() const {
    DebugAssert(!isNull(), "CVCL::Theorem::isRewrite(): we are Null");
    return d_thm->isRewrite();
  }

  // Return the theorem value as an Expr
  const Expr& Theorem::getExpr() const {
    DebugAssert(!isNull(), "CVCL::Theorem::getExpr(): we are Null");
    return d_thm->getExpr();
  }

  const Expr& Theorem::getLHS() const {
    DebugAssert(!isNull(), "CVCL::Theorem::getLHS: we are Null");
    return d_thm->getLHS();
  }

  const Expr& Theorem::getRHS() const {
    DebugAssert(!isNull(), "CVCL::Theorem::getRHS: we are Null");
    return d_thm->getRHS();
  }

// Return the assumptions.
const Assumptions& Theorem::getAssumptions() const
{
  if (!d_thm->isAssump() || !withAssumptions()) return getAssumptionsRef();
  DebugAssert(!isNull(), "CVCL::Theorem::getAssumptions: we are Null");
  Assumptions& a = d_thm->d_assump;
  if (a.isNull()) a.init();
  if (a.empty()) {
    a.add(*this);
    a.setConst();
  }
  return a;
}


void Theorem::getAssumptionsRec(set<Expr>& assumptions) const
{
  if(isFlagged()) return;
  setFlag();
  if(isAssump()) {
    assumptions.insert(getExpr());
  }
  else {
    Assumptions a(getAssumptions());
    for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
      (*i).getAssumptionsRec(assumptions);
  }
}


void Theorem::getLeafAssumptions(vector<Expr>& assumptions,
                                 bool negate) const
{
  if (isNull()) return;
  set<Expr> assumpSet;
  clearAllFlags();
  getAssumptionsRec(assumpSet);
  // Order assumptions by their creation time
  for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
      i!=iend; ++i)
    assumptions.push_back(negate ? (*i).negate() : *i);
}


const Assumptions& Theorem::getAssumptionsRef() const
{
  static Assumptions null;
  DebugAssert(!isNull(), "CVCL::Theorem::getAssumptionsRef: we are Null");
  if(withAssumptions()) {
    DebugAssert(!isAssump(), "CVCL::Theorem::getAssumptionsRef: "
                "should call getAssumptions() on leaf assumptions");
    return d_thm->getAssumptionsRef();
  }
  else return null;
}


  bool Theorem::isAssump() const {
    DebugAssert(!isNull(), "CVCL::Theorem::isAssump: we are Null");
    return d_thm->isAssump();
  }

  // This method returns a *clean copy* of the Assumptions.
  // It can be modified without any effect on the theorem.
  // It's an error if called while running without assumptions.
  Assumptions Theorem::getAssumptionsCopy() const {
    return getAssumptions().copy();
  }
  // Return the proof of the theorem.  If running without proofs,
  // return the Null proof.
  const Proof& Theorem::getProof() const {
    static Proof null;
    DebugAssert(!isNull(), "CVCL::Theorem::getProof: we are Null");
    if(withProof() == true)
      return d_thm->getProof();
    else
      return null;
  }

  bool Theorem::isFlagged() const {
    DebugAssert(!isNull(), "CVCL::Theorem::isFlagged: we are Null");
    return d_thm->isFlagged();
  }

  void Theorem::clearAllFlags() const {
    DebugAssert(!isNull(), "CVCL::Theorem::clearAllFlags: we are Null");
    d_thm->clearAllFlags();
  }

  void Theorem::setFlag() const {
    DebugAssert(!isNull(), "CVCL::Theorem::setFlag: we are Null");
    d_thm->setFlag();
  }

  void Theorem::setCachedValue(int value) const {
    DebugAssert(!isNull(), "CVCL::Theorem::setCachedValue: we are Null");
    d_thm->setCachedValue(value);
  }
  
  int Theorem::getCachedValue() const {
    DebugAssert(!isNull(), "CVCL::Theorem::getCachedValue: we are Null");
    return d_thm->getCachedValue();
  }
  
  void Theorem::setExpandFlag(bool val) const {
    DebugAssert(!isNull(), "CVCL::Theorem::setExpandFlag: we are Null");
    d_thm->setExpandFlag(val);
  }

  bool Theorem::getExpandFlag() const {
    DebugAssert(!isNull(), "CVCL::Theorem::getExpandFlag: we are Null");
    return d_thm->getExpandFlag();
  }

  void Theorem::setLitFlag(bool val) const {
    DebugAssert(!isNull(), "CVCL::Theorem::setLitFlag: we are Null");
    d_thm->setLitFlag(val);
  }

  bool Theorem::getLitFlag() const {
    DebugAssert(!isNull(), "CVCL::Theorem::getLitFlag: we are Null");
    return d_thm->getLitFlag();
  }

  bool Theorem::isAbsLiteral() const {
    return getExpr().isAbsLiteral();
  }

  int Theorem::getScope() const {
    DebugAssert(!isNull(), "CVCL::Theorem::getScope: we are Null");
    return d_thm->getScope();
  }

  void Theorem::recursivePrint(int& i) const {
    cout << "[" << getCachedValue()
         << "]@" << getScope() << "\tTheorem: {";

    if (isAssump()) {
      cout << "assump";
    }
    else if (getAssumptions().empty()) {
      cout << "empty";
    }
    else {
      const Assumptions::iterator iend = getAssumptions().end();
      for (Assumptions::iterator it = getAssumptions().begin();
           it != iend; ++it) {
        if (!it->isFlagged()) it->setCachedValue(i++);
        cout << "[" << it->getCachedValue() << "], " ;
      }
      cout << "}" << endl << "\t\t|- " << getExpr() << endl;
      for (Assumptions::iterator it = getAssumptions().begin();
           it != iend; ++it) {
        if (it->isFlagged()) continue;
        it->recursivePrint(i);
        it->setFlag();
      }
      return;
    }
    cout << "}" << endl << "\t\t|- " << getExpr() << endl;
  }


  // Return the scope level at which this theorem was created
//   int Theorem::getScope() const {
//     DebugAssert(!isNull(), "CVCL::Theorem::getScope: we are Null");
//     return d_thm->getScope();
//   }

//   Assumptions Theorem::getUserAssumptions() const {
//     ExprMap<Theorem> em;
//     Assumptions a = getAssumptionsCopy();

//     collectAssumptions(a, em);
    
//     return a;
//   }

//   void collectAssumptions(Assumptions &a, ExprMap<Theorem> em ) const {
//     if (isAssump()) {
//       // cache?
//       return;
//     }
    
//     const Assumptions a2 = d_thm->getAssumptions();
//     a.add(a2);
//     Assumptions::iterator a2begin = a2.begin();
//     const Assumptions::iterator a2end = a2.end();


//   }


  // Printing Theorem
  ostream& Theorem::print(ostream& os, const string& name) const {
    if(isNull()) return os << name << "(Null)";
    ExprManager *em = getExpr().getEM();
    if(withAssumptions()) {
      em->incIndent(name.size()+2);
      os << name << "([" << d_thm << "#" << d_thm->d_refcount << "]@"
         << getScope() << "\n[";
      if(isAssump()) os << "Assump";
      else {
        if(d_thm->d_tm->getFlags()["print-assump"].getBool()
           && em->isActive())
          os << getAssumptions();
        else
          os << "<assumptions>";
      }
      os << "]\n  |--- ";
      em->indent(7);
      if(em->isActive()) os << getExpr();
      else os << "(being destructed)";
      if(withProof())
        os << "\n Proof = " << getProof();
      return os << ")";
    }
    else {
      em->incIndent(name.size()+1);
      os << name << "(";
      if(em->isActive()) os << getExpr();
      else os << "being destructed";
      return os << ")";
    }
  }

} // end of namespace CVCL

---