#include <stdio.h>
#include <string.h>
#include "color.h"
#include "set.h"
#include "quals.h"
#include "util.h"

/* #define DEBUG */      /* Enable printing of generated constraints */
/* #define BITSET */     /* Enable bitset code; not fully implemented */

#ifdef BITSET
#include "bitset.h"
#endif

struct po_info_S;
typedef struct po_info_S *po_info;
struct cond_set_S;
typedef struct cond_set_S *cond_set;

typedef enum { qk_constant, qk_variable, qk_link } type_qualifier_kind_t;
struct type_qualifier {
  type_qualifier_kind_t kind;
  bool mark;                       /* For traversing the graph */
  qual parent;                     /* Parent in current spanning tree. */
  union {

    /* Constant */
    struct {
      const char *name;		     /* Name of this qualifier */
      const char *color;             /* Color information for PAM mode */
      level_qual_t level;            /* Level information for qtype */
      sign_qual_t sign;              /* Sign information for qtype */
      qual_set lbc, ubc;             /* Upper- and lower-bounds in order */
#ifdef BITSET
      int index;                     /* Position in bitset for this
					qualifier */
      bitset lb_mask, ub_mask;       /* Sets of qualifiers consistent with
					this being a lower/upper bound */
#endif
      po_info po;                    /* Partial order this qual is in */
    } elt;

    /* Variable */
    struct {
      const char *name;
      location loc;                  /* Where did this qualifier come from */
      qual_set lbv, ubv;             /* lower/upper bound variables */
#ifdef BITSET
      bitset bounds;                 /* Set of possible constant qualifiers
					we could assign this variable
					qual to */
#endif
      qual_set lbc, ubc;             /* lower/upper bound constants */
      qual_set orig_lbc, orig_ubc;   /* subset of lbc, ubc that were not
					added through transitivity */
      cond_set vcond_set;             /* conditional constraints pending
					on this variable */
      int num_equiv;                 /* # of vars unified with this one */
      bool preferred;                /* True we should try to keep the
				        name of this variable as the ecr */
    } var;

    /* Variable that's just been unified with another variable.  In
       this case, mark and parent don't make sense. */
    qual link;
  } u;
};

struct po_info_S {
  qual_set qualifiers;       /* The qualifiers in this partial order */
  bool dynamic;              /* True if these qualifiers are dynamic */
  bool nonprop;              /* True if these qualifiers don't propagate
				through constraints */
#ifdef BITSET
  int first, last;           /* Index in bitset of first and last element */
#endif
};


struct qual_set_elt_S {
  qual q;
  struct qual_set_elt_S *tl;
};
typedef struct qual_set_elt_S *qual_set_elt;

struct Qual_Set {
  region r;
  struct qual_set_elt_S *hd;
};

typedef enum cond_dir { c_leq_v, v_leq_c} cond_dir;

struct cond_set_S {
  cond_dir dir;
  qual c, left, right;         /* constraint is
				   c <= v ==> left <= right   if dir = c_leq_v
				   v <= c ==> left <= right   if dir = v_leq_c
				  where v is the variable this constraint
				  is associated with */
  struct cond_set_S *next;
};

void cond_set_insert(cond_set *conds, cond_dir dir, qual c, qual left,
		     qual right);
bool cond_set_trigger(cond_set *conds, cond_dir dir, qual c);

static qual ecr_qual(qual q);

/**************************************************************************
 *                                                                        *
 * Global Variables and Initialization                                    *
 *                                                                        *
 **************************************************************************/

/* Used to prevent some catastrophic errors from occurring */
enum { state_start, state_init, state_pos_defined } state = state_start;

int flag_print_quals_graph = 0; /* Set (externally) to true if we should
				   print out the qualifier constraint
				   graph in dot form. */
static region quals_region = NULL;
static int next_qual = 0;
static int max_index = 0;
static FILE *graph_file = NULL;
qual_set all_quals = NULL;
set all_pos = NULL;
po_info current_po;
qual const_qual = NULL;
qual nonconst_qual = NULL;
qual volatile_qual = NULL;
qual restrict_qual = NULL;
int num_hotspots = 0;           /* Set (externally) to number of hotspots
				   to track. 0 = track no hotspots. */
qual *hotspots; /* Array of size num_hotspots */

/* Called before any other functions in quals.h are called. */
void init_quals(void)
{
  assert(!quals_region);
  quals_region = newregion();
  next_qual = 0;
  max_index = 0;
  all_quals = new_qual_set(quals_region);
  all_pos = set_new(quals_region, ptr_cmp, TRUE);
  current_po = NULL;
  assert(num_hotspots >= 0);
  if (num_hotspots != 0)
    /* rarrayalloc initializes hotspots to 0 */
    hotspots = rarrayalloc(quals_region, num_hotspots, qual);
  else
    hotspots = NULL;
  /*  constq = add_qual("const");
      nonconstq = add_qual("$nonconst");
      volatileq = add_qual("volatile");
      add_qual_lt(nonconstq, constq); */
  if (flag_print_quals_graph)
    {
      if (graph_file)
	fclose(graph_file);
      graph_file = fopen("quals.dot", "w");
      fprintf(graph_file, "digraph G {\n");
    }
  state = state_init;
}

#ifdef BITSET
/* Print b, but with names */
void bitset_print_pretty(bitset b)
{
  qual_set_scanner qs;
  qual q;
  bool first;

  first = TRUE;
  scan_quals(q, qs, all_quals)
    if (bitset_member(b, q->u.elt.index))
      {
	if (!first)
	  printf(" ");
	first = FALSE;
	printf(q->u.elt.name);
      }
}

/* Construct lb_mask and ub_mask fields for q.  lb_mask is the maximal
   set of qualifiers such that q <= lb_mask is valid.  ub_mask is the
   maximal set of qualifeirs such that ub_mask <= q is valid. */
void construct_qual_masks(qual q)
{
  qual_set_scanner qs;
  qual p;
  bitset lb_mask, ub_mask;

  assert(q->kind == qk_constant);

  /* Assume initially q consistent with all qualifiers */
  lb_mask = bitset_new(quals_region, max_index);
  ub_mask = bitset_new(quals_region, max_index);
  bitset_insert_all(lb_mask);
  bitset_insert_all(ub_mask);

  /* Remove any qualifiers that are inconsistent with q.  Note that
     these can only be qualifiers in q's partial order. */
  scan_quals(p, qs, q->u.elt.po->qualifiers)
    {
      if (!leq_qual(q, p))
	insist(bitset_remove(lb_mask, p->u.elt.index));
      if (!leq_qual(p, q))
	insist(bitset_remove(ub_mask, p->u.elt.index));
    }

  q->u.elt.lb_mask = lb_mask;
  q->u.elt.ub_mask = ub_mask;

  /*
  printf("lb_mask for %s: ", q->u.elt.name);
  bitset_print_pretty(lb_mask);
  printf("\nub_mask for %s: ", q->u.elt.name);
  bitset_print_pretty(ub_mask);
  printf("\n");
  */
}
#endif

/* Called when no more partial orders will be defined.  You *must*
   call this function before creating any qualifier variables. */
void end_define_pos(void)
{
  assert(state == state_init);
#ifdef BITSET
  {
    qual_set_scanner qs;
    qual q;

    scan_quals(q, qs, all_quals)
      construct_qual_masks(q);
  }
#endif
  state = state_pos_defined;
}

/* Called when no more constraints will be generated. */
void finish_quals(void)
{
  if (flag_print_quals_graph)
    {
      fprintf(graph_file, "}\n");
      fclose(graph_file);
    }
}

