instantiateiii.c

intel ipp4.1性能库的一些例子。

/* --> expand quantifiers
 * --> instantiate atoms, respecting inertia relations
 */
void expand_quantifiers_under_CodeNode( CodeNode **n, 
					short int var, short int constant )

{

  CodeNode *r = NULL, *tmp, *i;
  Integers *k;
  int l;
  Bool change;


  if ( !(*n) ) {
    return;
  }

  if ( (*n)->connective == ALL ) {
    if ( var != -1 ) { 
      expand_quantifiers_under_CodeNode( &((*n)->sons), var, constant );
      return;
    }

    (*n)->connective = AND;
    for ( k = (gtypes_table[(*n)->var_type]).integers; k; k=k->next ) {
      tmp = deep_copy_CodeTree( (*n)->sons );
      expand_quantifiers_under_CodeNode( &tmp, (*n)->var, k->index );
      tmp->next = r;
      r = tmp;
    }

    free_CodeNode( (*n)->sons );
    (*n)->sons = r;
    (*n)->var = 0;
    (*n)->var_type = 0;

    for ( i = (*n)->sons; i; i=i->next ) {
      expand_quantifiers_under_CodeNode( &i, -1, 0 );
    }

    return;
  }

  if ( (*n)->connective == EX ) {
    if ( var != -1 ) { 
      expand_quantifiers_under_CodeNode( &((*n)->sons), var, constant );
      return;
    }

    (*n)->connective = OR;
    for ( k = (gtypes_table[(*n)->var_type]).integers; k; k=k->next ) {
      tmp = deep_copy_CodeTree( (*n)->sons );
      expand_quantifiers_under_CodeNode( &tmp, (*n)->var, k->index );
      tmp->next = r;
      r = tmp;
    }
    
    free_CodeNode( (*n)->sons );
    (*n)->sons = r;
    (*n)->var = 0;
    (*n)->var_type = 0;

    for ( i = (*n)->sons; i; i=i->next ) {
      expand_quantifiers_under_CodeNode( &i, -1, 0 );
    }

    return;
  }
      

  if ( (*n)->connective == ATOM ) {
    if ( var == -1 ) {
      return;
    }

    if ( (*n)->predicate == -1 ) {
      if ( (*n)->arguments[0] == ((-1)*var)-1 ) {
	(*n)->arguments[0] = constant;
      }
      if ( (*n)->arguments[1] == ((-1)*var)-1 ) {
	(*n)->arguments[1] = constant;
      }
      if ( (*n)->arguments[0] == (*n)->arguments[1] ) {
	(*n)->connective = TRU;
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	return;
      }
      if ( (*n)->arguments[0] > -1 &&
	   (*n)->arguments[1] > -1 &&
	   (*n)->arguments[0] != (*n)->arguments[1] ) {
      	(*n)->connective = FAL;
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	return;
      }
      return;
    }

    change = FALSE;
    for ( l=0; l<garity[(*n)->predicate]; l++ ) {
      if ( (*n)->arguments[l] == ((-1)*var)-1 ) {
	(*n)->arguments[l] = constant;
	change = TRUE;
      }
    }
    if ( !change && (*n)->visited ) {
      /* we did not change anything and we've already seen that node
       * --> it cant be simplified
       */
      return;
    }
    if ( !possibly_positive( (*n)->predicate, (*n)->arguments ) ) {
      (*n)->connective = FAL;
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
      return;
    }
    if ( !possibly_negative( (*n)->predicate, (*n)->arguments ) ) {
      (*n)->connective = TRU;
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
    }
    (*n)->visited = TRUE;
    return;
  }

  if ( (*n)->connective == NOT ) {
    expand_quantifiers_under_CodeNode( &((*n)->sons), var, constant );
    return;
  }

  if ( (*n)->connective == AND ||
       (*n)->connective == OR ) {
    for ( i = (*n)->sons; i; i=i->next ) {
      expand_quantifiers_under_CodeNode( &i, var, constant );
    }
    return;
  }

  if ( (*n)->connective == TRU ||
       (*n)->connective == FAL ) {
    return;
  }
      
  printf("\nshouldn't get here: non ALL,EX,ATOM,NOT,AND,OR,TRU,FAL in expanding\n\n");
  exit( 1 );

}




/* --> instantiate atoms under inertia - constraints
 */
void make_inst_version_of_condition( CodeNode **n,
				     short int var, short int constant )

