solve.c

利用空间表示的rcc8模型进行空间推理

    fprintf(file,"  Nodes v.: %7.1f\t\t%7.1f %7.1f %7.1f %7.1f %7.1f\n",
	   avg, med, seventy, ninety, ninetynine, hundred);


  avg = 0.0;
  for (i = 0; i < trial; i++)
    avg += (float)(tmaxdepth[i]);
  avg = avg/((float)trial);
  qsort(tmaxdepth,trial,sizeof(long int),&int_compare);
  
  if (trial == 1) {
    med = (float)tmaxdepth[0];
    seventy = (float)tmaxdepth[0];
    ninety = (float)tmaxdepth[0];
    ninetynine = (float)tmaxdepth[0];
    hundred = (float)tmaxdepth[0];
  } else {
    med = ((float)(tmaxdepth[(trial/2)-1]+tmaxdepth[trial/2]))/2.0;
    seventy = ((float)(tmaxdepth[((trial*7)/10)-1]+
		       tmaxdepth[((trial*7)/10)]))/2.0;
    ninety = ((float)(tmaxdepth[((trial*9)/10)-1]+
		       tmaxdepth[((trial*9)/10)]))/2.0;
    ninetynine = ((float)(tmaxdepth[((trial*99)/100)-1]+
		       tmaxdepth[((trial*99)/100)]))/2.0;
    hundred = (float) tmaxdepth[trial-1];
  }
  if (brief)
    fprintf(file," %6.5f %6.5f %6.5f %6.5f %6.5f %6.5f (md)\n",
	   avg, med, seventy, ninety, ninetynine, hundred);
  else
    fprintf(file,"  Depth:    %7.1f\t\t%7.1f %7.1f %7.1f %7.1f %7.1f\n",
	   avg, med, seventy, ninety, ninetynine, hundred);
 

  init_statistics();

}

void copysplitfile(int newsplit)
{
  int i,j;

  if(newsplit==1) {
    for (i=0;i<MAXSET;i++) 
      for (j=0; j<9; j++) {
	splitinfo[i][j] = horninfo[i][j];
	}
      }
  if(newsplit==2) {
    for (i=0;i<MAXSET;i++) 
      for (j=0; j<9; j++) {
	splitinfo[i][j] = closebaseinfo[i][j];
	}
      }
  if(newsplit==3) {
    for (i=0;i<MAXSET;i++) 
      for (j=0; j<9; j++) {
	splitinfo[i][j] = c8info[i][j];
	}
      }
 if(newsplit==4) {
    for (i=0;i<MAXSET;i++) 
      for (j=0; j<9; j++) {
	splitinfo[i][j] = q8info[i][j];
	}
      }
 if(newsplit==5) {
    for (i=0;i<MAXSET;i++) 
      for (j=0; j<9; j++) {
	splitinfo[i][j] = intersectinfo[i][j];
	}
      }
}


void readsplitfile(char *s)
{
  int i,j,inp;

  if ((splitfile = fopen(s,"r")) == NULL) {
    fprintf(stderr, "***Relation-cover file '%s' not found\n",s);
    exit(-1);
  }
  fflush(stderr);
  for (i=0;i<MAXSET;i++) 
    for (j=0; j<9; j++) {
      if (fscanf(splitfile,"%d",&inp) != 1) {
	fprintf(stderr, "***Format error in relation-cover file '%s'\n",s);
	exit(-1);
      } else {
	splitinfo[i][j] = inp;
      }
    }
  if ((fscanf(splitfile,"%d",&inp) == 1) || (!feof(splitfile))) {
	fprintf(stderr, "***No eof in relation-cover file '%s'\n",s);
      	exit(-1);
      }
}

