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


    /*	At any stage, the MAXPOSSLIT best literals to use next are
	kept in the array Possible.  This procedure puts a new literal
	into the list if it qualifies  */


    ProposeLiteral(R, TF, A, Size, LitBits, OPos, OTot, Gain)
/*  --------------  */
    Relation R;
    Boolean TF;
    Vars A;
    int Size, OPos, OTot;
    float LitBits, Gain;
{
    int i, j;
    PossibleLiteral Entry;

    /*  See where this literal would go.  Other things being equal, prefer
	an unnegated literal  */

    i = NPossible;
    while ( i > 0 &&
	    ( Gain > Possible[i]->Gain + 1E-6 ||
	      Gain == Possible[i]->Gain && TF && ! Possible[i]->Sign ) ) i--;

    if ( i >= MAXPOSSLIT )  return;

    if ( NPossible < MAXPOSSLIT ) NPossible++;

    Entry = Possible[MAXPOSSLIT];

    for ( j = MAXPOSSLIT ; j > i+1 ; j-- )
    {
	Possible[j] = Possible[j-1];
    }

    Possible[i+1] = Entry;

    Entry->Gain    = Gain;
    Entry->Rel     = R;
    Entry->Sign    = TF;
    memcpy(Entry->Args, A, R->Arity+1);
    Entry->Bits	   = LitBits;
    Entry->NewSize = Size;
    Entry->PosCov  = OPos;
    Entry->TotCov  = OTot;
}



    /*  When all possible literals have been explored, the best of them
	(if there are any) is extracted and used.  Others with gain
	close to the best are entered as backups  */

Literal SelectLiteral()
/*      -------------  */
{
    int i;
    Literal MakeLiteral();

    if ( ! NPossible ) return Nil;

    ForEach(i, 2, NPossible)
    {
	if ( Possible[i]->Gain >= MINALTFRAC * Possible[1]->Gain )
	{
	    Remember(MakeLiteral(i), Possible[i]->PosCov, Possible[i]->TotCov);
	}
    }

    NewSize = Possible[1]->NewSize;

    return MakeLiteral(1);
}



Literal MakeLiteral(i)
/*      -----------  */
    int i;
{
    int N;
    Literal L;

    L = (Literal) malloc(sizeof(struct _lit_rec));

    L->Rel  = Possible[i]->Rel;
    L->Sign = Possible[i]->Sign;
    L->Bits = Possible[i]->Bits;

    N = L->Rel->Arity + 1;
    L->Args = (Vars) malloc(N);
    memcpy(L->Args, Possible[i]->Args, N);

    return L;
}



    /*  The array ToBeTried contains all backup points so far.
	This procedure sees whether another proposed backup will fit
	or will displace an existing backup  */

    Remember(L, OPos, OTot)
/*  --------  */
    Literal L;
    int OPos, OTot;
{
    int i, j;
    Alternative Entry;
    float InfoGain, Info();
    extern Clause NewClause; 	/* from FindClause */

    InfoGain = OPos * (Info(CyclePos, CycleTot) - Info(OPos, OTot));

    /*  See where this entry would go  */

    for ( i = NToBeTried ; i && ToBeTried[i]->Value < InfoGain ; i-- )
	;

    if ( i >= MAXALTS )  return;

    if ( NToBeTried < MAXALTS ) NToBeTried++;

    Entry = ToBeTried[MAXALTS];

    for ( j = MAXALTS ; j > i+1 ; j-- )
    {
	ToBeTried[j] = ToBeTried[j-1];
    }

    ToBeTried[i+1] = Entry;

    if ( Entry->UpToHere ) free(Entry->UpToHere);

    Entry->UpToHere = (Clause) malloc((MAXLITS+1) * sizeof(Literal));
    memcpy(Entry->UpToHere, NewClause, (NLit+1) * sizeof(Literal));
    Entry->UpToHere[NLit]   = L;
    Entry->UpToHere[NLit+1] = Nil;
    Entry->Value	    = InfoGain;

    VERBOSE(1)
    {
	printf("\tSave ");
	PrintLiteral(L->Rel, L->Sign, L->Args);
	printf(" (%d,%d value %.1f)\n", OPos, OTot, InfoGain);
    }
}



Boolean Recover()
/*      -------  */
{
    int i;
    Clause C;
    Literal L;
    extern Clause NewClause;	/* from FindClause */
    Alternative Entry;

    if ( ! NToBeTried ) return Nil;

    Entry = ToBeTried[1];
    C = ToBeTried[1]->UpToHere;

    VERBOSE(1)
    {
	printf("\nRecover to ");
	PrintClause(Target, C);
    }

    RecoverTrainingSet(C);

    ForEach(i, 2, NToBeTried)
    {
	ToBeTried[i-1] = ToBeTried[i];
    }
    ToBeTried[NToBeTried] = Entry;
    NToBeTried--;

    UsedSoFar = 0;
    NLit = 0;
    while ( L = C[NLit] )
    {
	NewClause[NLit++] = L;
	if ( L->Sign != 2 ) UsedSoFar += L->Bits;
    }
    AvailableBits = Except(CycleTot, PosCovered) - UsedSoFar;

    VERBOSE(1)
    {
	printf("\t%.1f bits used, %.1f bits available\n", UsedSoFar, AvailableBits);
    }

    return true;
}