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

extern int FoundSize;


    main(Argc, Argv)
/*  ----  */
    int Argc;
    char *Argv[];
{
    int o;
    extern char *optarg;
    extern int optind;

    Boolean ShowPosNeg, FirstTime = true;
    int i, a, MaxInitTrainSet = 0, InitTrainSet, Cases, Errors, *Case;
    Relation TestRel, ReadRelation();
    Index MakeIndex();
    char PlusOrMinus, Line[200];
    long clock();

    /*  Process options  */

    printf("FOIL.2\n------\n");

    while ( (o = getopt(Argc, Argv, "a:f:l:t:v:d:g:n")) != EOF )
    {
	if ( FirstTime )
	{
	    printf("\n    Options:\n");
	    FirstTime = false;
	}

	switch (o)
	{
	    case 'a':	MINACCURACY = atof(optarg);
			printf("\tminimum clause accuracy %g%%\n", MINACCURACY);
			MINACCURACY /= 100;
			break;
	    case 'f':	MINALTFRAC = atof(optarg);
			printf("\tbacked-up literals have %g%% of best gain\n", MINALTFRAC);
			MINALTFRAC /= 100;
			break;
	    case 'l':	MAXPOSSLIT = atoi(optarg);
			printf("\tmaximum %d backups from one literal\n", MAXPOSSLIT);
			break;
	    case 't':	MAXALTS = atoi(optarg);
			printf("\tmaximum %d total backups\n", MAXALTS);
			break;
	    case 'v':	Verbosity = atoi(optarg);
			printf("\tverbosity level %d\n", Verbosity);
			break;
	    case 'd':	MAXVARDEPTH = atoi(optarg);
			printf("\tmaximum variable depth %d\n", MAXVARDEPTH);
			break;
	    case 'g':	i = atoi(optarg);
			printf("\tuse determinate literals when gain <= %d%% possible\n", i);
			DETERMINATE = i / 100.0;
			break;
	    case 'n':	NEGLITERALS = false;
			printf("\tno negative literals\n");
			break;
	    case '?':	printf("unrecognised option\n");
			exit(1);
	}
    }

    clock();

    Found = (Tuples) malloc((FoundSize+1) * sizeof(Tuple));

    ToBeTried = (Alternative *) malloc((MAXALTS+1) * sizeof(Alternative));
    ForEach(i, 1, MAXALTS)
    {
	ToBeTried[i] = (Alternative) malloc(sizeof(struct _backup_rec));
	ToBeTried[i]->UpToHere = Nil;
    }

    Possible = (PossibleLiteral *) malloc((MAXPOSSLIT+1) * sizeof(PossibleLiteral));
    ForEach(i, 1, MAXPOSSLIT)
    {
	Possible[i] = (PossibleLiteral) malloc(sizeof(struct _poss_lit_rec));
	Possible[i]->Args = (Vars) malloc(MAXARITY+1);
    }

    /*  Nominal allocations  */

    ConstName = (char **) malloc(sizeof(char *));
    SortedConst= (Const *) malloc(sizeof(Const));

    ReadTypes();

    i = 1;
    while ( Reln[i] = ReadRelation() )
    {
	printf("\nRelation %s\n", Reln[i]->Name);
	ShowPosNeg = Reln[i]->Neg != Nil;
	PrintTuples(Reln[i]->Arity, Reln[i]->Pos, ShowPosNeg);
	if ( ShowPosNeg )
	{
	    PrintTuples(Reln[i]->Arity, Reln[i]->Neg, ShowPosNeg);
	}
	i++;
    }
    MaxRel = i - 1;

    /*  Set up equality relation in Reln[0]  */

    SAMEVAR = (Relation) malloc(sizeof(struct _rel_rec));

    SAMEVAR->Name = "=";
    SAMEVAR->Arity = 2;
    SAMEVAR->Neg = Nil;
    SAMEVAR->Pos = (Tuple *) malloc((MaxConst+1) * sizeof(Tuple));
    ForEach(i, 0, MaxConst - 1)
    {
	SAMEVAR->Pos[i] = (Tuple) malloc(3 * sizeof(int));
	SAMEVAR->Pos[i][1] = SAMEVAR->Pos[i][2] = i + 1;
    }
    SAMEVAR->Pos[MaxConst] = Nil;
    /*SAMEVAR->PosPartialOrders[0] = SAMEVAR->NegPartialOrders[0] = 0;*/

    /*  Determine order to try relations  */

    FindRelationOrder();

    /*  Make indices and optional tuples, if necessary  */

    ForEach(i, 0, MaxRel)
    {
	Reln[i]->PosIndex = MakeIndex(Reln[i]->Pos, Reln[i]->Arity);

	if ( Reln[i]->Neg )
	{
	    InitTrainSet = Number(Reln[i]->Pos) + Number(Reln[i]->Neg);
	    Reln[i]->NegIndex = MakeIndex(Reln[i]->Neg, Reln[i]->Arity);

	    if ( USEOPT )
	    {
		ConstructOptionalTuples(Reln[i]);
		Reln[i]->OptIndex = MakeIndex(Reln[i]->Opt, Reln[i]->Arity);
	    }
	}
	else
	{
	    InitTrainSet = 1;
	    ForEach(a, 1, Reln[i]->Arity)
	    {
		InitTrainSet *= MaxConst;
	    }
	}

	if ( Reln[i]->Name[0] != '*' )
	{
	    MaxInitTrainSet = Max(InitTrainSet, MaxInitTrainSet);
	}

    }

    /*  Determine type compatibilities  */

    Compatible = (Boolean **) malloc((MaxType+1) * sizeof(Boolean *));
    ForEach(i, 1, MaxType)
    {
	Compatible[i] = (Boolean *) malloc(MaxType+1);
    }

    CheckTypeCompatibility();

    /*  Check for partial orders in the relations  */

    /*VERBOSE(1) printf("\nChecking partial orders...\n");*/

    Bits = malloc(1);
    /*ForEach(i, 1, MaxRel)
    {
	FindPartialOrders(Reln[i]);
    }*/

    LogFact = (float *) malloc((MaxInitTrainSet+2) * sizeof(float));
    LogFact[0] = LogFact[1] = 0;
    ForEach(i, 2, MaxInitTrainSet+1)
    {
	LogFact[i] = LogFact[i-1] + Log2(i);
    }

    ForEach(i, 1, MaxRel)
    {
	if ( Reln[i]->Name[0] != '*' )
	{
	    FindDefinition(Reln[i]);
	}
    }

    printf("\nTime %.1f secs\n", clock() / 1.0E6);

    /*  Test definitions  */

    MaxVar = MAXARITY;

    while ( gets(Line) )
    {
	TestRel = Nil;
	for ( i = 0 ; i <= MaxRel && ! TestRel ; i++ )
	{
	    if ( ! strcmp(Reln[i]->Name, Line) ) TestRel = Reln[i];
	}

	if ( ! TestRel )
	{
	    printf("\nUnknown relation %s\n", Line);
	    exit();
	}
	else
	{
	    printf("\nTest relation %s\n", Line);
	}

	Cases = Errors = 0;

	while ( Case = ReadTuple(TestRel) )
	{
	    while ( (PlusOrMinus = getchar()) == ' ' || PlusOrMinus == '\t' )
		;
	    ReadToEOLN;

	    Cases++;

	    if ( Interpret(TestRel, Case) != ( PlusOrMinus == '+' ) )
	    {
		VERBOSE(1)
		{
		    printf("\terror on ");
		    PrintTuple(Case, TestRel->Arity);
		    newline;
		}
		Errors++;
	    }
	}

	printf("Summary: %d errors in %d trials\n", Errors, Cases);
    }
}



    FindRelationOrder()
