combine_whens(plnode);	}      break;    default:      fprintf(stdout,"wrong connective in combine_whens");/* spaeter weg */    }  end_of_function_pl("Combine_whens",plnode);}/********************************************************************* * This is the analogue function to distribute_unary. * It looks quite different due to the structure of WHEN plnodes * Instead of rec_fn both possible calling case are integrated into this  * function (I call it: inner functions, 1st/2nd branch * * INPUT  plnode: WHEN node * OUTPUT plnode: copies the WHEN node to above all the sons of the son, *   calls inner function applied to all these copied nodes afterwards, *  the original WHEN is deleted (resp. replaced by its son) * USING   *********************************************************************/voiddistribute_when (PlNode * plnode,const Bool lowest){   PlNode * i_pl, * new_pl, * k_pl;    i_pl=new_pl_node(DUMMY);  i_pl->next=plnode->sons->next->sons;  plnode->sons->next->sons=i_pl;  for (;i_pl->next!=NULL;i_pl=i_pl->next)    {      new_pl=new_pl_node(WHEN);      new_pl->sons=copy_pl_node(plnode->sons);      new_pl->sons->sons=deep_copy_tree(plnode->sons->sons);      new_pl->sons->next=i_pl->next;      i_pl->next=new_pl;      new_pl->next=new_pl->sons->next->next;      new_pl->sons->next->next=NULL;      /* inner functions */      if (lowest)	{	  /* 1st branch */	  	  /* quantifiers above WHEN */	  if (ALL==new_pl->sons->next->connective)	    {	      k_pl=new_pl->sons->next;	      while (k_pl->sons->connective!=ALL)		{		  k_pl=k_pl->sons;		}	      i_pl->next=new_pl->sons->next;	      i_pl->next->next=new_pl->next;	      new_pl->sons->next=k_pl->sons->sons->next;	      free(k_pl->sons->sons);/*  WHEN */	      free(k_pl->sons);/* TRU */	      k_pl->sons=new_pl;	      new_pl->next=NULL;	    }	}      else	{	  /* 2nd branch */	  if (contains_when(i_pl->next->sons->next)) 	    {	      combine_whens(i_pl->next);	    }		}    }  i_pl=plnode->sons->next->sons->next;  free(plnode->sons->next->sons);/* DUMMY */  plnode->connective=plnode->sons->next->connective;  plnode->atom=plnode->sons->next->atom;  free_pl_node(plnode->sons->next);  free_tree(plnode->sons->sons);  free_pl_node(plnode->sons);  plnode->sons=i_pl;}/********************************************************************* * INPUT  plnode: effect tree, multiple WHENs * OUTPUT plnode: effect tree, *            1st single AND (already melted together) *            2nd :(ALL) quantifiers,  *            3rd single WHENs (melted together using combine_whens) *                   on paths without WHEN, Literal is replaced by  *                   (WHEN TRU Literal)  * USING   *********************************************************************/voidands_to_top ( PlNode * plnode ){  PlNode * new_pl,*new_pl2,*i_pl,*j_pl;  TokenList *t1, *t2;  begin_of_function_pl("Ands to top",plnode);  if (FALSE==contains_when(plnode))    {      nots_down_quantifiers_up_pl(plnode);/* quants_up reicht */      /* state jetzt:ALL AND Lit */      /*   jetzt IF TRU zwischen Quantoren und ANDs haengen */      if (ALL==plnode->connective)	{	  /* step through quantifiers */	  i_pl=plnode;	  while (ALL==i_pl->sons->connective )	    {	      i_pl=i_pl->sons;	    }	  new_pl=new_pl_node(TRU);	  new_pl->next=i_pl->sons;	  new_pl2=new_pl_node(WHEN);	  new_pl2->sons=new_pl;	  i_pl->sons=new_pl2;	}      else	{	  new_pl=new_pl_node(TRU);	  new_pl->next=copy_pl_node(plnode);	  new_pl->next->sons=plnode->sons;	  plnode->connective=WHEN;	  plnode->sons=new_pl;	  t1 = plnode->atom;	  while ( t1 ) {	    t2 = t1->next;	    if ( '?' == *(t1->item) ) {	      free( t1->item );	    }	    free( t1 );	    t1 = t2;	  }	}    }  if (0 && gcmd_line.display_info>=20)    {       printf("\n%u MITTEN in andstotop\n",dep);      print_plnode( plnode ,0);    }  switch (plnode->connective)    {    case AND:      for(i_pl=plnode->sons;NULL!=i_pl;i_pl=i_pl->next)	    {	      ands_to_top(i_pl);	    }      combine_ands_pl(plnode);      break;    case ALL:      ands_to_top(plnode->sons);      if (plnode->sons->connective!=AND)	{	  spec_error("Ands_to_top1");	}      distribute_unary_pl(plnode,NULL);      break;    case WHEN:       if (TRUE==contains_when(plnode->sons->next))	{	  combine_whens(plnode);	  ands_to_top(plnode);	}      else	{ 	  /* pop_pl(AND,plnode)=schiebe an Stelle von plnode neuen AND */	  new_pl=new_pl_node(WHEN); 	  new_pl->sons=plnode->sons; 	  plnode->connective=AND;	  i_pl=plnode->sons->next;	  if (ALL==i_pl->connective )	    {	      j_pl=i_pl;	      while (ALL==i_pl->sons->connective )		{		  i_pl=i_pl->sons;		}	      plnode->sons=j_pl;	      new_pl->sons->next=i_pl->sons;	      i_pl->sons=new_pl;	      if (new_pl->sons->next->connective!=NOT && 		  new_pl->sons->next->connective!=ATOM)		{		  combine_ands_pl(new_pl->sons->next);		}	    }	  else	    {	      plnode->sons=new_pl;	      if (i_pl->connective!=NOT && i_pl->connective!=ATOM)		{		  combine_ands_pl(i_pl);		}	    }	}      break;    default:      spec_error("Ands to top");    }  end_of_function_pl("Ands to top",plnode);}  /********************************************************************* * INPUT  plnode: NOT, ALL, EX node * OUTPUT plnode: copies the unary node to above all the sons of the son, *   calls rec_fn appled to all these copied nodes afterwards, the original * plnode is deleted (resp. replaced by its son) * eg. NOT                      AND *      |                        | *     AND            becomes   NOT----NOT *      |                        |      | *     node 1--node 2           node 1 node 2 *  and rec_fn ( NOT ) and rec_fn( NOT ) are called *                |                 | *              node 1            node2 * USING   *********************************************************************/voiddistribute_unary_pl (PlNode * plnode,void ( * rec_fn)(PlNode * plnode)){  PlNode * i_pl, * new_pl;    TokenList *t1, *t2;  i_pl=new_pl_node(DUMMY);  i_pl->next=plnode->sons->sons;  plnode->sons->sons=i_pl;  for (;i_pl->next!=NULL;i_pl=i_pl->next)    {      new_pl=copy_pl_node(plnode);      new_pl->sons=i_pl->next;      i_pl->next=new_pl;      new_pl->next=new_pl->sons->next;      new_pl->sons->next=NULL;      if (NULL!=rec_fn)	{	  ( * rec_fn)(new_pl);	}    }  i_pl=plnode->sons->sons->next;  free(plnode->sons->sons);/* DUMMY */  plnode->connective=plnode->sons->connective;  t1 = plnode->atom;  while( t1 ) {    t2 = t1->next;    if ( '?' == *(t1->item) ) {      free( t1->item );    }    free( t1 );    t1 = t2;  }  plnode->atom=plnode->sons->atom;  free(plnode->sons);  plnode->sons=i_pl;}/********************************************************************* * INPUT  plnode: condition tree (no WHENs) * OUTPUT plnode: equivalent precondition tree, *            1st layer at the top: quantifiers *            2nd : ANDs/ORs (not melted together yet) *            3rd : Literals (NOTs and ATOMs) * USING   *********************************************************************/voidnots_down_quantifiers_up_pl (PlNode * plnode){  PlNode * i_pl;  begin_of_function_pl("Nots_down_quantifiers_up_pl",plnode);  switch (plnode->connective)    {    case NOT:      nots_down_quantifiers_up_pl(plnode->sons);      switch (plnode->sons->connective)	{	case NOT:	  /* delete both NOT nodes */	  i_pl=plnode->sons;	  plnode->atom=plnode->sons->sons->atom;	  plnode->connective=plnode->sons->sons->connective;	  plnode->sons=plnode->sons->sons->sons;	  free(i_pl->sons);	  free(i_pl);	  break;	case AND:	  distribute_unary_pl(plnode,nots_down_quantifiers_up_pl);	  plnode->connective=OR;	  break;	case OR:	  distribute_unary_pl(plnode,nots_down_quantifiers_up_pl);	  plnode->connective=AND;	  break;	case ALL:	  plnode->atom=plnode->sons->atom;	  plnode->connective=EX;	  plnode->sons->atom=NULL;	  plnode->sons->connective=NOT;	  nots_down_quantifiers_up_pl(plnode);	  break;	case EX:	  plnode->atom=plnode->sons->atom;	  plnode->connective=ALL;	  plnode->sons->atom=NULL;	  plnode->sons->connective=NOT;	  nots_down_quantifiers_up_pl(plnode);	  break;	case ATOM:	  break;	default:	  spec_error("Nots_down_pl");	}      break;    case AND:    case OR:      all_the_quantifiers_top_pl(plnode);      break;    case ALL:    case EX:      nots_down_quantifiers_up_pl(plnode->sons);      break;    case ATOM:    case TRU:      break;    default:      spec_error("Nots_down_quantifiers_up_pl");    }  end_of_function_pl("Nots_down_quantifiers_up_pl",plnode);}/********************************************************************* * INPUT  plnode: condition tree (no WHENs) * OUTPUT plnode: equivalent precondition tree, *            1st layer at the top: quantifiers *            2nd : ANDs/ORs (not melted together yet) *            3rd : Literals (NOTs and ATOMs) * USING   *********************************************************************/voidnots_down (PlNode * plnode){  PlNode * i_pl;  begin_of_function_pl("Nots_down",plnode);  switch (plnode->connective)    {    case NOT:      nots_down(plnode->sons);      switch (plnode->sons->connective)	{	case NOT:	  /* delete both NOT nodes */	  i_pl=plnode->sons;	  plnode->atom=plnode->sons->sons->atom;	  plnode->connective=plnode->sons->sons->connective;	  plnode->sons=plnode->sons->sons->sons;	  free(i_pl->sons);	  free(i_pl);	  break;	case AND:	  distribute_unary_pl(plnode,nots_down_quantifiers_up_pl);	  plnode->connective=OR;	  break;	case OR:	  distribute_unary_pl(plnode,nots_down_quantifiers_up_pl);	  plnode->connective=AND;	  break;	case ALL:	  plnode->atom=plnode->sons->atom;	  plnode->connective=EX;	  plnode->sons->atom=NULL;	  plnode->sons->connective=NOT;	  nots_down_quantifiers_up_pl(plnode);	  break;	case EX:	  plnode->atom=plnode->sons->atom;	  plnode->connective=ALL;	  plnode->sons->atom=NULL;	  plnode->sons->connective=NOT;	  nots_down_quantifiers_up_pl(plnode);	  break;	case ATOM:	  break;	default:	  spec_error("Nots_down");	}      break;    case AND:    case OR:      i_pl=plnode->sons;      while (i_pl!=NULL)	{	  nots_down(i_pl);	  i_pl=i_pl->next;	}      break;    case ALL:    case EX:      nots_down(plnode->sons);      break;    case ATOM:    case TRU:      break;    default:      spec_error("Nots_down");    }  end_of_function_pl("Nots_down",plnode);}/********************************************************************* * This function removes vertical quantifier list at bef_from_pl->next *  and copies it between bef_to_pl and bef_to_pl->next, returns last  *  quantifier * INPUT  plnode * OUTPUT plnode: the  last element of the new quantifier list * USING   *********************************************************************/PlNode *move_quantifier_pl (PlNode * bef_from_pl ,PlNode * bef_to_pl)  {  PlNode *i_pl,*from_pl,*to_pl;  from_pl=bef_from_pl->next;  to_pl=bef_to_pl->sons;      /*step through quantifiers */  i_pl=from_pl;  while (ALL==i_pl->sons->connective || EX==i_pl->sons->connective)    {      i_pl=i_pl->sons;    }  bef_from_pl->next=i_pl->sons;  i_pl->sons->next=from_pl->next;  i_pl->sons=bef_to_pl->sons;  bef_to_pl->sons=from_pl;  return i_pl;}/********************************************************************* * This function does the same as (is just the AND/OR branch of)  *   nots_down_qunatifiers_up_pl * INPUT  plnode: AND or OR node  * OUTPUT plnode: see nots_down_qunatifiers_up_pl * USING