{

  CodeNode *i;
  int l;
  Bool change;

  if ( !(*n) ) {
    return;
  }

  if ( (*n)->connective == ATOM ) {
    if ( var == -1 ) {
      return;
    }

    if ( (*n)->predicate == -1 ) {
      if ( (*n)->arguments[0] == ((-1)*var)-1 ) {
	(*n)->arguments[0] = constant;
      }
      if ( (*n)->arguments[1] == ((-1)*var)-1 ) {
	(*n)->arguments[1] = constant;
      }
      if ( (*n)->arguments[0] == (*n)->arguments[1] ) {
	(*n)->connective = TRU;
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	return;
      }
      if ( (*n)->arguments[0] > -1 &&
	   (*n)->arguments[1] > -1 &&
	   (*n)->arguments[0] != (*n)->arguments[1] ) {
      	(*n)->connective = FAL;
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	return;
      }
      return;
    }

    change = FALSE;
    for ( l=0; l<garity[(*n)->predicate]; l++ ) {
      if ( (*n)->arguments[l] == ((-1)*var)-1 ) {
	(*n)->arguments[l] = constant;
	change = TRUE;
      }
    }
    if ( !change && (*n)->visited ) {
      return;
    }
    if ( !possibly_positive( (*n)->predicate, (*n)->arguments ) ) {
      (*n)->connective = FAL;
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
      return;
    }
    if ( !possibly_negative( (*n)->predicate, (*n)->arguments ) ) {
      (*n)->connective = TRU;
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
    }
    (*n)->visited = TRUE;
    return;
  }

  if ( (*n)->connective == NOT ) {
    expand_quantifiers_under_CodeNode( &((*n)->sons), var, constant );
    return;
  }

  if ( (*n)->connective == AND || 
       (*n)->connective == OR ) {
    for ( i = (*n)->sons; i; i=i->next ) {
      expand_quantifiers_under_CodeNode( &i, var, constant );
    }
    return;
  }
      
  if ( (*n)->connective != TRU &&
       (*n)->connective != FAL ) {
    printf("\ninst shouldn't get here: non ATOM,NOT,AND,OR,TRU,FAL %d in inst version\n\n",
	   (*n)->connective);
    exit( 1 );
  }

}



/* --> schlicht atome instanziieren.
 */
void make_inst_version_of_effect( CodeNode **n,
				  short int var, short int constant )

{

  CodeNode *i;
  int l;

  if ( !(*n) ) {
    return;
  }
  
  for ( i=(*n)->sons; i; i=i->next ) {
    if ( i->connective == NOT ) {
      for ( l=0; l<garity[i->sons->predicate]; l++ ) {
	if ( i->sons->arguments[l] == ((-1)*var)-1 ) {
	  i->sons->arguments[l] = constant;
	}
      }
      continue;
    }
    for ( l=0; l<garity[i->predicate]; l++ ) {
      if ( i->arguments[l] == ((-1)*var)-1 ) {
	i->arguments[l] = constant;
      }
    }
  }

}



/* during expansion, multiple trees of ANDs / ORs can arise.
 *
 * a little INEFFICIENT: should happen during expanding, but is
 * extremely difficult to implemet there. not that critical
 * with respect to computation time anyway, I think
 */
void merge_multiple_ANDs_and_ORs( CodeNode **n )

{

  CodeNode *i, *j, *prev, *r = NULL;

  if ( !(*n) ) {
    return;
  }

  if ( (*n)->connective == AND ) {

    for ( i = (*n)->sons; i; i = i->next ) {
      merge_multiple_ANDs_and_ORs( &i );
    }

    i = (*n)->sons;
    while ( i && i->connective == AND ) {
      if ( i->sons ) {
	for ( j=i->sons; j->next; j=j->next );
	j->next = r;
	r = i->sons;
      }

      j = i;
      i = i->next;
      free( j );
    }
    (*n)->sons = i;
    prev = i;
    if ( i ) i = i->next;
    while ( i ) {
      if ( i->connective == AND ) {
	if ( i->sons ) {
	  for ( j=i->sons; j->next; j=j->next );
	  j->next = r;
	  r = i->sons;
	}
	
	prev->next = i->next;
	j = i;
	i = i->next;
	free( j );
      } else {
	prev = prev->next;
	i = i->next;
      }
    }
    for ( j = r; j && j->next; j = j->next );
    if ( j ) {
      j->next = (*n)->sons;
      (*n)->sons = r;
    }

    return;
  }

  if ( (*n)->connective == OR ) {

    for ( i = (*n)->sons; i; i = i->next ) {
      merge_multiple_ANDs_and_ORs( &i );
    }

    i = (*n)->sons;
    while ( i && i->connective == OR ) {
      if ( i->sons ) {
	for ( j=i->sons; j->next; j=j->next );
	j->next = r;
	r = i->sons;
      }

      j = i;
      i = i->next;
      free( j );
    }
    (*n)->sons = i;
    prev = i;
    if ( i ) i = i->next;
    while ( i ) {
      if ( i->connective == OR ) {
	if ( i->sons ) {
	  for ( j=i->sons; j->next; j=j->next );
	  j->next = r;
	  r = i->sons;
	}
	
	prev->next = i->next;
	j = i;
	i = i->next;
	free( j );
      } else {
	prev = prev->next;
	i = i->next;
      }
    }
    for ( j = r; j && j->next; j = j->next );
    if ( j ) {
      j->next = (*n)->sons;
      (*n)->sons = r;
    }

    return;
  }

  if ( (*n)->connective == NOT ) {
    merge_multiple_ANDs_and_ORs( &((*n)->sons) );
    return;
  }

  if ( (*n)->connective == ATOM ) {
    return;
  }

  if ( (*n)->connective != TRU &&
       (*n)->connective != FAL ) {
    printf("\nmerge: non AND,OR,NOT,ATOM,TRU,FAL node %d in expanded condition\n\n",
	   (*n)->connective);
    exit( 1 );
  }

}