/****************************************************************************
  This is the common include file for the ELS project
****************************************************************************/
#ifdef C2
#define malloc(x) mymalloc(x)
#define free(x) myfree(x)
#define realloc(x,y) myrealloc(x,y)
void *mymalloc(unsigned short x);
void *myrealloc(void *Ptr,unsigned short x);
unsigned myfree(void *Ptr);
#endif
/*---------------------------------------------------------------------------
  error handler macros (and dprintf is for debug)
*/
#define eprintf(f,a,b,c) printf(f "\n",a,b,c)
#define dprintf(f,a)
#define ERR(m) { printf(m "\n"); return -1; }

/*---------------------------------------------------------------------------
  parser data structures
*/
enum loxtype { SKOL, VAR, TERM,
               ALL, SOME,
               NOT, AND, OR, XOR, IF, IFF };

typedef struct lox {
  int  type;
  int  id;              /* key for symbol table */
  int  vc;              /* var count or index */
  struct lox *a,*b;     /* a=arglist, b=next brother */
} lox;

/*---------------------------------------------------------------------------
  Data structures for term instances and clauses

  The use of tin is:  When st=NULL and nx=NULL, this is an unbound
  variable term.  When st=NULL and nx<>NULL this is a chain, follow
  the nx to the next tin in the chain.  When st<>NULL this is a term instance,
  look at st->vc to get number of variables (the structure size can vary).
  The copy field is usually NULL.  When the term is copied, copy is set to
  its copy.  This handles DAGs and cyclic structures.
*/
typedef struct tin {
  struct tin *copy;
  lox  *st;
  struct vars {
    struct vars *copy;
    struct tin  *var[1];
  } *nx;              /* points to either a tin or a vars */
} tin;

typedef struct vars vars;

/*---------------------------------------------------------------------------
  clause structures.
  the use,pos,t are parallel arrays.
  k is an array of link indices.  the k array is allocated in chunks CKC.
  note: prev points to the previous next pointer. (only used for del clause)
  It is assumed that all links to a clause belong to the same heap.
*/
#define LNKCHK 8
#define DEAD -99
enum clause_flag { ACTIVE=1, SOS=2, PRUNE=4 };

typedef struct clause {
  unsigned sos:1;
  unsigned proof:1;
  unsigned pruned:1;
  int  topic;
  int  id;
  int  depth;
  int  numtins;
  int  *use;      /* number of times each tin is used in a link  */
  int  *pos;      /* the signs of the tins 1=pos 0=neg  */
  tin  **t;
  int  numlinks;
  long *k;
  struct clause *mom,*dad;      /* parent clauses */
  struct clause *next,**prev;
} clause;

enum linktype { RES, FAC };

typedef struct link {
  int  type;
  int  score;
  clause *p,*n;         /* two clauses */
  int  pit,nit;         /* index to tin array in clause */
  int  pik,nik;         /* index to link array in clause */
} link;

/*---------------------------------------------------------------------------
  A heap is a complicated structure, it is a two dimensional array to allow
  more that one segment to be addressed.  The number of links stored in
  each segment of the heap can vary, but the size of each segment usually
  must be less than 64K.
*/

#define HEXP 4
#define HSEG (1<<HEXP)
#define HMASK (HSEG-1)
#define HL(h,i)  (h[(i)>>HEXP][(i)&HMASK])

typedef struct graph {
  long hsize;
  link **h;            /* two dimensional array of links */
  clause *cl;           /* doubly-linked list of clauses */
  char name[80];
} graph;

/*----------- SYMT.C -----------*/
int NewSymTable();
int EmptySymTable();
int AddSymbol(char *s);
int FindSymbol(char *s);
char *GetSymbol(int key);
int DeleteSymbol(int key);
int NumSymbols();
int NumBytes();
int NewSkolem();
int DumpTable(FILE *f);
/*----------- PARS.C -----------*/
int InitParser();
lox *ParseLox();
int PrintLox(lox *t);
/*----------- SCAN.C -----------*/
int SetSrc(char *fn);
int GetToken(void);
int GetLine(char *s);
/*----------- CCNF.C -----------*/
lox *Negate(lox *t);
int ConvertCNF(lox *t);
/*----------- LOXX.C -----------*/
lox *NewLox(int kind);
int FreeLox(lox *t);
lox *DeepCopyLox(lox *t);
lox *CopyLox(lox *t);
/*----------- HEAP.C -----------*/
long HeapInsert(graph *d, link *k);
int HeapDelete(graph *d, long r,int hard);
long HeapAdjust(graph *d, long r);
int AdjustLink(graph *d,long r);
int Evaluate(link *k);
link *HeapMax(graph *d);
int ReleaseHeap(graph *d);
int InheritLink(graph *d,long r,clause *p, clause *c,int i,int j);
int PrintLink(graph *d, long r);
/*----------- STRU.C -----------*/
int AddStrucs(lox *t);
/*----------- CLAU.C -----------*/
int PrintClause(clause *c);
int DumpClause(clause *c);
int FreeClause(clause *c, graph *d,int hard);
clause *NewClause(lox *t);
clause *Clausify(lox *cnft);
int GrowLink(clause *c);
/*----------- GRAF.C -----------*/
graph *NewGraph(char *name);
int PrintClauseList(clause *c);
int DumpGraph(graph *d);
int PrintGraph(graph *d);
int addreslink(graph *d,clause *p,int pit,clause *n,int nit);
int AddLinks(graph *d,clause *c1,clause *c2);
int AddClauses(graph *d,clause *c,int topic,int sos);
int BuildGraphLinks(graph *d);
int RemoveClauses(graph *d,int topic);
int ReleaseGraph(graph *d);
int DisplayProof(clause *c);
int MarkProof(clause *c);
int Unprune(graph *d);
int RestoreGraph(graph *d);
clause *MakeChild(graph *d,clause *p1,int i1,clause *p2,int i2);
clause *FindProof(graph *d,int maxsteps,int debug,int occur);
/*----------- TINN.C -----------*/
int PrintTin(tin *t,int depth);
int DumpTin(tin *t,int depth);
tin *NewTin(lox *st);
vars *NewVars(int size);
tin *CopyTin(tin *t);
int ClearCopy2(vars *t,int size);
int ClearCopy(tin *t);
int DeleteTin(tin *t);
int InitUnify(void);
int Unify(tin *t1, tin *t2,int occur);
int Ununify(void);