/* Parser for .log files, C version.
   Copyright (C) 2004 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*/

%{
#include <stdlib.h>
#include <stddef.h>
#include <stdio.h>
#include <string.h>
#include "cproof.tab.h"

  extern FILE *yyin, *yyout;
  extern char *yytext;
  extern int yyleng;

  void *xmalloc (size_t n)
    {
      void *p = malloc (n);

      if (p==NULL)
	{
	  fprintf (stderr, "No more memory allocating %ld bytes.\n", n);
	  fflush (stderr);
	  exit (10);
	}
      return p;
    }

  char bsd_cursors[] = { '-', '\\', '|', '/' };

  struct bsd_cursor {
    int time;
  };

#define BSD_CURSOR(name) struct bsd_cursor name = { -1, }

  void bump_bsd_cursor (struct bsd_cursor *cur)
    {
      if (cur->time<0)
	;
      else fputc (8, stderr);
      if (++cur->time==4)
	cur->time = 0;
      fputc (bsd_cursors [cur->time], stderr);
      fflush (stderr);
    }

  int verbose = 2;
  long nClauses = 0;
#define CLAUSE_STEP 1000
  long nClausesMod = 0;

  long nDeds = 0;

#define TABLE_RECORD
  /* define TABLE_RECORD to get a definitely unique hash code for each clause;
     this involves storing the clause names, which is probably a bad idea, as
     far as memory usage is concerned. */

#ifdef OBSOLETE
#define yyerror(msg) yy_error(yylloc.first_line,yylloc.first_column,yylloc.last_line,yylloc.last_column,msg)
#endif

#define yyerror(msg) yy_error (msg)

  void yy_error (/*int l1, int c1, int l2, int c2,*/
		 char *msg)
    {
      fputs (msg, stderr);
#ifdef OBSOLETE
      fprintf (stderr, "line%s %d",((l1!=l2)?"s":""), l1+1);
      if (c1!=0)
	fprintf (stder, "(%d)", c1);
      if (l2!=l1 || c2!=c1)
	{
	  fprintf (stderr, "-%d", l2+1);
	  if (c2!=0)
	    fprintf (stderr, "(%d)", c2);
	}
#endif
      if (yytext[0]!=0)
	{
	  fputs (" (at '", stderr);
	  fputs (yytext, stderr);
	  fputs ("')", stderr);
	}
      fputc ('\n', stderr);
      fflush (stderr);
    }

#ifdef TOO_MANY_COLLISIONS
  /* The following hash function comes from a post on comp.theory and comp.lang.misc
     by wang@cup.hp.com (Thomas Wang), Thu, 3 Aug 1995 01:03:59 GMT.

     Message (source code elided; the first elided source code is the one I am using,
     up to a few minor changes):

Article: 1829 of comp.theory
Newsgroups: comp.theory,comp.lang.misc
Path: frclnews!bullnews.bull.fr!news2.EUnet.fr!EU.net!howland.reston.ans.net!swrinde!sdd.hp.com!hpscit.sc.hp.com!hpax!wang
From: wang@cup.hp.com (Thomas Wang)
Subject: Re: Looking for high-quality hashing function for dynamic linker
Sender: news@hpax (News Admin)
Message-ID: <DCpMyn.7oC@cup.hp.com>
Date: Thu, 3 Aug 1995 01:03:59 GMT
References: <95-08-021@comp.compilers>
Nntp-Posting-Host: capella.cup.hp.com
Organization: Hewlett-Packard
X-Newsreader: TIN [version 1.2 PL0.7]
Lines: 92
Xref: frclnews comp.theory:1829 comp.lang.misc:4388

Eric Benson (eb@kaleida.com) wrote:

> Is it feasible to compute a signature consisting of a few (say, less than
> ten) 32 bit words and use this for comparison instead of the entire set of
> names?  A false positive comparison would probably result in a severe
> malfunction so it should be extremely unlikely, say one-in-a-billion or
> less.  I can spend a big chunk of CPU time in the compilation environment
: to compute this signature if necessary.  I have a 29-bit CRC hash function
: already available.  Is this, or some multi-word variant of it, good enough
> If so, does anyone have a larger-than-29-bit CRC
> implementation?  Does anyone have any references to relevant research?


This is my string hashing function.  It came from an ACM article.

[...]

This is an integer hash function.  I am not comfortable with this, since it
uses floating point arithmetic.  Who knows what kind of rounding modes each
machine have?  It came from the Knuth book.

[...]

I am still looking for good 32 bit hash function.  Feel free to send some
to me.


  -Thomas Wang              (Software Engineer, Enterprise Objects Program)
   wang@cup.hp.com          http://hpeopose.cup.hp.com/~wang/wang.html
  */

  const static u_int8_t uuHashTab256[256] =
    {
      1,   87,  49,  12,  176, 178, 102, 166, 121, 193, 6,   84,  249, 230, 44,  163,
      14,  197, 213, 181, 161, 85,  218, 80,  64,  239, 24,  226, 236, 142, 38,  200,
      110, 177, 104, 103, 141, 253, 255, 50,  77,  101, 81,  18,  45,  96,  31,  222,
      25,  107, 190, 70,  86,  237, 240, 34,  72,  242, 20,  214, 244, 227, 149, 235,
      97,  234, 57,  22,  60,  250, 82,  175, 208, 5,   127, 199, 111, 62,  135, 248,
      174, 169, 211, 58,  66,  154, 106, 195, 245, 171, 17,  187, 182, 179, 0,   243,
      132, 56,  148, 75,  128, 133, 158, 100, 130, 126, 91,  13,  153, 246, 216, 219,
      119, 68,  223, 78,  83,  88,  201, 99,  122, 11,  92,  32,  136, 114, 52,  10,
      138, 30,  48,  183, 156, 35,  61,  26,  143, 74,  251, 94,  129, 162, 63,  152,
      170, 7,   115, 167, 241, 206, 3,   150, 55,  59,  151, 220, 90,  53,  23,  131,
      125, 173, 15,  238, 79,  95,  89,  16,  105, 137, 225, 224, 217, 160, 37,  123,
      118, 73,  2,   157, 46,  116, 9,   145, 134, 228, 207, 212, 202, 215, 69,  229,
      27,  188, 67,  124, 168, 252, 42,  4,   29,  108, 21,  247, 19,  205, 39,  203,
      233, 40,  186, 147, 198, 192, 155, 33,  164, 191, 98,  204, 165, 180, 117, 76,
      140, 36,  210, 172, 41,  54,  159, 8,   185, 232, 113, 196, 231, 47,  146, 120,
      51,  65,  28,  144, 254, 221, 93,  189, 194, 139, 112, 43,  71,  109, 184, 209
    };

  u_int32_t uuHashCharStar(char *buf_ptr)
    {
      u_int8_t hash1 = 17;
      u_int8_t hash2 = 233;
      u_int8_t hash3 = 61;
      u_int8_t hash4 = 109; /* all prime numbers */

      while (*buf_ptr != '\0')
	{
	  hash1 = uuHashTab256[ hash4 ^ *((u_int8_t*) buf_ptr++) ];
	  if (*buf_ptr == '\0')
	    break;
	  hash2 = uuHashTab256[ hash1 ^ *((u_int8_t*) buf_ptr++) ];
	  if (*buf_ptr == '\0')
	    break;
	  hash3 = uuHashTab256[ hash2 ^ *((u_int8_t*) buf_ptr++) ];
	  if (*buf_ptr == '\0')
	    break;
	  hash4 = uuHashTab256[ hash3 ^ *((u_int8_t*) buf_ptr++) ];
	};
      return(
	     ((u_int32_t) hash1) |
	     (((u_int32_t) hash2) << 8) |
	     (((u_int32_t) hash3) << 16) |
	     (((u_int32_t) hash4) << 24)
	     );
    }
#endif

#define EXACT_HASH

#ifdef EXACT_HASH
#undef TABLE_RECORD
  struct trie_alt {
    struct trie *next; /* otherwise, eat up prefix s, then go to next */
    char s[1];
  };

  struct trie {
    struct cinfo *cinfo;
    int n_alt;
    struct trie_alt *alt[1]; /* list of trie_alts, encoding map from prefixes of
				recorded strings to corresponding tries.
				Each prefix is pairwise incomparable with each
				other in the prefix ordering; in fact they even do
				not start with the same letter. */
  };

  struct trie *theTrie = NULL;

  struct trie *uuHashCharStar(char *buf_ptr, int createp)
    {
      if (theTrie==NULL)
	{ /* initialization. */
	  theTrie = xmalloc (offsetof(struct trie, alt[0]));
	  theTrie->cinfo = NULL;
	  theTrie->n_alt = 0;
	}
      {
	struct trie **tp = &theTrie;
	struct trie *t;
	char cb;

      again:
	t = *tp;
	cb = buf_ptr[0];
	if (cb==0)
	  {
	    return t;
	  }
	{
	  int j, nalt;

	  nalt = t->n_alt;
	  for (j=0; j<nalt; j++)
	    {
	      struct trie_alt *alt = t->alt[j];
	      char cs = alt->s[0];

	      if (cb>cs)
		continue;
	      if (cs==cb) /* then share a subbranch */
		{
		  char *s, *b;
		  int i;

		  /* find longest common prefix first */
		  for (s=alt->s, b=buf_ptr; (cs = *s++)!=0; )
		    {
		      cb = *b++;
		      if (cb!=cs)
			break;
		    }
		  if (cs==0) /* alt->s is a prefix of buf_ptr */
		    {
		      buf_ptr = b;
		      tp = &alt->next;
		      goto again; /* so insert rest of buf_ptr into son trie. */
		    }
		  s--;
		  i = s-alt->s;
		  /* otherwise, split alt into prefix + suffix, and insert. */
		  if (createp)
		    {
		      struct trie *newt;
		      struct trie_alt *pre_alt, *suf_alt;
		      int reml = strlen (s);

		      suf_alt = xmalloc (offsetof(struct trie_alt, s[reml+1]));
		      suf_alt->next = alt->next;
		      strcpy (suf_alt->s, s);
		      newt = xmalloc (offsetof(struct trie, alt[1]));
		      newt->cinfo = NULL;
		      newt->n_alt = 1;
		      newt->alt[0] = suf_alt;
		      pre_alt = xmalloc (offsetof(struct trie_alt, s[i+1]));
		      pre_alt->next = newt;
		      memcpy (pre_alt->s, alt->s, i);
		      pre_alt->s[i] = 0;
		      t->alt[j] = pre_alt;
		      free (alt);
		      buf_ptr = b-1;
		      tp = &pre_alt->next;
		      goto again; /* so insert rest of buf_ptr into son trie. */
		    }
		  else return NULL;
		}
	      else break;
	    }
	  /* here cb<cs, so create a new branch */
	  if (createp)
	    {
	      struct trie_alt *new_alt;
	      struct trie *newt, *tt;
	      int len = strlen(buf_ptr);

	      newt = xmalloc (offsetof(struct trie, alt[0]));
	      newt->cinfo = NULL;
	      newt->n_alt = 0;
	      new_alt = xmalloc (offsetof(struct trie_alt, s[len+1]));
	      strcpy (new_alt->s, buf_ptr);
	      new_alt->next = newt;
	      tt = xmalloc (offsetof(struct trie, alt[nalt+1]));
	      memcpy (tt, t, offsetof(struct trie, alt[j]));
	      tt->alt[j] = new_alt;
	      if (j!=nalt)
		memcpy (&tt->alt[j+1],&t->alt[j], (nalt-j)*sizeof(struct trie_alt *));
	      tt->n_alt = nalt+1;
	      free (t);
	      *tp = tt;
	      return newt;
	    }
	  else return NULL;
	}
      }
    }
#define hash(name,createp) uuHashCharStar(name,createp)
#else
#define HASH_FUN 1

  u_int32_t uuHashCharStar(char *buf_ptr)
    {
      register u_int32_t i = 0;
      register u_int32_t c;

      while (c = (u_int32_t)(unsigned char)*buf_ptr++)
	{
#if HASH_FUN==1
	  i = 71 * i + c + 13;
#elif HASH_FUN==2
	  i = 271 * i + c + 13;
#elif HASH_FUN==3
#define W            (32)
#define WW           (W / 8)
#define ROT_MASK     (W - 1)
#define SHL(x,s)    ((u_int32_t)((x)<<((s)&ROT_MASK)))
#define SHR(x,s,w)  ((u_int32_t)((x)>>((w)-((s)&ROT_MASK))))
#define ROTL(x,s,w) ((u_int32_t)(SHL((x),(s))|SHR((x),(s),(w))))
	  i = ROTL(i,3,W) + c;
#elif HASH_FUN==4
	  i = 71 * i + (u_int32_t)(c - 96);
#endif
	}
      return i;
    }
#endif

#define PHASE_SKIP_INTRO 0
#define PHASE_GET_DEPS 1
#define PHASE_COPY_INTRO 2
#define PHASE_OUT_REACHABLE 3

  int phase = PHASE_SKIP_INTRO;
  int expecting_premises = 0;

#define BUFFER_SIZE 256

  struct buffer {
    size_t size;
    size_t len;
    char s[BUFFER_SIZE];
  };

  struct buffer *new_buf (void)
    {
      struct buffer *b = xmalloc (sizeof(struct buffer));

      b->size = BUFFER_SIZE;
      b->len = 0;
      return b;
    }

  void bput (struct buffer **bp, char *s, int n)
    {
      switch (phase)
	{
	case PHASE_SKIP_INTRO: break;
	case PHASE_COPY_INTRO:
	  fputs (s, yyout);
	  break;
	default:
	  {
	    struct buffer *b = *bp;
	    int newlen = b->len + n;

	    if (newlen>=b->size)
	      {
		size_t newsize = newlen + BUFFER_SIZE;
		struct buffer *newb = xmalloc (offsetof(struct buffer, s[newsize]));
		
		newb->size = newsize;
		newb->len = newlen;
		memcpy (newb->s, b->s, b->len);
		strcpy (newb->s+b->len, s);
		*bp = newb;
		free (b);
	      }
	    else
	      {
		strcpy (b->s+b->len, s);
		b->len = newlen;
	      }
	    break;
	  }
	}
    }

  /* BPUT not (yet) used. */
#define BPUT(bp,s,n) {\
  switch (phase)\
	{\
	case PHASE_SKIP_INTRO: break;\
	case PHASE_COPY_INTRO:\
	  fputs (s, yyout);\
	  break;\
	default:\
	  {\
	    struct buffer *b = *bp;\
	    int newlen = b->len + n;\
	    if (newlen>=b->size) bput (bp,s,n);\
	    else\
	      {\
		strcpy (b->s+b->len, s);\
		b->len = newlen;\
	      }\
	    break;\
	  }\
	}\
  }


  struct buffer **theBufp = NULL;

  struct header {
    unsigned int kind : 2;
#define H_NONE 0
#define H_CINFO 1
#define H_MAP 2
#define H_CLAUSE 3
    unsigned int mark : 1;
    unsigned int n : 29;
  };

