/**************************************************************************

   Convert to conjuctive normal form.

   This function converts a wff in lox format to a lox in cnf.
   The result will have only AND, OR, NOT (in that order of nesting)
   and the AND and ORs will be right associated.  The other terms will be
   either SKOL, TERM, or VAR.  There may not be shared children.

***************************************************************************/

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

int removeimp(lox *t)       /* STEP 1 - convert to and,or,not. */
{
  lox *u,*v;

  if (t==NULL) return 0;

  switch (t->type) {
  case IF:
    removeimp(t->a);
    removeimp(t->b);
    u = NewLox(NOT);
    t->type = OR;
    u->a = t->b;
    t->b = u;
    break;
  case IFF:         /* a iff b ==> (-a or b) and (a or -b) */
    removeimp(t->a);
    removeimp(t->b);
    u = DeepCopyLox(t);
    v = NewLox(NOT);
    v->a = u->a;
    u->a = v;
    v = t->a;
    t->a = u;
    u->type = OR;
    u = NewLox(OR);
    u->a = v;
    v = NewLox(NOT);
    v->a = t->b;
    t->b = u;
    u->b = v;
    t->type = AND;
    break;
  case XOR:         /* a xor b ==> (a or b) and (-a or -b) */
    removeimp(t->a);
    removeimp(t->b);
    u = DeepCopyLox(t);
    v = NewLox(NOT);
    v->a = u->a;
    u->a = v;
    v = NewLox(NOT);
    v->a = u->b;
    u->b = v;
    v = t->b;
    t->b = u;
    u->type = OR;
    u = NewLox(OR);
    u->b = v;
    u->a = t->a;
    t->a = u;
    t->type = AND;
    break;
  case AND:
    removeimp(t->a);
    removeimp(t->b);
    break;
  case OR:
    removeimp(t->a);
    removeimp(t->b);
    break;
  case NOT:
    removeimp(t->a);
    break;
  case ALL:
    removeimp(t->b);
    break;
  case SOME:
    removeimp(t->b);
    break;
  default:
    ;
  }
  return 0;
}

int reducenot(lox *t)       /* reduce the scope of negation */
{
  lox *u,*v;

  if (t==NULL) return 0;

  switch (t->type) {
  case NOT:
    u = t->a;
    switch(u->type) {
    case NOT:
      v = u->a;
      memcpy(t,v,sizeof(*t));
      v->a = v->b = NULL;
      FreeLox(u);
      reducenot(t);
      break;
    case AND: case OR:           /* demorgan's law */
      v = NewLox(NOT);
      v->a = u->b;
      t->type = (AND + OR) - u->type;
      u->type = NOT;
      u->b = NULL;
      t->b = v;
      reducenot(v);
      reducenot(u);
      break;
    case ALL: case SOME:
      t->a = u->a;
      t->b = u;
      t->type = (ALL + SOME) - u->type;
      u->type = NOT;
      u->a = u->b;
      u->b = NULL;
      reducenot(u);
      break;
    default:
      ;
    }
    break;
  case AND: case OR:
    reducenot(t->a);
    reducenot(t->b);
    break;
  case ALL: case SOME:
    reducenot(t->b);
    break;
  default:
    ;
  }
  return 0;
}

/*-----------------------------------------------------------------------
  Set vc to the number of vars in a term.  If term is a var, then set
  vc to the index in the var list of the tin.  p is a list of all the
  vars defined in the current scope.  Existencial vars are converted to
  skolem functions with an arg list of all the vars in the current
  scope.
*/

