void simplify_wff()

in grolp/gen/ff_planner/inst_pre.c [1673:1875]


void simplify_wff( WffNode **w )

{

  WffNode *i, *tmp;
  int m;
  Bool ct;

  switch ( (*w)->connective ) {
  case ALL:
  case EX:
    simplify_wff( &((*w)->son) );
    if ( (*w)->son->connective == TRU ||
	 (*w)->son->connective == FAL ) {
      (*w)->connective = (*w)->son->connective;
      free( (*w)->son );
      (*w)->son = NULL;
      if ( (*w)->var_name ) {
	free( (*w)->var_name );
      }
    }
    break;
  case AND:
    m = 0;
    i = (*w)->sons;
    while ( i ) {
      simplify_wff( &i );
      if ( i->connective == FAL ) {
	(*w)->connective = FAL;
	/* free_WffNode( (*w)->sons ); */
	(*w)->sons = NULL;
	return;
      }
      if ( i->connective == TRU ) {
	if ( i->prev ) {
	  i->prev->next = i->next;
	} else {
	  (*w)->sons = i->next;
	}
	if ( i->next ) {
	  i->next->prev = i->prev;
	}
	tmp = i;
	i = i->next;
	free( tmp );
	continue;
      }
      i = i->next;
      m++;
    }
    if ( m == 0 ) {
      (*w)->connective = TRU;
      free_WffNode( (*w)->sons );
      (*w)->sons = NULL;
    }
    if ( m == 1 ) {
      (*w)->connective = (*w)->sons->connective;
      (*w)->var = (*w)->sons->var;
      (*w)->var_type = (*w)->sons->var_type;
      if ( (*w)->var_name ) {
	free( (*w)->var_name );
      }
      (*w)->var_name = (*w)->sons->var_name;
      (*w)->son = (*w)->sons->son;
      if ( (*w)->fact ) {
	free( (*w)->fact );
      }
      (*w)->fact = (*w)->sons->fact;
      (*w)->comp = (*w)->sons->comp;
      if ( (*w)->lh ) free_ExpNode( (*w)->lh );
      if ( (*w)->rh ) free_ExpNode( (*w)->rh );
      (*w)->lh = (*w)->sons->lh;
      (*w)->rh = (*w)->sons->rh;

      tmp = (*w)->sons;
      (*w)->sons = (*w)->sons->sons;
      free( tmp );
    }
    break;
  case OR:
    m = 0;
    i = (*w)->sons;
    while ( i ) {
      simplify_wff( &i );
      if ( i->connective == TRU ) {
	(*w)->connective = TRU;
	free_WffNode( (*w)->sons );
	(*w)->sons = NULL;
	return;
      }
      if ( i->connective == FAL ) {
	if ( i->prev ) {
	  i->prev->next = i->next;
	} else {
	  (*w)->sons = i->next;
	}
	if ( i->next ) {
	  i->next->prev = i->prev;
	}
	tmp = i;
	i = i->next;
	free( tmp );
	continue;
      }
      i = i->next;
      m++;
    }
    if ( m == 0 ) {
      (*w)->connective = FAL;
      /* free_WffNode( (*w)->sons ); */
      (*w)->sons = NULL;
    }
    if ( m == 1 ) {
      (*w)->connective = (*w)->sons->connective;
      (*w)->var = (*w)->sons->var;
      (*w)->var_type = (*w)->sons->var_type;
      if ( (*w)->var_name ) {
	free( (*w)->var_name );
      }
      (*w)->var_name = (*w)->sons->var_name;
      (*w)->son = (*w)->sons->son;
      if ( (*w)->fact ) {
	free( (*w)->fact );
      }
      (*w)->fact = (*w)->sons->fact;
      (*w)->comp = (*w)->sons->comp;
      if ( (*w)->lh ) free_ExpNode( (*w)->lh );
      if ( (*w)->rh ) free_ExpNode( (*w)->rh );
      (*w)->lh = (*w)->sons->lh;
      (*w)->rh = (*w)->sons->rh;

      tmp = (*w)->sons;
      (*w)->sons = (*w)->sons->sons;
      free( tmp );
    }
    break;
  case NOT:
    simplify_wff( &((*w)->son) );
    if ( (*w)->son->connective == TRU ||
	 (*w)->son->connective == FAL ) {
      (*w)->connective = ( (*w)->son->connective == TRU ) ? FAL : TRU;
      free( (*w)->son );
      (*w)->son = NULL;
    }
    break;
  case ATOM:
    if ( (*w)->visited ) {
      /* already seen and not changed
       */
      break;
    }
    if ( !possibly_negative( (*w)->fact ) ) {
      (*w)->connective = TRU;
      free( (*w)->fact );
      (*w)->fact = NULL;
      break;
    }
    if ( !possibly_positive( (*w)->fact ) ) {
      (*w)->connective = FAL;
      free( (*w)->fact );
      (*w)->fact = NULL;
      break;
    }
    (*w)->visited = TRUE;
    break;
  case COMP:
    simplify_exp( &((*w)->lh) );
    simplify_exp( &((*w)->rh) );
    if ( (*w)->lh->connective != NUMBER ||
	 (*w)->rh->connective != NUMBER ) {
      /* logical simplification only possible if both parts are numbers
       */
      break;
    }
    ct = number_comparison_holds( (*w)->comp, (*w)->lh->value, (*w)->rh->value );
    if ( ct ) {
      (*w)->connective = TRU;
      free_ExpNode( (*w)->lh );
      (*w)->lh = NULL;
      free_ExpNode( (*w)->rh );
      (*w)->rh = NULL;
      (*w)->comp = -1;
      break;
    } else {
      (*w)->connective = FAL;
      free_ExpNode( (*w)->lh );
      (*w)->lh = NULL;
      free_ExpNode( (*w)->rh );
      (*w)->rh = NULL;
      (*w)->comp = -1;
      break;
    }
    break;
  case TRU:
  case FAL:
    break;
  default:
    printf("\nwon't get here: simplify, non logical %d\n\n",
	   (*w)->connective);
    exit( 1 );
  }

}