#ifdef EXACT_HASH
  struct cinfo {
    struct header h;
    struct trie *conc;
    struct trie *prem[1];
  };
#else
  struct cinfo {
    struct header h;
    struct cinfo *next;
    u_int32_t conc;
    u_int32_t prem[1];
  };
#endif

  struct clause {
    struct header h;
    u_int32_t n;
    char s[1];
  };

#ifndef EXACT_HASH
  struct map {
    struct header h;
    struct header *left, *right;
  };

  struct header *theClauseNames = NULL;

  struct header *table_get (struct header *h, u_int32_t clause)
    {
      u_int32_t mask;

      for (mask = 1; h!=NULL; mask <<= 1)
	{
	  switch (h->kind)
	    {
	    case H_CINFO:
	      {
		struct cinfo *ci = (struct cinfo *)h;

		if (ci->conc==clause)
		  return (struct header *)ci;
		return NULL;
	      }
	    case H_MAP:
	      if (clause & mask)
		h = ((struct map *)h)->right;
	      else h = ((struct map *)h)->left;
	      break;
	    case H_CLAUSE:
	      {
		struct clause *c = (struct clause *)h;

		if (c->n==clause)
		  return (struct header *)c;
		return NULL;
	      }
	    default:
	      abort ();
	      break;
	    }
	}
      return NULL;
    }

