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 );
}
}