/*---------------------------------------------------------------------------
  These are the graph management functions.
  A graph is simply a list of clauses and possibly a list of
  links between clauses in the graph and maybe other
  graphs.
*/

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


/*---------------------------------------------------------------------------
  create a new graph.
*/
graph *NewGraph(char *name)
{
  graph *d;

  d = malloc(sizeof(*d));
  if (d==NULL) {
    eprintf("Allocation error in create graph",0,0,0);
    return d;
  }
  d->h = NULL;
  d->hsize = 0L;
  strcpy(d->name,name);
  d->cl = NULL;
  return d;
}

/*---------------------------------------------------------------------------
  prints a list of clauses
*/
int PrintClauseList(clause *c)
{
  int r;

  r = 1;
  while (c!=NULL) {
    c->id = r++;
    printf("%2d. ",c->id);
    PrintClause(c); printf("\n");
    c = c->next;
  }
  return 0;
}

/*---------------------------------------------------------------------------
  dump a list of clauses
*/
int DumpClauseList(clause *c)
{
  int r;

  r = 1;
  while (c!=NULL) {
    c->id = r++;
    DumpClause(c);
    c = c->next;
  }
  return 0;
}

/*---------------------------------------------------------------------------
  dump graph
*/
int DumpGraph(graph *d)
{
  long r;

  printf("\n------------------------------------------------------------\n");
  printf("Graph listing: '%s'\n",d->name);
  printf("Clauses:\n");
  DumpClauseList(d->cl);
  printf("Links:\n");
  if (d->hsize == 0) printf("  There are no links.\n");
  else
    for (r=0; r<d->hsize; ++r)
      PrintLink(d,r);
  printf("------------------- End of Listing ----------------------------\n");
  return 0;
}

/*---------------------------------------------------------------------------
  print graph
*/
int PrintGraph(graph *d)
{
  long r;

  printf("\n------------------------------------------------------------\n");
  printf("Graph listing: '%s'\n",d->name);
  PrintClauseList(d->cl);
  printf("Links:\n");
  if (d->hsize == 0) printf("  There are no links.\n");
  else
    for (r=0; r<d->hsize; ++r)
      PrintLink(d,r);
  printf("------------------- End of Listing ----------------------------\n");
  return 0;
}

/*---------------------------------------------------------------------------
  adds a resolution link.
  note that HeapInsert will update the k list in each clause.
  Since use changes, we recalc the score of all link (new and
  old) to either of the literals.
*/
int addreslink(graph *d,clause *p,int pit,clause *n,int nit)
{
  link k;

  k.type = RES;
  k.score= 0;
  k.p    = p;
  k.n    = n;
  k.pit  = pit;
  k.nit  = nit;
  k.pik  = p->numlinks;
  GrowLink(p);
  k.nik  = n->numlinks;               /* it is possible that p==n */
  GrowLink(n);
  ++p->use[pit];
  ++n->use[nit];
  HeapInsert(d,&k);
  return 0;
}
/*---------------------------------------------------------------------------
  This adds all the links it can between clauses c1 and c2 to the heap in d.
  If clause
*/
int AddLinks(graph *d,clause *c1,clause *c2)
{
  int i,j,rc;

  for (i=0; i<c1->numtins; ++i) {
    for (j=0; j<c2->numtins; ++j) {
      if (c1->pos[i] != c2->pos[j] && (c1!=c2 || i<j)) {
        rc = Unify(c1->t[i],c2->t[j],0);
        Ununify();
        if (rc<4) {                          /* success */
          if (c1->pos[i])
            addreslink(d,c1,i,c2,j);
          else
            addreslink(d,c2,j,c1,i);
        }
      }
    }
  }
  return 0;
}

/*---------------------------------------------------------------------------
  This adds a linked list of clauses to the graph.
  NOT-
  It also adds all
  the needed links.  If some clauses are subsumed, they are removed.
  Tautologies are removed.  If a clause has purities, it's links are
  all removed.
*/
int AddClauses(graph *d,clause *c,int topic,int sos)
{
  clause *p;

  while (c != NULL) {
    p = c->next;
    c->next = d->cl;
    c->prev = &d->cl;
    c->topic = topic;
    c->sos = sos;
    d->cl = c;
    if (c->next != NULL) c->next->prev = &c->next;
    c = p;
  }
  return 0;
}

