#include  "defns.i"
#include  "extern.i"

extern Boolean CheckOrders;	/* for interpret */



	/*  See whether literals can be dropped from a clause  */

    PruneClause(C, Lits)
/*  -----------  */
    Clause C;
    int Lits;
{
    Boolean JunkLiteral();
    int i, Errs;
    Tuple *TSP, Case;

    Errs = TotCovered - PosCovered;

    VERBOSE(1)
	printf("\n\tAttempting to prune clause %d (%d initial errors)\n", NCl, Errs);

    /*  Allocate stuff for checking partial order restrictions  */

    ForEach(i, 0, Lits-1)
    {
	if ( C[i]->Rel == Target )
	{
	    C[i]->OrderedArg = (Boolean *) malloc(Target->Arity+1);
	}
    }

    CheckOrders = true;

    if ( JunkLiteral(C, Lits, Errs) )
    {
	RenameVariables(C, Target->Arity);

	VERBOSE(1)
	{
	    printf("\tRevised clause: ");
	    PrintClause(Target, C);
	    newline;
	}

	RecoverTrainingSet(C);
    }

    CheckOrders = false;
}



	/*  Omit the first unnecessary literal  */

	/*  This version prunes from the end of the clause; if a literal
	    can't be dropped when it is examined, it will always be
	    needed, since dropping earlier literals can only increase
	    the number of minus tuples getting through to this literal  */


Boolean JunkLiteral(C, Lits, ErrsNow)
/*      -----------  */
    Clause C;
    int Lits, ErrsNow;
{
    int i, j, k, V, Errs, Verb;
    Boolean Needed = true, Pruned = false, RecursiveLits, NegatedLits,
	CheckRHS(), EssentialBinding();
    Tuple *TSP;
    Literal Try[MAXLITS];

    /*  Check for the last literal, omitting which would not increase
	the number of errors.  */

    /*  Remember whether there are negated lits following the current literal  */

    NegatedLits = false;

    for ( i = Lits-1 ; i >= 0 ; i-- )
    {
	/*  Can't omit a literal that is needed to bind a variable appearing in
	    a later negated literal  */

	if ( NegatedLits && C[i]->Sign && EssentialBinding(i, C, Lits) ) continue;

	Needed = RecursiveLits = false;
	Errs = 0;

	k = 0;
	ForEach(j, 0, Lits-1)
	{
	    if ( j != i )
	    {
		Try[k++] = C[j];

		/*  Check for recursive literals and clear part order stuff  */

		if ( C[j]->Rel == Target )
		{
		    RecursiveLits = true;
		    memset(C[j]->OrderedArg, true, Target->Arity+1);
		    C[j]->OrderedArgs = Target->Arity;
		}
	    }
	}
	Try[k] = Nil;

	for ( TSP = CopyTrainingSet ; *TSP && ! Needed ; TSP++ )
	{
	    if ( ! Positive(*TSP) )  /* a minus tuple */
	    {
		InitialiseValues(*TSP, Target->Arity);
		if ( CheckRHS(Try) )
		{
		    if ( Needed = ++Errs > ErrsNow )
		    {
			VERBOSE(2)
			{
			    printf("\t\t");
			    PrintLiteral(C[i]->Rel, C[i]->Sign, C[i]->Args);
			    printf(" needed for ");
			    PrintTuple(*TSP, Target->Arity);
			    newline;
			}
		    }
		}

		if ( ! RecursiveLits ) continue;

		ForEach(j, i, Lits-2)
		{
		    if ( Try[j]->Rel == Target && ! Try[j]->OrderedArgs )
		    {
			Needed = true;

			VERBOSE(2)
			{
			    printf("\t\t");
			    PrintLiteral(C[i]->Rel, C[i]->Sign, C[i]->Args);
			    printf(" needed for partial order on ");
			    PrintLiteral(Try[j]->Rel, Try[j]->Sign, Try[j]->Args);
			    newline;
			}
		    }
		}
	    }
	}

	if ( Needed )
	{
	    NegatedLits |= ! C[i]->Sign;
	}
	else
	{
	    VERBOSE(1)
	    {
		printf("\t\t");
		PrintLiteral(C[i]->Rel, C[i]->Sign, C[i]->Args);
		printf(" removed\n");
	    }

	    Lits--;
	    ForEach(j, i, Lits)
	    {
		C[j] = C[j+1];
	    }

	    Pruned = true;
	}
    }

    return Pruned;
}



	/*  Can't omit a literal that is needed to bind a variable appearing in
	    a later negated literal  */