/* Disposes of all memory internally allocated by functions in
   quals.c.  All qualifiers and qualifier variables become invalid
   after calling this function. */
void dispose_quals(void)
{
  assert(quals_region);
  deleteregion(quals_region);
  quals_region = 0;
  state = state_start;
}

/**************************************************************************
 *                                                                        *
 * Qualifier Constants                                                    *
 *                                                                        *
 **************************************************************************/

/* Begin and end defining a partial order.  All the qualifiers created
   between calls to begin and end are exclusively related. */
void begin_po_qual(void)
{
  if (current_po)
    fail("begin_po_qual called without previous end_po_qual\n");
  current_po = ralloc(quals_region, struct po_info_S);
  current_po->qualifiers = new_qual_set(quals_region);
  current_po->dynamic = FALSE;
  current_po->nonprop = FALSE;
}

void end_po_qual(void)
{
  if (!current_po)
    fail("end_po_qual called without previous begin_po_qual\n");
  set_insert(all_pos, current_po);
  current_po = NULL;
}

/* Mark the current partial order dynamic */
void set_po_dynamic(void)
{
  current_po->dynamic = TRUE;
  current_po->nonprop = TRUE;
}

/* Mark the current partial order as non-propagating */
void set_po_nonprop(void)
{
  current_po->nonprop = TRUE;
#ifdef BITSET
  current_po->first = -1;
  current_po->last = -1;
#endif
}

/* Make a new (constant) qualifier */
qual add_qual(const char *name)
{
  /* qual_set_insert does pointer comparisons, not strcmps, so we need
     to do a special search by name first. */
  qual new_qual;

  assert(state != state_pos_defined);
  if (!current_po)
    fail("add_qual called without previous begin_po_qual\n");
  if ((new_qual = find_qual(name)))
    {
      if (new_qual->u.elt.po != current_po)
	fail("Qualifier %s in two different partial orders\n",
	     new_qual->u.elt.name);
      return new_qual;
    }
  /* We didn't find the qualifier */
  /*  printf("Adding qualifier %s\n", name);*/
  new_qual = ralloc(quals_region, struct type_qualifier);
  new_qual->kind = qk_constant;
  new_qual->mark = FALSE;
  new_qual->u.elt.name = rstrdup(quals_region, name);
  new_qual->u.elt.color = NULL;
  new_qual->u.elt.level = level_value;
  new_qual->u.elt.sign = sign_pos;
  new_qual->u.elt.lbc = new_qual_set(quals_region);
  new_qual->u.elt.ubc = new_qual_set(quals_region);
  new_qual->u.elt.po = current_po;
#ifdef BITSET
  if (!current_po->nonprop)
    {
      new_qual->u.elt.index = max_index++;
      if (qual_set_empty(current_po->qualifiers))
	current_po->first = new_qual->u.elt.index;
      current_po->last = new_qual->u.elt.index;
    }
#endif
  qual_set_insert(all_quals, new_qual);
  qual_set_insert(current_po->qualifiers, new_qual);
  if (!strcmp(name, "const"))
    const_qual = new_qual;
  else if (!strcmp(name, "$nonconst"))
    nonconst_qual = new_qual;
  else if (!strcmp(name, "volatile"))
    volatile_qual = new_qual;
  else if (!strcmp(name, "restrict"))
    restrict_qual = new_qual;
  return new_qual;
}

/* Add assumption left < right */
void add_qual_lt(qual left, qual right)
{
  bool new_edge;

  assert(left->kind == qk_constant);
  assert(right->kind == qk_constant);
  new_edge = qual_set_insert(left->u.elt.ubc, right);
  /*  if (new_edge)
      {
      printf("Adding assumption ");
      print_qual_raw(printf, left);
      printf(" < ");
      print_qual_raw(printf, right);
      printf("\n");
      }*/
  if (new_edge)
    {
      qual_set_scanner qs;
      qual q;

      insist(qual_set_insert(right->u.elt.lbc, left));

      /* Add transitively-implied assumptions */
      scan_quals(q, qs, right->u.elt.ubc)
	add_qual_lt(left, q);

      scan_quals(q, qs, left->u.elt.lbc)
	add_qual_lt(q, right);
    }
}

/* Add color for qualifier */
void add_color_qual(qual q, const char *color)
{
  assert(q->kind == qk_constant);
  q->u.elt.color = rstrdup(quals_region, color);
}

/* Assert that q is a qualifier on level lev */
void add_level_qual(qual q, level_qual_t lev)
{
  assert(q->kind == qk_constant);
  assert(lev == level_value || lev == level_ref);

  q->u.elt.level = lev;
}

/* Assert that q is a qualifier on values */
void add_sign_qual(qual q, sign_qual_t sign)
{
  assert(q->kind == qk_constant);
  assert(sign == sign_pos || sign == sign_neg || sign == sign_eq);
  q->u.elt.sign = sign;
}

/* Look up a qualifier */
qual find_qual(const char *name)
{
  qual_set_scanner qs;
  qual q;

  scan_quals(q, qs, all_quals)
    {
      assert(q->kind == qk_constant);
      if (!strcmp(q->u.elt.name, name))
	return q;
    }
  return NULL;
}

/* Change dynamic quals from nonprop to regular quals for this pass */
void reset_dynamic_quals(void)
{
  set_scanner ss;
  po_info po;

  scan_set(po, ss, all_pos)
    if (po->dynamic)
      po->nonprop = FALSE;
}

/**************************************************************************
 *                                                                        *
 * Qualifier Variables                                                    *
 *                                                                        *
 **************************************************************************/

/* Make a fresh qualifier variable */
qual make_qvar(const char *name, location loc, bool preferred)
{
  qual fresh;

  assert(state == state_pos_defined);
  fresh = ralloc(quals_region, struct type_qualifier);
  fresh->kind = qk_variable;
  fresh->mark = FALSE;
  fresh->u.var.name = name;
  fresh->u.var.loc = loc;
  fresh->u.var.lbv = new_qual_set(quals_region);
  fresh->u.var.ubv = new_qual_set(quals_region);
#ifdef BITSET
  fresh->u.var.bounds = bitset_new(quals_region, max_index);
  bitset_insert_all(fresh->u.var.bounds);
#endif
  fresh->u.var.lbc = new_qual_set(quals_region);
  fresh->u.var.ubc = new_qual_set(quals_region);
  fresh->u.var.orig_lbc = new_qual_set(quals_region);
  fresh->u.var.orig_ubc = new_qual_set(quals_region);
  fresh->u.var.vcond_set = NULL;
  fresh->u.var.num_equiv = 1;
  fresh->u.var.preferred = preferred;
  return fresh;
}

/* Make a fresh qvar, with a (somewhat) unique name. */
qual make_fresh_qvar(location loc)
{
  const char *name;

  name = rstrcat(quals_region, "q",
		 inttostr(quals_region, next_qual++));
  return make_qvar(name, loc, FALSE);
}

/* Return the ECR for this qualifier */
static qual ecr_qual(qual q)
{
  switch (q->kind)
    {
    case qk_constant:
    case qk_variable:
      return q;
    case qk_link:
      {
	qual ecr = q, cur, temp;
	
	/* Find root */
	while (ecr->kind == qk_link)
	  ecr = ecr->u.link;
	
	/* Compress path */
	cur = q;
	while (cur->u.link != ecr)
	  {
	    temp = cur->u.link;
	    cur->u.link = ecr;
	    cur = temp;
	  }
	return ecr;
      }
      break;
    default:
      fail("Unexpected qual kind %x\n", q->kind);
    }
}

