/******************************************************************************/
/*									      */
/*	All input routines						      */
/*									      */
/******************************************************************************/


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

#define  Space(s)	(s == ' ' || s == '\t')
#define  SkipComment	while ( ( c = getchar() ) != '\n' )
#define  EndLine	while ( getchar() != '\n' )


char    Name[200],
	SectionDelim;
Const   *SortedConst = Nil;
Boolean	ContinuousVars = false;


/******************************************************************************/
/*									      */
/*	Routines for reading types					      */
/*									      */
/******************************************************************************/



Boolean  ReadType()
/*       --------  */
{
    int		i;
    char	Delim;
    TypeInfo	T;
    Boolean	FirstTime=true, RecordTheoryConst;
    Const	C;

    Delim = ReadName(Name);

    if ( ! *Name ) return false;
    else
    if ( Delim != ':' ) Error(1, Name);

    T = AllocZero(1, struct _type_rec);

    T->NValues = T->NTheoryConsts = 0;
    T->Value   = T->TheoryConst   = Nil;

    if ( Name[0] == '*' )	/* order specified by user */
    {
        T->FixedPolarity = true;
	T->Ordered = true;
        T->Name = CopyString(Name+1);
    }
    else
    if ( Name[0] == '#' )	/* specified to be unordered */
    {
        T->FixedPolarity = true;
        T->Ordered = false;
        T->Name = CopyString(Name+1);
    }
    else
    {
        T->FixedPolarity = false;
	T->Name = CopyString(Name);
    }

    /*  Read first name  */

    while ( (Delim = ReadName(Name)) == '\n' )
	;

    if ( ! Name ) Error(1, Name);

    /*  Check for continuous type  */

    if ( ! strcmp(Name, "continuous") )
    {
        T->Continuous = true;
	T->FixedPolarity = true;
	T->Ordered = false; /* Never match on continuous value - hence
			       no point in checking for orders on it */
	ContinuousVars = true;

	/* Check overlaying of Const and float */

	if ( sizeof(Const) != sizeof(float) )
	{
	    printf("\nThis version cannot be used with continuous types\n");
	    printf("Integers and floating point numbers are different sizes\n");
	    printf("Alter declaration of type Const (defns.i) and recompile\n");
	    exit(1);
	}
    }
    else
    {
	/*  Discrete type, read the values  */

        T->Continuous = false;

	do
	{
	    while ( ( FirstTime ? ! (FirstTime = false) :
				    (Delim = ReadName(Name)) ) &&
		    Delim == '\n' )
			;

	    if ( Name[0] == '*' )
	    {
		/*  Theory constant  */

		RecordTheoryConst = true;

		for ( i = 0 ; Name[i++] ; )
		{
		    Name[i-1] = Name[i];
		}
	    }
	    else
	    {
		RecordTheoryConst = false;
	    }
		
	    if ( T->NValues % 100 == 0 )
	    {
		Realloc(T->Value, T->NValues+100, Const);
	    }

	    C = T->Value[ T->NValues++ ] = FindConstant(Name, false);

	    if ( RecordTheoryConst )
	    {
		if ( T->NTheoryConsts % 10 == 0 )
		{
		    Realloc(T->TheoryConst, T->NTheoryConsts+10, Const);
		}

		T->TheoryConst[ T->NTheoryConsts++ ] = C;
	    }
	}
	while ( Delim == ',' );
    }

    if ( Delim != '.' ) Error(2, Name, T->Name);
    EndLine;

    /* Enter Type */

    MaxType++;

    if ( MaxType % 100 == 1 )
    {
        Realloc(Type, MaxType + 100, TypeInfo);
    }

    Type[MaxType] = T;

    return true;
}