void standardsplitfile(void)
{
  int i,j,inp;

  if ((splitfile = fopen("hornsplit","r")) == NULL) {
    fprintf(stderr, "****Relation-cover file 'hornsplit' not found\n");
    exit(-1);
  }
  fflush(stderr);
  for (i=0;i<MAXSET;i++) 
    for (j=0; j<9; j++) {
      if (fscanf(splitfile,"%d",&inp) != 1) {
	fprintf(stderr, "****Format error in relation-cover file 'hornsplit'\n");
	exit(-1);
      } else {
	horninfo[i][j] = inp;
      }
    }
  if ((fscanf(splitfile,"%d",&inp) == 1) || (!feof(splitfile))) {
	fprintf(stderr, "****No eof in relation-cover file 'hornsplit'\n");
      	exit(-1);
      }
  fclose(splitfile);

 if ((splitfile = fopen("c8split","r")) == NULL) {
    fprintf(stderr, "****Relation-cover file 'c8split' not found\n");
    exit(-1);
  }
  fflush(stderr);
  for (i=0;i<MAXSET;i++) 
    for (j=0; j<9; j++) {
      if (fscanf(splitfile,"%d",&inp) != 1) {
	fprintf(stderr, "****Format error in relation-cover file 'c8split'\n");
	exit(-1);
      } else {
	c8info[i][j] = inp;
      }
    }
  if ((fscanf(splitfile,"%d",&inp) == 1) || (!feof(splitfile))) {
	fprintf(stderr, "****No eof in relation-cover file 'c8split'\n");
      	exit(-1);
      }
  fclose(splitfile);

 if ((splitfile = fopen("q8split","r")) == NULL) {
    fprintf(stderr, "****Relation-cover file 'q8split' not found\n");
    exit(-1);
  }
  fflush(stderr);
  for (i=0;i<MAXSET;i++) 
    for (j=0; j<9; j++) {
      if (fscanf(splitfile,"%d",&inp) != 1) {
	fprintf(stderr, "****Format error in relation-cover file 'q8split'\n");
	exit(-1);
      } else {
	q8info[i][j] = inp;
      }
    }
  if ((fscanf(splitfile,"%d",&inp) == 1) || (!feof(splitfile))) {
	fprintf(stderr, "****No eof in relation-cover file 'q8split'\n");
      	exit(-1);
      }
  fclose(splitfile);


  if ((splitfile = fopen("closebasesplit","r")) == NULL) {
    fprintf(stderr, "****Relation-cover file 'closebasesplit' not found\n");
    exit(-1);
  }
  fflush(stderr);
  for (i=0;i<MAXSET;i++) 
    for (j=0; j<9; j++) {
      if (fscanf(splitfile,"%d",&inp) != 1) {
	fprintf(stderr, "****Format error in relation-cover file 'closebasesplit'\n");
	exit(-1);
      } else {
	closebaseinfo[i][j] = inp;
      }
    }
  if ((fscanf(splitfile,"%d",&inp) == 1) || (!feof(splitfile))) {
	fprintf(stderr, "****No eof in relation-cover file 'closebasesplit'\n");
      	exit(-1);
      }
  fclose(splitfile);

 if ((splitfile = fopen("intersplit","r")) == NULL) {
    fprintf(stderr, "****Relation-cover file 'intersectsplit' not found\n");
    exit(-1);
  }
  fflush(stderr);
  for (i=0;i<MAXSET;i++) 
    for (j=0; j<9; j++) {
      if (fscanf(splitfile,"%d",&inp) != 1) {
	fprintf(stderr, "****Format error in relation-cover file 'intersplit'\n");
	exit(-1);
      } else {
	intersectinfo[i][j] = inp;
      }
    }
  if ((fscanf(splitfile,"%d",&inp) == 1) || (!feof(splitfile))) {
	fprintf(stderr, "****No eof in relation-cover file 'intersplit'\n");
      	exit(-1);
      }
  fclose(splitfile);
}