/**************************************************************************
 *                                                                        *
 * Predicates and Queries                                                 *
 *                                                                        *
 **************************************************************************/

/* Return the level of qualifier q */
level_qual_t level_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.level;
}

/* Return the sign of qualifier q */
sign_qual_t sign_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.sign;
}

/* Return TRUE iff q is dynamic */
bool dynamic_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.po->dynamic;
}

/* Return TRUE iff q is non-propagating */
bool nonprop_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.po->nonprop;
}

/* Return TRUE iff q is a variable (or a link to a variable) */
bool variable_qual(qual q)
{
  q = ecr_qual(q);
  return q->kind == qk_variable;
}

/* Return TRUE iff q is a constant */
bool constant_qual(qual q)
{
  q = ecr_qual(q);
  return q->kind == qk_constant;
}

/* Return the location a qualifier variable came from */
location location_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.loc;
}

/* Lower-bound variables of q */
qual_set lbv_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.lbv;
}

/* Upper-bound variables of q */
qual_set ubv_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.ubv;
}

/* Lower-bound constants of q */
qual_set lbc_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.lbc;
}

/* Upper-bound constants of q */
qual_set ubc_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.ubc;
}

/* Lower-bound constants of q added directly, not through transitivity */
qual_set orig_lbc_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.orig_lbc;
}

/* Upper-bound constants of q added directly, not through transitivity */
qual_set orig_ubc_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.orig_ubc;
}

/**************************************************************************
 *                                                                        *
 * Qualifier Sets (currently just lists)                                  *
 *                                                                        *
 **************************************************************************/

qual_set new_qual_set(region r)
{
  qual_set s = ralloc(r, struct Qual_Set);
  s->r = r;
  s->hd = NULL;
  return s;
}

bool qual_set_empty(qual_set qs)
{
  return qs->hd == NULL;
}

/* Add q to set ql.  Don't add duplicates.  Returns true if q was
   actually added (i.e., q wasn't there already). */
bool qual_set_insert(qual_set quals, qual q)
{
  struct qual_set_elt_S *new_elt;
  struct qual_set_elt_S **e;

  q = ecr_qual(q);
  e = &quals->hd;
  while (*e)
    if (ecr_qual((*e)->q) != q)
      e = &((*e)->tl);
    else
      return FALSE;
  new_elt = ralloc(quals->r, struct qual_set_elt_S);
  new_elt->q = q;
  *e = new_elt;
  return TRUE;
}

/* Return true iff q is in quals */
bool qual_set_member(qual_set quals, qual q)
{
  qual_set_scanner qs;
  qual curq;

  scan_quals(curq, qs, quals)
    if (ecr_qual(curq) == ecr_qual(q))
      return TRUE;
  return FALSE;
}

/* Return number of elements in quals */
int qual_set_size(qual_set quals)
{
  qual_set_scanner qs;
  qual curq;
  int i;

  i = 0;
  scan_quals(curq, qs, quals)
    i++;
  return i;
}

void qual_set_scan(qual_set quals, qual_set_scanner *e)
{
  *e = quals->hd;
}

qual qual_set_next(qual_set_scanner *e)
{
  qual q;

  if (!*e)
    return NULL;
  q = (*e)->q;
  *e = (*e)->tl;
  return ecr_qual(q);
}

/**************************************************************************
 *                                                                        *
 * Conditional Constraint Sets                                            *
 *                                                                        *
 **************************************************************************/

/* Add condition to conds.  May add duplicates. */
void cond_set_insert(cond_set *conds, cond_dir dir, qual c, qual left,
		     qual right)
{
  cond_set new_elt;

  new_elt = ralloc(quals_region, struct cond_set_S);
  new_elt->dir = dir;
  new_elt->c = c;
  new_elt->left = left;
  new_elt->right = right;
  new_elt->next = *conds;
  *conds = new_elt;
}

/**************************************************************************
 *                                                                        *
 * Qualifier Sequences                                                    *
 *                                                                        *
 **************************************************************************/

struct Qual_Seq_Element {
  qual q;
  struct Qual_Seq_Element *prev, *next;
};

struct Qual_Seq {
  region r;
  qual_seq_element head, tail;
};

qual_seq new_qual_seq(region r)
{
  qual_seq nqs = ralloc(r, struct Qual_Seq);
  nqs->r = r;
  nqs->head = NULL;
  nqs->tail = NULL;
  return nqs;
}

bool qual_seq_empty(qual_seq qs)
{
  return (qs->head == NULL);
}

qual_seq_element qual_seq_head(qual_seq qs)
{
  return qs->head;
}

qual_seq_element qual_seq_tail(qual_seq qs)
{
  return qs->tail;
}

qual get_qual_seq_element(qual_seq_element qse)
{
  return qse->q;
}

qual_seq_element qual_seq_next(qual_seq_element qse)
{
  return qse->next;
}

qual_seq_element qual_seq_prev(qual_seq_element qse)
{
  return qse->prev;
}

/* qs = q;qs */
void qual_seq_push_left(qual_seq qs, qual q)
{
  qual_seq_element new_elt = ralloc(qs->r, struct Qual_Seq_Element);
  new_elt->q = q;
  new_elt->prev = NULL;
  new_elt->next = qs->head;
  qs->head = new_elt;
  if (!qs->tail)
    qs->tail = new_elt;
  else
    new_elt->next->prev = new_elt;
}

/* qs = qs;q */
void qual_seq_push_right(qual_seq qs, qual q)
{
  qual_seq_element new_elt = ralloc(qs->r, struct Qual_Seq_Element);
  new_elt->q = q;
  new_elt->prev = qs->tail;
  new_elt->next = NULL;
  qs->tail = new_elt;
  if (!qs->head)
    qs->head = new_elt;
  else
    new_elt->prev->next = new_elt;
}

/* qs = (let q;qs' = qs in qs') */
void qual_seq_pop_left(qual_seq qs)
{
  assert(qs->head && qs->tail);
  qs->head = qs->head->next;
  if (qs->head)
    qs->head->prev = NULL;
  else
    qs->tail = NULL;    
}

/* qs = (let qs';q = qs in qs') */
void qual_seq_pop_right(qual_seq qs)
{
  assert(qs->head && qs->tail);
  qs->tail = qs->tail->prev;
  if (qs->tail)
    qs->tail->next = NULL;
  else
    qs->head = NULL;
}

/**************************************************************************
 *                                                                        *
 * Constraint Generation                                                  *
 *                                                                        *
 **************************************************************************/

int print_graph_file(const char *fmt, ...)
{
  va_list args;
  va_start(args, fmt);
  return vfprintf(graph_file, fmt, args);
}

#ifdef BITSET
/* Return TRUE if there exists a partial order po such that b contains
   no elements of po. */
static bool invalid_bounds(bitset b)
{
  set_scanner ss;
  po_info po;
  bool result;

  result = FALSE;
  scan_set(po, ss, all_pos)
    if (!po->nonprop)
      result = result || bitset_empty_range(b, po->first, po->last);
  return result;
}

/* Make the bounds on left <= the bounds on right, propagating as
   necessary.  left and right must be variables. */
