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


char	ArgList[MAXARITY+1];
float	LitBits, ComputeGain();


	/*  In this version, unbound variables are ok in recursive literals  */

#define	ExtraUnboundVars 1


	/*  Examine bindings on relation R; check the best against the
	    best so far  */

int Tried;

    CheckRelation(R, Tries, NRelns)
/*  -------------  */
    Relation R;
    int Tries, NRelns;
{
    long clock();

    LitBits = NEGLITERALS	/* sign (if negated literals ok) */
	      + Log2(NRelns)	/* which relation? */
	      + Log2(Tries)	/* different argument lists */
	      - Log2(NLit+1);	/* credit for ordering of literals */

    if ( LitBits > AvailableBits )
    {
	VERBOSE(1)
	    printf("\tliterals using %s require %.1f bits\n", R->Name, LitBits);

	return;
    }

    if ( R == SAMEVAR )
    {
	CheckSameVar(Tries, NRelns);
	return;
    }

    Tried = 0;
    TryArgs(1, MaxVar, 0, 0, false, R, 0);

    VERBOSE(1)
    {
	printf("\t\t\t\t[%s tried %d / %d, %.1f secs]\n",
		R->Name, Tried, Tries, clock() / 1.0E6);
    }
}


    /*  Special version for '='  */

    CheckSameVar(Tries, NRelns)
/*  ------------  */
    int Tries, NRelns;
{
    long clock();

    Tried = 0;

    for ( ArgList[1] = 1 ;
          ArgList[1] < MaxVar && BestLitGain < MaxPossibleGain ;
	  ArgList[1]++ )
    {
	for ( ArgList[2] = ArgList[1]+1 ;
	      ArgList[2] <= MaxVar && BestLitGain < MaxPossibleGain ;
	      ArgList[2]++ )
	{
	    if ( Compatible[VarType[ArgList[1]]][VarType[ArgList[2]]] )
	    {
		ComputeGain(SAMEVAR, ArgList, LitBits, true);
		Tried++;
	    }
	}
    }

    VERBOSE(1)
    {
	printf("\t\t\t\t[= tried %d / %d, %.1f secs]\n",
		Tried, Tries, clock() / 1.0E6);
    }
}



    /*  Examine possible argument lists for relation R.
	Any such list must select at least one case in the
	training set.  */

    TryArgs(This, HiVar, FreeVars, MaxDepth, SomePartOrd, R, Key)
/*  -------  */
    int This, HiVar, FreeVars, MaxDepth, Key;
    Boolean SomePartOrd;
    Relation R;
{
    Var V, VMax;
    Boolean Free, NewFree;

    VMax = HiVar + ExtraUnboundVars;

    for ( V = 1 ; V <= VMax && BestLitGain < MaxPossibleGain ; V++ )
    {
	Free = V > MaxVar;

	if ( NewFree = V > HiVar )
	{
	    if ( MaxDepth >= MAXVARDEPTH ) return;

	    Key |= (1 << This);
	    if ( IllegalKey(Key, R) ) return;

	    HiVar = V;
	    VarType[V] = R->Type[This];
	}
	else
	if ( ! Free && VarDepth[V] + (FreeVars > 0) > MAXVARDEPTH ||
	     ! Compatible[VarType[V]][R->Type[This]] )
	{
	    continue;
	}

	ArgList[This] = V;

	if ( This < R->Arity )
	{
	    if ( NewFree  /* V unconstrained */  ||
		 PossibleGain(This, R, HiVar) )
	    {
		TryArgs(This+1, HiVar,
			FreeVars + Free,
			Free || VarDepth[V] <= MaxDepth ? MaxDepth : VarDepth[V],
			(Boolean) (SomePartOrd || ! NewFree && PartialOrder[V][This]),
			R, Key);
	    }
	}
	else
	if ( FreeVars + Free < R->Arity &&
	     ( R != Target || SomePartOrd || ! NewFree && PartialOrder[V][This] ) )
	{
	    ComputeGain(R, ArgList, LitBits, true);
	    Tried++;
	}
    }
}