void  ReadTypes()
/*    ---------  */
{
    int		i, j;
    TypeInfo	T;

    /*  Record missing value name  */

    FindConstant("?", false);

    /*  Read all type definitions  */

    while ( ReadType() )
	;

    /*  Generate collating sequences  */

    ForEach(i, 1, MaxType)
    {
	T = Type[i];

	if ( T->Continuous ) continue; /* Skip continuous type */

	T->CollSeq = Alloc(MaxConst+1, int);

	ForEach(j, 0, MaxConst)
	{
	    T->CollSeq[j] = 0;
	}

	ForEach(j, 0, T->NValues-1)
	{
	    T->CollSeq[T->Value[j]] = j+1;
	}

	T->CollSeq[MISSING_DISC] = T->NValues+1;
    }
}



/******************************************************************************/
/*									      */
/*	Routines for reading tuples and relations			      */
/*									      */
/******************************************************************************/



Tuple  ReadTuple(Relation R)
/*     ---------  */
{
    char	Delim;
    int		N, i;
    Tuple	T;

    N = R->Arity;

    if ( (Delim = ReadName(Name)) == '.' || Delim == ';' ) return Nil;

    T = Alloc(N+1, Const);

    ForEach(i, 1, N)
    {
	if ( i > 1 )
	{
	    Delim = ReadName(Name);
	}

	if ( R->TypeRef[i]->Continuous )
	{
	    if ( ! strcmp(Name,"?") )
	    {
	        FP(T[i]) = MISSING_FP;
		MissingVals = true;
	    }
	    else
	    {
	        FP(T[i]) = atof(Name);

		if ( FP(T[i]) == MISSING_FP )
		{
		    printf("An input continuous values is equal to the\n");
		    printf("magic number used to designate missing values.\n");
		    printf("Change the definition of MISSING_FP in defns.i\n");
		    printf("and recompile.\n");
		    exit(1);
	        }
	    }
	}
	else
	{
	    if ( ! strcmp(Name,"?") )
	    {
	        T[i] = MISSING_DISC;
		MissingVals = true;
	    }
	    else
	    {
		T[i] = FindConstant(Name, true);
	    }
	}
    }

    if ( Delim != ':' && Delim != '\n' ) ReadToEOLN;

    ForEach(i, 1, N)
    {
	if ( ! R->TypeRef[i]->Continuous && ! R->TypeRef[i]->CollSeq[T[i]] ) 
	{
            Error(4, ConstName[T[i]], Type[R->Type[i]]->Name);
	}
    }

    return T;
}



Tuple  *ReadTuples(Relation R, Boolean Pos)
/*      ----------  */
{
    Tuple	T, *TheTuples=Nil;
    int		ND=0;

    while ( T = ReadTuple(R) )
    {
	T[0] = Pos ? PosMark : 0;

        if ( ND % 100 == 0 ) 
	{
	    Realloc(TheTuples, ND+101, Tuple);
	}
	TheTuples[ND++] = T;
    }

    TheTuples[ND] = Nil;

    return TheTuples;
}