static bool propagate_bounds_change(qual q);
static bool mkleq_var_bounds(qual left, qual right)
{
  bool result;
  region scratch_region;
  bitset left_lb_mask, right_ub_mask;
  qual_set_scanner qs;
  qual q;
  bool change_left, change_right;

  assert(left->kind == qk_variable && right->kind == qk_variable);
  result = FALSE;

  scratch_region = newregion();
  left_lb_mask = bitset_new(scratch_region, max_index);
  right_ub_mask = bitset_new(scratch_region, max_index);

  /*
  printf("Mkleq bounds ");
  bitset_print_pretty(left->u.var.bounds);
  printf(" <= ");
  bitset_print_pretty(right->u.var.bounds);
  printf("\n");
  */

  /* Construct left_lb_mask and right_lb_mask */
  scan_quals(q, qs, all_quals)
    {
      if (bitset_member(left->u.var.bounds, q->u.elt.index))
	{
	  /* If q is a possible value of left, add it and all its
	     upper bounds to left_lb_mask */
	  qual_set_scanner qs2;
	  qual ub;
	  
	  bitset_insert(left_lb_mask, q->u.elt.index);
	  scan_quals(ub, qs2, q->u.elt.ubc)
	    bitset_insert(left_lb_mask, ub->u.elt.index);
	}

      if (bitset_member(right->u.var.bounds, q->u.elt.index))
	{
	  /* If q is a possible value of right, add it and all its
	     lower bounds to right_ub_mask */
	  qual_set_scanner qs2;
	  qual lb;
	  
	  bitset_insert(right_ub_mask, q->u.elt.index);
	  scan_quals(lb, qs2, q->u.elt.lbc)
	    bitset_insert(right_ub_mask, lb->u.elt.index);
	}
    }

  /* Compute new possible bounds for left and right */
  change_left = bitset_intersect(left->u.var.bounds, right_ub_mask);
  change_right = bitset_intersect(right->u.var.bounds, left_lb_mask);

  /*
  printf("      result ");
  bitset_print_pretty(left->u.var.bounds);
  printf(" <= ");
  bitset_print_pretty(right->u.var.bounds);
  printf("\n");
  */

  /* Check for any errors */
  if (change_left || change_right)
    {
      result = (invalid_bounds(left->u.var.bounds) ||
		invalid_bounds(right->u.var.bounds) ||
		result);
      if (change_left)
	result = propagate_bounds_change(left) || result;
      if (change_right)
	result = propagate_bounds_change(right) || result;
    }
  deleteregion(scratch_region);
  return result;
}

/* Call mkleq_var_bounds for all bounds of variable q */
static bool propagate_bounds_change(qual q)
{
  bool result;
  qual_set_scanner qs;
  qual b;

  assert(q->kind == qk_variable);
  result = FALSE;
  scan_quals(b, qs, q->u.var.lbv)
    result = mkleq_var_bounds(b, q) || result;
  scan_quals(b, qs, q->u.var.ubv)
    result = mkleq_var_bounds(q, b) || result;
  return result;
}

/* Add constraint left <= right to the system and solve.  Returns TRUE
   iff an error occurred. */
bool _mkleq_qual(qual left, qual right)
{
  bool result;

  result = FALSE;
  if (flag_print_quals_graph)
    {
      /*
      fprintf(graph_file, "%p %p\n", left, right);
      */
      print_qual_raw(print_graph_file, left);
      fprintf(graph_file, " -> ");
      print_qual_raw(print_graph_file, right);
      fprintf(graph_file, "\n");
    }
#ifdef DEBUG
  print_qual_raw(printf, left);
  printf(" %s <= ", ptr_to_ascii(left));
  print_qual_raw(printf, right);
  printf(" %s\n", ptr_to_ascii(right));
#endif
  left = ecr_qual(left);
  right = ecr_qual(right);
  if (left == right)
    /* Reflexivity */
    return FALSE;

  if (left->kind == qk_constant && right->kind == qk_constant)
    result = !leq_qual(left, right) || result;
  else if (left->kind == qk_constant && right->kind == qk_variable)
    {
      int first, last;

      /*
      printf("Mkleq lconst ");
      bitset_print_pretty(left->u.elt.lb_mask);
      printf(" <= ");
      bitset_print_pretty(right->u.var.bounds);
      printf("\n");
      */

      if (qual_set_insert(right->u.var.orig_lbc, left))
	{
	  first = left->u.elt.po->first;
	  last  = left->u.elt.po->last;
	  if (bitset_intersect(right->u.var.bounds, left->u.elt.lb_mask))
	    {
	      /* If we changed something, check whether the constraints
		 became unsatisfiable */
	      result = bitset_empty_range(right->u.var.bounds, first,
					  last) || result;
	      result = propagate_bounds_change(right) || result;
	    }
	}
      /*
      printf("      result ");
      bitset_print_pretty(left->u.elt.lb_mask);
      printf(" <= ");
      bitset_print_pretty(right->u.var.bounds);
      printf("\n");
      */
    }
  else if (left->kind == qk_variable && right->kind == qk_constant)
    {
      int first, last;

      /*
      printf("Mkleq rconst ");
      bitset_print_pretty(left->u.var.bounds);
      printf(" <= ");
      bitset_print_pretty(right->u.elt.ub_mask);
      printf("\n");
      */

      if (qual_set_insert(left->u.var.orig_ubc, right))
	{
	  first = right->u.elt.po->first;
	  last  = right->u.elt.po->last;
	  if (bitset_intersect(left->u.var.bounds, right->u.elt.ub_mask))
	    {
	      /* If we changed something, check whether the constraints
		 became unsatisfiable */
	      result = bitset_empty_range(left->u.var.bounds, first,
					  last) || result;
	      result = propagate_bounds_change(left) || result;
	    }
	}
      /*
      printf("      result ");
      bitset_print_pretty(left->u.var.bounds);
      printf(" <= ");
      bitset_print_pretty(right->u.elt.ub_mask);
      printf("\n");
      */
    }
  else
    {
      assert(left->kind == qk_variable && right->kind == qk_variable);
      if (qual_set_insert(left->u.var.ubv, right))
	insist(qual_set_insert(right->u.var.lbv, left));
      result = mkleq_var_bounds(left, right) || result;
    }

  if (result)
    {
      printf("Unsatisfiable ");
      print_qual_raw(printf, left);
      printf(" <= ");
      print_qual_raw(printf, right);
      printf("\n");
    }

  return result;
}

bool mkleq_qual(qual left, qual right)
{
  return _mkleq_qual(left, right);
}

/* left == right */
bool mkeq_qual(qual left, qual right)
{
  bool result;
  result = mkleq_qual(left, right);
  result = mkleq_qual(right, left) || result;
  return result;
}

/* left == right, plus cannot distinguish left and right anymore */
bool unify_qual(qual left, qual right)
{
  bool result;

  left = ecr_qual(left);
  right = ecr_qual(right);
  if (left == right) /* Short circuit to prevent loops in ecr_qual */
    return FALSE;
#ifdef DEBUG
  print_qual_raw(printf, left);
  printf(" %s = ", ptr_to_ascii(left));
  print_qual_raw(printf, right);
  printf(" %s\n", ptr_to_ascii(right));
#endif

  result = mkeq_qual(left, right);
  if (left->kind == qk_variable && right->kind == qk_variable)
    {
      qual new_ecr, new_link;

      if (right->u.var.preferred ||
	  (left->u.var.num_equiv <= right->u.var.num_equiv))
	{
	  new_ecr = right;
	  new_link = left;
	}
      else
	{
	  new_ecr = left;
	  new_link = right;
	}

      new_ecr->u.var.num_equiv += new_link->u.var.num_equiv;
      new_link->kind = qk_link;
      new_link->u.link = new_ecr;
    }
  return result;
}

/* Returns TRUE iff left <= right.  Requires that at least one of
   left, right is a constant.  By defn, returns TRUE if left and right
   are in distinct partial orders. */