#define MAPCHUNK_N 128

  struct mapchunk {
    struct map m[MAPCHUNK_N];
  };

  struct map *theFreeMaps = NULL;

  struct map *newmap (void)
    {
      struct map *m, *next;

      if (theFreeMaps==NULL)
	{
	  struct mapchunk *mc = xmalloc (sizeof (struct mapchunk));
	  int i;

	  next = NULL;
	  for (i=0, m=mc->m; i<MAPCHUNK_N; i++, m++)
	    {
	      m->right = (struct header *)next;
	      next = m;
	    }
	  theFreeMaps = next;
	}
      m = theFreeMaps;
      theFreeMaps = (struct map *)m->right;
      return m;
    }

  int table_put (struct header **hp, struct cinfo *ci)
    {
      struct header *h;
      u_int32_t clause = ci->conc;
      u_int32_t mask;
      struct cinfo *ci0;
      struct map *m;

      for (mask = 1; (h = *hp)!=NULL; mask <<= 1)
	{
	  switch (h->kind)
	    {
	    case H_CINFO:
	      ci0 = (struct cinfo *)h;
	      if (ci0->conc==clause)
		{
#if defined(TABLE_RECORD) || defined(EXACT_HASH)
		    /* otherwise, just free ci, we are sure to get at least one proof
			  of clause.  We then just drop the others.  We cannot do this
			  if there is a conflict, because we are not sure that the proof
			  we get is really a proof of the same clause. */
		    {
		      do {
			ci0 = ci->next;
			free (ci);
			ci = ci0;
		      } while (ci!=NULL);
		    }
#else
		  *hp = (struct header *)ci; /* concatenate ci in front of ci0 */
		  while (ci->next!=NULL)
		    ci = ci->next;
		  ci->next = ci0;
#endif
		  return 0;
		}
	      m = newmap ();
	      m->h.kind = H_MAP;
	      m->h.mark = 0;
	      m->h.n = 0;
	      if (ci0->conc & mask)
		{
		  m->left = NULL;
		  m->right = (struct header *)ci0;
		}
	      else
		{
		  m->left = (struct header *)ci0;
		  m->right = NULL;
		}
	      *hp = h = (struct header *)m;
	      /*fallthrough*/
	    case H_MAP:
	      if (clause & mask)
		hp = &((struct map *)h)->right;
	      else hp = &((struct map *)h)->left;
	      break;
	    default:
	      abort ();
	      break;
	    }
	}
      *hp = (struct header *)ci;
      return 1;
    }

