assumptions_value.cpp

Go to the documentation of this file.

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


#include "assumptions_value.h"


using namespace std;
using namespace CVCL;


static bool TheoremEq(const Theorem& t1, const Theorem& t2) 
{ 
  DebugAssert(!t1.isNull() && !t2.isNull(), 
        "AssumptionsValue() Null Theorem passed to constructor");
  return t1 == t2;
}


AssumptionsValue::AssumptionsValue(const std::vector<Theorem>& v)
  : d_refcount(0), d_const(false)
{ 
  TRACE_MSG("assumptions", "AssumptionsValue {");
  d_vector.reserve(v.size());

  const vector<Theorem>::const_iterator iend = v.end();
  vector<Theorem>::const_iterator i = v.begin();

//   if (i != iend) {
//     i->clearAllFlags();
//   }

  for (;i != iend; ++i) {
    if (//!i->isFlagged() && 
        (i->isAssump() || !i->getAssumptions().empty())) {
      d_vector.push_back(*i);
      //      i->setFlag();
    }
  }

  if (d_vector.size() <= 1) return;
  sort(d_vector.begin(), d_vector.end());
  vector<Theorem>::iterator newend =
    unique(d_vector.begin(), d_vector.end(), TheoremEq);

  d_vector.resize(newend - d_vector.begin());

  IF_DEBUG(
    if (CVCL::debugger.trace("assumptions")) {
      cout << *this << endl;
    }
  )

  TRACE_MSG("assumptions", "}");
}


AssumptionsValue::AssumptionsValue(const Theorem& t1, const Theorem& t2)
  : d_refcount(0), d_const(false)
{
  TRACE_MSG("assumptions", "AssumptionsValue2 {");
//   d_vector.push_back(t1);
//   if (t1 != t2) d_vector.push_back(t2);

//   if (CVCL::debugger.trace("assumptions")) {
//     cout << *this << endl;
//   }

  if (t1.isAssump() || !t1.getAssumptions().empty()) {
    if (t2.isAssump() || !t2.getAssumptions().empty()) {
      switch(compare(t1, t2)) {
        case -1: // t1 < t2:
          d_vector.push_back(t1);
          d_vector.push_back(t2);
          break;
        case 0: // t1 == t2:
          d_vector.push_back(t1);
          break;
        case 1: // t1 > t2:
          d_vector.push_back(t2);
          d_vector.push_back(t1);
          break;
      }
    } else d_vector.push_back(t1);
  } else if (t2.isAssump() || !t2.getAssumptions().empty()) {
    d_vector.push_back(t2);
  }

  TRACE_MSG("assumptions", "}");

}


void AssumptionsValue::mergeVectors(const vector<Theorem>& v1,
                                    const vector<Theorem>& v2,
                                    vector<Theorem>& v)
{
  v.reserve(v1.size() + v2.size());

  vector<Theorem>::const_iterator i = v1.begin();
  vector<Theorem>::const_iterator j = v2.begin();
  const vector<Theorem>::const_iterator v1end = v1.end();
  const vector<Theorem>::const_iterator v2end = v2.end();

  // merge
  while (i != v1end && j != v2end) {
    switch(compare(*i, *j)) {
      case 0:
        // copy only 1, drop down to next case
        ++j;
      case -1: // <
        v.push_back(*i);
        ++i;
        break;
      default: // >
        v.push_back(*j);
        ++j;
    };
  }
  // Push in the remaining elements
  for(; i != v1end; ++i) v.push_back(*i);
  for(; j != v2end; ++j) v.push_back(*j);
}


void AssumptionsValue::add(const Theorem& t)
{
  TRACE_MSG("assumptions", "add");
  DebugAssert(!d_const, 
        "AssumptionsValue::add() called on constant assumptions");
  DebugAssert(!t.isNull(),
        "AssumptionsValue::add() Null Assumption!");

  if (!t.isAssump() && t.getAssumptions().empty()) return;

  TRACE_MSG("assumptions", "AssumptionsValue::add(" + t.toString() + ")");

  //  d_vector.push_back(t);

   // TODO: linear search is bad
   vector<Theorem>::iterator iter = d_vector.begin();
   const vector<Theorem>::const_iterator vend = d_vector.end();
   for (; iter != vend; ++iter) {
     int c(compare(t, *iter));
     if(c == 0) return; // t == *iter
     if(c < 0) break; // t < *iter
   }
   d_vector.insert(iter, t);
}


void AssumptionsValue::add(const AssumptionsValue& a) {
  TRACE_MSG("assumptions", "add2");
  DebugAssert(!d_const, 
        "AssumptionsValue::add() called on constant assumptions");

  vector<Theorem>::const_iterator iend = a.d_vector.end();
  for (vector<Theorem>::const_iterator i = a.d_vector.begin(); 
       i != iend; ++i) {
    d_vector.push_back(*i);
  }

  vector<Theorem> v;
  mergeVectors(d_vector, a.d_vector, v);
  d_vector.swap(v);
}


const Theorem& AssumptionsValue::find(const Expr& e) const {
  static Theorem null;
  //    binary search
  int lo = 0; 
  int hi = d_vector.size() - 1;
  int loc;
  while (lo <= hi) {
    loc = (lo + hi) / 2;
 
    switch (compare(d_vector[loc], e)) {
      case 0: return d_vector[loc];
      case -1: // t < e
        lo = loc + 1;
        break;
      default: // t > e
        hi = loc - 1;
    };
  }

  return null;
}


// Print function: print the comma-separated list of assumptions
string AssumptionsValue::toString() const {
  ostringstream ss;
  ss << (*this);
  return ss.str();
}


////////////////////////////////////////////////////////////////////
// AssumptionsValue friend methods
////////////////////////////////////////////////////////////////////


namespace CVCL {


ostream &operator<<(ostream& os, const AssumptionsValue &assump) {
  vector<Theorem>::const_iterator i = assump.d_vector.begin();
  const vector<Theorem>::const_iterator iend = assump.d_vector.end();
  if(i != iend) { os << i->getExpr(); i++; }
  for(; i != iend; i++) os << ",\n " << i->getExpr();
  return os;
}


}

---