xlate_remove_duplicates.cpp

vxworks的系统故障诊断项目

/***
 *** See the file "mba/disclaimers-and-notices-L2.txt" for
 *** information on usage and redistribution of this file,
 *** and for a DISCLAIMER OF ALL WARRANTIES.
 ***/

/* $Id: xlate_remove_duplicates.cpp,v 1.1.1.1 2006/10/09 06:58:18 shao Exp $ */
#include <readers/xlate_remove_duplicates.h>

#include <readers/L2_file.h>
#include <readers/clause.h>

// The do-while(0) is the only portable way to block.
#ifdef ENABLE_L2_VERBOSE
#  define verbose(expr) \
   do { if (isVerbose()) { get_output() << expr; } } while(0)
#else
#  define verbose(expr)
#endif

/**
 * This inner class is a wrapper for an L2rProposition that has a hash code.
 * It is used as a key in a hash table that maps L2rProposition objects to
 * the "representative" of their equalivance class.
 */

class xlate_remove_duplicates::Hashable_prop {
public:

  /**
   * Construct from an existing L2rProposition and the enclosing
   * L2_file_translator.
   * L2rProposition is an abstract class, so parameter pL2rProposition must be
   * of type either L2rPropVarVar or L2rPropVarValue. However, we cannot
   * dispatch on the type of that parameter. Subclassing is probably best, but
   * that is a major redesign.
   */

  Hashable_prop(const L2rProposition *pL2rProposition,
		L2_file_translator *x) {
    if (pL2rProposition->isEquality()) {
      // Class L2rPropVarVar (variable1 == variable2)
      const L2rPropVarVar *pL2rPropVarVar =
	static_cast<const L2rPropVarVar*>(pL2rProposition);
      initialize(x->get_dest_var(pL2rPropVarVar->var()),
		 x->get_dest_var(pL2rPropVarVar->otherVar()),
		 pL2rPropVarVar->isPositive());
    } else {
      // Class L2rPropVarValue (variable == value)
      const L2rPropVarValue *pL2rPropVarValue =
	static_cast<const L2rPropVarValue*>(pL2rProposition);
      initialize(x->get_dest_var(pL2rPropVarValue->var()),
		 pL2rPropVarValue->value(),
		 pL2rPropVarValue->isPositive());
    }
  }


  /**
   * Construct variable1 == variable2
   * This apparently isn't used; comment it out for now.
  Hashable_prop(const L2rVariable *pL2rVariable1,
		const L2rVariable *pL2rVariable2,
		bool isPositive) {
    initialize(pL2rVariable1, pL2rVariable2, isPositive);
  }
  */
  

  /**
   * Construct variable == value
   * This apparently isn't used; comment it out for now.
  Hashable_prop(const L2rVariable *pL2rVariable,
                unsigned valueIndex,
		bool isPositive) {
    initialize(pL2rVariable, valueIndex, isPositive);
  }
  */


  /**
   * Auxiliary to constructors for L2rPropVarValue (variable == value)
   */

  void initialize(const L2rVariable *pL2rVariable, unsigned valueIndex,
		  bool isPositive) {
    var = pL2rVariable;
    value = valueIndex;
    is_equality = false;
    is_positive = isPositive;
  }


  /**
   * Auxiliary to constructors for L2rPropVarVar (variable1 == variable2).
   * Put the two variables in a canonical order -- increasing IDs.
   */

  void initialize(const L2rVariable *pL2rVariable1,
		  const L2rVariable *pL2rVariable2,
		  bool isPositive) {
    if (pL2rVariable1->id() < pL2rVariable2->id()) {
      // Increasing; as is
      var      = pL2rVariable1;
      otherVar = pL2rVariable2;
    } else if (pL2rVariable1->id() > pL2rVariable2->id()) {
      // Decreasing; swap
      var      = pL2rVariable2;
      otherVar = pL2rVariable1;
    } else {
      // Equal; we should check and not create these
      L2_assert(pL2rVariable1->id() != pL2rVariable2->id(),
		L2_fatal_error,
		("creating var=var prop with only one var=" +
		 MBA_string(pL2rVariable1)));
    }
    is_equality = true;
    is_positive = isPositive;
  }


