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

int	FalsePositive,
	FalseNegative;


Literal FindLiteral(NotFirstLit)
/*      -----------  */
    Boolean NotFirstLit;
{
    int i, PossibleRelns = 0, PossibleArgLists[MAXRELS+1];
    Literal L, SelectLiteral();
    Tuple *TSP;

    NPossible = 0;
    BaseInfo = Info(Pos, Tot);
    MaxPossibleGain = Pos * BaseInfo;

    VERBOSE(1)
    {
	printf("\nTraining set (%d/%d=%.1f bits, %.1f bits available):\n",
	       Pos, Tot, MaxPossibleGain, AvailableBits);
	VERBOSE(3)
	    PrintTuples(MaxVar, TrainingSet, true);
	newline;
    }

    ForEach(i, 0, MaxRel)
    {
	/*  Recursive lits can't be first and require a partial order  */

	if ( RelnOrder[i] != Target || NotFirstLit && AnyPartialOrder )
	{
	    if ( PossibleArgLists[i] = NumberArgLists(1, MaxVar, true, RelnOrder[i], 0) )
	    {
		PossibleRelns++;
	    }
	    /*else printf("no possible args for %s\n", RelnOrder[i]->Name);*/
	}
	else
	{
	    PossibleArgLists[i] = 0;
	}
    }

    for ( i = 0 ; i <= MaxRel && BestLitGain < MaxPossibleGain ; i++ )
    {
	if ( PossibleArgLists[i] )
	{
	    CheckRelation(RelnOrder[i], PossibleArgLists[i], PossibleRelns);
	}
    }

    if ( NDeterminate && BestLitGain < DETERMINATE * MaxPossibleGain )
    {
	return Nil;
    }
    else
    if ( NPossible )
    {
	return SelectLiteral();
    }
    else
    {
	VERBOSE(1) printf("\nNo literals\n");
	return Nil;
    }
}



Clause FindClause()
/*     ----------  */
{
    Tuple Case, *TSP;
    Boolean Progress = true, Recover();
    Literal L;

    NewClause = (Clause) malloc((MAXLITS+1) * sizeof(Literal));
    NToBeTried = NLit = 0;

    UsedSoFar = WeakLiterals = 0;
    CyclePos = Pos;
    CycleTot = Tot;
    AvailableBits = Except(CycleTot, Pos);

    memset(PartialOrder, false, (MAXARITY+1)*(MAXARITY+1));
    AnyPartialOrder = false;

    while ( Progress && Pos < Tot && NLit < MAXLITS )
    {
	NDeterminate = 0;

	L = FindLiteral(NLit > 0);

	if ( L )
	{
	    NewClause[NLit++] = L;

	    NewTrainingSet(L->Rel, L->Sign, L->Args);

	    /*  Update encoding bits  */

	    UsedSoFar += L->Bits;
	    AvailableBits = Except(CycleTot, PosCovered) - UsedSoFar;

	    VERBOSE(1)
	    {
		printf("\nBest literal ");
		PrintLiteral(L->Rel, L->Sign, L->Args);
		printf(" (%.1f bits; %.1f bits left)\n", L->Bits, AvailableBits);
	    }

	}
	else
	if ( NDeterminate )
	{
	    ProcessDeterminateLiterals();
	}
	else
	Progress = Recover();
    }

    if ( ! NLit  || PosCovered < MINACCURACY * TotCovered )
    {
	if ( NLit )
	{
	    VERBOSE(1) printf("\nClause too inaccurate (%d/%d)\n", PosCovered, TotCovered);
	}

	free(NewClause);
	return Nil;
    }

    NewClause[NLit] = Nil;
    PruneClause(NewClause, NLit);

    FalsePositive += TotCovered - PosCovered;
    FalseNegative -= PosCovered;

    MaxVar = Target->Arity;

    /*  Set bits for positive covered tuples  */

    ClearBits;

    for ( TSP = TrainingSet ; Case = *TSP ; TSP++ )
    {
	if ( Positive(Case) ) SetBit(Case[0]&Mask, TrueBit);
    }

    /*  Copy all negative tuples and uncovered positive tuples  */

    Tot = Pos = 0;

    for ( TSP = CopyTrainingSet ; Case = *TSP ; TSP++ )
    {
	if ( ! Positive(Case) || ! TestBit(Case[0]&Mask, TrueBit) )
	{
	    CopyTrainingSet[Tot++] = Case;
	    if ( Positive(Case) ) Pos++;
	}
    }
    CopyTrainingSet[Tot] = Nil;

    if ( Pos )
    {
	Discard(TrainingSet, true);
	TrainingSet = CopyTrainingSet;
    }

    return NewClause;
}



    FindDefinition(R)
/*  --------------  */
    Relation R;
{
    Literal L;

    Target = R;
    NCl = 0;

    printf("\n----------\n%s:\n", R->Name);
    InitialiseTrainingSet(R);
    CopyTrainingSet = TrainingSet;

    FalsePositive = 0;
    FalseNegative = Pos;

    R->Def = (Clause *) malloc((MAXCLS+1) * sizeof(Clause));

    while ( Pos && NCl < MAXCLS && (R->Def[NCl] = FindClause()) )
    {
	R->Def[NCl++][NLit] = Nil;
    }

    R->Def[NCl] = Nil;

    SiftClauses();

    if ( FalsePositive || FalseNegative )
    {
	printf("\n***  Warning: the following definition\n");

	if ( FalsePositive )
	{
	    printf("***  matches %d tuple%s not in the relation\n",
		FalsePositive, Plural(FalsePositive));
	}

	if ( FalseNegative )
	{
	    printf("***  does not cover %d tuple%s in the relation\n",
		FalseNegative, Plural(FalseNegative));
	}
    }

    PrintDefinition(R);
}