bool leq_qual(qual left, qual right)
{
  left = ecr_qual(left);
  right = ecr_qual(right);

  assert(constant_qual(left) || constant_qual(right));
  if (left == right)
    return TRUE;     /* Reflexivity */

  /* XXX Fix for transitive partial order constraints */
  if (left->kind == qk_constant && right->kind == qk_constant)
    return (qual_set_member(left->u.elt.ubc, right) ||
	    !qual_set_member(left->u.elt.po->qualifiers, right));
  else if (left->kind == qk_variable)
    {
      region scratch_region;
      bitset b;
      bool result;

      scratch_region = newregion();
      b = bitset_copy(scratch_region, left->u.var.bounds);

      /* If adding the constraint that left <= right doesn't change
	 anything, then return TRUE, else return FALSE. */
      result = !bitset_intersect(b, right->u.elt.ub_mask);

      deleteregion(scratch_region);
      return result;
    }
  else
    {
      region scratch_region;
      bitset b;
      bool result;

      assert (right->kind == qk_variable);
      scratch_region = newregion();
      b = bitset_copy(scratch_region, right->u.var.bounds);

      /* If adding the constraint that left <= right doesn't change
	 anything, then return TRUE, else return FALSE. */
      result = !bitset_intersect(b, left->u.elt.lb_mask);

      deleteregion(scratch_region);
      return result;
    }
}

#else /* #IFDEF BITSET */

/* left <= right.  orig is true iff this constraint was generated
   directly instead of added through transitivity. */
bool _mkleq_qual(qual left, qual right, bool orig)
{
  if (flag_print_quals_graph && orig)
    {
      /*
      fprintf(graph_file, "%p %p\n", left, right);
      */
      print_qual_raw(print_graph_file, left);
      fprintf(graph_file, " -> ");
      print_qual_raw(print_graph_file, right);
      fprintf(graph_file, "\n");
    }
#ifdef DEBUG
  print_qual_raw(printf, left);
  printf(" %s <= ", ptr_to_ascii(left));
  print_qual_raw(printf, right);
  printf(" %s\n", ptr_to_ascii(right));
#endif
  left = ecr_qual(left);
  right = ecr_qual(right);
  if (left == right)
    /* Reflexivity */
    return FALSE;
  if (left->kind == qk_constant && right->kind == qk_constant)
    {
      /* Do comparison in lattice. */
      bool result = !leq_qual(left, right);

      if (result)
	{
	  printf("Unsatisfiable ");
	  print_qual_raw(printf, left);
	  printf(" <= ");
	  print_qual_raw(printf, right);
	  printf("\n");
	}
	
      return result;
    }
  else if (left->kind == qk_constant && right->kind == qk_variable)
    {
      bool result = FALSE;
      if (orig) /* Add no matter what -- may add to orig_lbc after has
		   also been added through transitivity */
	{
	  qual_set_insert(right->u.var.orig_lbc, left);
	  if (sign_qual(left) == sign_eq)
	    qual_set_insert(right->u.var.orig_ubc, left);
	}
      if ((!nonprop_qual(left) || orig) &&
	  qual_set_insert(right->u.var.lbc, left))
	{
	  /* Propagate if we haven't already */
	  qual q;
	  qual_set_scanner qs;

	  scan_quals(q, qs, right->u.var.ubc)
	    result = _mkleq_qual(left, q, FALSE) || result;
	  scan_quals(q, qs, right->u.var.ubv)
	    result = _mkleq_qual(left, q, FALSE) || result;
	  if (sign_qual(left) == sign_eq || qual_set_empty(left->u.elt.ubc))
	    /* Nonvariant qualifiers propagate in both directions.
	       Also, if left has no upper bounds then left <= right
	       ==> left = right. */
	  result = _mkleq_qual(right, left, FALSE) || result;
	  result = cond_set_trigger(&right->u.var.vcond_set,
				    c_leq_v, left) || result;
	}
      return result;
    }
  else if (left->kind == qk_variable && right->kind == qk_constant)
    {
      bool result = FALSE;
      if (orig) /* Add no matter what -- may add to orig_lbc after has
		   also been added through transitivity */
	{
	  qual_set_insert(left->u.var.orig_ubc, right);
	  if (sign_qual(right) == sign_eq)
	    qual_set_insert(left->u.var.orig_lbc, right);
	}
      if ((!nonprop_qual(right) || orig) &&
	  qual_set_insert(left->u.var.ubc, right))
	{
	  /* Propagate if we haven't already */
	  qual q;
	  qual_set_scanner qs;

	  scan_quals(q, qs, left->u.var.lbc)
	    result = _mkleq_qual(q, right, FALSE) || result;
	  scan_quals(q, qs, left->u.var.lbv)
	    result = _mkleq_qual(q, right, FALSE) || result;
	  if (sign_qual(right) == sign_eq || qual_set_empty(right->u.elt.lbc))
	    /* Nonvariant qualifiers propagate in both directions.
	       Also, if right has no lower bounds then left <= right
	       ==> left = right. */
	  result = _mkleq_qual(right, left, FALSE) || result;
	  result = cond_set_trigger(&left->u.var.vcond_set,
				    v_leq_c, right) || result;
	}
      return result;
    }
  else
    {
      /* Both variables -- Propagate constants in both directions */
      bool result = FALSE;
      qual q1, q2;
      qual_set_scanner qs;

      if (qual_set_insert(left->u.var.ubv, right))
	{
	  insist(qual_set_insert(right->u.var.lbv, left));
	  scan_quals(q1, qs, left->u.var.lbc)
	    result = _mkleq_qual(q1, right, FALSE) || result;
	  
	  scan_quals(q2, qs, right->u.var.ubc)
	    result = _mkleq_qual(left, q2, FALSE) || result;
	}
      return result;
    }
}

bool mkleq_qual(qual left, qual right)
{
  return _mkleq_qual(left, right, TRUE);
}

/* left == right */
bool mkeq_qual(qual left, qual right)
{
  bool result;
  result = mkleq_qual(left, right);
  result = mkleq_qual(right, left) || result;
  return result;
}

/* left == right, plus cannot distinguish left and right anymore */
bool unify_qual(qual left, qual right)
{
  left = ecr_qual(left);
  right = ecr_qual(right);
  if (left == right) /* Short circuit to prevent loops in ecr_qual */
    return FALSE;
#ifdef DEBUG
  print_qual_raw(printf, left);
  printf(" %s = ", ptr_to_ascii(left));
  print_qual_raw(printf, right);
  printf(" %s\n", ptr_to_ascii(right));
#endif
  if (left->kind == qk_variable && right->kind == qk_variable)
    {
      qual new_ecr, new_link, q;
      qual_set_scanner qs;
      bool result = FALSE;

      if (right->u.var.preferred ||
	  (left->u.var.num_equiv <= right->u.var.num_equiv))
	{
	  new_ecr = right;
	  new_link = left;
	}
      else
	{
	  new_ecr = left;
	  new_link = right;
	}

      scan_quals(q, qs, new_link->u.var.lbv)
	result = _mkleq_qual(q, new_ecr, FALSE) || result; /* not original */

      scan_quals(q, qs, new_link->u.var.lbc)
	result = _mkleq_qual(q, new_ecr, FALSE) || result; /* not original */

      scan_quals(q, qs, new_link->u.var.orig_lbc)
	result = _mkleq_qual(q, new_ecr, TRUE) || result;  /* are original */

      scan_quals(q, qs, new_link->u.var.ubv)
	result = _mkleq_qual(new_ecr, q, FALSE) || result; /* not original */

      scan_quals(q, qs, new_link->u.var.ubc)
	result = _mkleq_qual(new_ecr, q, FALSE) || result; /* not original */

      scan_quals(q, qs, new_link->u.var.orig_ubc)
	result = _mkleq_qual(new_ecr, q, TRUE) || result;  /* are original */

      new_ecr->u.var.num_equiv += new_link->u.var.num_equiv;
      new_link->kind = qk_link;
      new_link->u.link = new_ecr;

      return result;
    }
  else
    {
      return mkeq_qual(left, right);
    }
}