Relation  ReadRelation()
/*        ------------  */
{
    Relation	R;
    char	Delim, c;
    int		NArgs=0, Key[100], NKeys=0, i, t;

    if ( ReadName(Name) != '(' ) return Nil;

    printf("\nRelation %s\n", Name);

    /*  Create a new record with all zero counts  */

    R = AllocZero(1, struct _rel_rec);

    if ( Name[0] == '*' )
    {
	/*  Background relation  */

        R->PossibleTarget = false;
        R->Name = CopyString(Name+1);
    }
    else
    {
        R->PossibleTarget = true;
	R->Name = CopyString(Name);
    }

    do
    {
	NArgs++;

        Realloc(R->Type, NArgs+1, int);
        Realloc(R->TypeRef, NArgs+1, TypeInfo); 
	Delim = ReadName(Name);
        t = FindType(Name);
	R->Type[NArgs] = t; 
        R->TypeRef[NArgs] = Type[t]; 
    }
    while ( Delim != ')' );

    R->Arity = NArgs;
    if ( NArgs > MAXARGS ) MAXARGS = NArgs;
    if ( R->PossibleTarget && NArgs > MAXVARS ) MAXVARS = NArgs;

    /*  Read and store access keys  */
    do
    {
	do
	{
	    c = getchar();
	}
	while ( Space(c) ) ;

	if ( c != '\n' )
	{
	    Key[NKeys] = 0;

	    ForEach(i, 1, NArgs)
	    {
		if ( c == '-' ) Key[NKeys] |= (1 << i);
		c = getchar();
	    }
	    NKeys++;
	}
    }
    while ( c == '/');

    R->NKeys = NKeys;
    if ( NKeys )
    {
	R->Key   = Alloc(NKeys, int);
	memcpy(R->Key, Key, NKeys * sizeof(int));
    }

    R->Pos      = ReadTuples(R, true);
    R->PosIndex = MakeIndex(R->Pos, NArgs, R);

    if ( SectionDelim == '.' )
    {
	R->Neg = Nil;
    }
    else
    {
	R->Neg      = ReadTuples(R, false);

	/*  The index of negative tuples isn't currently used, but may be
	    useful if you are adapting the system  */

	/*  R->NegIndex = MakeIndex(R->Neg, NArgs, R);  */
    }

    R->BinSym = SymmetryCheck(R);

    DuplicateTuplesCheck(R);

    return R;
}



void  ReadRelations()
/*    -------------   */
{
    int		i, Search, Next, Best;
    Relation	R;
    Tuple	*T;
    Boolean	*Waiting;

    while ( R = ReadRelation() )
    {
	/*  Make sure room for one more  */

        if ( ++MaxRel % 10 == 0 ) 
        {
            Realloc(Reln, MaxRel+10, Relation);
        }

	Reln[MaxRel] = R;

	Verbose(4)
	{
	    if ( Reln[MaxRel]->BinSym )
	    {
		printf("    is binary symmetric\n");
	    }

	    for ( T = Reln[MaxRel]->Pos ; *T ; T++ )
	    {
		PrintTuple(*T, Reln[MaxRel]->Arity,
			   Reln[MaxRel]->TypeRef, Reln[MaxRel]->Neg != Nil);
	    }
		
	    if ( Reln[MaxRel]->Neg )
	    {
		for ( T = Reln[MaxRel]->Neg ; *T ; T++ )
		{
		    PrintTuple(*T, Reln[MaxRel]->Arity,
			       Reln[MaxRel]->TypeRef, true);
		}
	    }
	}
    }

    /*  Now put the relations into the order in which they should be tried.
	The idea is to put lower arity relations earlier to maximise the
	effect of pruning  */

    Waiting = Alloc(MaxRel+1, Boolean);
    RelnOrder = Alloc(MaxRel+1, Relation);

    memset(Waiting, true, MaxRel+1);

    Search = MaxRel;

    if ( ! ContinuousVars )
    {
	Waiting[2] = Waiting[3] = false;
	MaxRel -= 2;
    }

    ForEach(Next, 0, MaxRel)
    {
	Best = -1;

	ForEach(i, 0, Search)
	{
	    if ( Waiting[i] &&
		 ( Best < 0 ||
		   Reln[i]->Arity < Reln[Best]->Arity ||
		   Reln[i]->Arity == Reln[Best]->Arity
		   && Best > 3
		   && Number(Reln[i]->Pos) > Number(Reln[Best]->Pos) ) )
	    {
		Best = i;
	    }
	}

	RelnOrder[Next] = Reln[Best];
	Waiting[Best] = false;
    }

    pfree(Waiting);
}


	/*  Find a type by name  */

int  FindType(char *N)
/*   --------  */
{
    int i;

    ForEach(i, 1, MaxType)
    {
	if ( ! strcmp(N, Type[i]->Name) ) return i;
    }

    Error(5, N);
    return 0; /* keep lint happy */
}



/******************************************************************************/
/*                                                                            */
/*	DuplicateTuplesCheck(R) - check for duplicate tuples in R             */
/*                                                                            */
/******************************************************************************/