#ifdef TABLE_RECORD
#define CONFLICT_INC 611707

  int table_record (struct header **hp, u_int32_t clause, char *name)
    {
      struct header *h;
      u_int32_t mask;
      struct map *m;
      struct clause *c;

      for (mask = 1; (h = *hp)!=NULL; mask <<= 1)
	{
	  switch (h->kind)
	    {
	    case H_CLAUSE:
	      c = (struct clause *)h;
	      if (c->n==clause)
		{
		  if (strcmp (name, c->s) != 0) /* conflict */
		    return 1;
		  return 0; /* otherwise, OK, already there and no conflict. */
		}
	      m = newmap ();
	      m->h.kind = H_MAP;
	      m->h.mark = 0;
	      m->h.n = 0;
	      if (c->n & mask)
		{
		  m->left = NULL;
		  m->right = (struct header *)c;
		}
	      else
		{
		  m->left = (struct header *)c;
		  m->right = NULL;
		}
	      *hp = h = (struct header *)m;
	      /*fallthrough*/
	    case H_MAP:
	      if (clause & mask)
		hp = &((struct map *)h)->right;
	      else hp = &((struct map *)h)->left;
	      break;
	    default:
	      abort ();
	      break;
	    }
	}
      {
	int len = strlen (name);

	c = xmalloc (offsetof(struct clause, s[len])+1);
	c->h.kind = H_CLAUSE;
	c->h.mark = 0;
	c->h.n = 0;
	c->n = clause;
	strcpy (c->s, name);
	*hp = (struct header *)c;
      }
      return 0;
    }

  long nTableRecords = 0;
  long nHash = 0;

  u_int32_t hash (char *name)
    {
      u_int32_t clause = uuHashCharStar (name);

      nHash++;
      while (nTableRecords++, table_record (&theClauseNames, clause, name))
	clause += CONFLICT_INC;
      return clause;
    }