/*  -----------------  */
{
    Boolean Waiting[MAXRELS+1];
    int Best, Next = 0, i;

    ForEach(i, 0, MaxRel)
    {
	Waiting[i] = true;
    }

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

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

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



    ConstructOptionalTuples(R)
/*  -----------------------  */
    Relation R;
{
    int i, j, index, No, Opt = 0;
    Tuple Case;

    MaxVar = R->Arity;
    No = 1;
    ForEach(i, 1, MaxVar)
    {
	No *= MaxConst;
    }

    R->Opt = (Tuple *) malloc((No + 1 - Number(R->Pos) - Number(R->Neg)) * sizeof(Tuple));

    ForEach(i, 0, No-1)
    {
	Case = (Tuple) malloc((MaxVar+1) * sizeof(int));
	index = i;
	for ( j = MaxVar ; j > 0 ; j-- )
	{
	    Case[j] = index % MaxConst + 1;
	    index /= MaxConst;
	}
	if ( Join(R->Pos, R->PosIndex, DefVars, Case, MaxVar, true) ||
	     Join(R->Neg, R->NegIndex, DefVars, Case, MaxVar, true) )
	{
	    free(Case);
	}
	else
	{
	    R->Opt[Opt++] = Case;
	}
    }

    R->Opt[Opt] = Nil;
}



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

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

    VERBOSE(2) newline;

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

	ForEach(T2, T1+1, MaxType)
	{
	    Compatible[T1][T2] = Compatible[T2][T1] =
		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(N1, V1, N2, V2)
/*      -----------  */
    Const N1, *V1, N2, *V2;
{
    if ( ! N1 || ! N2 )	return false;
    else
    if ( *V1 == *V2 )	return true;
    else
    if ( *V1 < *V2 )	return CommonValue(N1-1, V1+1, N2, V2);
    else
			return CommonValue(N1, V1, N2-1, V2+1);
}