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


Boolean ProposeDeterminateLiteral(R, A, LitBits, FreeVars)
/*      -------------------------  */
    Relation R;
    Vars A;
    float LitBits;
    int FreeVars;
{
    int MaxSoFar, PreviousMax, This, i, j;
    Var V;
    Literal L;
    static int Variables;
    Boolean SensibleBinding = false;

    if ( ! NDeterminate ) Variables = MaxVar;

    if ( (This = NLit + NDeterminate) >= MAXLITS ||
	 Variables + FreeVars >= MAXARITY ) return false;

    /*  See whether have something effectively the same, or whether this
	determinate literal's bound variables were all bound by determinate
	literals on the same relation  */

    ForEach(j, 1, R->Arity)
    {
	SensibleBinding |= ( A[j] <= Target->Arity );
    }

    MaxSoFar = Target->Arity;
    ForEach(i, 0, NLit+NDeterminate-1)
    {
	if ( ! NewClause[i]->Sign ) continue;

	if ( NewClause[i]->Rel == R &&
	     Unifiable(R->Arity, NewClause[i]->Args, MaxVar, A, MaxVar) )
	{
            VERBOSE(2)
	    {
		printf("\tunifiable with ");
		PrintLiteral(R, true, NewClause[i]->Args);
		printf("\n");
	    }
	    return false;
	}

	if ( i >= NLit ) continue;

	PreviousMax = MaxSoFar;
	ForEach(j, 1, NewClause[i]->Rel->Arity)
	{
	    if ( (V = NewClause[i]->Args[j]) > MaxSoFar ) MaxSoFar = V;
	}

	if ( NewClause[i]->Rel != R || NewClause[i]->Sign != 2 )
	{
	    ForEach(j, 1, R->Arity)
	    {
		SensibleBinding |= ( A[j] <= MaxSoFar && A[j] > PreviousMax );
	    }
	}
    }

    if ( ! SensibleBinding )
    {
	VERBOSE(2)
	{
	    printf("\tall variables bound by determinate lits on same relation\n");
	}
	return false;
    }

    /*  Record this determinate literal  */

    L = NewClause[This] = (Literal) malloc(sizeof(struct _lit_rec));

    L->Rel  = R;
    L->Sign = 2;
    L->Bits = LitBits;
    L->Args = (Vars) malloc(R->Arity+1);
    memcpy(L->Args, A, R->Arity+1);

    NDeterminate++;
    Variables += FreeVars;

    return true;
}



	/*  See whether two arg lists can be unified.  "Free"
	    variables in A1 are those with values above Bound1;
	    similarly for A2  */

Boolean Unifiable(N, A1, Bound1, A2, Bound2)
/*      ---------  */
    int N, Bound1, Bound2;
    Vars A1, A2;
{
    int X1[MAXARITY+1], X2[MAXARITY+1], i, V, T;

    /*  Make all free variables > 1000  */

    ForEach(i, 1, N)
    {
	/*X1[i] = (A1[i] > Bound1 ? 1000 + A1[i]-Bound1 : A1[i]);*/
	X1[i] = A1[i];
	X2[i] = (A2[i] > Bound2 ? 2000 + A2[i]-Bound2 : A2[i]);
    }

    ForEach(i, 1, N)
    {
	if ( X1[i] == X2[i] ) continue;

	if ( X1[i] > 1000 )
	{
	    V = X1[i];
	    T = X2[i];
	}
	else
	if ( X2[i] > 1000 )
	{
	    V = X2[i];
	    T = X1[i];
	}
	else return false;

	Substitute(V, T, X1, i, N);
	Substitute(V, T, X2, i, N);
    }

    return true;
}


    Substitute(V, T, X, i, N)
/*  ----------  */
    int V, T, X[], i, N;
{
    for ( ; i <= N ; i++ )
    {
	if ( X[i] == V ) X[i] = T;
    }
}


	/*  External variables from FormNewTrainingSet  */

extern Tuple	*NewTS;
extern int	NewMaxVar;


    ProcessDeterminateLiterals()
/*  --------------------------  */
{
    int SaveWeakLiterals, SaveMaxVar, OldMaxVar, i, j, l, ll, PossibleDuplicates;
    Literal L;
    Var V, LHSV;
    Boolean Unique, SameVar();

    SaveWeakLiterals = WeakLiterals;
    OldMaxVar = MaxVar;

    VERBOSE(1) printf("\nDeterminate literals\n");

    ForEach(l, 1, NDeterminate)
    {
	L = NewClause[NLit++];

	/*  Rename free variables  */

	ForEach(i, 1, L->Rel->Arity)
	{
	    if ( L->Args[i] > OldMaxVar ) L->Args[i] += MaxVar - OldMaxVar;
	}

	SaveMaxVar = MaxVar;
	NewSize = 0;
	FormNewTrainingSet(L->Rel, true, L->Args);
	MaxVar = NewMaxVar;

	/*  Verify that new variables don't replicate existing variables  */

	for ( i = SaveMaxVar+1 ; i <= MaxVar ; )
	{
	    Unique = true;

	    for ( j = 1 ; Unique && j <= SaveMaxVar ; j++ )
	    {
		Unique = ! SameVar(i, j);
	    }

	    if ( Unique )
	    {
		i++;
	    }
	    else
	    {
		j--;

		VERBOSE(1)
		{
		    printf("\t\t\t!!! %c = %c\n", Variable[i], Variable[j]);
		}

		ShiftVarsDown(i);

		/*ForEach(V, i, MaxVar)
		{
		    ForEach(LHSV, 1, Target->Arity)
		    {
			PartialOrder[V][LHSV] = PartialOrder[V+1][LHSV];
		    }
		}*/

		ForEach(V, 1, L->Rel->Arity)
		{
		    if ( L->Args[V] == i ) L->Args[V] = j;
		    else
		    if ( L->Args[V] >  i ) L->Args[V]--;
		}
	    }
	}

	VERBOSE(1)
	{
	    putchar('\t');
	    PrintLiteral(L->Rel, L->Sign, L->Args);
	    printf(" (%.1f bits)", L->Bits);
	}

	/*  If no variables remain, delete this literal  */

	if ( SaveMaxVar == MaxVar )
	{
	    VERBOSE(1) printf(" -- no remaining variables\n");
	
	    NLit--;

	    ForEach(ll, 1, NDeterminate-l)
	    {
		NewClause[NLit+ll-1] = NewClause[NLit+ll];
	    }

	    Discard(NewTS, true);
	}
	else
	{
	    VERBOSE(1) newline;

	    AcceptNewTrainingSet();
	}
    }

    WeakLiterals = SaveWeakLiterals + 1;
}



Boolean SameVar(a, b)
/*      -------  */
    Var a, b;
{
    Tuple *TSP, Case;

    for ( TSP = NewTS ; Case = *TSP++; )
    {
	if ( Case[a] != Case[b] ) return false;
    }

    return true;
}



    ShiftVarsDown(s)
/*  -------------  */
    int s;
{
    Tuple *TSP, Case;
    Var V;

    MaxVar--;

    for ( TSP = NewTS ; Case = *TSP++ ; )
    {
	ForEach(V, s, MaxVar)
	{
	    Case[V] = Case[V+1];
	}
    }
}