instantiateii.c

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

  while ( i && 
	  has_contradicting_unconditional( i->conditionals ) ) {
    j = i;
    i = i->next;
    free_CodeOperator( j );
  }
  ginst_code_operators = i;
  prev = i;
  if ( i ) i = i->next;
  while ( i ) {
    if ( has_contradicting_unconditional( i->conditionals ) ) {
      prev->next = i->next;
      j = i;
      i = i->next;
      free_CodeOperator( j );
    } else {
      prev = prev->next;
      i = i->next;
    }
  }

}



void simplify_condition_CodeNode( CodeNode **n, Bool warnings, Bool condition )

{

  CodeNode *i, *j, *prev;
  int count = 0;

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

  if ( (*n)->connective == ATOM ) {
    if ( (*n)->predicate == -1 ) {
      if ( (*n)->arguments[0] < 0 ||
	   (*n)->arguments[1] < 0 ) {
	return;
      }
      if ( (*n)->arguments[0] == (*n)->arguments[1] ) {
	if ( warnings ) {
	  printf("\ndetected eq predicate on equal constants");
	}
	(*n)->connective = TRU;
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	return;
      } else {
	if ( warnings ) {
	  printf("\ndetected eq predicate on different constants");
	}
      	(*n)->connective = FAL;
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	return;
      }
    }

    return;
  }

  if ( (*n)->connective == NOT ) {
    simplify_condition_CodeNode( &((*n)->sons), warnings, condition );
    if ( (*n)->sons->connective == TRU ) {
      if ( warnings ) {
	printf("\npropagating TRUE over NOT");
      }
      (*n)->connective = FAL;
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
      return;
    }
    if ( (*n)->sons->connective == FAL ) {
      if ( warnings ) {
	printf("\npropagating FALSE over NOT");
      }
      (*n)->connective = TRU;
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
      return;
    }
    return;
  }

  if ( (*n)->connective == AND ) {
    for ( i = (*n)->sons; i; i=i->next ) {
      simplify_condition_CodeNode( &i, warnings, condition );
      if ( i->connective == FAL ) {
	if ( warnings ) {
	  printf("\nson of AND got FALSE");
	}
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	(*n)->connective = FAL;
	return;
      }
    }
    i = (*n)->sons;
    while ( i && i->connective == TRU ) {
      if ( warnings ) {
	printf("\nson of AND got TRU");
      }
      j = i;
      i = i->next;
      free_CodeNode( j->sons );
      free( j );
    }
    (*n)->sons = i;
    prev = i;
    if ( i ) {
      i = i->next;
      count++;
    }
    while ( i ) {
      if ( i->connective == TRU ) {
	if ( warnings ) {
	  printf("\nson of AND got TRU");
	}
	prev->next = i->next;
	j = i;
	i = i->next;
	free_CodeNode( j->sons );
	free( j );
      } else {
	count++;
	prev = prev->next;
	i = i->next;
      }
    }
    if ( count == 0 ) {
      if ( warnings ) {
	printf("\nAND has no sons (anymore)");
      }
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
      (*n)->connective = TRU;
      return;
    }
    if ( count == 1 && condition ) {
      if ( warnings ) {
	printf("\nAND has only one son (anymore)");
      }
      i = (*n)->sons;
      copy_contents_of_CodeNode( n, i );
      (*n)->sons = i->sons;
      free( i );
      return;
    }
    return;
  }
      
  if ( (*n)->connective == OR ) {
    for ( i = (*n)->sons; i; i=i->next ) {
      simplify_condition_CodeNode( &i, warnings, condition );
      if ( i->connective == TRU ) {
	if ( warnings ) {
	  printf("\nson of OR got TRUE");
	}
	free_CodeNode( (*n)->sons );
	(*n)->sons = NULL;
	(*n)->connective = TRU;
	return;
      }
    }
    i = (*n)->sons;
    while ( i && i->connective == FAL ) {
      if ( warnings ) {
	printf("\nson of OR got FALSE");
      }
      j = i;
      i = i->next;
      free_CodeNode( j->sons );
      free( j );
    }
    (*n)->sons = i;
    prev = i;
    if ( i ) {
      i = i->next;
      count++;
    }
    while ( i ) {
      if ( i->connective == FAL ) {
	if ( warnings ) {
	  printf("\nson of OR got FALSE");
	}
	prev->next = i->next;
	j = i;
	i = i->next;
	free_CodeNode( j->sons );
	free( j );
      } else {
	count++;
	prev = prev->next;
	i = i->next;
      }
    }
    if ( count == 0 ) {
      if ( warnings ) {
	printf("\nOR has no sons (anymore)");
      }
      free_CodeNode( (*n)->sons );
      (*n)->sons = NULL;
      (*n)->connective = FAL;
      return;
    }
    if ( count == 1 && condition ) {
      if ( warnings ) {
	printf("\nOR has only one son (anymore)");
      }
      i = (*n)->sons;
      copy_contents_of_CodeNode( n, i );
      (*n)->sons = i->sons;
      free( i );
      return;
    }
    return;
  }

  if ( (*n)->connective == ALL ||
       (*n)->connective == EX ) {
    if ( !((*n)->sons) ) {
      return;
    }
    simplify_condition_CodeNode( &(*n)->sons, warnings, condition );
    if ( (*n)->sons->connective == TRU ) {
      if ( warnings ) {
	printf("\npropagating TRUE over ALL/EX");
      }
      free_CodeNode( (*n)->sons );
      (*n)->connective = TRU;
      return;
    }
    if ( (*n)->sons &&
	 (*n)->sons->connective == FAL ) {
      if ( warnings ) {
	printf("\npropagating FALSE over ALL/EX");
      }
      free_CodeNode( (*n)->sons );
      (*n)->connective = FAL;
      return;
    }
    return;
  }

  if ( (*n)->connective != TRU &&
       (*n)->connective != FAL ) {
    printf("\nsimplify shouldn't get here: non ATOM,NOT,AND,OR,ALL,EX,FAL,TRU %s in cond\n\n",
	   gconnectives[(*n)->connective] );
  }


}