void  DuplicateTuplesCheck(Relation R)
/*    --------------------  */
{
    int		i, j, k, N, NPos, NNeg;
    Tuple	*PosCopy, *NegCopy, PosTuple, NegTuple;
    Boolean	MutualDuplicate;

    /* First copy the positive tuples and check number of duplicates */

    NPos = Number(R->Pos);

    PosCopy = Alloc(NPos+1, Tuple);
    ForEach(i, 0, NPos)
    {
	PosCopy[i] = (R->Pos)[i];
    }

    N = R->Arity;

    if ( R->PosDuplicates = CountDuplicates(PosCopy,N,0,NPos-1) )
    {
	printf("    (warning: contains duplicate positive tuples)\n");
    }

    /* If there are neg tuples, check for duplicates and mutual duplicates */

    if ( R->Neg )
    {
        NNeg = Number(R->Neg);
        NegCopy = Alloc(NNeg+1, Tuple);
	ForEach(i, 0, NNeg)
	{
	    NegCopy[i] = (R->Neg)[i];
	}

	if ( CountDuplicates(NegCopy,N,0,NNeg-1) )
        {
	    printf("    (warning: contains duplicate negative tuples)\n");
	}


	/* Existence check for mutual duplicates */

	MutualDuplicate = false;
	i = j = 0;

	while( i < NPos && j < NNeg )
	{
	    PosTuple = PosCopy[i];
	    NegTuple = NegCopy[j];

	    for ( k = 1 ; k <= N && PosTuple[k] == NegTuple[k] ; k++ )
		;

	    if ( k > N ) /* tuples are duplicates */
	    {
	        MutualDuplicate = true;
		break;
	    }
	    else
	    if ( PosTuple[k] < NegTuple[k] )
	    {
		i++;
	    }
	    else
	    {
		j++;
	    }
	}

	if ( MutualDuplicate ) 
	{
	    printf("    (warning: contains tuples that are both ");
	    printf("positive and negative)\n");
	}

	pfree(NegCopy);
    }

    pfree(PosCopy);
}



/******************************************************************************/
/*                                                                            */
/*	CountDuplicates(T,N,left,right) - count the number of duplicate	      */
/*	    tuples in T between left and right.       			      */
/*		Sorts tuples on order given by comparison of Const type.      */
/*		N.B. This comparison is used even for continuous values as    */
/*		only checking for duplicates. 				      */
/*                                                                            */
/******************************************************************************/


int  CountDuplicates(Tuple *T, int N, int Left, int Right)
/*   ---------------  */
{
    register int	i, j, last, first, swap, count=0;
    register Tuple	temp, comp, other;

    if ( Left >= Right ) return 0;

    temp = T[Left];
    T[Left] = T[swap=(Left+Right)/2];
    T[swap] = temp;

    last = Left;

    comp = T[Left];

    for ( i = Left + 1; i <= Right; i++ )
    {
        other = T[i];
	for( j = 1 ; j <= N && other[j] == comp[j] ; j++ )
	    ;

        if ( j > N || other[j] < comp[j] ) /* other <= comp */
	{
	    temp = T[++last];
	    T[last] = T[i];
	    T[i] = temp;
	}
    }

    temp = T[Left];
    T[Left] = T[last];
    T[last] = temp;

    first = last;

    for ( i = last - 1; i >= Left ; i-- )
    {
        other = T[i];
	for ( j = 1 ; j <= N && other[j] == comp[j] ; j++ )
	    ;

	if ( j > N ) /* other == comp */
	{
	    temp = T[--first];
	    T[first] = T[i];
	    T[i] = temp;
	    count++;
	}
    }

    count += CountDuplicates(T,N,Left,first-1);
    count += CountDuplicates(T,N,last+1,Right);

    return count;
}