Boolean PossibleGain(This, R, HiVar)
/*    ------------  */
    int This, HiVar;
    Relation R;
{
    int i, Neg, YesPos = 0, YesNeg = 0, NoPos = 0, NoNeg = 0;
    float MinUsefulGain, YesPosThresh, NoNegThresh;
    Boolean RuleOutYes, RuleOutNo;
    Tuple *Scan;

    RuleOutYes = false;
    RuleOutNo  = ! NEGLITERALS;

    /*  Maximum possible gain:
	    Yes:	exclude all but existing YesPos positive cases
	    No:		exclude only YesPos positive cases  */

    Neg = Tot - Pos;

    /*  The minimum gain that would be of interest is just enough to give
	a literal a chance to be saved by the backup procedure or, if
	there are determinate literals, to reach the required fraction
	of the maximum possible gain  */

    MinUsefulGain = NPossible < MAXPOSSLIT ? MINALTFRAC * BestLitGain :
			Max(Possible[MAXPOSSLIT]->Gain, MINALTFRAC * BestLitGain);

    if ( NDeterminate && MinUsefulGain < DETERMINATE * MaxPossibleGain )
    {
	MinUsefulGain = DETERMINATE * MaxPossibleGain;
    }

    YesPosThresh = MinUsefulGain / BaseInfo - 0.001;
    NoNegThresh = (Pos + 1) * (pow(2.0, BaseInfo - MinUsefulGain / Pos) - 1) + 0.001;

    ForEach(i, This+1, R->Arity)
    {
	ArgList[i] = HiVar + i - This; /*** HiVar?? ***/
    }

    for ( Scan = TrainingSet + Tot - 1 ; Scan >= TrainingSet ; Scan-- )
    {
	if ( Join(R->Pos, R->PosIndex, ArgList, *Scan, R->Arity, true) )
	{
	    if ( Positive(*Scan) )
	    {
		if ( ++YesPos >= YesPosThresh ) return true;
	    }
	    else
	    {
		if ( Neg - (++YesNeg) < NoNegThresh ) return true;
	    }
	}
	else
	{
	    if ( Positive(*Scan) )
	    {
		if ( Pos - (++NoPos) < YesPosThresh && ! RuleOutYes )
		{
		    RuleOutYes = true;
		    if ( RuleOutNo ) break;
		}
	    }
	    else
	    {
		if ( ++NoNeg > NoNegThresh && ! RuleOutNo )
		{
		    RuleOutNo = true;
		    if ( RuleOutYes ) break;
		}
	    }
	}
    }

    VERBOSE(2)
    {
	ForEach(i, This+1, R->Arity)
	{
	    ArgList[i] = 0;
	}

	printf("\t");
	PrintLiteral(R, true, ArgList);
	printf("\tTrue [%d,%d], False [%d,%d]: gain below threshold\n",
		YesPos, YesPos+YesNeg, NoPos, NoPos+NoNeg);
    }

    return false;
}



    /*  Count possible argument lists for relation R.  */

int NumberArgLists(This, HiVar, AllFree, R, Key)
/*  --------------  */
    int This, HiVar, Key;
    Boolean AllFree;
    Relation R;
{
    int V, V1, VMax, PossibleArgs = 0;
    Boolean Free;

    if ( R == SAMEVAR )
    {
	ForEach(V, 1, MaxVar-1)
	{
	    ForEach(V1, V+1, MaxVar)
	    {
		if ( Compatible[VarType[V]][VarType[V1]] ) PossibleArgs++;
	    }
	}
    }
    else
    {
	VMax = HiVar + ExtraUnboundVars;

	for ( V = 1 ; V <= VMax ; V++ )
	{
	    if ( V > HiVar )
	    {
		Key |= (1 << This);
		if ( IllegalKey(Key, R) ) continue;

		VarType[V] = R->Type[This];
	    }
	    else
	    if ( ! Compatible[VarType[V]][R->Type[This]] )
	    {
		continue;
	    }

	    Free = V > MaxVar;
	    ArgList[This] = V;
	    HiVar = Max(HiVar, V);

	    if ( This < R->Arity )
	    {
		PossibleArgs += NumberArgLists(This+1, HiVar, AllFree && Free, R, 0);
	    }
	    else
	    {
		if ( ! Free || ! AllFree ) PossibleArgs++;
	    }
	}
    }

    return PossibleArgs;
}


	/*  Determine whether a partial key matches one of
	    the defined keys for this relation.  */

Boolean IllegalKey(Key, R)
/*      ----------  */
    int Key;
    Relation R;
{
    int i;

    if ( ! R->NKeys ) return false;

    ForEach(i, 0, R->NKeys-1)
    {
	if ( (R->Key[i] | Key) == R->Key[i] ) return false;
    }

    return true;
}