/* Returns TRUE iff left <= right.  Requires that at least one of
   left, right is a constant.  By defn, returns TRUE if left and right
   are in distinct partial orders. */
bool leq_qual(qual left, qual right)
{
  left = ecr_qual(left);
  right = ecr_qual(right);

  assert(constant_qual(left) || constant_qual(right));
  if (left == right)
    return TRUE;     /* Reflexivity */

  /* XXX Fix for transitive partial order constraints */
  if (left->kind == qk_constant && right->kind == qk_constant)
    return (qual_set_member(left->u.elt.ubc, right) ||
	    !qual_set_member(left->u.elt.po->qualifiers, right));
  else if (left->kind == qk_variable)
    return (qual_set_member(left->u.var.ubc, right));
  else
    {
      assert (right->kind == qk_variable);
      return qual_set_member(right->u.var.lbc, left);
    }
}

#endif /* #IFDEF BITSET else */


/* Compute q such that left <= q and right <= q */
/*
bool lub_qual(qual left, qual right, qual *lub, location loc)
{
  bool result = FALSE;

  *lub = make_fresh_qvar(dummy_location);
  result = mkleq_qual(left, *lub);
  assert(!result);
  result = mkleq_qual(right, *lub) || result;
  return result;
}
*/

/* Returns TRUE iff left and right are the same.  Does not generate a
   constraint. */
bool eq_qual(qual left, qual right)
{
  return (ecr_qual(left) == ecr_qual(right));
}

/* A total ordering on qualifiers.  Returns 0 if left = right, a value
   <0 if left < right, or a value >0 if left > right */
int cmp_qual(qual left, qual right)
{
  left = ecr_qual(left);
  right = ecr_qual(right);
  return left - right;
}

/* Adds the conditional constraint l1<=r1 ==> l2<=r2.  This constraint
   is allowed only if at least one of {l1,r1} is a constant. */
bool cond_mkleq_qual(qual l1, qual r1, qual l2, qual r2)
{
  assert(constant_qual(l1) || constant_qual(r1));
#ifdef DEBUG
  print_qual_raw(printf, l1);
  printf(" %s <= ", ptr_to_ascii(l1));
  print_qual_raw(printf, r1);
  printf(" %s  ==>  ", ptr_to_ascii(r1));
  print_qual_raw(printf, l2);
  printf(" %s <= ", ptr_to_ascii(l2));
  print_qual_raw(printf, r2);
  printf(" %s\n", ptr_to_ascii(r2));
#endif

  l1 = ecr_qual(l1);
  r1 = ecr_qual(r1);
  l2 = ecr_qual(l2);
  r2 = ecr_qual(r2);
  if (leq_qual(l1, r1))
    /* Condition is true */
    return mkleq_qual(l2, r2);
  else if (constant_qual(l1) && constant_qual(r1))
    /* Conditional will never be true -- ignore constraint */
    return FALSE;
  else
    {
      /* Condition is not true yet; add constraint to pending set */
      qual v, c;
      cond_dir dir;

      if (constant_qual(l1))
	{ c = l1; v = ecr_qual(r1); dir = c_leq_v; }
      else
	{ c = r1; v = ecr_qual(l1); dir = v_leq_c; }
      assert (constant_qual(c) && variable_qual(v));
      cond_set_insert(&v->u.var.vcond_set, dir, c, l2, r2);
      return FALSE;
    }
}

/* If there are any conditions in conds triggered by dir and c, add them
   and remove the conditions from conds. */
bool cond_set_trigger(cond_set *conds, cond_dir dir, qual c)
{
  cond_set cur, prev;
  bool result = FALSE;

  prev = NULL;
  cur = *conds;
  while (cur)
    {
      /* XXX Also check transitivity in partial order */
      if (cur->dir == dir && cur->c == c)
	{
	  /* We found a match.  Remove from list... */
	  if (prev)
	    /* make prev's next skip over cur */
	    prev->next = cur->next;
	  else
	    /* no prev -- make conds (head of list) skip over cur */
	    *conds = cur->next;

	  /* ...and add constraint */
	  result = mkleq_qual(cur->left, cur->right) || result;
	}
      else
	/* Advance prev */
	prev = cur;

      /* Advance cur in any case */
      cur = cur->next;
    }
  return result;
}

/**************************************************************************
 *                                                                        *
 * Print/View Qualifiers                                                  *
 *                                                                        *
 **************************************************************************/

/* Apply f to all possible values of q.  f is applied to NULL in
   the error case. */
void scan_bounds(qual q, void (*f)(qual, void *), void *arg)
{
#ifdef BITSET
  set_scanner ss;
  po_info po;
  
  assert(q->kind == qk_variable);
  set_scan(all_pos, &ss);
  while ((po = set_next(&ss)))
    {
      if (!po->nonprop &&
	  bitset_full_range(q->u.var.bounds, po->first, po->last))
	/* Don't do anything if all quals in the partial order
	   are possible */
	;
      else if (!po->nonprop &&
	       bitset_empty_range(q->u.var.bounds, po->first, po->last))
	{
	  /* If none of the quals in the p.o. are possible, it's
	     an error */

	  /* XXX: Hack to make look like lattice case */
	  qual_set_scanner qs;
	  qual p;

	  scan_quals(p, qs, po->qualifiers)
	    f(p, arg);
	}
      else if (!po->nonprop)
	{
	  qual_set_scanner qs;
	  qual p;

	  scan_quals(p, qs, po->qualifiers)
	    if (bitset_member(q->u.var.bounds, p->u.elt.index))
	      f(p, arg);
	}
      else
	{
	  qual_set_scanner qs;
	  qual p;

	  assert(po->nonprop);
	  scan_quals(p, qs, po->qualifiers)
	    if (qual_set_member(q->u.var.orig_ubc, p) ||
		qual_set_member(q->u.var.orig_lbc, p))
	      f(p, arg);
	}
    }
#else /* #ifdef BITSET */
	qual_set_scanner qs;
	qual qcur;

	scan_quals(qcur, qs, q->u.var.lbc)
	  if ((sign_qual(qcur) == sign_pos) ||
	      (sign_qual(qcur) == sign_eq))
	    f(qcur, arg);

	scan_quals(qcur, qs, q->u.var.ubc)
	  if (sign_qual(qcur) == sign_neg)    /* eq handled above */
	    f(qcur, arg);
#endif
}

typedef struct print_info_S {
  printf_func pf;
  bool first;
  int size;
} *print_info;

void print_qual_fn(qual q, void *arg)
{
  print_info pi = (print_info) arg;

  assert(q->kind == qk_constant);
  if (!pi->first)
    pi->size += pi->pf(" ");
  pi->size += pi->pf("%s", q->u.elt.name);
  pi->first = FALSE;
}