Boolean  SymmetryCheck(Relation R)
/*       -------------    */
{
    Tuple	*TheTuples;
    Boolean	*SymCheck;
    int		i, j, NPos;
    Const	T1, T2;

    if ( R->Arity != 2 ||
	 R->TypeRef[1]->Continuous || R->TypeRef[2]->Continuous )
    {
        return false;
    }

    TheTuples = R->Pos;
    NPos = Number(TheTuples);

    SymCheck = Alloc(NPos, Boolean);
    memset(SymCheck, false, NPos*sizeof(Boolean));

    ForEach(i, 0, NPos-1)
    {
        if ( SymCheck[i] ) continue; 

        T1 = TheTuples[i][1];
        T2 = TheTuples[i][2];
        for ( j = i ;
	      j < NPos && ( T1 != TheTuples[j][2] || T2 != TheTuples[j][1] ) ;
	      j++ )
	    ;

        if ( j == NPos )
	{
	    pfree(SymCheck);
	    return false;
        }
        SymCheck[j] = true;
    }

    pfree(SymCheck);
    return true;
}


	/*  Construct the index for a set of tuples for relation R  */

Index  MakeIndex(Tuple *T, int N, Relation R)
/*     ---------  */
{
    Index	IX;
    Tuple	Case, *Scan;
    int		**Next, Arg, Val, No = 0;

    /*  Allocate storage  */

    IX = Alloc(N+1, int **);
    Next = Alloc(N+1, int *);

    ForEach(Arg, 1, N)
    {
	IX[Arg] = Alloc(MaxConst+1, int *);
	Next[Arg] = AllocZero(MaxConst+1, int);
    }

    for ( Scan = T ; Case = *Scan++ ; )
    {
	ForEach(Arg, 1, N)
	{
	    if ( ! R->TypeRef[Arg]->Continuous )
	        Next[Arg][Case[Arg]]++;
	}
    }

    ForEach(Arg, 1, N)
    {
	ForEach(Val, 1, MaxConst)
	{
	    IX[Arg][Val] = Next[Arg][Val] ? Alloc(Next[Arg][Val]+1, int) : Nil;
	    Next[Arg][Val] = 0;
	}
    }

    /*  Construct the index  */

    for ( Scan = T ; *Scan ; Scan++ )
    {
	ForEach(Arg, 1, N)
	{
	    if ( ! R->TypeRef[Arg]->Continuous )
	    {
	        Val = (*Scan)[Arg];
		IX[Arg][Val][Next[Arg][Val]++] = No;
	    }
	}

	No++;
    }

    /*  Terminate index and free Next  */

    ForEach(Arg, 1, N)
    {
	ForEach(Val, 1, MaxConst)
	{
	    if ( IX[Arg][Val] )
	    {
		IX[Arg][Val][Next[Arg][Val]] = FINISH;
	    }
	}
	pfree(Next[Arg]);
    }
    pfree(Next);

    return IX;
}



/******************************************************************************/
/*									      */
/*	Basic routine -- read a delimited name into string s		      */
/*									      */
/*	  - Embedded spaces are permitted, but multiple spaces are replaced   */
/*	    by a single space						      */
/*	  - Any character escaped by \ is ok				      */
/*	  - Characters after | are ignored				      */
/*									      */
/******************************************************************************/



char  ReadName(char *s)
/*    ---------  */
{
    register char	*Sp = s;
    register int	c;

    /*  Skip to first non-space character  */

    while ( ( c = getchar() ) == '|' || Space(c) )
    {
	if ( c == '|' ) SkipComment;
    }

    /*  Return period if no names to read  */

    if ( c == EOF )
    {
	return (SectionDelim = '.');
    }
    else
    if ( c == ';' || c == '.' )
    {
	getchar();
	return (SectionDelim = c);
    }

    /*  Read in characters up to the next delimiter  */

    while ( c != ',' && c != '\n' && c != '|' && c != EOF &&
	    c != '(' && c != ')'  && c != ':' && c != '.' )
    {
	if ( c == '\\' ) c = getchar();

	*Sp++ = c;
	if ( c == ' ' )
	    while ( ( c = getchar() ) == ' ' );
	else
	    c = getchar();

	if ( c == '.' ) /* Check for embedded period in number */
	{
	    c = getchar();
	    if (isdigit(c))
	    {
	        *Sp++ = '.';
	    }
	    else
	    {
	        ungetchar(c);
		c = '.';
	    }
	}
    }

    if ( c == '|' )
    {
	SkipComment;
	c = '\n';
    }

    /*  Strip trailing spaces  */

    while ( Space(*(Sp-1)) ) Sp--;
    *Sp++ = '\0';

    return c;
}



	/*  Find a constant using binary chop search  */