#else
#define hash(name,createp) uuHashCharStar(name)
#endif
#endif

  BSD_CURSOR(clauseCursor);

  void new_clause (void)
    {
      nClauses++;
      if (verbose>=2 && ++nClausesMod==CLAUSE_STEP)
	{
	  nClausesMod = 0;
	  bump_bsd_cursor (&clauseCursor);
	}
    }

#ifndef EXACT_HASH
  struct header *theDeds = NULL;
#endif

#ifdef EXACT_HASH
  typedef struct trie *cindex;
#else
  typedef u_int32_t cindex;
#endif

#ifdef EXACT_HASH
 cindex theClause = NULL;
#else
 cindex theClause = 0;
#endif
  int theOffset = 0;

  struct ilist {
    struct ilist *next;
    cindex i;
  };

  struct ilist *thePrems = NULL;
  struct ilist *thePremList = NULL;
  struct ilist *theTargets = NULL;

  struct ilist *icons (cindex i, struct ilist *next)
    {
      struct ilist *il;

      if (thePremList==NULL)
	{
	  struct ilist* il = xmalloc (sizeof(struct ilist));

	  il->next = NULL;
	  thePremList = il;
	}
      il = thePremList;
      thePremList = il->next;
      il->next = next;
      il->i = i;
      return il;
    }

  unsigned int ilen (struct ilist *il)
    {
      unsigned int n;

      for (n=0; il!=NULL; n++, il=il->next);
      return n;
    }

  void ifree (struct ilist *il)
    {
      struct ilist *next, *il0=il;

      if (il==NULL)
	return;
      while ((next = il->next)!=NULL)
	il = next;
      il->next = thePremList;
      thePremList = il0;
    }

  int target_p (char *s)
    {
      /* By default, target is "false".
	 That is, either a clause of the form '?.' or
	 one of the form '#false([^()]*).'. */
      if (strcmp (s, "?.")==0)
	return 1;
      if (memcmp (s, "#false", 6)!=0)
	return 0;
      if (strstr (s, ":-")==NULL)
	return 1;
      return 0;
    }
  %}