/*---------------------------------------------------------------------------
  this removes the k-list from each clause
*/
int RemoveLinks(clause *c)
{
  int i;

  while (c!=NULL) {
    if (c->k != NULL)
      free(c->k);
    c->k = NULL;
    c->numlinks = 0;
    for (i=0; i<c->numtins; ++i) c->use[i] = 0;
    c = c->next;
  }
  return 0;
}

/*---------------------------------------------------------------------------
  This deletes the heap in d and recreates a new one.
*/
int BuildGraphLinks(graph *d)
{
  clause *c,*p;
  long i;

  ReleaseHeap(d);
  RemoveLinks(d->cl);

  c = d->cl;
  while (c != NULL) {
    p = c;
    while (p != NULL) {
      AddLinks(d,c,p);
      p = p->next;
    }
    c = c->next;
  }
  for (i=0; i<d->hsize; ++i)
    AdjustLink(d,i);

  return 0;
}

/*---------------------------------------------------------------------------
  remove clauses, of a certain topic or sos when topic is zero
*/
int RemoveClauses(graph *d,int topic)
{
  clause *c,*c2;
  int i=0;

  ReleaseHeap(d);
  RemoveLinks(d->cl);

  c = d->cl;
  while (1) {
    while (c!=NULL && !(topic?c->topic&topic:c->sos)) c=c->next;
    if (c==NULL) break;
    c2 = c->next;
    c->depth = 5;
    c->pruned = 1;
    FreeClause(c,d,1);
    c = c2;
    ++i;
  }
  return i;
}

/*---------------------------------------------------------------------------
  release all memory associated with the graph
*/
int ReleaseGraph(graph *d)
{
  clause *c1,*c2;

  ReleaseHeap(d);
  RemoveLinks(d->cl);

  c1 = d->cl;
  while (c1 != NULL) {
    c2 = c1->next;
    c1->depth = 5;
    c1->pruned = 1;
    FreeClause(c1,d,1);
    c1 = c2;
  }
  return 0;
}

/*---------------------------------------------------------------------------
  display the proof, returns number of steps
  it prints the parent with most depth first to make the proof more readable
*/
static int stepnum;

static int dispproof(clause *c)
{
  int a,b;

  if (c == NULL) return 0;
  if (c->mom==NULL || c->dad!=NULL && c->mom->depth < c->dad->depth) {
    dispproof(c->dad);    b=stepnum;
    dispproof(c->mom);    a=stepnum;
  } else {
    dispproof(c->mom);    a=stepnum;
    dispproof(c->dad);    b=stepnum;
  }

  printf("%2d. ",++stepnum);
  if (a==b)
    if (c->sos) printf("(quest) ");
    else        printf("(given) ");
  else          printf("(%2d,%2d) ",a,b);
  PrintClause(c);
  printf("\n");
  return 0;
}

int DisplayProof(clause *c)
{
  stepnum = 0;
  dispproof(c);
  return stepnum;
}

/*---------------------------------------------------------------------------
  Sets all the ancestors of the empty clause to depth=0.
*/
int MarkProof(clause *c)
{
  if (c == NULL) return 0;
  if (c->depth == 0) return 0;
  c->depth = 0;
  MarkProof(c->mom);
  MarkProof(c->dad);
  return 0;
}

/*---------------------------------------------------------------------------
  adjust all the links in a clause (re-evaluate them)
*/
int AdjustClause(graph *d,clause *c)
{
  int i;

  for (i=0; i<c->numlinks; ++i)
    AdjustLink(d,c->k[i]);

  return 0;
}

/*---------------------------------------------------------------------------
  remove prune marks
*/
int Unprune(graph *d)
{
  clause *c;

  for (c=d->cl; c!=NULL; c=c->next)
    c->pruned = 0;
  return 0;
}

/*---------------------------------------------------------------------------
  This deletes (hard) all clauses and links that were not in the
  original graph. (i.e. with depth != 0)
*/
int RestoreGraph(graph *d)
{
  clause *c;

  while (1) {
    c = d->cl;              /* find first non-0 */
    while (c!=NULL && c->depth==0) c=c->next;
    if (c==NULL) break;
    FreeClause(c,d,1);      /* hard delete */
  }
  Unprune(d);
  return 0;
}


#define getmem(x,s)                                             \
  if ((x = malloc(s))==NULL) {                                  \
    eprintf("Error in memory allocation in make child",0,0,0);  \
    return c;                                                   \
  }