void clean_up_effects( CodeNode **n, Bool warnings )

{

  CodeNode *i, *j, *prev;
  int count = 0;

  i = (*n)->sons;
  while ( i && 
	  ( impossible_effect( i, warnings ) ||
	    no_transition_effect( i, warnings ) ) ) {
    if ( warnings ) {
      printf("\nremoving effect");
    }
    j = i;
    i = i->next;
    free_CodeNode( j->sons );
    free( j );
  }
  (*n)->sons = i;
  prev = i;
  if ( i ) {
    i = i->next;
    count++;
  }
  while ( i ) {
    if ( impossible_effect( i, warnings ) ||
	 no_transition_effect( i, warnings ) ) {
      if ( warnings ) {
	printf("\nremoving effect");
      }
      prev->next = i->next;
      j = i;
      i = i->next;
      free_CodeNode( j->sons );
      free( j );
    } else {
      count++;
      prev = prev->next;
      i = i->next;
    }
  }

  if ( count == 0 ) {
    free_CodeNode( (*n) );
    (*n) = NULL;
  }
   

}



Bool impossible_effect( CodeNode *n, Bool warnings )

{

  CodeNode *nn;

  for ( nn = n; nn->connective != WHEN; nn = nn->sons );
  if ( nn->sons->connective == FAL ) {
    if ( warnings ) {
      printf("\ndetected impossible effect");
    }
    return TRUE;
  }

  return FALSE;

}



Bool no_transition_effect( CodeNode *n, Bool warnings )

{

  CodeNode *nn;

  for ( nn = n; nn->connective != WHEN; nn = nn->sons );
  if ( nn->sons->next->connective == TRU ) {
    if ( warnings ) {
      printf("\neffect causes no state transition");
    }
    return TRUE;
  }

  return FALSE;

}



Bool has_contradicting_unconditional( CodeNode *n )

{

  CodeNode *i;

  for ( i = n->sons; i; i = i->next ) {
    if ( contradicting_unconditional_effect( i ) ) {
      return TRUE;
    }
  }

  return FALSE;

}



Bool contradicting_unconditional_effect( CodeNode *n )

{


  CodeNode *nn;

  for ( nn = n; nn->connective != WHEN; nn = nn->sons );
  if ( nn->sons->connective == TRU &&
       nn->sons->next->connective == FAL ) {
    return TRUE;
  }

  return FALSE;

}



Bool var_used_under_CodeNode( int var_num, CodeNode *n )