%start problem

%token identifier
%token kw_open_paren kw_close_paren kw_provided kw_comma kw_semicolon
%token kw_period kw_question_mark kw_subst
%token kw_open_source kw_close_source kw_open_clause kw_close_clause kw_end_tag
%token kw_open_definitions kw_close_definitions
%token kw_open_approximation kw_close_approximation
%token kw_open_justifications kw_close_justifications
%token VAR kw_ne kw_false string_constant kw_axiom kw_open_rule
%token kw_clause_def kw_clause_use
%token kw_close_rule

%%

problem : source definitions approximation justifications deductions
{ switch (phase)
  {
  case PHASE_GET_DEPS: phase = PHASE_COPY_INTRO; break;
  case PHASE_OUT_REACHABLE: phase = PHASE_SKIP_INTRO; break;
  }
}
;

source : open_source named_clause_list close_source
;

definitions : open_definitions clause_list close_definitions
;

approximation : open_approximation clause_list close_approximation
;

justifications : open_justifications deduction_list close_justifications
;

deductions : deduction_list
;

named_clause_list :
| named_clause_list named_clause
;

named_clause : open_clause string end_tag clause close_clause
;

deduction_list :
| deduction_list deduction
;

deduction : processed_clause axiom {
  switch (phase)
    {
    case PHASE_GET_DEPS:
      {
	struct cinfo *ci = xmalloc (offsetof (struct cinfo, prem[0]));

#ifndef EXACT_HASH
	ci->next = NULL;
#endif
	ci->conc = theClause;
	ci->h.kind = H_CINFO;
	ci->h.mark = 0;
	ci->h.n = 0;
#ifdef EXACT_HASH
	if (theClause->cinfo==NULL)
	  {
	    theClause->cinfo = ci;
	    new_clause ();
	  }
#else
	if (table_put (&theDeds, ci))
	  new_clause ();
#endif
	nDeds++;
	break;
      }
    case PHASE_OUT_REACHABLE:
      if (theClause!=NULL)
	{
	  struct cinfo *ci =
#ifdef EXACT_HASH
	    theClause->cinfo;
#else
	  (struct cinfo *)table_get (theDeds, theClause);
#endif

	  if (ci!=NULL && ci->h.mark)
	    {
	      fputs ((*theBufp)->s, yyout);
#ifdef EXACT_HASH
	      ci->h.mark = 0; /* we are happy with the first deduction of the clause,
				 and won't output any other. */
#endif
	    }
      }
      break;
    }
  (*theBufp)->len = 0;
}
| processed_clause open_rule premise_list close_rule {
  switch (phase)
    {
    case PHASE_GET_DEPS:
      {
	unsigned int n = ilen (thePrems);
	struct cinfo *ci = xmalloc (offsetof (struct cinfo, prem[n]));
	struct ilist *il;
	cindex *ip;

#ifndef EXACT_HASH
	ci->next = NULL;
#endif
	ci->conc = theClause;
	ci->h.kind = H_CINFO;
	ci->h.mark = 0;
	ci->h.n = n;
	for (ip=ci->prem, il=thePrems; il!=NULL; il=il->next)
	  *ip++ = il->i;
#ifdef EXACT_HASH
	if (theClause->cinfo==NULL)
	  {
	    theClause->cinfo = ci;
	    new_clause ();
	  }
#else
	if (table_put (&theDeds, ci))
	  new_clause ();
#endif
	nDeds++;
	break;
      }
    case PHASE_OUT_REACHABLE:
      if (theClause!=NULL)
	{
	  struct cinfo *ci =
#ifdef EXACT_HASH
	    theClause->cinfo;
#else
	  (struct cinfo *)table_get (theDeds, theClause);
#endif

	  if (ci!=NULL && ci->h.mark)
	    {
	      fputs ((*theBufp)->s, yyout);
#ifdef EXACT_HASH
	      ci->h.mark = 0; /* we are happy with the first deduction of the clause,
				 and won't output any other. */
#endif
	    }
	}
      break;
    }
  (*theBufp)->len = 0;
  ifree (thePrems);
  thePrems = NULL;
}
;