void getnextcsp(char csp[100])
{
  int d;
  char line[256];

  d = 1;
  while ((d != 0) && (!feof(solveonlyfile))) {
    fgets(line,255,solveonlyfile);
    if (sscanf(line,"%s %d",csp,&d) != 2) d = 1;
    if ((d == taggedwith) && (csp[strlen(csp)-1] == ':')) 
      csp[strlen(csp)-1] = '\0';
    if (swdebug) fprintf(stderr,"SO: %s -> %s %d\n",line,csp,d);
  }
  if (feof(solveonlyfile)) csp[0] = '\0';
}

float readfloatarg(int *xarg, char **argv)
{
  float result;
  
  (*xarg)++;
  if (sscanf(argv[*xarg],"%f",&result) != 1) usage();
  return(result);
}


unsigned int readintarg(int *xsw, int *xarg, char **argv)
{
  unsigned int result;

  if (argv[*xarg][++(*xsw)] == '\0') {
    (*xarg)++;
    if (sscanf(argv[*xarg],"%d",&result) != 1) usage();
  } else {
    if (sscanf(&argv[*xarg][*xsw],"%d",&result) != 1) usage();
  }
  *xsw = strlen(argv[*xarg])-1;
  return(result);
}

int heuristic(char *s, int i, int *oldsplit)
{
  int error=0,newsplit=0; 
  /* printf("heuristic %c, old: %i\n",s[i],*oldsplit); */
  switch (s[i])
    {
    case '1': 
      swfixed = 0;
      swenvcons = 0;
      swsplitinfo=1;     
      newsplit=1;
      break;
    case '2': 
      swfixed = 0;
      swenvcons = 1;
      swsplitinfo=1;     
      newsplit=1;
      break;
    case '3': 
      swfixed = 1;
      swenvcons = 0; 
      swsplitinfo=1;    
      newsplit=1;
       break;
    case '4': 
      swfixed = 1;
      swenvcons = 1; 
      swsplitinfo=1;     
      newsplit=1;
      break;
    case 'A': 
      swfixed = 0;
      swenvcons = 0;
      swsplitinfo=1;
      newsplit=2;
       break;
    case 'B': 
      swfixed = 0;
      swenvcons = 1;
      swsplitinfo=1;
      newsplit=2;
      break;
    case 'C': 
      swfixed = 1;
      swenvcons = 0;
      swsplitinfo=1;
      newsplit=2;
      break;
    case 'D': 
      swfixed = 1;
      swenvcons = 1;
      swsplitinfo=1;
      newsplit=2;
      break; 
    case 'a': 
      swfixed = 0;
      swenvcons = 0;
      swsplitinfo=0;
      newsplit=0;
       break;
    case 'b': 
      swfixed = 0;
      swenvcons = 1;
      swsplitinfo=0;
      newsplit=0;
      break;
    case 'c': 
      swfixed = 1;
      swenvcons = 0;
      swsplitinfo=0;
      newsplit=0;
      break;
    case 'd': 
      swfixed = 1;
      swenvcons = 1;
      swsplitinfo=0;
      newsplit=0;
      break;
    case 's': 
      swfixed = 0;
      swenvcons = 0;
      swsplitinfo=1;     
      newsplit=3;
      break;
    case 't': 
      swfixed = 0;
      swenvcons = 1;
      swsplitinfo=1;     
      newsplit=3;
      break;
    case 'u': 
      swfixed = 1;
      swenvcons = 0; 
      swsplitinfo=1;    
      newsplit=3;
       break;
    case 'v': 
      swfixed = 1;
      swenvcons = 1; 
      swsplitinfo=1;     
      newsplit=3;
      break;
    case 'S': 
      swfixed = 0;
      swenvcons = 0;
      swsplitinfo=1;     
      newsplit=4;
      break;
    case 'T': 
      swfixed = 0;
      swenvcons = 1;
      swsplitinfo=1;     
      newsplit=4;
      break;
    case 'U': 
      swfixed = 1;
      swenvcons = 0; 
      swsplitinfo=1;    
      newsplit=4;
       break;
    case 'V': 
      swfixed = 1;
      swenvcons = 1; 
      swsplitinfo=1;     
      newsplit=4;
      break;
    case 'i': 
      swfixed = 0;
      swenvcons = 0;
      swsplitinfo=1;     
      newsplit=5;
      break;
    case 'j': 
      swfixed = 0;
      swenvcons = 1;
      swsplitinfo=1;     
      newsplit=5;
      break;
    case 'k': 
      swfixed = 1;
      swenvcons = 0; 
      swsplitinfo=1;    
      newsplit=5;
       break;
    case 'l': 
      swfixed = 1;
      swenvcons = 1; 
      swsplitinfo=1;     
      newsplit=5;
      break;
    default: error=1;
    }
  /* printf("swfixed: %i,swenvcons %i, splitfilename: %s, error: %i, i: %i, old: %i, new: %i\n",swfixed,swenvcons,splitfilename,error,i,*oldsplit,newsplit); */
  if ((!error) && (newsplit!=0) && (*oldsplit!=newsplit) ) {
    copysplitfile(newsplit);
    *oldsplit=newsplit;
  }
 
  /* printf("old: %i,  sfn: %s\n",*oldsplit,splitfilename);*/
  return error;
}

