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

Boolean CheckOrders = false;	/* flag set by prune */


Boolean CheckRHS(C)
/*      --------  */
    Clause C;
{
    int CopyValue[MAXARITY+1];
    Tuple Case, *Try, *Scan;
    Literal L;
    Relation R;
    int i, N, V;
    Boolean Result;

    if ( ! (L = C[0]) )
    {
	return true;
    }

    R = L->Rel;
    N = R->Arity;

    if ( CheckOrders && R == Target )
    {
	ForEach(i, 1, N)
	{
	    if ( L->OrderedArg[i] &&
	         ( ! Value[V = L->Args[i]] ||
		   Type[Target->Type[i]]->CollSeq[Value[V]] >=
		   Type[Target->Type[i]]->CollSeq[Value[i]] ) )
	    {
		L->OrderedArg[i] = false;
		if ( ! --L->OrderedArgs ) return false;
	    }
	}
    }

    if ( ! L->Sign )
    {
	return ! Join(R->Pos, R->PosIndex, L->Args, Value, N, true) && CheckRHS(C+1);
    }
    else
    {
	if ( ! Join(R->Pos, R->PosIndex, L->Args, Value, N, false) ) return false;

	memcpy(CopyValue, Value, (MAXARITY+1) * sizeof(int));

	Try = (Tuple *) malloc((NFound+1) * sizeof(Tuple));
	memcpy(Try, Found, (NFound+1) * sizeof(Tuple));

	Scan = Try;
	while ( Case = *Scan++ )
	{
	    ForEach(i, 1, N)
	    {
		V = L->Args[i];
		if ( ! Value[V] )
		{
		    Value[V] = Case[i];
		}
	    }

	    if ( CheckRHS(C+1) )
	    {
		free(Try);
		return true;
	    }

	    memcpy(Value, CopyValue, (MAXARITY+1) * sizeof(int));
	}

	free(Try);
	return false;
    }
}



    InitialiseValues(Case, N)
/*  ----------------  */
    Tuple Case;
    int N;
{
    int i;

    MaxVar = MAXARITY;

    ForEach(i, 1, N)
    {
	Value[i] = Case[i];
    }
    ForEach(i, N+1, MAXARITY)
    {
	Value[i] = 0;
    }
}



Boolean Interpret(R, Case)
/*      ---------  */
    Relation R;
    Tuple Case;
{
    int i;

    InitialiseValues(Case, R->Arity);

    for ( i = 0 ; R->Def[i] ; i++ )
    {
	if ( CheckRHS(R->Def[i]) ) return true;
    }

    return false;
}