premise_list : premise
| premise_list premise
;

premise : processed_clause substitution {
  if (phase==PHASE_GET_DEPS)
    (*theBufp)->len = 0;
  else bput (theBufp, "\n  ", 3); }
;

processed_clause : { theOffset = (*theBufp)->len; } clause {

  switch (phase)
    {
    case PHASE_GET_DEPS:
      {
	cindex i = hash (&(*theBufp)->s[theOffset], 1);

	if (expecting_premises)
	  thePrems = icons (i, thePrems);
	else
	  {
	    theClause = i;
	    if (target_p ((*theBufp)->s))
	      {
		theTargets = icons (i, theTargets);
	      }
	  }
	(*theBufp)->len = 0;
      }
      break;
    case PHASE_OUT_REACHABLE:
      {
	cindex i = hash (&(*theBufp)->s[theOffset], 0);

	if (expecting_premises)
	  ;
	else theClause = i;
      }
      break;
    } 
}
;

substitution :
| kw_subst { if (phase==PHASE_GET_DEPS) (*theBufp)->len = 0;
 else bput (theBufp, yytext, yyleng); }
;

clause_list :
| clause_list clause { if (phase==PHASE_COPY_INTRO) bput (theBufp, "\n", 1); }
;

clause : raw_clause
/* !!!clause_def and clause_use not recognized for now
| kw_clause_def raw_clause
| kw_clause_use
*/
;

raw_clause : question_mark clause_body period
| head provided clause_body period
| head period
;

head : atomhead
 | head semicolon atomhead
;

atomhead : atom
| false
;

clause_body :
| non_empty_clause_body
;

non_empty_clause_body : atom
| non_empty_clause_body comma atom
;

atom : id open_paren term_list close_paren
| id { bput (theBufp, " ", 1); } term
| id
| ne
;

term_list : term
| term_list comma term
;

term : var
| application
;

application : id open_paren term_list close_paren
| id
;

id : identifier { bput (theBufp, yytext, yyleng); }
;

var : VAR { bput (theBufp, yytext, yyleng); }
;

ne : kw_ne { bput (theBufp, yytext, yyleng); }
;

false : kw_false { bput (theBufp, yytext, yyleng); }
;

open_paren : kw_open_paren { bput (theBufp, yytext, yyleng); }
;

close_paren : kw_close_paren { bput (theBufp, yytext, yyleng); }
;

comma : kw_comma { bput (theBufp, yytext, yyleng);
 /* bput (theBufp, ", ", 2); */ }
;

semicolon : kw_semicolon { bput (theBufp, ";", 1); }
;

period : kw_period { bput (theBufp, yytext, yyleng); }
;

provided : kw_provided { bput (theBufp, " :- ", 4); }
;

question_mark : kw_question_mark { bput (theBufp, yytext, yyleng); }
;

axiom : kw_axiom { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

open_rule : kw_open_rule { bput (theBufp, yytext, yyleng); bput (theBufp, "\n  ", 3);
 expecting_premises = 1;
 if (phase==PHASE_GET_DEPS) (*theBufp)->len = 0;
}
;

close_rule : kw_close_rule { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1);
 expecting_premises = 0;
}
;

open_clause : kw_open_clause { bput (theBufp, yytext, yyleng); }
;