Boolean EssentialBinding(n, C, Lits)
/*      ----------------  */
    Clause C;
    int n, Lits;
{
    int i, j, TimesBound[MAXARITY+1], LastBound[MAXARITY+1], V;

    memset(TimesBound, 0, (MAXARITY+1) * sizeof(int));

    ForEach(i, 0, Lits-1)
    {
	if ( C[i]->Sign )
	{
	    ForEach(j, 1, C[i]->Rel->Arity)
	    {
		TimesBound[V = C[i]->Args[j]]++;
		LastBound[V] = i;
	    }
	}
	else
	if ( i > n )
	{
	    ForEach(j, 1, C[i]->Rel->Arity)
	    {
		if ( TimesBound[V = C[i]->Args[j]] == 1 && V > Target->Arity &&
		     LastBound[V] == n )
		{
		    VERBOSE(2)
		    {
			printf("\t\t");
			PrintLiteral(C[n]->Rel, C[n]->Sign, C[n]->Args);
			printf(" needed for binding on ");
			PrintLiteral(C[i]->Rel, C[i]->Sign, C[i]->Args);
			newline;
		    }
		    return true;
		}
	    }
	}
    }

    return false;
}



    RenameVariables(C, N)
/*  ---------------  */
    Clause C;
    int N;
{
    char i, Map[MAXARITY+1], Next, SaveNext, Lit;
    int V;
    Literal L;
    Relation R;

    memset(Map, 0, MAXARITY+1);
    Next = N + 1;

    for ( Lit = 0 ; (L = C[Lit]) ; Lit++ )
    {
	SaveNext = Next;

	R = L->Rel;
	ForEach(i, 1, R->Arity)
	{
	    V = L->Args[i];

	    if ( V > N )
	    {
		if ( ! Map[V] ) Map[V] = Next++;

		L->Args[i] = Map[V];
	    }
	}

	/*  Restore next variable after negative literal  */

	if ( ! L->Sign )
	{
	    Next = SaveNext;

	    ForEach(V, 1, MAXARITY)
	    if ( Map[V] >= Next ) Map[V] = 0;
	}
    }
}



	/*  See whether some clauses can be dispensed with  */

    SiftClauses()
/*  -----------  */
{
    int i, Covers, Last, Remaining, Retain = 0;
    Tuple *TSP;
    Boolean Need[MAXCLS+1], Delete[MAXCLS+1];

    memset(Delete, false, NCl);
    memset(Need, false, NCl);
    Remaining = NCl;

    while ( true )
    {
	for ( TSP = InitialTrainingSet ; *TSP && Retain < Remaining ; TSP++)
	{
	    if ( ! Positive(*TSP) ) continue;

	    Covers = 0;
	    for ( i = 0 ; i < NCl && Covers <= 1 ; i++ )
	    {
		if ( Delete[i] ) continue;

		InitialiseValues(*TSP, Target->Arity);

		if ( CheckRHS(Target->Def[i]) )
		{
		    Covers++;
		    Last = i;
		}
	    }

	    if ( Covers == 1 && ! Need[Last] )
	    {
		VERBOSE(2)
		{
		    printf("Clause %d needed for ", Last);
		    PrintTuple(*TSP, Target->Arity);
		    newline;
		}

		Need[Last] = true;
		Retain++;
	    }
	}

	Last = -1;
	ForEach(i, 0, NCl-1)
	{
	    if ( ! Need[i] && ! Delete[i] ) Last = i;
	}

	if ( Last >= 0 )
	{
	    Delete[Last] = true;
	    Remaining--;
	}
	else
	{
	    break;
	}
    }

    if ( Retain < NCl )
    {
	VERBOSE(1) printf("\nDelete clause%s\n", Plural(NCl - Retain));

	Retain = 0;

	ForEach(i, 0, NCl-1)
	{
	    if ( Delete[i] )
	    {
		VERBOSE(1)
		{
		    printf("\t");
		    PrintClause(Target, Target->Def[i]);
		}
	    }
	    else
	    {
		Target->Def[Retain++] = Target->Def[i];
	    }
	}
	Target->Def[Retain] = Nil;
    }
}