/* Tiny activity monitoring script for h1.
   Copyright (C) 2003 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 <stdio.h>

int main (int argc, char *argv[])
{
  FILE *f;
  int c;
  int vdash = 0, pick = 0, facts = 0, bot = 0, autom = 0, univ = 0, ne = 0, split_def = 0,
    nondet_split_def = 0,
    cond = 0, fully_defined = 0,
    abbrv = 0,
    sort_simplify = 0,
    pruned = 0, fully_defined_parent = 0, fully_defined_backward = 0,
    subsumed_premise = 0, subsumed_forward = 0, subsumed_backward = 0,
    subsumed_forward_auto = 0, subsumed_backward_auto = 0,
    rem_cond = 0;
  int narg;

  narg=1;
  if (argc==1)
    f = stdin;
  else
    {
      narg++;
      f = fopen (argv[1], "r");
      if (f==NULL)
	{
	  perror ("Cannot open file: ");
	  return 1;
	}
    }
  while ((c = fgetc (f)) != EOF)
    {
      switch (c)
	{
	case '>': vdash++; break;
	case '<': pick++; break;
	case 'f': facts++; break;
	case '!': bot++; break;
	case '+': autom++; break;
	case '*': univ++; break;
	case 'q': ne++; break;
	case 'c': cond++; break;
	case 's': split_def++; break;
	case 'S': nondet_split_def++; break;
	case 'a': abbrv++; break;
	case 'k': sort_simplify++; break;
	case '/': pruned++; break;
	case 'd': fully_defined++; break;
	case '^': fully_defined_parent++; break;
	case 'D': fully_defined_backward++; break;
	case '\\': subsumed_premise++; break;
	case '-': subsumed_forward++; break;
	case '_': subsumed_forward_auto++; break;
	case 'b': subsumed_backward++; break;
	case 'B': subsumed_backward_auto++; break;
	case 'C': rem_cond++; break;
	}
    }
  printf ("Derived clauses: %d (%d splitting defs, %d ne facts)\n", vdash, split_def, ne);
  printf ("Dealt with, not subsumed: %d\n", pick);
  printf ("Subsumed clauses [forward] : %d (of which %d automata clauses)\n",
	  subsumed_forward+subsumed_forward_auto, subsumed_forward_auto);
  printf ("Subsumed clauses [backward]: %d (of which %d automata clauses)\n",
	  subsumed_backward+subsumed_backward_auto, subsumed_backward_auto);
  printf ("Frozen clauses: %d, awaken: %d.\n", cond, rem_cond);
  printf ("Intersection predicates: %d.\n", nondet_split_def);
  printf ("Fully defined predicate symbols: %d\n", fully_defined);
  printf ("  Backward subsumed clauses because of fully defined symbols: %d\n",
	  fully_defined_backward);
  printf ("  Subsumed parent clauses because of fully defined symbols: %d\n",
	  fully_defined_parent);
  printf ("Abbreviations: %d\n", abbrv);
  printf ("Sort simplifications: %d\n", sort_simplify);
  printf ("Ground facts: %d\n", facts);
  printf ("Pruned clauses: %d\n", pruned);
  printf ("Automata clauses: %d\n", autom);
  printf ("\tTotal generated (derived+subsumed forward+frozen): %d\n",
	  vdash+subsumed_forward+subsumed_forward_auto+cond);
  printf ("\tTotal subsumed (forward+backward+fully defined): %d\n",
	  subsumed_forward+subsumed_forward_auto+
	  subsumed_backward+subsumed_backward_auto+
	  fully_defined_backward+fully_defined_parent);
  fflush (stdout);
  return 0;
}
