solve.c

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

    if(field->next==NULL) {
      strcpy(field->name,emptystring);
      return 1;
      }
    save=field->next;
    strcpy(field->name,save->name);
    field->next=save->next;
    free(save);
    return 1;
  }

  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;
    }
    free(field);
    return 1;
  }
  return 0;
}


int main(int argc, char **argv)
{
  int xarg, xsw;
  int result,i,minnodes,totalnodes,orthcons,oldsplit=0;
  char nextcsp[100];
  char order[30];
  int ordernode[30];
  char first='0';
  double clocks_per_second = (double) CLOCKS_PER_SEC;
  int newsize;
  float newdegree, newlabel, newdensity, factor=1.0;
 

  swhard = 0;
  swdebug = 0;
  swverbose = 0;
  swquiet = 0;
  swsummary = 0;
  swpositive = 0;
  swnegative = 0;
  swposneg = 0;
  swsplitinfo = 0;
  swrandomorder = 0;
  swwqueue = 0;
  swenvcons = 0;
  swfixed = 0;
  swsolveonly = 0;
  swonlypathcons =0;
  swpcprint=0;
  swtesting=0; 
  summaryfile=stdout;
  swmaxvisit = NV_UPPER_LIMIT;
  swfactor=0;
  sworthogonal = 0;
  swallorthogonal = 0;
  swheuristicout = 0;
  swheader=0;
  swminsize=0;
  strcpy(splitfilename,"none");
  
  xarg = 1;
  while ((xarg < argc) && (argv[xarg][0] == '-')) {
    xsw = 1;
    while (argv[xarg][xsw] != '\0') {
      switch (argv[xarg][xsw]) {
      case 'b':
	swbrief = 1;
	swsummary = 1;
	break;
      case 'c':
	swsplitinfo = 1;
	if (argv[xarg][++xsw] == '\0') {
	  if(xarg+1 >= argc) usage();
	  strcpy(splitfilename, argv[++xarg]);
	} else {
	  strcpy(splitfilename, &argv[xarg][xsw]);
	}
	xsw = strlen(argv[xarg])-1;
	readsplitfile(splitfilename);
	break;
      case 'd': 
	swdebug = 1;
	break;
      case 'e':
	swenvcons = 1;
	break;
      case 'f':
	swfixed = 1;
	break;
      case 'g':
	if(xarg+1 >= argc) usage();
	minsize = readintarg(&xsw,&xarg,argv);
	swminsize = 1;
	break;
      case 'h': 
	if(argv[xarg][++xsw]=='a')	 
	  swallorthogonal = 1;
	if(argv[xarg][xsw]=='A') {	 
	  swallorthogonal = 1;
	  swheuristicout = 1;
	  strcpy(heuristicfilename, argv[++xarg]);
	  if ((heuristicfile = fopen(heuristicfilename,"a")) == NULL) {
	    fprintf(stderr,"***Cannot open file '%s'\n",heuristicfilename);
	    exit(-1);
	  }
	}
	if(xarg+1 >= argc) usage();
	strcpy(order, argv[++xarg]);
	sworthogonal = 1;
	swfixed = 1;
	swsplitinfo = 1;
	standardsplitfile();
	xsw = strlen(argv[xarg])-1;
	break;
      case 'l':
	if(argv[xarg][++xsw]=='i') { 
	  swheader=1;
	  if(xarg+1 >= argc) usage();
	  strcpy(headerfilename, argv[++xarg]);
	  if ((headerfile = fopen(headerfilename,"r")) == NULL) {
	    fprintf(stderr,"***Cannot open file '%s'\n",headerfilename);
	    exit(-1);
	  }
	  init_headers();
	  add_headers(headerfile);
	}
	else if(argv[xarg][xsw]=='e') {
	  if(swheader!=1) {printf("Specify option '-li' first.\n");exit(0);} 
	  if(xarg+1 >= argc) usage();
	  strcpy(headerfilename, argv[++xarg]); 
	  if ((headerfile = fopen(headerfilename,"r")) == NULL) {
	    fprintf(stderr,"***Cannot open file '%s'\n",headerfilename);
	    exit(-1);
	  }
	  delete_headers(headerfile);
	}
	xsw = strlen(argv[xarg])-1;
	break;
      case 'm':
	if(argv[xarg][2]=='f') {
	  swfactor=1;
	}
	if(xarg+1 >= argc) usage(); 
	if(swfactor) factor=readfloatarg(&xarg,argv);
	else swmaxvisit= readintarg(&xsw,&xarg,argv);
	maxnodes=swmaxvisit;
	xsw = strlen(argv[xarg])-1;
	break;
      case 'n':
	swpositive = 0;
	swnegative = 1;
	swsummary = 1;
	swposneg = 1;
	break;
      case 'o':
	swsolveonly = 1;
	if (argv[xarg][++xsw] == '\0') {
	  if(xarg+1 >= argc) usage();
	  strcpy(solveonlyname, argv[++xarg]);
	} else {
	  strcpy(solveonlyname, &argv[xarg][xsw]);
	}
	xsw = strlen(argv[xarg])-1;



	if((xarg+1 <= argc) && ( !strcmp(argv[xarg+1],"-1") || !strcmp(argv[xarg+1],"0") || !strcmp(argv[xarg+1],"1"))){
	  taggedwith=readintarg(&xsw,&xarg,argv);
	}
	break;
      case 'p':
	swpositive = 1;
	swnegative = 0;
	swsummary = 1;
	swposneg = 1;
	break;
      case 'q': 
	swquiet = 1;
	break;
      case 'r':
	swrandomorder = 1;
	break;
      case 's':
	swsummary = 1;
	break;
      case 't':
	swtesting=1;
	swsummary=1;
	if (argv[xarg][++xsw] == '\0') {
	  if(xarg+1 >= argc) usage();
	  strcpy(summaryname, argv[++xarg]);
	} else {
	  strcpy(summaryname, &argv[xarg][xsw]);
	}
	xsw = strlen(argv[xarg])-1;
	if ((summaryfile = fopen(summaryname,"w+")) == NULL) {
	  fprintf(stderr,"***Cannot open summary file '%s'\n",summaryname);
	  exit(-1);
	}
	break;
      case 'v':
	swverbose = 1;
	break;
      case 'w':
        if(argv[xarg][2]=='v')	 
	  swwqueue = 2;	
	else swwqueue = 1;
	break;
      case 'x':
        swhard = 1;
        if (argv[xarg][++xsw] == '\0') {
	  if(xarg+1 >= argc) usage();
          strcpy(hardfilename, argv[++xarg]);
        } else {
          strcpy(hardfilename, &argv[xarg][xsw]);
        }
        xsw = strlen(argv[xarg])-1;
        if ((hardfile = fopen(hardfilename,"a")) == NULL) {
          fprintf(stderr,"***Cannot open hard file '%s'\n",hardfilename);
          exit(-1);
        }
        break;
      case 'z': 
	if(argv[xarg][2]=='p')	 
	  swpcprint = 1;	
	swonlypathcons =1;
	break;
      default:
	usage();
      }
      xsw++;
    }
    xarg++;
  }

  if (xarg >= argc) infile = stdin;
  else infile = NULL;

  if (swdebug) {
    putc('I',stderr);
    fflush(stderr);
  }
  initfop();
  if (swdebug) {
    putc('!',stderr);
    fflush(stderr);
  }

  init_statistics();
  size = -1;

  getrusage(RUSAGE_SELF,&rus_glb_before);

  do {
    if (infile == NULL) {
      strcpy(infilename,argv[xarg]);
      if ((infile = fopen(infilename,"r")) == NULL) {
	fprintf(stderr,"\n*** Cannot open '%s' for reading\n",infilename);
	exit(-1);
      }
    }

    while (!feof(infile)) {
      if (swsolveonly) getnextcsp(nextcsp);
      if (swdebug) fprintf(stderr,"Next: %s\n",nextcsp);

      do {
#if defined(DYNAMIC)
	result = parsecsp_vsd(infile, MAXCSP-1, prevmax, &maxnodeid,csptype,&csp);
	
	if (swdebug) fprintf(stderr,"Check: %s\n",csptype);

	if (size == -1) { /* First CSP */
	  if (swtesting) {
	    parse_type(csptype,&newsize,&newlabel,&newdegree,&newdensity);
	    strcpy(lasttype,csptype);
	  }
	  prevmax = maxnodeid + 1;
	  size = prevmax;
	  mark = (char **)malloc(prevmax*sizeof(char *));
	  if((mark[0] = (char *)malloc(prevmax*prevmax*sizeof(char))) == NULL){
	    fprintf(stderr,"\n*** No more memory available\n");
	    exit(-1);
	  }
	  for(i=1;i<prevmax;i++)
	    mark[i] = mark[0] + i * prevmax;
	  if(swwqueue){
	    entry = (struct entry **)malloc(MAXWT*sizeof(struct entry *));
	    if((entry[0] = (struct entry *)malloc(MAXWT*prevmax*prevmax*sizeof(struct entry)))== NULL){
	      fprintf(stderr,"\n*** No more memory available\n");
	      exit(-1);
	    }
	    for(i=1;i<MAXWT;i++)
	      entry[i] = entry[0] + i * prevmax * prevmax;
	  }
	  if(swfixed || sworthogonal) {
	    consval = (int **)malloc(prevmax*sizeof(int *));
	    if((consval[0] = (int *)malloc(prevmax*prevmax*sizeof(int))) ==NULL){
	      fprintf(stderr,"\n*** No more memory available\n");
	      exit(-1);
	    }
	    for(i=1;i<prevmax;i++)
	      consval[i] = consval[0] + i * prevmax;
	  }
	}


	if (size != prevmax) size = 0;
	if (result == -1) exit(-1);
	if (prevmax <= maxnodeid) { /* new CSP larger than previous ones */
	  prevmax = maxnodeid+1;

	  free((void *) mark[0]); free((void *) mark); 

	  mark = (char **)malloc(prevmax*sizeof(char *));
	  if((mark[0] = (char *)malloc(prevmax*prevmax*sizeof(char))) ==NULL){
	    fprintf(stderr,"\n*** No more memory available\n");
	    exit(-1);
	  }
	  for(i=1;i<prevmax;i++)
	    mark[i] = mark[0] + i * prevmax;

	  if(swwqueue) {

	    free((void *) entry[0]); free((void *) entry); 

	    entry = (struct entry **)malloc(MAXWT*sizeof(struct entry *));
	    if((entry[0] = (struct entry *)malloc(MAXWT*prevmax*prevmax*sizeof(struct entry)))==NULL){
	      fprintf(stderr,"\n*** No more memory available\n");
	      exit(-1);
	    }
	    for(i=1;i<MAXWT;i++)
	      entry[i] = entry[0] + i * prevmax * prevmax;
	  }
	  if(swfixed || sworthogonal) {

	    free((void *) consval[0]); free((void *) consval); 

	    consval = (int **)malloc(prevmax*sizeof(int *));
	    if((consval[0] = (int *)malloc(prevmax*prevmax*sizeof(int)))==NULL){
	      fprintf(stderr,"\n*** No more memory available\n");
	      exit(-1);
	    }
	    for(i=1;i<prevmax;i++)
	      consval[i] = consval[0] + i * prevmax;
	  }
	}

#else
	result = parsecsp(infile, MAXCSP-1,&maxnodeid,csptype,csp);
	
	if (swdebug) fprintf(stderr,"Check: %s\n",csptype);
	
	if (size == -1) {
	  size = maxnodeid + 1;
	  if(swtesting) {
	    parse_type(csptype,&newsize,&newlabel,&newdegree,&newdensity);     
	  }
	}
	if (size != maxnodeid + 1) size = 0;
	if (result == -1) exit(-1);
#endif

      } while ((swsolveonly) &&
	       (strcmp(nextcsp,csptype) != 0) &&
	       (result != 0));

      if (result == 0) break;
      
      if ((trial >= MAXTRIAL) && (swsummary)) {
	fprintf(stderr,"\n*** More than %d CSPs given! Quitting now\n",MAXTRIAL);
	getrusage(RUSAGE_SELF,&rus_glb_after);
	cumcputicks = (double)(((double) rus_glb_after.ru_utime.tv_usec+clocks_per_second*(double)rus_glb_after.ru_utime.tv_sec) - ((double)rus_glb_before.ru_utime.tv_usec+clocks_per_second*(double)rus_glb_before.ru_utime.tv_sec))/clocks_per_second;  
	print_summary(swbrief,csptype,summaryfile);
	if (swquiet) exit(!consistent);
	else exit(0);
      }

      pcops = 0;
      pcits = 0;
      nodesvisited = 0;
      searchdepth = 0;
      minnodes = maxnodes;
      maxdepth = 0;
      pathconsistent = 0;
      if (swdebug) {
	fprintf(stderr,"\nSolving %s:\n", csptype);
	fflush(stderr);
      }   

      if(swheader) {
	if(pop_header(maxnodeid,csptype)!=1) continue;
      }

      if(swminsize) {
	if(maxnodeid+1<minsize) continue; 
      }

      getrusage(RUSAGE_SELF,&rus_lcl_before);
      
      if(swfactor){ 
	swmaxvisit=factor*(maxnodeid+1);
	maxnodes=swmaxvisit;
      }

      if(sworthogonal){
	/* use different heuristics */
	i=0;
	totalnodes=0;
	minnodes = maxnodes;
	first = '0';
	consistent = -1;
	while (order[i] != '\0') {
	  nodesvisited=0;
	  searchdepth=0;
	  ordernode[i]=0;
	  if(heuristic(order,i,&oldsplit)) {
	    fprintf(stderr, "**** `%c' is not a valid method! \n Please choose another <order> argument for the `-h[a|A <file>] <order>' switch.\n",order[i]);
	    exit(-1);
	  }

	  orthcons = global_cons(csp,maxnodeid,-1,-1); 

	  if(orthcons!=-1) ordernode[i]=nodesvisited;
	  if(nodesvisited < minnodes) {
	    minnodes=nodesvisited;
	    if(!swheuristicout) swmaxvisit=minnodes;
	    consistent = orthcons;
	    first=order[i];
	  }
	  totalnodes+=nodesvisited;
	
	  if((!swallorthogonal) && (consistent != -1)) break;
	  i++;
	}
	if(swheuristicout) heuristic_summary(minnodes, order, first, ordernode, heuristicfile);
        swmaxvisit=maxnodes;
      }
      else if(swonlypathcons){
	/* check only path-consistency */
	pathconsistent=path_cons(csp,maxnodeid, -1,-1);
	if(swpcprint && pathconsistent) printcsp(stdout,maxnodeid,csptype,csp);
	consistent=pathconsistent;
      }
      else{
	/* check global consistency */
	consistent = global_cons(csp,maxnodeid,-1,-1);
      }
      getrusage(RUSAGE_SELF,&rus_lcl_after);

      if(swtesting && parse_type(csptype,&newsize,&newlabel,&newdegree,&newdensity)) {
       print_summary(swbrief,lasttype,summaryfile);
       strcpy(lasttype,csptype);
      }
     

      if (swdebug) {
	putc('\n',stderr);
	if (swquiet){ 
	  fprintf(stderr,"... solved. path-cons=%d, cons=%d\n",
		  pathconsistent,consistent);
	}
	fflush(stderr);
      }

      /* statistics */
     
      cputicks = (double)(((double) rus_lcl_after.ru_utime.tv_usec+clocks_per_second*(double)rus_lcl_after.ru_utime.tv_sec) - ((double)rus_lcl_before.ru_utime.tv_usec+clocks_per_second*(double)rus_lcl_before.ru_utime.tv_sec))/clocks_per_second;  
     
      if(consistent != -1) {
	if (consistent) cntconsistent++;
	if (pathconsistent) cntpathconsistent++;
	cntsize += maxnodeid+1;
	if (!swposneg || 
	    ((consistent) && swpositive) || 
	    ((!consistent) && swnegative)) {
	  tpcops[rectrial] = pcops;
	  tpcits[rectrial] = pcits;
	  tnodesvisited[rectrial] = nodesvisited;
	  tmaxdepth[rectrial] = maxdepth;
	  tcputicks[rectrial] = cputicks; 
	  tconsistent[rectrial] = consistent;
	  rectrial++;
	}
	trial++;
      }
   /*    if ((swhard) && (nodesvisited >= HARD_NODES)) printcsp(hardfile,maxnodeid,csptype,csp); */
      if ((swhard) && (consistent == -1)) printcsp(hardfile,maxnodeid,csptype,csp);

      /* output result */
      if (!swquiet) {
	if (!swverbose) {
	  if (!sworthogonal)
	    fprintf(stderr,"%s: %d\n", csptype, consistent);
	  else 
	    fprintf(stdout,"%s: %d, nodes: %i, method: %c\n", csptype, consistent,minnodes,first);
	}
	else
	  fprintf(stdout,"%s: %d  CPU=%f, PC-ops=%d, PC-it=%d, Nodes=%d,Depth=%d\n",
		 csptype, consistent,
		 cputicks, pcops, pcits, nodesvisited, maxdepth);
      }

      
    }
    xarg++;
    if (infile != stdin) fclose(infile);
    infile = NULL;
  } while (xarg < argc);

  getrusage(RUSAGE_SELF,&rus_glb_after); 
  cumcputicks = (double)(((double) rus_glb_after.ru_utime.tv_usec+clocks_per_second*(double)rus_glb_after.ru_utime.tv_sec) - ((double)rus_glb_before.ru_utime.tv_usec+clocks_per_second*(double)rus_glb_before.ru_utime.tv_sec))/clocks_per_second;  
 
  if (swsummary) print_summary(swbrief,csptype,summaryfile);
  if (swquiet) exit(!consistent);
  else exit(0);
}