close_clause : kw_close_clause { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

end_tag : kw_end_tag { bput (theBufp, yytext, yyleng); }
;

string : string_constant { bput (theBufp, yytext, yyleng); }
;

open_source : kw_open_source { bput (theBufp, yytext, yyleng); }
;

close_source : kw_close_source { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

open_definitions : kw_open_definitions { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

close_definitions : kw_close_definitions { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

open_approximation : kw_open_approximation { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

close_approximation : kw_close_approximation { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

open_justifications : kw_open_justifications { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1); }
;

close_justifications : kw_close_justifications { bput (theBufp, yytext, yyleng); bput (theBufp, "\n", 1);
 switch (phase)
  {
  case PHASE_SKIP_INTRO: phase = PHASE_GET_DEPS; break;
  case PHASE_COPY_INTRO: phase = PHASE_OUT_REACHABLE; break;
  }
}
;

%%

long nMarks = 0;
#define MARKS_STEP 1000
long nMarksMod = 0;

BSD_CURSOR(marksCursor);

void mark (cindex i)
{
  struct cinfo *ci =
#ifdef EXACT_HASH
    i->cinfo;
#else
  (struct cinfo *)table_get (theDeds, i);
#endif
  unsigned int k, n;

#ifdef EXACT_HASH
  if (ci==NULL)
    return;
#else
  for (; ci!=NULL; ci=ci->next)
#endif
    {
      if (ci->h.mark) /* already marked */
	return;
      ci->h.mark = 1;
      nMarks++;
      if (verbose>=2 && ++nMarksMod==MARKS_STEP)
	{
	  nMarksMod = 0;
	  bump_bsd_cursor (&marksCursor);
	}
      n = ci->h.n;
      for (k=0; k<n; k++)
	mark (ci->prem[k]);
    }
}

void stringify (char *to, char *from)
{
  char c;

  *to++ = '"';
  while (c = *from++)
    {
      switch (c)
	{
	case '"': case '\\':
	  *to++ = '\\';
	  *to++ = c;
	  break;
	default:
	  *to++ = c;
	  break;
	}
    }
  *to++ = '"';
  *to = 0;
}

int gz (char *s)
{
  int len = strlen (s);

  return (len>=3 && strcmp (s+len-3, ".gz")==0);
}

FILE *hopen (char *name)
{
  char *cmd;
  FILE *f;

  cmd = xmalloc (16 + 2*strlen (name));
  strcpy (cmd, "zcat ");
  stringify (cmd+strlen(cmd), name);
  if (gz (name))
    f = popen (cmd, "r");
  else f = fopen (name, "r");
  free (cmd);
  return f;
}

void hclose (char *name, FILE *f)
{
  if (gz (name))
    pclose (f);
  else fclose (f);
}

int main (int argc, char **argv)
{
  struct buffer *buf = new_buf ();
  char *name;
  FILE *f;

  if (argc!=2)
    {
      fprintf (stderr, "Expecting 1 argument, got %d.\n", argc-1);
      fflush (stderr);
      exit (10);
    }
  name = argv[1];
  f = hopen (name);
  if (f==NULL)
    {
      perror (argv[0]);
      fprintf (stderr, " (file %s).\n", name);
      exit (10);
    }
  yyin = f;
  theBufp = &buf;
  if (verbose>=1)
    {
      fprintf (stderr, "Scanning ");
      fflush (stderr);
    }
  yyparse ();
  hclose (name, f);
  if (verbose>=1)
    {
      fprintf (stderr, "%c... done: %ld deduction steps, %ld clauses.\n", 8, nDeds, nClauses
	       /*, ((double) nTableRecords) / ((double) nHash)*/);
      fflush (stderr);
    }
  {
    struct ilist *il;

    if (verbose>=1)
      {
	fprintf (stderr, "Marking ");
	fflush (stderr);
      }
    for (il = theTargets; il!=NULL; il=il->next)
      mark (il->i);
    ifree (theTargets);
    theTargets = NULL;
  }
  if (verbose>=1)
    {
      fprintf (stderr, "%c... done: %ld live clauses.\n", 8, nMarks);
      fflush (stderr);
    }
  f = hopen (name);
  if (f==NULL)
    {
      perror (argv[0]);
      fprintf (stderr, " (file %s).\n", name);
      exit (10);
    }
  yyin = f;
  yyparse ();
  hclose (name, f);
  return 0;
}