  /**
   * Two Hashable_prop objects are equal if (1) their two variables are
   * equal; (2) their senses (positive vs. negative) are equal; (3) they
   * are both variable1 == variable2 or both variable == value; and (4) if
   * variable1 == variable2, the variable2's must be the same and if 
   * variable == value, the two values are the same.
   */

  bool operator == (const Hashable_prop& other) const {
    return
      (var         == other.var) &&
      (is_positive == other.is_positive) &&
      (is_equality == other.is_equality) &&
      ((is_equality  && (otherVar == other.otherVar)) ||
       (!is_equality && (value    == other.value)));
  }


  /**
   * Definition of the hash code
   * For variable1 == variable2 propositions: the sum of variable pointers
   * For variable == value propositions :the sum of the variable pointer and
   * the value index.
   * For both propositions, if the sense is positive, multiply by two
   */

  unsigned hashcode() const {
    unsigned ret = unsigned(var);
    if (is_equality) {
      ret += unsigned(otherVar);
    } else {
      ret += value;
    }
    if (is_positive)
      ret <<= 1;
    return ret;
  }


  /**
   * Return the hash code for this object. This is passed to the constructor
   * for a Hash_table with Hashable_prop key in copy_all_clauses().
   */

  static unsigned hash(const Hashable_prop& hp) {
    return hp.hashcode();
  }


  /**
   * Create an L2rProposition using the supplied propositionID and the
   * object's data members.
   */

  L2rProposition *create_prop(unsigned id) const {
    // note: no safeguard against creating several.
    if (is_equality) {
      return new L2rPropVarVar(id, var, is_positive, otherVar);
    } else {
      return new L2rPropVarValue(id, var, is_positive, value);
    }
  }

private:
  // If variable1 == variable2, variable1; if variable == value, variable
  const L2rVariable *var;
  // If variable1 == variable2, variable2
  const L2rVariable *otherVar;
  // If variable == value, value
  unsigned value;
  // If true, variable1 == variable2; else variable == value
  bool is_equality;
  // Whether the proposition is negated
  bool is_positive;
};


/** This inner class is a wrapper for an L2rClause that has a hash code.
 *  It is used as a key in a hash table that maps L2rClause objects onto the
 *  "representative" of their equivalence class.
 */

class xlate_remove_duplicates::Hashable_clause {
public:
  Hashable_clause(const L2rClause *pL2rClause, L2_file_translator *x) {
    hash_cache = 0;  // The clause's hash code
    nprops_ = 0;     // The number of L2rPropositions in the L2rClause
    
    const L2rVariable *unsatisfiable = 0;
    
    // For each L2rProposition in the L2rClause
    for (unsigned i = 0; i < pL2rClause->nprops(); ++i) {
      // Retrieve the L2rProposition
      const L2rProposition *original = pL2rClause->prop(i);
      if (original->isEquality()) {
	// L2rPropVarVar (variable1 == variable2)
	const L2rPropVarVar *pL2rPropVarVar =
	  static_cast<const L2rPropVarVar*>(original);
	if (pL2rPropVarVar->var() == pL2rPropVarVar->otherVar()) {
	  // v1=v1 is trivially true ;
	  // ! v1=v1 is trivially false.
	  if (original->isPositive()) {
	    // v1=v1 is true, so the entire clause is already satisfied by
	    // this true disjunct, so don't bother.
	    nprops_ = 0;
	    return;
	  } else {
	    // ! v1=v1 is false, so this false disjunct proposition doesn't
	    // affect the truth value -- except if this is a singleton clause.
	    unsatisfiable = pL2rPropVarVar->var();
	    continue;
	  }
	} else {
	  // L2rPropVarValue (variable == value); can't be optimized away
	}
      }

      // The general case, nothing weird is up.
      const L2rProposition *translated = x->get_dest_prop(original);
      L2_assert(translated,
		L2_fatal_error,
		("failed to map prop " + MBA_string(original->id())));
      add_prop(translated);
    }
    
    L2_assert(!unsatisfiable || nprops_ > 0,
	      L2_reader_error,
	      ("unsatisfiable clause asserting v" +
	       MBA_string(unsatisfiable->id()) + "!=v" +
	       MBA_string(unsatisfiable->id())));

#ifdef ENABLE_L2_DEBUG_SECTIONS
    if (pL2rClause->hasDebug()) {
      component_name =
	static_cast<const dbg_L2rClause*>(pL2rClause)->component();