/*---------------------------------------------------------------------------
  heap functions
*/

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include "glob.h"

#define parent(i) ((i)-1>>1)
#define left(i) (((i)<<1)+1)
#define right(i) ((i)+1<<1)

/*---------------------------------------------------------------------------
  When a link is moved, its index changes.  Fix the clauses refering to
  this link.
*/
static int postmove(link *j,long r)
{
  j->p->k[j->pik] = r;
  j->n->k[j->nik] = r;
  return 0;
}


/*---------------------------------------------------------------------------
  Ascend the tree, insert k into the hole r.  if the parent is less than
  k, bring the parent down.
*/
static int upinsert(link **h,long r,link *k)
{
  long p;

  while (1) {
    p = parent(r);
    if (!r || HL(h,p).score >= k->score) break;
    memcpy(&HL(h,r),&HL(h,p),sizeof(*k));
    postmove(&HL(h,r),r);
    r=p;
  }
  memcpy(&HL(h,r),k,sizeof(*k));
  postmove(k,r);
  return r;
}

/*---------------------------------------------------------------------------
  descend the tree, if a child is greater than the insertion k, copy the
  child up.
*/
static int downinsert(link **h,long sz,long r,link *k)
{
  long c1,c2;

  while (1) {
    c1 = left(r);
    c2 = right(r);
    if (c1 >= sz) break;
    if (c2 >= sz || HL(h,c1).score > HL(h,c2).score)
      if (HL(h,c1).score > k->score) {
        memcpy(&HL(h,r),&HL(h,c1),sizeof(*k));
        postmove(&HL(h,r),r);
        r = c1;
      }
      else break;
    else if (HL(h,c2).score > k->score) {
      memcpy(&HL(h,r),&HL(h,c2),sizeof(*k));
      postmove(&HL(h,r),r);
      r = c2;
    }
    else break;
  }
  memcpy(&HL(h,r),k,sizeof(*k));
  postmove(k,r);
  return r;
}


/*---------------------------------------------------------------------------
  The heap insert function adds a new link to the heap according to the
  score of the link.  The index is returned.  Note that the index may
  not be valid following a delete (except in the link endpoints).
  the value -1 is returned on failure.
*/

long HeapInsert(graph *d, link *k)
{
  void *p;

  if (!(d->hsize & HMASK)) {            /* grow is needed */
    p = realloc(d->h,sizeof(p)*((d->hsize>>HEXP)+1));
    if (p==NULL) ERR("Realloc error in heap-insert");
    d->h = p;
    p = malloc(sizeof(link)*HSEG);
    if (p==NULL) ERR("Alloc error in heap-insert");
    d->h[d->hsize>>HEXP] = p;
  }
  d->hsize++;
  return upinsert(d->h,d->hsize-1,k);
}


/*---------------------------------------------------------------------------
  When a link is removed, fix the clauses refering to this link.
  If the clause has a pruned marker, it is already deleted.
*/

static int postdel(graph *d,clause *c,int i)
{
  link *k1;
  long m;

  if (c->pruned) return 0;

  --c->numlinks;

  /* if i was not the last link in the k-list, then copy
     the last one to position i and then adjust the other link, k1 */

  if (i < c->numlinks) {
    c->k[i] = m = c->k[c->numlinks];
    k1 = &HL(d->h,m);
    if (k1->p == c && k1->pik == c->numlinks)  k1->pik = i;
    if (k1->n == c && k1->nik == c->numlinks)  k1->nik = i;
  }
  return 0;
}


/*---------------------------------------------------------------------------
  this decrements the use counter for term t, and if any other links
  also refer to term t, then they are reevaluated.
*/
static int adjustterm(graph *d,clause *c,int t)
{
  link *k1;
  int i;
  long m;

  if (c->pruned) return 0;

  --c->use[t];
  for (i=0; i < c->numlinks; ++i) {
    m = c->k[i];
    k1 = &HL(d->h,m);
    if (k1->p == c && k1->pit == t)  AdjustLink(d,m);
    else
    if (k1->n == c && k1->nit == t)  AdjustLink(d,m);
  }
  return 0;
}


/*---------------------------------------------------------------------------
  This deletes a link from the heap, zero is returned when success.
  Since some links will get rearranged, their indices will change, but
  the endpoint clauses will get updated.
*/
int HeapDelete(graph *d, long r,int hard)
{
  long p;
  link k;

  if (!d->hsize || r>=d->hsize)
    ERR("Invalid heap-delete attempted");

  memcpy(&k,&HL(d->h,r),sizeof(k));

  d->hsize--;
  p = d->hsize;                         /* p is the bottom of the heap */
  if (p != r)
    if (k.score > HL(d->h,p).score)
      downinsert(d->h,d->hsize,r,&HL(d->h,p));
    else
      upinsert(d->h,r,&HL(d->h,p));
  if (!(p & HMASK)) free(&HL(d->h,p));   /* is p in the front of a seg? */

  k.p->k[k.pik] = DEAD;             /* prevent deleting the link twice */
  k.n->k[k.nik] = DEAD;

  postdel(d,k.p,k.pik);               /* remove k from link list */
  postdel(d,k.n,k.nik);

  adjustterm(d,k.p,k.pit);            /* adjust all links to same term */
  adjustterm(d,k.n,k.nit);

  /* check for purity */

  if (k.p->use[k.pit]<=0) FreeClause(k.p,d,hard);
  if (k.n->use[k.nit]<=0) FreeClause(k.n,d,hard);

  return 0;
}