/* Print the qualifiers, nicely */
int print_qual(printf_func pf, qual q)
{
  q = ecr_qual(q);
  switch(q->kind)
    {
    case qk_constant:
      {
	return pf("%s", q->u.elt.name);
      }
    case qk_variable:
      {
	struct print_info_S pi = {0, TRUE, 0};
	pi.pf = pf;

	scan_bounds(q, print_qual_fn, &pi);
	return pi.size;
      };
      break;
    default:
      fail("Unexpected kind %d for qualifiers\n", q->kind);
    }
}

/* Print the raw qualifiers */
int print_qual_raw(printf_func pf, qual q)
{
  if (!q)
    fail("Null qualifier in print_qual_raw\n");
  switch(q->kind)
    {
    case qk_constant: return pf("%s", q->u.elt.name);
    case qk_variable: return pf("%s", q->u.var.name);
    case qk_link:
      {
	int result = pf("[");
	result += print_qual_raw(pf, q->u.link);
	result += pf("]");
	return result;
      }
    default: fail("Unexpected kind %d for qualifier\n", q->kind);
    }
}

/* Returns color we should use for lub of colors 1 and 2 */
const char *combine_colors_pam(const char *color1, const char *color2)
{
  if (!color1) return color2;
  if (!color2) return color1;
  if (strcmp(color1, color2) == 0)
    return color1;
  return pam_color_multiqual;
}

void color_qual_fn(qual q, void *arg)
{
  const char **color = (const char **) arg;

  *color = combine_colors_pam(*color, color_qual(q));
}

/* Return the color of qualifier q.  q may be a constant or a variable */
const char *color_qual(qual q)
{
  q = ecr_qual(q);
  switch (q->kind)
    {
    case qk_constant:
      return q->u.elt.color;
    case qk_variable:
      {
	const char *color = NULL;

	scan_bounds(q, color_qual_fn, &color);
	return color;
    }
      break;
    default:
      fail("Unexpected kind %d for qualifier\n", q->kind);
    }
}

/* Return the name of qualifier q.  q may be a constant or a variable. */
const char *name_qual(qual q)
{
  q = ecr_qual(q);
  switch (q->kind)
    {
    case qk_constant: return q->u.elt.name;
    case qk_variable: return q->u.var.name;
    default:
      fail("Unexpected kind %d for qualifier\n", q->kind);
    }
}

/**************************************************************************
 *                                                                        *
 * Constraint Graph Traversal                                             *
 *                                                                        *
 **************************************************************************/

typedef enum direction {dir_lower, dir_upper, dir_both} dir;

/* Erase all the marks marked as TRUE reachable via TRUE marked nodes
   from q. */
static void traverse_clear_marks(qual q)
{
  qual qual_bound;
  qual_set_scanner qs;

  q = ecr_qual(q);
  if (!q->mark)
    return;
  q->mark = FALSE;

  if (q->kind == qk_variable)
    {
      scan_quals(qual_bound, qs, q->u.var.lbv)
	traverse_clear_marks(qual_bound);
      
      scan_quals(qual_bound, qs, q->u.var.ubv)
	traverse_clear_marks(qual_bound);
    }
  else
    assert(q->kind == qk_constant);
}

/* Reset the parent pointers on the spanning tree rooted at q to NULL. */
static void traverse_clear_parents(qual q)
{
  qual_set_scanner qs;
  qual b;

  q = ecr_qual(q);
  if (q->parent == NULL)
    return;
  q->parent = NULL;

  if (q->kind == qk_variable)
    {
      scan_quals(b, qs, q->u.var.lbv)
	traverse_clear_parents(b);

      scan_quals(b, qs, q->u.var.orig_lbc)
	traverse_clear_parents(b);

      scan_quals(b, qs, q->u.var.ubv)
	traverse_clear_parents(b);

      scan_quals(b, qs, q->u.var.orig_ubc)
	traverse_clear_parents(b);
    }
  else
    assert(q->kind == qk_constant);
}

/* Traverse the constraint graph starting from qualifier variable q,
   looking for constant qualifier c in direction d.  If such a path
   exists, set the parent pointers to create a shortest such path from
   c to q and return TRUE.  Otherwise return FALSE. */
bool find_shortest_path(qual q, qual c, dir d)
{
  region scratch_region;
  qual_seq queue;

  assert(variable_qual(q) && constant_qual(c));
  scratch_region = newregion();
  queue = new_qual_seq(scratch_region);
  qual_seq_push_right(queue, q);
  q->parent = q; /* Mark as root */
  assert(c->parent == NULL); /* Should be */

  while (!qual_seq_empty(queue))
    {
      qual q;

      q = get_qual_seq_element(qual_seq_head(queue));
      qual_seq_pop_left(queue);
      q = ecr_qual(q);
      if (q->mark)
	continue;

      q->mark = TRUE;
      if (q == c)
	break;
      else
	{
	  qual_set_scanner qs;
	  qual b;

	  if (d == dir_lower && qual_set_member(q->u.var.lbc, c))
	    {
	      scan_quals(b, qs, q->u.var.orig_lbc)
		if (!b->mark)
		  {
		    b->parent = q;
		    qual_seq_push_right(queue, b);
		  }
	      scan_quals(b, qs, q->u.var.lbv)
		if (!b->mark)
		  {
		    b->parent = q;
		    qual_seq_push_right(queue, b);
		  }
	    }
	  if (d == dir_upper && qual_set_member(q->u.var.ubc, c))
	    {
	      scan_quals(b, qs, q->u.var.orig_ubc)
		if (!b->mark)
		  {
		    b->parent = q;
		    qual_seq_push_right(queue, b);
		  }
	      scan_quals(b, qs, q->u.var.ubv)
		if (!b->mark)
		  {
		    b->parent = q;
		    qual_seq_push_right(queue, b);
		  }
	    }
	}
    }

  deleteregion(scratch_region);
  traverse_clear_marks(q);
  return (c->parent != NULL);
}

/* Traverse parent pointer chain from q */
static void traverse_parent_edges(qual q, qual_traverse_edge_func f, void *arg)
{
  qual b;

  q = ecr_qual(q);
  for (b = q; b->parent != b; b = ecr_qual(b->parent))
    f(b, b->parent, arg);
}

/* Traverse parent pointer chain from q in reverse */
void traverse_parent_edges_reverse(qual q, qual_traverse_edge_func f,
				   void *arg) {
  if (q->parent != q)
    {
      traverse_parent_edges_reverse(q->parent, f, arg);
      f(q->parent, q, arg);
    }
}

/* Call f(q1, q2, arg) for every edge q1->q2 on a shortest
   unidirectional path from qualifier variable q to constant qualifier
   c.  Does nothing if there is no such path.  If there are paths in
   both directions, traverses both. */
void traverse_shortest_path_edges(qual q, qual c, qual_traverse_edge_func f,
				  void *arg)
{
  if (find_shortest_path(q, c, dir_lower))
    traverse_parent_edges(c, f, arg);
  traverse_clear_parents(q);

  if (find_shortest_path(q, c, dir_upper))
    traverse_parent_edges_reverse(c, f, arg);
  traverse_clear_parents(q);
}

/* Call f(q', arg) for every node q' on all paths from qualifier q to
   constant qualifier c.  Does nothing if there is no such path. */