int skolemize(lox *t, lox *p)
{
  lox *u,*v;

  if (t==NULL) return 0;

  switch (t->type) {
  case NOT:
    skolemize(t->a,p);
    break;
  case AND: case OR:
    skolemize(t->a,p);
    skolemize(t->b,p);
    break;
  case ALL:
    v = t->a;               /* the variable being quantified */
    if (v->a != NULL)
      eprintf("Warning, a variable has an arg list.",0,0,0);
    if (p == NULL) v->vc = 0;      /* the first var in the scope */
    else v->vc = p->vc + 1;
    v->type = VAR;
    v->a = p;
    skolemize(t->b,v);
    v->a = NULL;
    break;
  case SOME:
    v = t->a;
    if (v->a != NULL)
      eprintf("Warning, a variable has an arg list.",0,0,0);
    if (p == NULL) v->vc = -1;
    else v->vc = p->vc;
    v->type = SKOL;
    v->a = p;
    v->b = NewLox(SKOL);
    v->b->id = NewSkolem();
    skolemize(t->b,v);
    v->a = NULL;
    FreeLox(v);                    /* remove the SOME quantifier */
    u = t->b;
    memcpy(t,u,sizeof(*t));
    u->a = u->b = NULL;
    FreeLox(u);
    break;
  case TERM:
    v = p;
    while (v != NULL && v->id != t->id) v = v->a;
    if (v == NULL)
      skolemize(t->a,p);
    else {                  /* t is a variable declared in v */
      if (t->a != NULL)
        eprintf("Warning, a variable cannot have an arg list.",0,0,0);
      if (v->type == VAR)
        t->type = VAR;
      else {            /* v is a skolem function, create var list */
        t->type = SKOL;
        t->id = v->b->id;
        t->vc = v->vc + 1;
        t->a = NULL;
        while (v != NULL) {
          if (v->type == VAR) {
            u = NewLox(VAR);
            u->b = t->a;
            t->a = u;
            u->id = v->id;
            u->vc = v->vc;
          }
          v = v->a;
        }
      }
    }
    skolemize(t->b,p);      /* tail recursion */
    break;
  default:
    ;
  }
  return 0;
}

#define TT t->type
#define LT u->type
#define RT v->type

int reduceor(lox *t)       /* put ors under the ands. */
{
  lox *u,*v;

  if (t==NULL) return 1;
  if (TT != AND && TT != OR && TT != ALL) return 1;

  reduceor(t->a);              /* bottom up reduction */
  reduceor(t->b);

  while (1) {
    u = t->a;
    v = t->b;
    if (TT == AND && LT == AND) {
      t->a = u->b;                    /* make and right assoc. */
      t->b = u;
      u->b = v;
    }
    else if (TT == OR && RT == AND) {
      TT = AND;                       /* convert a+bc to (a+b)(a+c) */
      RT = OR;
      u = NewLox(OR);
      u->a = t->a;
      t->a = u;
      u->b = v->a;
      v->a = DeepCopyLox(u->a);
      reduceor(u);
      reduceor(v);
    }
    else if (TT == OR && LT == AND) {
      TT = AND;                       /* convert ab+c to (a+c)(b+c) */
      LT = OR;
      v = NewLox(OR);
      v->b = t->b;
      t->b = v;
      v->a = u->b;
      u->b = DeepCopyLox(v->b);
      reduceor(u);
      reduceor(v);
    }
    else if (TT == ALL && RT == AND) {
      TT = AND;                       /* convert all ab to all a & all b */
      RT = ALL;
      u = NewLox(ALL);
      u->b = v->a;
      v->a = t->a;
      t->a = u;
      u->a = DeepCopyLox(v->a);
      reduceor(v);
    }
    else if (TT == OR && LT == OR) {
      t->a = u->b;                    /* make or right assoc. */
      t->b = u;
      u->b = v;
    }
    else break;
  }
  return 0;
}


/*---------------------------------------------------------------------------
  Negates a lox (not in cnf).
*/
lox *Negate(lox *t)
{
  lox *u;

  u = NewLox(NOT);
  u->a = t;
  return u;
}


/*---------------------------------------------------------------------------
  main function of this file.
*/
int ConvertCNF(lox *t)
{
  removeimp(t);
  reducenot(t);
  skolemize(t,NULL);
  reduceor(t);
  return 0;
}