/*---------------------------------------------------------------------------
  This create a child clause from p1, and p2.  It inherits all the
  terms except i1,i2 and all the links to them.
  Also parent pointers, depth,... are set.
*/
clause *MakeChild(graph *d,clause *p1,int i1,clause *p2,int i2)
{
  clause *c;
  int sz,i,j;

  getmem(c,sizeof(*c));

  c->next = d->cl;
  if (c->next != NULL) c->next->prev = &c->next;
  c->prev = &d->cl;
  d->cl = c;

  c->sos = p1->sos | p2->sos;
  c->proof = 0;
  c->pruned = 0;
  c->topic = p1->topic | p2->topic;
  c->id = 0;
  c->depth = 1 + (p1->depth < p2->depth ? p2->depth : p1->depth);
  c->mom = p1;
  c->dad = p2;
  c->numlinks = 0;
  c->k = NULL;
  c->t = NULL;
  c->use = NULL;
  c->pos = NULL;

  c->numtins = sz = p1->numtins + p2->numtins - 2;
  if (sz <= 0) return c;

  getmem(c->use,sz*sizeof(*c->use));
  getmem(c->pos,sz*sizeof(*c->pos));
  getmem(c->t  ,sz*sizeof(*c->t  ));

  for (j=0,i=0; i<p1->numtins; ++i)
    if (i != i1) {
      c->t[j] = CopyTin(p1->t[i]);
      c->pos[j] = p1->pos[i];
      c->use[j] = 0;
      ++j;
    }

  for (i=0; i<p2->numtins; ++i)
    if (i != i2) {
      c->t[j] = CopyTin(p2->t[i]);
      c->pos[j] = p2->pos[i];
      c->use[j] = 0;
      ++j;
    }

  for (i=0; i<p1->numtins; ++i)
    if (i != i1) ClearCopy(p1->t[i]);

  for (i=0; i<p2->numtins; ++i)
    if (i != i2) ClearCopy(p2->t[i]);

  for (i=0; i<p1->numlinks; ++i)
    InheritLink(d,p1->k[i],p1,c,i1,0);

  for (i=0; i<p2->numlinks; ++i)
    InheritLink(d,p2->k[i],p2,c,i2,p1->numtins-1);

  return c;
}

/*---------------------------------------------------------------------------
  Create a proof.  This returns NULL if no proof found, an empty clause
  if proof found, and non-empty clause if the set was proven satisfiable.

  Before calling, you must ensure that all links are connected and
  evaluated.  When this returns, all the original links will be in the
  heap, but they might be dead and disconnected.  Clauses with depth > 0
  are removed.  Those in the proof tree (except the leaves) should be
  deleted after displaying the proof.
*/
clause *FindProof(graph *d,int maxsteps,int debug,int occur)
{
  link *k;
  int n,rc;
  char s[10];
  clause *c;

  InitUnify();

  n = 0;
  while (1) {
    if (maxsteps==0) {                  /* max steps is zero */
      if ((++n & 31)==0)
        printf("steps %d, links %d \r",n,d->hsize);
    }
    else if (++n > maxsteps) {
      printf("\nNo proof found in %d steps.  Continue (yes)? ",n);
      scanf(" %8[^\n]",s);
      if (*s && *s!='y') break;
      maxsteps *=2;
    }
    k = HeapMax(d);
    if (k == NULL) {                      /* SATISFIABLE */
      RestoreGraph(d);
      return d->cl;
    }
    if (debug) DumpGraph(d);

    if (k->type != RES) {
      printf("unknown link type\n");
      HeapDelete(d,0L,0);
      continue;
    }
    rc = Unify(k->p->t[k->pit],k->n->t[k->nit],occur);
    if (rc < 4) {
      c = MakeChild(d,k->p,k->pit,k->n,k->nit);

      if (debug) {
        printf("After Make-child\n");
        DumpGraph(d);
      }
      if (c->numtins == 0) {
        Ununify();
        MarkProof(c);
        HeapDelete(d,0L,0);
        RestoreGraph(d);             /* EMPTY CLAUSE FOUND */
        return c;
      }
    }
    Ununify();
    HeapDelete(d,0L,0);
    AdjustClause(d,c);      /* evaluate all the links */
  }
  RestoreGraph(d);

  return NULL;                  /* PROOF NOT FOUND */
}