void __traverse_qual_graph_nodes(qual q, qual c, qual_traverse_node_func f,
			       void *arg)
{
  q = ecr_qual(q);
  assert(constant_qual(c));

  if (q->mark)
    return;
  q->mark = TRUE;

  if (q->kind == qk_variable)
    {
      bool traverse_upper, traverse_lower;
      qual_set_scanner qs;
      qual b;

      traverse_upper = qual_set_member(q->u.var.ubv, c);
      traverse_lower = qual_set_member(q->u.var.lbv, c);

      if (traverse_upper || traverse_lower)
	f(q, arg);

      if (traverse_upper)
	scan_quals(b, qs, q->u.var.ubv)
	  __traverse_qual_graph_nodes(b, c, f, arg);

      if (traverse_lower)
	scan_quals(b, qs, q->u.var.lbv)
	  __traverse_qual_graph_nodes(b, c, f, arg);
    }
  else
    {
      assert(q->kind == qk_constant);
      f(q, arg);
    }
}

/* Apply qtf to every *node* in the quals graph reachable in direction
   dir from q. */
static void _traverse_qual_graph_nodes(qual q, enum direction dir,
				       qual_traverse_node_func qtf,
				       void *arg) {
  qual qual_bound;
  qual_set_scanner qs;

  q = ecr_qual(q);

  if (q->mark)
    return;
  q->mark = TRUE;
  qtf(q, arg);
  if (q->kind == qk_variable)
    {
      bool
	traverse_lower = (dir == dir_lower || dir == dir_both),
	traverse_upper = (dir == dir_upper || dir == dir_both);

      if (traverse_lower)
	{
	  scan_quals(qual_bound, qs, q->u.var.lbv)
	    _traverse_qual_graph_nodes(qual_bound, dir, qtf, arg);
	  
	  scan_quals(qual_bound, qs, q->u.var.orig_lbc)
	    _traverse_qual_graph_nodes(qual_bound, dir, qtf, arg);
	}
      if (traverse_upper)
	{
	  scan_quals(qual_bound, qs, q->u.var.ubv)
	    _traverse_qual_graph_nodes(qual_bound, dir, qtf, arg);
	  
	  scan_quals(qual_bound, qs, q->u.var.orig_ubc)
	    _traverse_qual_graph_nodes(qual_bound, dir, qtf, arg);
	}
    }
  else
    assert(q->kind == qk_constant);
}

/* Apply qtf to every *non-transitive edge* in the quals graph
   reachable in direction dir from q. */
static void _traverse_qual_graph_edges(qual q, enum direction dir,
				       qual_traverse_edge_func qtf,
				       void *arg) {
  qual qual_bound;
  qual_set_scanner qs;

  q = ecr_qual(q);

  assert(q->kind == qk_variable);
  if (q->mark)
    return;
  q->mark = TRUE;
  switch (dir)
    {
    case dir_lower:
      scan_quals(qual_bound, qs, q->u.var.lbv)
	{
	  qtf(qual_bound, q, arg);
	  _traverse_qual_graph_edges(qual_bound, dir, qtf, arg);
	}
      scan_quals(qual_bound, qs, q->u.var.orig_lbc)
	qtf(qual_bound, q, arg);
      break;
    case dir_upper:
      scan_quals(qual_bound, qs, q->u.var.ubv)
	{
	  qtf(q, qual_bound, arg);
	  _traverse_qual_graph_edges(qual_bound, dir, qtf, arg);
	}
      scan_quals(qual_bound, qs, q->u.var.orig_ubc)
	qtf(q, qual_bound, arg);
      break;
    case dir_both:
      scan_quals(qual_bound, qs, q->u.var.lbv)
	{
	  if (!qual_bound->mark)
	    {
	      qtf(qual_bound, q, arg);
	      _traverse_qual_graph_edges(qual_bound, dir, qtf, arg);
	    }
	}
      scan_quals(qual_bound, qs, q->u.var.orig_lbc)
	qtf(qual_bound, q, arg);
      scan_quals(qual_bound, qs, q->u.var.ubv)
	{
	  if (!qual_bound->mark)
	    {
	      qtf(q, qual_bound, arg);
	      _traverse_qual_graph_edges(qual_bound, dir, qtf, arg);
	    }
	}
      scan_quals(qual_bound, qs, q->u.var.orig_ubc)
	qtf(q, qual_bound, arg);
      break;
    }
}

/* Traverse the edges in the qualifier graph.  po_bounds_only as above.
   arg is passed to f. */
struct traverse_edge_data {
  qual_traverse_edge_func f;
  void *arg;
  bool po_bounds_only;
};

void traverse_qual_graph_edges_lower(qual left, qual right, void *arg)
{
  struct traverse_edge_data *data = (struct traverse_edge_data *) arg;
  if (left->kind == qk_constant || !data->po_bounds_only ||
      !(qual_set_empty(left->u.var.lbc)))
    data->f(left, right, data->arg);
}

void traverse_qual_graph_edges_upper(qual left, qual right, void *arg)
{
  struct traverse_edge_data *data = (struct traverse_edge_data *) arg;
  if (right->kind == qk_constant || !data->po_bounds_only ||
      !(qual_set_empty(right->u.var.ubc)))
    data->f(left, right, data->arg);
}

void traverse_qual_graph_edges_both(qual left, qual right, void *arg)
{
  struct traverse_edge_data *data = (struct traverse_edge_data *) arg;
  if (left->kind == qk_constant || right->kind == qk_constant ||
      !data->po_bounds_only ||
      !(qual_set_empty(left->u.var.lbc)) ||
      !(qual_set_empty(left->u.var.ubc)) ||
      !(qual_set_empty(right->u.var.lbc)) ||
      !(qual_set_empty(right->u.var.ubc)))
    data->f(left, right, data->arg);
}

void traverse_qual_graph_edges(qual q, bool po_bounds_only,
			       qual_traverse_edge_func f, void *arg)
{
  struct traverse_edge_data data;
  bool traverse_both = FALSE;
  qual qual_bound;
  qual_set_scanner qs;

  data.f = f;
  data.po_bounds_only = po_bounds_only;
  data.arg = arg;

  q = ecr_qual(q);
  assert(q->kind == qk_variable);

  if (po_bounds_only)
    {
      scan_quals(qual_bound, qs, q->u.var.ubc)
	if (sign_qual(qual_bound) == sign_eq)
	  traverse_both = TRUE;
      scan_quals(qual_bound, qs, q->u.var.lbc)
	if (sign_qual(qual_bound) == sign_eq)
	  traverse_both = TRUE;
    }
  if (traverse_both)
      {
	_traverse_qual_graph_edges(q, dir_both, traverse_qual_graph_edges_both,
				   &data);
	traverse_clear_marks(q);
      }
  else
    {
      _traverse_qual_graph_edges(q, dir_lower, traverse_qual_graph_edges_lower,
				 &data);
      traverse_clear_marks(q);
      _traverse_qual_graph_edges(q, dir_upper, traverse_qual_graph_edges_upper,
				 &data);
      traverse_clear_marks(q);
    }
}

/* Print the graph of qualifiers for q to file.  If po_bounds_only is
   true, then only print the graph showing how partial order elements
   affect q; otherwise print all qualifiers reachable from q. */
void print_qual_graph_edge(qual left, qual right, void *arg)
{
  FILE *graph_file = (FILE *) arg;
  fprintf(graph_file, "%s -> %s\n", name_qual(left), name_qual(right));
}

void print_qual_graph(qual q, const char *file, bool po_bounds_only)
{
  FILE *graph_file;

  if (!(graph_file = fopen(file, "w")))
    {
      perror(file);
      return;
    }
  fprintf(graph_file, "digraph G {\n");
  traverse_qual_graph_edges(q, po_bounds_only, print_qual_graph_edge,
			    graph_file);
  fprintf(graph_file, "}\n");
  fclose(graph_file);
}

/**************************************************************************
 *                                                                        *
 * Hotspots                                                               *
 *                                                                        *
 **************************************************************************/