void init_headers()
{
  int i;
  char emptystring[] = "empty";
  for(i=0;i<MAXHEADER;i++) {
    headers[i].next=NULL;
    strcpy(headers[i].name,emptystring);
  }
printf("init_headers done\n");
}

int add_headers(FILE *headerfile)
{
  int number=0;
  char line[100],head[100],size[100];
  hp field,new;
  char emptystring[] = "empty";

  while (!feof(headerfile)) {
    while (fgets(line,100,headerfile) && ((line[0] == '\n') || (line[0] == '\0'))); 

    if (sscanf(line,"%s %s",size,head) !=2) {
      fprintf(stderr,"\n*** Header line not found: '%s'\n",line);
      exit(0);
    }

    field=&headers[atoi(size)];

    if(strcmp(field->name,emptystring)==0) {
      strcpy(field->name,head); 
      number++;
      continue;
    }
    
    while((strcmp(field->name,head)!=0) && (field->next!=NULL)) {
      field = field->next;
    }

    if(strcmp(field->name,head)==0) continue;

    if(field->next==NULL) {
      new = malloc(sizeof(hdr));
      strcpy(new->name,head);
      new->next=NULL;
      field->next=new;
      number++;
      continue;
    }
    printf("something is wrong!!\n");
  }
  printf("add_headers done (%i)\n",number);
  return number;
}

int delete_headers(FILE *headerfile)
{
  int number=0;
  char line[100],head[100],size[100];
  hp field,save=NULL;
  char emptystring[] = "empty";


  while (!feof(headerfile)) {
    while (fgets(line,100,headerfile) && ((line[0] == '\n') || (line[0] == '\0'))); 
    if (sscanf(line,"%s %s",size,head) != 2) {
      fprintf(stderr,"\n*** Header line not found: '%s'\n",line);
      exit(0);
    }
    field=&headers[atoi(size)];

    if(strcmp(field->name,emptystring)==0) {
      continue;
    }

    if(strcmp(field->name,head)==0) {
      if(field->next==NULL) {
	strcpy(field->name,emptystring);
	number++;
	continue;
      }
      save=field->next;
      strcpy(field->name,save->name);
      field->next=save->next;
      free(save);
      continue;
    }

    while((strcmp(field->name,head)!=0) && (field->next!=NULL)) {
      save=field;
      field = field->next;
    }

    if(strcmp(field->name,head)==0) {
      if(field->next==NULL) {
	save->next=NULL;
      }
      else {
	save->next=field->next;
      }
      number++;
      free(field);
      continue;
    }
  }
  printf("delete_headers done (%i)\n",number);
  return number;
}

int pop_header(int size, char *head) {
  
  hp field,save=NULL;
  char emptystring[] = "empty";

  field=&headers[size];

  if(strcmp(field->name,emptystring)==0) {
    return 0;
  }

  if(strcmp(field->name,head)==0) {