Const  FindConstant(char *N, Boolean MustBeThere)
/*     ------------  */
{
    int	i, Hi=MaxConst+1, Lo=1, Differ=1;

    while ( Lo < Hi-1 )
    {
	Differ = strcmp(N, ConstName[SortedConst[i = (Hi + Lo)/2]]);

	if ( ! Differ )		return SortedConst[i];
	else
	if ( Differ > 0 )	Lo = i;
	else			Hi = i;
    }

    if ( MustBeThere ) Error(3, N);

    /*  This is a new constant -- record it  */

    MaxConst++;
    if ( MaxConst % 1000 == 1 )
    {
	Realloc(ConstName, MaxConst+1000, char *);
	Realloc(SortedConst, MaxConst+1000, int);
    }

    Lo++;
    for ( i = MaxConst ; i > Lo ; i-- )
    {
	SortedConst[i] = SortedConst[i-1];
    }
    SortedConst[Lo] = MaxConst;
    ConstName[MaxConst] = CopyString(N);

    return MaxConst;
}



	/*  Check whether different types are compatible, i.e.
	    share at least one common value  */

void  CheckTypeCompatibility()
/*    ----------------------  */
{
    int T1, T2;

    Compatible = Alloc(MaxType+1, Boolean *);
    ForEach(T1, 1, MaxType)
    {
	Compatible[T1] = Alloc(MaxType+1, Boolean);
    }

    Verbose(2) putchar('\n');

    ForEach(T1, 1, MaxType)
    {
	Compatible[T1][T1] = true;

	ForEach(T2, T1+1, MaxType)
	{
	    Compatible[T1][T2] = Compatible[T2][T1] =
	        ( Type[T1]->Continuous || Type[T2]->Continuous ) ?
		false:
		CommonValue(Type[T1]->NValues, Type[T1]->Value,
		            Type[T2]->NValues, Type[T2]->Value);

	    Verbose(2)
	    {
		printf("Types %s and %s %s compatible\n",
			Type[T1]->Name, Type[T2]->Name,
			Compatible[T1][T2] ? "are" : "are not");
	    }
	}
    }
}


Boolean  CommonValue(int N1, Const *V1, int N2, Const *V2)
/*       -----------  */
{
    int i, j;

    ForEach(i, 0, N1-1)
    {
        ForEach(j, 0, N2-1)
	{
	    if ( V1[i] == V2[j] ) return true;
	}
    }

    return false;
}



int  Number(Tuple *T)
/*   ------  */
{
    int Count=0;

    if ( ! T ) return 0;

    while ( *T++ )
    {
	Count++;
    }

    return Count;
}



char  *CopyString(char *s)
/*     ----------  */
{
    char *new;
    int l;

    l = strlen(s) + 1;
    new = Alloc(l, char);
    memcpy(new, s, l);

    return new;
}



void  Error(int n, char *s1, char *s2)
/*    -----  */
{
    switch ( n )
    {
        case 1:	printf("Illegal delimiter after %s\n", s1);
		exit(1);

	case 2:	printf("Something wrong after %s in type %s\n", s1, s2);
		exit(1);

	case 3: printf("Undeclared constant %s\n", s1);
		exit(1);

	case 4: printf("Constant %s is not of type %s\n", s1, s2);
		exit(1);

	case 5: printf("Undeclared type %s\n", s1);
		exit(1);
    }
}