{

  int i;

  if ( !n ) {
    return FALSE;
  }

  if ( n->connective == ATOM ) {
    if ( n->predicate == -1 ) {
      if ( n->arguments[0] == ((-1)*var_num)-1 ) {
	return TRUE;
      }
      if ( n->arguments[1] == ((-1)*var_num)-1 ) {
	return TRUE;
      }
    } else {
      for ( i=0; i<garity[n->predicate]; i++ ) {
	if ( n->arguments[i] == ((-1)*var_num)-1 ) {
	  return TRUE;
	}
      }
    }
  }

  if ( var_used_under_CodeNode( var_num, n->next ) ) {
    return TRUE;
  }
  if ( var_used_under_CodeNode( var_num, n->sons ) ) {
    return TRUE;
  }

  return FALSE;

}



void remove_unused_vars_under_CodeNode( CodeNode **n, Bool warnings )

{

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

  rec_remove_unused_vars_under_CodeNode( n, warnings );

  if ( (*n)->connective == EMPTY ) {
    free( *n );
    *n = NULL;
  }

}



void rec_remove_unused_vars_under_CodeNode( CodeNode **n, Bool warnings )

{

  CodeNode *tmp;

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

  rec_remove_unused_vars_under_CodeNode( &((*n)->next), warnings );
  if ( (*n)->next && 
       (*n)->next->connective == EMPTY ) {
    free( (*n)->next );
    (*n)->next = NULL;
  }
  rec_remove_unused_vars_under_CodeNode( &((*n)->sons), warnings );
  if ( (*n)->sons && 
       (*n)->sons->connective == EMPTY ) {
    free( (*n)->sons );
    (*n)->sons = NULL;
  }

  if ( (*n)->connective == ALL ||
       (*n)->connective == EX ) {
    if ( !var_used_under_CodeNode( (*n)->var, (*n)->sons ) ) {
      if ( warnings ) {
	printf("\nwarning: quantified variable x%d is not used. removing it",
	       (*n)->var );
      }
      if ( !((*n)->sons) ) {
	if ( !((*n)->next) ) {
	  (*n)->connective = EMPTY;
	  return;
	}
	copy_contents_of_CodeNode( n, (*n)->next );
	tmp = (*n)->next;
	(*n)->sons = (*n)->next->sons;
	(*n)->next = (*n)->next->next;
	free( tmp );
	return;
      }
      copy_contents_of_CodeNode( n, (*n)->sons );
      tmp = (*n)->sons;
      (*n)->sons = (*n)->sons->sons;
      /* pointer (*n)->sons->next gets lost!!
       *
       * make use of the fact, that this pointer can not have a ->next
       */
      free( tmp );
    }
  }

}




void rename_vars_under_CodeNode( CodeNode **n, int num_vars )

{

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

  if ( (*n)->connective == ALL ||
       (*n)->connective == EX ) {
    if ( (*n)->var != num_vars ) {
      replace_var_with_newvar_under_CodeNode( (*n)->var, num_vars, 
					      &((*n)->sons) );
      (*n)->var = num_vars;
    }
    rename_vars_under_CodeNode( &((*n)->sons), num_vars+1 );
    rename_vars_under_CodeNode( &((*n)->next), num_vars );
    return;
  }

  rename_vars_under_CodeNode( &((*n)->next), num_vars );
  rename_vars_under_CodeNode( &((*n)->sons), num_vars );

}



void replace_var_with_newvar_under_CodeNode( int var, int new_var, 
					     CodeNode **n )

{

  int i;

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

  if ( (*n)->connective == ATOM ) {
    if ( (*n)->predicate == -1 ) {
      if ( (*n)->arguments[0] == ((-1)*var)-1 ) {
	(*n)->arguments[0] = ((-1)*new_var)-1;
      }
      if ( (*n)->arguments[1] == ((-1)*var)-1 ) {
	(*n)->arguments[1] = ((-1)*new_var)-1;
      }
    } else {
      for ( i=0; i<garity[(*n)->predicate]; i++ ) {
	if ( (*n)->arguments[i] == ((-1)*var)-1 ) {
	  (*n)->arguments[i] = ((-1)*new_var)-1;
	}
      }
    }
  }

  replace_var_with_newvar_under_CodeNode( var, new_var, 
					  &((*n)->next) );
  replace_var_with_newvar_under_CodeNode( var, new_var, 
					  &((*n)->sons) );
 
}