/*---------------------------------------------------------------------------
  These are the clause management functions.
*/

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


/*---------------------------------------------------------------------------
  Dump clause
*/
int DumpClause(clause *c)
{
  int i;

  printf("%d. f=%d-%d-%d t=%d d=%d nt=%d nl=%d\n",
    c->id,c->sos,c->proof,c->pruned,c->topic,
    c->depth,c->numtins,c->numlinks);
  for (i=0; i<c->numtins; ++i) {
    printf("    %d, ",c->use[i]);
    if (!c->pos[i]) printf("not ");
    DumpTin(c->t[i],0);
    printf("\n");
  }
  printf("    k=");
  for (i=0; i<c->numlinks; ++i) printf("%d ",c->k[i]);
  printf("\n");
  return 0;
}

/*---------------------------------------------------------------------------
  Print clause
*/
int PrintClause(clause *c)
{
  int i;

  for (i=0; i<c->numtins; ++i) {
    if (i) printf(" or ");
    if (!c->pos[i]) printf("not ");
    PrintTin(c->t[i],0);
  }
  printf(";");
  return 0;
}

/*---------------------------------------------------------------------------
  Deletes a clause from the graph.  This calls HeapDelete which might call
  us back, that is why the "pruned" is used to ignore call backs.
  The memory is not actually freed unless depth>0 and hard=1.
*/
#define kfree(x) if (x!=NULL) { free(x); x=NULL;}

int FreeClause(clause *c, graph *d,int hard)
{
  int i;

  if (!c->pruned) {
    c->pruned = 1;                 /* this means "already deleted" */
    for (i=0; i<c->numlinks; ++i)
      if (c->k[i] != DEAD)
        HeapDelete(d,c->k[i],hard);

    c->numlinks = 0;
    kfree(c->k);
    for (i=0; i<c->numtins; ++i)
      c->use[i] = 0;
  }
  if (c->depth && hard) {
    if (c->next != NULL) c->next->prev = c->prev;
    *c->prev = c->next;
    if (c->numtins) {
      kfree(c->use);
      kfree(c->pos);
      for (i=0; i<c->numtins; ++i)
        DeleteTin(c->t[i]);
      kfree(c->t);
    }
    kfree(c);
  }
  return 0;
}

/*---------------------------------------------------------------------------
  fix vc, this counts the vars in a term, assigns each one a unique id,
  sets the vc at all levels, it returns a list of all the unique vars.
  To call, first init numvars=0 and p=NULL.
*/
static int numvars;

lox *FixVC(lox *t,lox *p)
{
  lox *u;

  if (t==NULL) return p;
  if (t->type==VAR) {
    for (u=p; u!=NULL; u=u->a)
      if (u->id==t->id) {
        t->vc = u->vc;                /* t is not unique */
        return FixVC(t->b,p);
      }
    t->vc = numvars++;                /* t is unique */
    t->a = p;                         /* thread the vars together */
    return FixVC(t->b,t);
  }

  u=FixVC(t->a,p);
  t->vc = numvars;
  u=FixVC(t->b,u);
  return u;
}

int newc3(clause *c,lox *t, lox *v,int pos)
{
  int i,n;
  lox *u,*w,*u2;
  vars *h;

  if (t==NULL || t->type !=TERM) {
    eprintf("Error in parameters to newc3, type=%d",t->type,0,0);
    return 1;
  }
  n = ++c->numtins;                           /* grow the clause */
  c->use = realloc(c->use,n*sizeof(*c->use));
  c->pos = realloc(c->pos,n*sizeof(*c->pos));
  c->t   = realloc(c->t  ,n*sizeof(*c->t));
  if (c->use==NULL || c->pos==NULL || c->t==NULL)
    eprintf("Error in memory reallocation in newc3",0,0,0);

  --n;
  c->use[n] = 0;
  c->pos[n] = pos;
  numvars = 0;                      /* this is used by fixvc */
  u = FixVC(t,NULL);                /* get u=list of vars */
  c->t[n] = NewTin(t);
  h = c->t[n]->nx = NewVars(numvars);
  if (u!=NULL && u->vc != numvars-1)
    eprintf("Inconsistency in newc3",0,0,0);

  for (i=0; i<numvars; ++i)
    h->var[i] = NULL;
  for ( ; u!=NULL; u=u2) {
    for (w=v; w!=NULL; w=w->a)
      if (w->id == u->id) break;
    if (w == NULL) eprintf("Internal error - undeclared var",0,0,0);
    else h->var[u->vc] = (tin *)w->b;
    u2 = u->a;
    u->a = NULL;                    /* unthread the vars */
  }
  for (i=0; i<numvars; ++i)
    if (h->var[i] == NULL) eprintf("Internal error - unfound var",0,0,0);
  return 0;
}

int newc2(clause *c,lox *t, lox *v)
{
  if (t==NULL) return 0;

  switch (t->type) {
  case OR:
    newc2(c,t->a,v);
    newc2(c,t->b,v);
    break;
  case ALL:
    t->a->a = v;
    v = t->a;
    v->b = (lox *)NewTin(NULL);          /* unbound var */
    newc2(c,t->b,v);
    v->a = NULL;
    v->b = NULL;
    break;
  case NOT:
    newc3(c,t->a,v,0);
    break;
  case TERM:
    newc3(c,t,v,1);
    break;
  default:
    eprintf("Error, top of clause has type %d.",t->type,0,0);
  }
  return 0;
}

/*---------------------------------------------------------------------------
  Creates a new clause given a lox tree of disjuncts.
  This sets numtins,use,pos,t only.  input t cannot be NULL.
*/
clause *NewClause(lox *t)
{
  clause *c;

  c = malloc(sizeof(*c));
  if (c==NULL)
    eprintf("Error in memory allocation in new-clause",0,0,0);
  c->numtins = 0;
  c->use = NULL;
  c->pos = NULL;
  c->t = NULL;
  newc2(c,t,NULL);
  return c;
}


/*---------------------------------------------------------------------------
  Convert a cnf expression into a list of clauses.
  The cnf tree is not altered by this function.
*/
clause *Clausify(lox *cnft)
{
  lox *t;
  clause *c,*p;

  p = NULL;
  for (t=cnft; t!=NULL; t=t->b) {
    if (t->type == AND)
      c = NewClause(t->a);
    else
      c = NewClause(t);
    c->next = p;
    c->sos = 0;
    c->proof = 0;
    c->pruned = 0;
    c->topic = 0;
    c->id = 0;
    c->depth = 0;
    c->numlinks = 0;
    c->k = NULL;
    c->mom = NULL;
    c->dad = NULL;
    if (p != NULL) p->prev = &c->next;
    p = c;
    if (t->type != AND) break;
  }
  if (p != NULL) p->prev = NULL;

  return p;
}


/*---------------------------------------------------------------------------
  makes the link list longer if needed
*/
int GrowLink(clause *c)
{
  void *p;
  if ((c->numlinks % LNKCHK)==0) {
    p = realloc(c->k,(c->numlinks+LNKCHK)*sizeof(c->k[0]));
    if (p==NULL) eprintf("Allocation error in grow links.",0,0,0);
    else c->k = p;
  }
  ++c->numlinks;
  return 0;
}