/*---------------------------------------------------------------------------
  This adjusts the location of a link in the heap.  This needs to be called
  whenever the score of a link in the heap changes.  The new index is
  returned.
*/
long HeapAdjust(graph *d, long r)
{
  link t;

  memcpy(&t,&HL(d->h,r),sizeof(t));              /* temp copy of r */

  if (!r || t.score < HL(d->h,parent(r)).score)
    return downinsert(d->h,d->hsize,r,&t);

  return upinsert(d->h,r,&t);
}

/*---------------------------------------------------------------------------
  This recalculates the score and adjusts the link r.
*/
int AdjustLink(graph *d,long r)
{
  int s1,s2;

  s1 = HL(d->h,r).score;
  s2 = Evaluate(&HL(d->h,r));
  if (s1 != s2) HeapAdjust(d,r);

  return 0;
}

/*---------------------------------------------------------------------------
  This evaluates a link between two clauses to determine what its
  score should be.  It can consider any information in the clause
  except for the use of literals other that pit and nit.
*/
int Evaluate(link *k)
{
  int size1,size2,use,topic;
  long depth;
  int t;

  if (k->p == k->n)                   /* never do self links */
    return k->score=0;
  if (k->p->pruned || k->n->pruned)   /* should never happen */
    return k->score=0;
  if (!k->p->sos && !k->n->sos)       /* set of support */
    return k->score=0;

  topic = k->p->topic | k->n->topic;
  size1 = k->p->numtins;
    t = k->n->numtins;
    size2 = size1 + t;                /* total size         */
    if (t<size1) size1=t;             /* min size           */
  use = k->p->use[k->pit];
    t = k->n->use[k->nit];
    if (t<use) use=t;                 /* min use            */
  depth = k->p->depth;
    t = k->n->depth;
    if (t>depth) depth=t;             /* max depth          */

  if (use   > 1) depth += 10;         /* purity prefer */
  if (size1 > 1) depth += 5;          /* unit prefer */
  depth += size2;
  if (size2 < 3) depth = 0;            /* double units */

  depth += 100;
  return k->score=(99900L/depth);
}

/*---------------------------------------------------------------------------
  This returns a pointer to the top of the heap.
  It returns NULL if the top has a score <= zero.
*/
link *HeapMax(graph *d)
{
  if (d->hsize < 1) return NULL;
  if (HL(d->h,0).score <= 0) return NULL;
  return &HL(d->h,0);
}

/*---------------------------------------------------------------------------
  Frees and empties the heap
*/
int ReleaseHeap(graph *d)
{
  int i,s;

  s = d->hsize >> HEXP;
  for (i=0; i<s; ++i)
    if (d->h[i] != NULL) free(d->h[i]);
  free(d->h);
  d->h = NULL;
  d->hsize = 0;
  return 0;
}

/*---------------------------------------------------------------------------
  Inherit a link from parent to child, always puts it in the last
  spot in c->k.  The new link is not re-evaluated, it has the same
  score as the parent.
  i is the term to skip, j is the offset into c.
*/
int InheritLink(graph *d,long r,clause *p, clause *c,int i,int j)
{
  link k;

  memcpy(&k,&HL(d->h,r),sizeof(k));

  if (k.p == p) {
    if (k.pit == i) return 1;   /* skip */
    k.p = c;
    if (k.pit > i) --k.pit;
    k.pit += j;
  }
  else if (k.n == p) {
    if (k.nit == i) return 1;   /* skip */
    k.n = c;
    if (k.nit > i) --k.nit;
    k.nit += j;
  }
  else {
    eprintf("Inconsistency found in inheritlink",0,0,0);
    return 1;
  }
  if (k.p == k.n) return 1;     /* omit self links */
  k.p->use[k.pit] ++;
  k.n->use[k.nit] ++;
  k.pik = k.p->numlinks;
  k.nik = k.n->numlinks;
  GrowLink(k.p);
  GrowLink(k.n);
  HeapInsert(d,&k);
  return 0;
}

/*---------------------------------------------------------------------------
  Print a link
*/
int PrintLink(graph *d, long r)
{
  link *k;

  k = &HL(d->h,r);
  printf("%ld. t=%d s=%d  (%d,%d,%d)  (%d,%d,%d)\n",
    r,k->type,k->score,k->p->id,k->pit,k->pik,k->n->id,k->nit,k->nik);
  return 0;
}