#include #include #include #include /******************************************************************************/ /* */ /* Type definitions, including synonyms for structure pointers */ /* */ /******************************************************************************/ typedef unsigned char Var; typedef char Boolean, Ordering; /* valid instances are <,=,>,# */ /* A tuple is stored as an array of int / fp. * T[0] = tuple number + POSMARK (pos tuples) * T[i] = constant number, or fp value NB: If continuous (fp) values are used, type Const must be the same size as float --if this is not the case, change Const to long. Relation tuple sets are indexed by 3D array. * I[i][j][k] = no. of kth tuple with T[j] = i The last entry is followed by FINISH */ typedef int Const, *Tuple; typedef int ***Index; typedef struct _rel_rec *Relation; typedef struct _type_rec *TypeInfo; typedef struct _state_rec State; typedef struct _lit_rec *Literal, **Clause; typedef struct _arg_ord_rec *ArgOrder; typedef struct _poss_lit_rec *PossibleLiteral; typedef struct _backup_rec *Alternative; typedef struct _var_rec *VarInfo; /******************************************************************************/ /* */ /* Structure definitions */ /* */ /******************************************************************************/ /* State */ /* A state represents information about the search for a new clause, including the tuples that satisfy the clause and various counts for the clause and the tuples */ struct _state_rec { int MaxVar, /* highest variable */ NPos, /* number of pos tuples */ NTot, /* number of all tuples */ NOrigPos, /* original pos tuples covered */ NOrigTot; /* original tuples covered */ Tuple *Tuples; /* training set */ float BaseInfo; /* information per pos tuple */ }; /* Literal */ struct _lit_rec { char Sign; /* 0=negated, 1=pos, 2=determinate */ Relation Rel; Var *Args; int WeakLits; /* value up to this literal */ Ordering *ArgOrders, /* recursive lits: =, <, >, # */ *SaveArgOrders; /* copy during pruning */ float Bits; /* encoding length */ }; /* Relation */ /* Note: Relations are represented by the (positive) tuples they contain; if the closed world assumption is not in force, negative tuples known not to be in the relation can be given explicitly. A key specifies a sensible way that a relation can be accessed by noting which arguments must have bound values. There can be any number of keys; if there are none, all possible ways of accessing the relation are ok. */ struct _rel_rec { char *Name; int Arity, /* number of arguments */ NKeys, /* number of keys (0=all ok) */ *Key, /* keys, each packed in an int */ *Type; /* types of arguments */ TypeInfo *TypeRef; /* redundant pointers to types */ Tuple *Pos, /* positive tuples */ *Neg; /* negative tuples or Nil (CWA) */ Index PosIndex, /* index for positive tuples */ NegIndex; /* ditto for explicit negative tuples */ int PosDuplicates, /* number of duplicate pos tuples*/ NTrialArgs, /* number of args to try (gain) */ NTried; /* number of them evaluated */ Clause *Def; /* definition is array of clauses */ Boolean BinSym, /* true for binary symmetric relns */ PossibleTarget, **PosOrder, /* argument order info for R() */ **NegOrder, /* " " " " ~R() */ *ArgNotEq; /* args that cannot be the same var (indexed by ArgPair) */ float Bits; /* current encoding cost */ }; /* Type */ struct _type_rec { char *Name; /* type name */ Boolean Continuous, /* continuous (non-discrete) */ Ordered, /* ordered discrete type */ FixedPolarity; int NValues, /* number of discrete constants */ NTheoryConsts; /* number of theory constants */ Const *Value, /* constants */ *TheoryConst; /* theory constants */ int *CollSeq; /* CollSeq[k] = x if (global) constant k is x'th const of this type */ }; /* Possible argument order -- used in discovering constant orders */ struct _arg_ord_rec { Relation Rel; /* relation */ Boolean Sign; /* sign */ int A1, A2, /* A1 < A2 or A1 > A2 */ In; /* 0, -1 (reverse) or +1 */ }; /* Structures used in backing up search */ struct _poss_lit_rec { Relation Rel; Boolean Sign; Var *Args; float Gain, Bits; int WeakLits, NewSize, TotCov, PosCov; }; struct _backup_rec { float Value; Clause UpToHere; }; /* Variables */ struct _var_rec { char *Name; int Type, Depth; TypeInfo TypeRef; }; #define FP(X) (*((float *)(&X))) /* The first four relations are predefined comparisons with aliased names defined here */ #define EQVAR Reln[0] /* var = var */ #define EQCONST Reln[1] /* var = theory const */ #define GTVAR Reln[2] /* var > var */ #define GTCONST Reln[3] /* var > threshold */ #define Predefined(R) (R==EQVAR||R==EQCONST||R==GTVAR||R==GTCONST) #define HasConst(R) (R==EQCONST||R==GTCONST) #define Verbose(x) if (VERBOSITY >= x) #define LN2 0.693147 #define Log2(x) (log((float) x)/LN2) #define Log2e 1.44269 #define Log2sqrt2Pi 1.32575 #define LogComb(n,r) (Log2Fact(n) - Log2Fact(r) - Log2Fact((n)-(r))) #define Except(n,e) ((n) ? (1.1*(Log2(n) + LogComb(n, e))) : 0.0) #define Encode(n) Except(AllTuples, n) #define Nil 0 #define false 0 #define true 1 #define Max(a,b) ( (a)>(b) ? a : b ) #define Min(a,b) ( (a)<(b) ? a : b ) #define ForEach(V,First,Last) for(V=First;V<=Last;V++) #define Mask 077777777 #define PosMark 0100000000 /* Max tuples = 16.7M */ #define Positive(T) ((T)[0]&PosMark) #define TrueBit 02 #define FalseBit 01 #define SetFlag(A,B) Flags[A] |= B #define TestFlag(A,B) (Flags[A] & B) #define ClearFlags memset(Flags,0,StartDef.NTot) #define BestLitGain (NPossible ? Possible[1]->Gain : 0.0) #define MonitorWeakLits(W) if (W) NWeakLits++; else NWeakLits=0 #define Plural(n) ((n) != 1 ? "s" : "") #define ReadToEOLN while ( getchar() != '\n' ) #define Alloc(N,T) (T *) pmalloc((N)*sizeof(T)) #define AllocZero(N,T) (T *) pcalloc(N, sizeof(T)) #define Realloc(V,N,T) V = (T *) prealloc(V, (N)*sizeof(T)) #define MissingValue(R,A,X) (MissingVals && MissingVal(R,A,X)) #define ungetchar(A) ungetc(A, stdin) #define ArgPair(A2,A1) (((A2-1)*(A2-2))/2 + A1-1) /* The following are used to pack and unpack parameters into argument lists. AV must be the address of an int or float */ #define SaveParam(A,AV) memcpy(A,AV,sizeof(Const)) #define GetParam(A,AV) memcpy(AV,A,sizeof(Const)) /******************************************************************************/ /* */ /* Various constants */ /* */ /******************************************************************************/ #define FINISH 10000000 /* large constant used as a terminator */ #define UNBOUND 0357357 /* odd marker used in interpret.c, join.c */ #define MISSING_DISC 1 /* missing value "?" is the first constant */ #define MISSING_FP 0.03125 /* arbitrary number used as the floating point equivalent of MISSING_DISC - if it clashes with a genuine data value, just change this */ #define OUT_OF_RANGE 2 /* denotes constant outside closed world */ /******************************************************************************/ /* */ /* Synopsis of functions */ /* */ /******************************************************************************/ /* main.c */ void main(int Argc, char *Argv[]); /* utility.c */ void *pmalloc(unsigned arg); void *prealloc(void * arg1, unsigned arg2); void *pcalloc(unsigned arg1, unsigned arg2); void pfree(void *arg); float CPUTime(); /* input.c */ Boolean ReadType(); void ReadTypes(); Tuple ReadTuple(Relation R); Tuple *ReadTuples(Relation R, Boolean Pos); Relation ReadRelation(); void ReadRelations(); int FindType(char *N); char *CopyString(char *s); void Error(); void DuplicateTuplesCheck(Relation R); int CountDuplicates(Tuple *T, int N, int Left, int Right); Boolean SymmetryCheck(Relation R); char ReadName(char *s); Const FindConstant(char *N, Boolean MustBeThere); int Number(Tuple *T); void CheckTypeCompatibility(); Boolean CommonValue(int N1, Const *V1, int N2, Const *V2); Index MakeIndex(Tuple *T, int N, Relation R); void UnequalArgsCheck(Relation R); Boolean NeverEqual(Tuple *T, Var F, Var S); /* output.c */ void PrintTuple(Tuple C, int N, TypeInfo *TypeRef, Boolean ShowPosNeg); void PrintTuples(Tuple *TT, int N); void PrintSpecialLiteral(Relation R, Boolean RSign, Var *A); void PrintComposedLiteral(Relation R, Boolean RSign, Var *A); void PrintLiteral(Literal L); void PrintClause(Relation R, Clause C); void PrintSimplifiedClause(Relation R, Clause C); void Substitute(char *Old, char *New); void PrintDefinition(Relation R); /* literal.c */ void ExploreArgs(Relation R, Boolean CountFlag); Boolean AcceptableKey(Relation R, int Key); Boolean Repetitious(Relation R, Var *A); Boolean SameArgs(int N, Var *A1, int MV1, Var *A2, int MV2, int LitN); void ExploreEQVAR(); void ExploreEQCONST(); void ExploreGTVAR(); void ExploreGTCONST(); Boolean TryArgs(Relation R, int This, int HiVar, int FreeVars, int MaxDepth, int Key, Boolean TryMostGeneral, Boolean RecOK); int EstimatePossibleArgs(int TNo); /* evaluatelit.c */ void EvaluateLiteral(Relation R, Var *A, float LitBits, Boolean *Prune); void PrepareForScan(Relation R, Var *A); float NegThresh(int P, int P1); Boolean TerminateScan(Relation R, Var *A); Boolean Satisfies(int RN, Const V, Const W, Tuple Case); void CheckForPrune(Relation R, Var *A); void CheckNewVars(Tuple Case); float Worth(int N, int P, int T, int UV); float Info(int P, int T); Boolean MissingVal(Relation R, Var *A, Tuple T); Boolean Unknown(Var V, Tuple T); void FindThreshold(Var *A); void PossibleCut(float C); int MissingAndSort(Var V, int Fp, int Lp); void Quicksort(Tuple *Vec, int Fp, int Lp, Var V); /* join.c */ Boolean Join(Tuple *T, Index TIX, Var *A, Tuple C, int N, Boolean YesOrNo); /* state.c */ void OriginalState(Relation R); void AddTuple(int N, Tuple T, int ByteSize, int Mark); Tuple NextConstTuple(Relation R, Tuple Case); void RandomTuple(Relation R, Tuple Result); void NewState(Literal L, int NewSize); void FormNewState(Relation R, Boolean RSign, Var *A, int NewSize); void AcceptNewState(Relation R, Var *A, int NewSize); void RecoverState(Clause C); void CheckSize(int SoFar, int Extra, int *NewSize, Tuple **TSAddr); Tuple Extend(Tuple Case, Tuple Binding, Var *A, int N); void CheckOriginalCaseCover(); void FreeTuples(Tuple *TT, Boolean TuplesToo); double Log2Fact(int n); /* determinate.c */ Boolean GoodDeterminateLiteral(Relation R, Var *A, float LitBits); void ProcessDeterminateLiterals(Boolean AllWeak); Boolean SameVar(Var A, Var B); void ShiftVarsDown(int s); /* search.c */ void ProposeLiteral(Relation R, Boolean TF, Var *A, int Size, float LitBits, int OPos, int OTot, float Gain, Boolean Weak); Boolean Recover(); void Remember(Literal L, int OPos, int OTot); Literal MakeLiteral(int i); Literal SelectLiteral(); void FreeLiteral(Literal L); void FreeClause(Clause C); /* order.c */ void ExamineVariableRelationships(); Boolean RecursiveCallOK(Var *A); void AddOrders(Literal L); void NoteRecursiveLit(Literal L); /* finddef.c */ void FindDefinition(Relation R); Clause FindClause(); void ExamineLiterals(); void GrowNewClause(); Boolean SameLiteral(Relation R, Boolean Sign, Var *A); Boolean AllLHSVars(Literal L); Boolean AllDeterminate(); float CodingCost(Clause C); /* prune.c */ void PruneNewClause(); void CheckVariables(); Boolean TheoryConstant(Const C, TypeInfo T); Boolean ConstantVar(Var V, Const C); Boolean IdenticalVars(Var V, Var W); Boolean Known(Relation R, Var V, Var W); void Insert(Var V, Relation R, Var A1, Const A2); Boolean Contains(Var *A, int N, Var V); Boolean QuickPrune(Clause C, Var MaxBound, Boolean *Used); Boolean SatisfactoryNewClause(int Errs); void RenameVariables(); Boolean RedundantLiterals(int ErrsNow); Boolean EssentialBinding(int LitNo); void ReplaceVariable(Var Old, Var New); void SiftClauses(); Var HighestVarInDefinition(Relation R); Boolean Recursive(Clause C); /* interpret.c */ Boolean CheckRHS(Clause C); Boolean Interpret(Relation R, Tuple Case); void InitialiseValues(Tuple Case, int N); /* constants.c */ void OrderConstants(); void FindArgumentOrders(); void ExamineArgumentPairs(Relation R, Boolean Sign, Tuple *TP); Boolean ConsistentClosure(Boolean **Table, Tuple *TP, Var A, Var B); Boolean AddPair(Boolean **Table, int A, int B); void AddArgOrder(Relation R, Boolean Sig, int A1, int A2); Boolean **AllocatePartOrd(int Size); void FreePartOrd(Boolean **PO, int Size); void ClearPartOrd(Boolean **PO); void FindConsistentSubset(int Included, int TryNext, Boolean **PO); int CountEntries(int K); /******************************************************************************/ /* */ /* Parameters set by options and variables accessible to many routines */ /* */ /******************************************************************************/ Boolean NEGLITERALS = true, /* negated literals ok */ NEGEQUALS = true, /* negated equality literals ok */ UNIFORMCODING = false, /* uniform coding of literals */ MissingVals = false, /* missing values in input? */ AnyPartialOrder, /* quick check to rule out recursive lits */ *Barred, /* duplicate variables */ OutOfWorld; /* flag ^ constant */ float SAMPLE = 1.0, /* fraction of negative tuples to sample */ MINACCURACY = 0.8, /* minimum acceptable clause accuracy */ MINALTFRAC = 0.8, /* fraction of best gain required for backup */ DETERMINATE = 0.8; /* use determinate literals unless a literal with this fraction of max possible gain */ int MAXVARS = 52, /* max number of variables */ MAXARGS = 5, /* max arity of any relation */ MAXWEAKLITS = 3, /* max weak literals in sequence */ MAXPOSSLIT = 5, /* 1 + max backups from single state */ MAXALTS = 20, /* max simultaneous backups */ MAXRECOVERS, /* max total backups */ MAXVARDEPTH = 4, /* max depth of var in literal */ MAXTUPLES = 100000, /* max number of tuples */ VERBOSITY = 1, /* level of output */ MaxConst = 0, /* no. constants */ MaxType = 0, /* no. types */ MaxRel = 0, /* highest relation no */ AllTuples, /* effective size of universe */ NCl, /* current clause number */ NLit, /* current literal number */ NDetLits, /* number of determinate lits in clause */ NWeakLits, /* current weak lits in sequence */ SavedClauseCover; /* coverage of saved clause */ char **ConstName, /* names of all discrete constants */ *Flags = Nil; /* flag bits for original tuples */ Relation *Reln, /* relations */ *RelnOrder, /* order to try relations */ Target; /* relation being induced */ State StartDef, /* at start of definition */ StartClause, /* at start of clause */ Current, /* current state */ New; /* possible next state */ float *LogFact = Nil, /* LogFact[i] = log2(i!) */ MaxPossibleGain, ClauseBits, /* bits used so far in this clause */ AvailableBits, /* bits available for this clause */ AdjMinAccuracy, /* min accuracy adjusted for sampling */ SavedClauseAccuracy; /* accuracy of saved clause */ Clause NewClause, /* clause being constructed */ SavedClause; /* best shorter clause discovered while developing current clause */ PossibleLiteral AlterSavedClause; /* last literal of saved clause */ Boolean **PartialOrder, /* partial orders on variables*/ **Compatible; /* Compatible[i][j] = true if types i, j have at least one common value */ Ordering **RecursiveLitOrders; /* pointers to orders in recursive lits */ int NRecLitClause, /* number of recursive lits in the new clause */ NRecLitDef; /* ditto in definition so far */ VarInfo *Variable; /* variables */ Var *DefaultVars; /* default variable list */ TypeInfo *Type; /* types */ Tuple *Found; /* join */ int NFound; /* number of tuples in join */ Alternative *ToBeTried; /* backup points */ int NToBeTried; PossibleLiteral *Possible; /* possible literals */ int NPossible, NDeterminate; /* Read parameters and initialise variables */ void main(int Argc, char *Argv[]) /* ---- */ { int o, i, Cases, Errors; extern char *optarg; extern int optind; Boolean FirstTime=true; Var V; extern Var *Arg; /* in literal.c */ Relation R; Tuple Case; char Line[200], PlusOrMinus; /* Check overlaying of Const and float */ if ( sizeof(Const) != sizeof(float) ) { printf("Integers and floating point numbers are different sizes\n"); printf("Alter declaration of type Const (defns.i) and recompile\n"); exit(1); } printf("FOIL 6.4 [January 1996]\n--------\n"); /* Process options */ while ( (o = getopt(Argc, Argv, "nNus:a:f:g:V:d:A:w:l:t:m:v:")) != EOF ) { if ( FirstTime ) { printf("\n Options:\n"); FirstTime = false; } switch (o) { case 'n': NEGLITERALS = NEGEQUALS = false; printf("\tno negated literals\n"); break; case 'N': NEGLITERALS = false; printf("\tnegated literals only for =, > relations\n"); break; case 'u': /*UNIFORMCODING = true;*/ printf("\tuniform coding of literals not available\n"); break; case 's': SAMPLE = atof(optarg); printf("\tsample %g%% of negative tuples\n", SAMPLE); SAMPLE /= 100; break; 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 'g': i = atoi(optarg); printf("\tuse determinate literals when gain <= "); printf("%d%% possible\n", i); DETERMINATE = i / 100.0; break; case 'V': MAXVARS = atoi(optarg); if ( MAXVARS > pow(2.0, 8*sizeof(Var)-1.0) ) { MAXVARS = pow(2.0, 8*sizeof(Var)-1.0) -0.9; } printf("\tallow up to %d variables\n", MAXVARS); break; case 'd': MAXVARDEPTH = atoi(optarg); printf("\tmaximum variable depth %d\n", MAXVARDEPTH); break; case 'w': MAXWEAKLITS = atoi(optarg); printf("\tallow up to %d consecutive weak literals\n", MAXWEAKLITS); break; case 'l': MAXPOSSLIT = atoi(optarg)+1; printf("\tmaximum %d backups from one literal\n", MAXPOSSLIT-1); break; case 't': MAXALTS = atoi(optarg); printf("\tmaximum %d total backups\n", MAXALTS); break; case 'm': MAXTUPLES = atoi(optarg); printf("\tmaximum %d tuples \n", MAXTUPLES); break; case 'v': VERBOSITY = atoi(optarg); printf("\tverbosity level %d\n", VERBOSITY); break; case '?': printf("unrecognised option\n"); exit(1); } } /* Set up predefined relations. These are treated specially in Join(). Rather than giving explicit pos tuples, the Pos field identifies the relation */ /* Note: EQCONST and GTCONST take one argument and one parameter (a theory constant or floating-point threshold). To simplify the code for all other relations, this parameter is packed into a "standard" arglist; the number of variable positions that it occupies will depend on the implementation. */ Reln = Alloc(10, Relation); EQVAR = AllocZero(1, struct _rel_rec); EQVAR->Name = "="; EQVAR->Arity = 2; EQVAR->Type = AllocZero(3, int); EQVAR->TypeRef = AllocZero(3, TypeInfo); EQVAR->Pos = (Tuple *) 0; EQVAR->BinSym = true; EQCONST = AllocZero(1, struct _rel_rec); EQCONST->Name = "=="; EQCONST->Arity = 1; EQCONST->Type = AllocZero(2, int); EQCONST->TypeRef = AllocZero(2, TypeInfo); EQCONST->Pos = (Tuple *) 1; EQCONST->BinSym = false; GTVAR = AllocZero(1, struct _rel_rec); GTVAR->Name = ">"; GTVAR->Arity = 2; GTVAR->Type = AllocZero(3, int); GTVAR->TypeRef = AllocZero(3, TypeInfo); GTVAR->Pos = (Tuple *) 2; GTVAR->BinSym = true; GTCONST = AllocZero(1, struct _rel_rec); GTCONST->Name = ">"; GTCONST->Arity = 1; GTCONST->Type = AllocZero(2, int); GTCONST->TypeRef = AllocZero(2, TypeInfo); GTCONST->Pos = (Tuple *) 3; GTCONST->BinSym = false; MaxRel = 3; ForEach(i, 0, MaxRel) { Reln[i]->PossibleTarget = false; } /* Read input */ ReadTypes(); CheckTypeCompatibility(); ReadRelations(); /* Initialise all global variables that depend on parameters */ Variable = Alloc(MAXVARS+1, VarInfo); DefaultVars = Alloc(MAXVARS+1, Var); ForEach(V, 0, MAXVARS) { Variable[V] = Alloc(1, struct _var_rec); if ( V == 0 ) { Variable[0]->Name = "_"; } else if ( V <= 26 ) { Variable[V]->Name = Alloc(2, char); Variable[V]->Name[0] = 'A' + V - 1; Variable[V]->Name[1] = '\0'; } else { Variable[V]->Name = Alloc(3, char); Variable[V]->Name[0] = 'A' + ((V-27) / 26); Variable[V]->Name[1] = 'A' + ((V-27) % 26); Variable[V]->Name[2] = '\0'; } DefaultVars[V] = V; } Barred = AllocZero(MAXVARS+1, Boolean); ToBeTried = Alloc(MAXALTS+1, Alternative); ForEach(i, 0, MAXALTS) { ToBeTried[i] = Alloc(1, struct _backup_rec); ToBeTried[i]->UpToHere = Nil; } PartialOrder = Alloc(MAXARGS+1, Boolean *); ForEach(V, 1, MAXARGS) { PartialOrder[V] = Alloc(MAXVARS+1, Boolean); } Possible = Alloc(MAXPOSSLIT+1, PossibleLiteral); ForEach(i, 1, MAXPOSSLIT) { Possible[i] = Alloc(1, struct _poss_lit_rec); Possible[i]->Args = Alloc(MAXARGS+1, Var); } Arg = Alloc(MAXARGS+1, Var); Arg[0] = 0; /* active */ /* Allocate space for trial recursive call */ RecursiveLitOrders = Alloc(1, Ordering *); RecursiveLitOrders[0] = Alloc(MAXARGS+1, Ordering); /* Find plausible orderings for constants of each type */ OrderConstants(); /* Find Definitions */ ForEach(i, 0, MaxRel) { R = RelnOrder[i]; if ( R->PossibleTarget ) { FindDefinition(R); } } /* Test definitions */ while ( gets(Line) ) { R = Nil; for ( i = 0 ; i <= MaxRel && ! R ; i++ ) { if ( ! strcmp(RelnOrder[i]->Name, Line) ) R = RelnOrder[i]; } if ( ! R ) { printf("\nUnknown relation %s\n", Line); exit(1); } else { printf("\nTest relation %s\n", Line); } Cases = Errors = 0; Current.MaxVar = HighestVarInDefinition(R); while ( Case = ReadTuple(R) ) { while ( (PlusOrMinus = getchar()) == ' ' || PlusOrMinus == '\t' ) ; ReadToEOLN; Cases++; if ( Interpret(R, Case) != ( PlusOrMinus == '+' ) ) { Verbose(1) { printf(" (%c)", PlusOrMinus); PrintTuple(Case, R->Arity, R->TypeRef, false); } Errors++; } } printf("Summary: %d error%s in %d trial%s\n", Errors, Plural(Errors), Cases, Plural(Cases)); } exit(0); } /******************************************************************************/ /* */ /* All input routines */ /* */ /******************************************************************************/ #define Space(s) (s == ' ' || s == '\t') #define SkipComment while ( ( c = 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; } 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); /* Check for duplicate constants */ ForEach(i, 0, T->NValues-2) { if ( T->Value[i] == C ) Error(7, Name, T->Name); } 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); ReadToEOLN; /* 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 names for missing value and out-of-range */ FindConstant("?", false); 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 && T[i] != OUT_OF_RANGE && ! 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; TheTuples = Alloc(101, Tuple); while ( T = ReadTuple(R) ) { T[0] = Pos ? PosMark : 0; if ( ND && 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); UnequalArgsCheck(R); return R; } void ReadRelations() /* ------------- */ { int i, j, Next, Best, PosSize, WorldSize; Relation R; Tuple *T; Boolean *Waiting; float *Imbalance; 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. Relations of the same arity are resolved by preferring relations with higher information */ RelnOrder = Alloc(MaxRel+1, Relation); Waiting = Alloc(MaxRel+1, Boolean); Imbalance = Alloc(MaxRel+1, float); memset(Waiting, true, MaxRel+1); ForEach(i, 4, MaxRel) { R = Reln[i]; PosSize = Number(R->Pos); if ( R->Neg ) { WorldSize = PosSize + Number(R->Neg); } else { WorldSize = 1; ForEach(j, 1, Reln[i]->Arity) { if ( ! R->TypeRef[j]->Continuous ) { WorldSize *= R->TypeRef[j]->NValues; } } } Imbalance[i] = fabs(0.5 - PosSize / (float) WorldSize); } RelnOrder[0] = Reln[1]; RelnOrder[1] = Reln[0]; RelnOrder[2] = Reln[3]; RelnOrder[3] = Reln[2]; /*ForEach(i, 0, 3) RelnOrder[i] = Reln[i];*/ Next = ( ContinuousVars ? 4 : 2 ); while ( true ) { Best = -1; ForEach(i, 4, MaxRel) { if ( Waiting[i] && ( Best < 0 || Reln[i]->Arity < Reln[Best]->Arity || Reln[i]->Arity == Reln[Best]->Arity && Imbalance[i] < Imbalance[Best] ) ) { Best = i; } } if ( Best < 0 ) break; RelnOrder[Next++] = Reln[Best]; Waiting[Best] = false; } MaxRel = Next-1; pfree(Waiting); pfree(Imbalance); } /* 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()) != EOF && ( c == '|' || Space(c) ) ) { if ( c == '|' ) SkipComment; } /* Return period if no names to read */ if ( c == EOF ) { return (SectionDelim = '.'); } else if ( c == ';' || c == '.' ) { ReadToEOLN; 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 ( Sp > s && 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); case 6: printf("Cannot use CWA for %s (continuous types)\n", s1); exit(1); case 7: printf("Type %s contains duplicate constant %s\n", s2, s1); exit(1); } } /* Check for arguments that cannot be equal */ void UnequalArgsCheck(Relation R) /* ---------------- */ { Var S, F; R->ArgNotEq = AllocZero(ArgPair(R->Arity,R->Arity), Boolean); ForEach(S, 2, R->Arity) { ForEach(F, 1, S-1) { R->ArgNotEq[ ArgPair(S,F) ] = NeverEqual(R->Pos, F, S); } } } Boolean NeverEqual(Tuple *T, Var F, Var S) /* ---------- */ { Tuple Case; while ( Case = *T++ ) { if ( Case[F] == Case[S] && Case[F] != OUT_OF_RANGE ) return false; } return true; } /******************************************************************************/ /* */ /* All output routines */ /* */ /******************************************************************************/ void PrintTuple(Tuple C, int N, TypeInfo *TypeRef, Boolean ShowPosNeg) /* ---------- */ { int i; printf("\t"); ForEach(i, 1, N) { if ( TypeRef ? TypeRef[i]->Continuous : Variable[i]->TypeRef->Continuous ) { /* Continuous value */ if ( FP(C[i]) == MISSING_FP ) { printf("?"); } else { printf("%g", FP(C[i])); } } else { printf("%s", ConstName[C[i]]); } if ( i < N ) putchar(','); } if ( ShowPosNeg ) { printf(": %c", (Positive(C) ? '+' : '-') ); } putchar('\n'); } void PrintTuples(Tuple *TT, int N) /* ----------- */ { while ( *TT ) { PrintTuple(*TT, N, Nil, true); TT++; } } void PrintSpecialLiteral(Relation R, Boolean RSign, Var *A) /* ------------------- */ { Const ThConst; float Thresh; if ( R == EQVAR ) { printf("%s%s%s", Variable[A[1]]->Name, RSign ? "=":"<>", Variable[A[2]]->Name); } else if ( R == EQCONST ) { GetParam(&A[2], &ThConst); printf("%s%s%s", Variable[A[1]]->Name, RSign ? "=" : "<>", ConstName[ThConst]); } else if ( R == GTVAR ) { printf("%s%s%s", Variable[A[1]]->Name, RSign ? ">" : "<=", Variable[A[2]]->Name); } else if ( R == GTCONST ) { GetParam(&A[2], &Thresh); if ( Thresh == MISSING_FP ) { printf("%s%s", Variable[A[1]]->Name, RSign ? ">" : "<="); } else { printf("%s%s%g", Variable[A[1]]->Name, RSign ? ">" : "<=", Thresh); } } } void PrintComposedLiteral(Relation R, Boolean RSign, Var *A) /* -------------------- */ { int i, V; if ( Predefined(R) ) { PrintSpecialLiteral(R, RSign, A); } else { if ( ! RSign ) { printf("not("); } printf("%s", R->Name); ForEach(i, 1, R->Arity) { printf("%c", (i > 1 ? ',' : '(')); if ( (V = A[i]) <= MAXVARS ) { printf("%s", Variable[V]->Name); } else { printf("_%d", V - MAXVARS); } } putchar(')'); if ( ! RSign ) { putchar(')'); } } } void PrintLiteral(Literal L) /* ------------ */ { PrintComposedLiteral(L->Rel, L->Sign, L->Args); } void PrintClause(Relation R, Clause C) /* ----------- */ { int Lit; PrintComposedLiteral(R, true, DefaultVars); for ( Lit = 0 ; C[Lit] ; Lit++ ) { printf("%s ", ( Lit ? "," : " :-" )); PrintLiteral(C[Lit]); } printf(".\n"); } /* Print clause, substituting for variables equivalent to constants */ void PrintSimplifiedClause(Relation R, Clause C) /* --------------------- */ { int i, Lit, NextUnbound; Literal L; Var V, Bound, *SaveArgs, *Unbound; char **HoldVarNames; Const TC; Boolean NeedComma=false; SaveArgs = Alloc(MAXVARS+1, Var); Unbound = Alloc(MAXVARS+1, Var); /* Save copy of variable names */ HoldVarNames = Alloc(MAXVARS+1, char *); ForEach(V, 1, MAXVARS) { HoldVarNames[V] = Variable[V]->Name; } /* Substitute for equal variables */ for ( Lit = 0 ; L = C[Lit] ; Lit++ ) { if ( L->Rel == EQVAR && L->Sign ) { Substitute(Variable[L->Args[2]]->Name, Variable[L->Args[1]]->Name); } } /* Set up alternate names for variables equated to theory constants */ for ( Lit = 0 ; L = C[Lit] ; Lit++ ) { if ( L->Rel == EQCONST && L->Sign ) { GetParam(&L->Args[2], &TC); Substitute(Variable[L->Args[1]]->Name, ConstName[TC]); } } PrintComposedLiteral(R, true, DefaultVars); Bound = R->Arity; for ( Lit = 0 ; L = C[Lit] ; Lit++ ) { /* Save literal args */ memcpy(SaveArgs, L->Args, (L->Rel->Arity+1) * sizeof(Var)); /* Update bound vars and change unbound vars in negated literals */ NextUnbound = MAXVARS; memset(Unbound, 0, MAXVARS+1); ForEach(i, 1, L->Rel->Arity ) { if ( (V = L->Args[i]) > Bound ) { if ( ! L->Sign ) { if ( ! Unbound[V] ) Unbound[V] = ++NextUnbound; L->Args[i] = Unbound[V]; } else { Bound = V; } } } /* Skip literals that are implicit in changed names */ if ( L->Rel != EQCONST && L->Rel != EQVAR || ! L->Sign ) { printf("%s", ( NeedComma ? ", " : " :- ") ); PrintLiteral(L); NeedComma = true; } /* Restore args */ memcpy(L->Args, SaveArgs, (L->Rel->Arity+1) * sizeof(Var)); } printf(".\n"); ForEach(V, 1, MAXVARS) { Variable[V]->Name = HoldVarNames[V]; } pfree(SaveArgs); pfree(Unbound); pfree(HoldVarNames); } void Substitute(char *Old, char *New) /* ---------- */ { Var V; ForEach(V, 1, MAXVARS) { if ( Variable[V]->Name == Old ) Variable[V]->Name = New; } } void PrintDefinition(Relation R) /* --------------- */ { int Cl, SecondPass=(-1); Clause C; putchar('\n'); for ( Cl = 0 ; C=R->Def[Cl] ; Cl++ ) { if ( Recursive(C) ) { SecondPass = Cl; } else { PrintSimplifiedClause(R, C); } } ForEach(Cl, 0, SecondPass) { if ( Recursive(C = R->Def[Cl]) ) PrintSimplifiedClause(R, C); } printf("\nTime %.1f secs\n", CPUTime()); } Boolean Recursive(Clause C) /* --------- */ { int Lit; for ( Lit = 0 ; C[Lit] ; Lit++ ) { if ( C[Lit]->Rel == Target ) return true; } return false; } /******************************************************************************/ /* */ /* A state, summarising a point in the search for a clause, consists */ /* of a set of tuples and various counts. The routines here set up */ /* an initial state for a relation and produce the new state that */ /* results when a literal is added to the current (partial) clause */ /* */ /******************************************************************************/ /* Set up original state for search for definition */ void OriginalState(Relation R) /* ------------- */ { int i, j, WorldSize=1, TupleArity, NegTuples, Remaining; Tuple Case, *Scan; double drand48(); if ( ! LogFact ) { LogFact = Alloc(1001, float); LogFact[0] = 0.0; ForEach(i, 1, 1000) { LogFact[i] = LogFact[i-1] + Log2(i); } } /* Establish number of variables hence size of tuples, and set variable types equal to the type of variable in that position in the relation, and variable depths to zero */ StartDef.MaxVar = Current.MaxVar = R->Arity; TupleArity = R->Arity+1; ForEach(i, 1, R->Arity) { Variable[i]->Type = R->Type[i]; Variable[i]->TypeRef = R->TypeRef[i]; Variable[i]->Depth = 0; } StartDef.NPos = Number(R->Pos); AdjMinAccuracy = MINACCURACY; /* Test whether negative tuples are already defined in the relation */ if ( R->Neg ) { /* Simply copy positive and negative tuples */ StartDef.NTot = AllTuples = Number(R->Neg) + StartDef.NPos; if ( StartDef.NTot > MAXTUPLES ) { printf("Training Set Size exceeds tuple limit: "); printf("%d > %d\n", StartDef.NTot, MAXTUPLES); printf("Rerun with larger MAXTUPLES to proceed further\n"); exit(0); } StartDef.Tuples = Alloc(StartDef.NTot+1, Tuple); i = 0; for ( Scan = R->Pos ; *Scan ; Scan++ ) { AddTuple(i, *Scan, TupleArity, PosMark); i++; } for ( Scan = R->Neg ; *Scan ; Scan++ ) { AddTuple(i, *Scan, TupleArity, 0); i++; } } else { /* Negative tuples not already defined */ /* Find maximum training set size */ ForEach(j, 1, R->Arity) { if ( R->TypeRef[j]->Continuous ) Error(6, R->Name, Nil); WorldSize *= R->TypeRef[j]->NValues; } Remaining = WorldSize - (StartDef.NPos - R->PosDuplicates); AllTuples = Remaining + StartDef.NPos; NegTuples = SAMPLE * Remaining; if ( SAMPLE < 0.99 ) { AdjMinAccuracy = MINACCURACY / (MINACCURACY + SAMPLE * (1-MINACCURACY)); Verbose(1) { printf("\t\t(Adjusted minimum clause accuracy %.1f%%)\n", 100*AdjMinAccuracy); } } StartDef.NTot = StartDef.NPos + NegTuples; if ( StartDef.NTot > MAXTUPLES ) { printf("Training Set Size will exceed tuple limit: "); printf("%d > %d\n", StartDef.NPos + NegTuples, MAXTUPLES); printf("Rerun with larger MAXTUPLES to proceed further\n"); printf("(or use smaller sample of negative tuples).\n"); exit(0); } StartDef.Tuples = Alloc(StartDef.NTot+1, Tuple); /* Copy positive tuples */ i = 0; for ( Scan = R->Pos ; *Scan ; Scan++ ) { AddTuple(i, *Scan, TupleArity, PosMark); i++; } if ( WorldSize <= 10*MAXTUPLES ) { /* Enumerate all possible tuples and add a sample of the negative tuples to the training set - note that if SAMPLE is 1, the default, all negative tuples are added to the training set */ Case = Nil; while ( NegTuples && (Case = NextConstTuple(R, Case)) ) { if ( ! Join(R->Pos, R->PosIndex, DefaultVars, Case, R->Arity, true) && drand48() <= NegTuples / (float) Remaining-- ) { AddTuple(i, Case, TupleArity, 0); i++; NegTuples--; } } if ( Case ) pfree(Case); } else { /* Might take too long to enumerate all tuples, so generate them randomly - can result in duplicate negative tuples */ Case = Alloc(TupleArity, Const); while ( i < StartDef.NTot ) { RandomTuple(R, Case); if ( ! Join(R->Pos, R->PosIndex, DefaultVars, Case, R->Arity, 1)) { AddTuple(i, Case, TupleArity, 0); i++; } } pfree(Case); } } StartDef.Tuples[StartDef.NTot] = Nil; StartDef.NOrigPos = StartDef.NPos; StartDef.NOrigTot = StartDef.NTot; Realloc(Flags, StartDef.NTot+1, char); StartDef.BaseInfo = Info(StartDef.NPos, StartDef.NTot); } void AddTuple(int N, Tuple T, int TupleArity, int Mark) /* -------- */ { StartDef.Tuples[N] = Alloc(TupleArity, Const); memcpy(StartDef.Tuples[N], T, TupleArity*sizeof(Const)); StartDef.Tuples[N][0] = N | Mark; } /* Generate in Case the next constant tuple taking note of type constraints */ Tuple NextConstTuple(Relation R, Tuple Case) /* -------------- */ { int i, v; TypeInfo T; if ( ! Case ) { Case = Alloc(R->Arity+1, Const); ForEach(i, 1, R->Arity) { Case[i] = R->TypeRef[i]->Value[0]; } } else { i = R->Arity; T = R->TypeRef[i]; while ( Case[i] == T->Value[T->NValues-1] ) { if ( i <= 1 ) { pfree(Case); return Nil; } Case[i] = T->Value[0]; T = R->TypeRef[--i]; } for ( v = 1; Case[i] != T->Value[v-1] ; v++ ) ; Case[i] = T->Value[v]; } return Case; } /*****************************************************************************/ /* */ /* RandomTuple - generate a random tuple satisfying type constraints for */ /* relation R */ /* */ /*****************************************************************************/ void RandomTuple(Relation R, Tuple Result) /* ----------- */ { int i, v; TypeInfo T; double drand48(); ForEach(i, 1, R->Arity) { T = R->TypeRef[i]; v = (int)(T->NValues * drand48()); Result[i] = T->Value[v]; } } void NewState(Literal L, int NewSize) /* -------- */ { FormNewState(L->Rel, L->Sign, L->Args, NewSize); AcceptNewState(L->Rel, L->Args, NewSize); } /* Construct new state in New */ void FormNewState(Relation R, Boolean RSign, Var *A, int NewSize) /* ------------ */ { Tuple *TSP, Case, *Bindings, Instance; int i, N, RN; Boolean BuiltIn=false, Match, NotNegated; Const X2; if ( Predefined(R) ) { /* Prepare for calls to Satisfies() */ BuiltIn = true; RN = (int) R->Pos; if ( HasConst(R) ) { GetParam(&A[2], &X2); } else { X2 = A[2]; } } N = R->Arity; /* Find highest variable in new clause */ New.MaxVar = Current.MaxVar; if ( RSign ) { ForEach(i, 1, N) { New.MaxVar = Max(A[i], New.MaxVar); } } New.Tuples = Alloc(NewSize+1, Tuple); New.NPos = New.NTot = 0; for ( TSP = Current.Tuples ; Case = *TSP++ ; ) { if ( MissingValue(R,A,Case) ) continue; Match = ( BuiltIn ? Satisfies(RN, A[1], X2, Case) : Join(R->Pos, R->PosIndex, A, Case, N, ! RSign) ); NotNegated = RSign != 0; if ( Match != NotNegated ) continue; if ( ! BuiltIn && RSign ) { /* Add tuples from R->Pos */ CheckSize(New.NTot, NFound, &NewSize, &New.Tuples); Bindings = Found; while ( Instance = *Bindings++ ) { New.Tuples[New.NTot] = Extend(Case, Instance, A, N); New.NTot++; if ( Positive(Case) ) New.NPos++; } } else { CheckSize(New.NTot, 1, &NewSize, &New.Tuples); New.Tuples[New.NTot] = Alloc(New.MaxVar+1, Const); memcpy(New.Tuples[New.NTot], Case, (New.MaxVar+1)*sizeof(Const)); New.NTot++; if ( Positive(Case) ) New.NPos++; } } New.Tuples[New.NTot] = Nil; } /* Move state in New to Current */ void AcceptNewState(Relation R, Var *A, int NewSize) /* -------------- */ { int i, N, MaxDepth=0; Var V; if ( Current.Tuples != StartClause.Tuples ) { FreeTuples(Current.Tuples, true); } if ( New.MaxVar > Current.MaxVar ) { /* New variable(s) - update type and depth info */ N = R->Arity; ForEach(i, 1, N) { if ( (V = A[i]) <= Current.MaxVar ) { MaxDepth = Max(MaxDepth, Variable[V]->Depth); } } MaxDepth++; ForEach(i, 1, N) { if ( (V = A[i]) > Current.MaxVar ) { Variable[V]->Type = R->Type[i]; Variable[V]->TypeRef = R->TypeRef[i]; Variable[V]->Depth = MaxDepth; } } } New.BaseInfo = Info(New.NPos, New.NTot); /* Move all information across and resize tuples if necessary */ Current = New; if ( New.NTot < NewSize ) { Realloc(Current.Tuples, Current.NTot+1, Tuple); } Current.BaseInfo = Info(Current.NPos, Current.NTot); } /* Rebuild a training set by applying the literals in a clause to the copy of the training set */ void RecoverState(Clause C) /* ------------ */ { int i, SaveVerbosity; Literal L; float ExtraBits; /* Turn off messages during recovery */ SaveVerbosity = VERBOSITY; VERBOSITY = 0; if ( Current.Tuples != StartClause.Tuples ) { FreeTuples(Current.Tuples, true); Current = StartClause; } ForEach(i, 1, Target->Arity) { memset(PartialOrder[i], '#', MAXVARS+1); PartialOrder[i][i] = '='; } AnyPartialOrder = false; memset(Barred, false, MAXVARS+1); NRecLitClause = NDetLits = ClauseBits = 0; for ( NLit = 0 ; (L = C[NLit]) ; NLit++ ) { NewClause[NLit] = L; if ( L->Rel == Target ) { ExamineVariableRelationships(); AddOrders(L); } NewState(L, Current.NTot); if ( L->Sign == 2 ) { NDetLits++; } else { ExtraBits = L->Bits - Log2(NLit+1.001-NDetLits); ClauseBits += Max(0, ExtraBits); } if ( L->Rel == Target ) NoteRecursiveLit(L); NWeakLits = L->WeakLits; } NewClause[NLit] = Nil; VERBOSITY = SaveVerbosity; } void CheckSize(int SoFar, int Extra, int *NewSize, Tuple **TSAddr) /* --------- */ { if ( SoFar+Extra > *NewSize ) { *NewSize += Max(Extra, 1000); Realloc(*TSAddr, *NewSize+1, Tuple); } } /* Tack extra variables on a tuple */ Tuple Extend(Tuple Case, Tuple Binding, Var *A, int N) /* ------ */ { Tuple NewCase; int i; NewCase = Alloc(New.MaxVar+1, Const); memcpy(NewCase, Case, (Current.MaxVar+1)*sizeof(Const)); ForEach(i, 1, N) { NewCase[A[i]] = Binding[i]; } return NewCase; } void CheckOriginalCaseCover() /* ---------------------- */ { Tuple *TSP, Case; ClearFlags; Current.NOrigPos = Current.NOrigTot = 0; for ( TSP = Current.Tuples ; Case = *TSP++ ; ) { if ( ! TestFlag(Case[0]&Mask, TrueBit) ) { SetFlag(Case[0]&Mask, TrueBit); Current.NOrigTot++; if ( Positive(Case) ) Current.NOrigPos++; } } } /* Free up a bunch of tuples */ void FreeTuples(Tuple *TT, Boolean TuplesToo) /* ------- */ { Tuple *P; if ( TuplesToo ) { for ( P = TT ; *P ; P++ ) { pfree(*P); } } pfree(TT); } /* Find log (base 2) factorials using tabulated values and Stirling's approximation (adjusted) */ double Log2Fact(int n) /* -------- */ { return ( n < 1000 ? LogFact[n] : (n+0.5) * Log2(n) - n * Log2e + Log2sqrt2Pi - (n*0.7623)/820000 ); } /******************************************************************************/ /* */ /* Examine the space of possible literals on a relation */ /* */ /******************************************************************************/ #define MAXTIME 100 Var *Arg = Nil; /* potential arguments */ Boolean CountOnly; float StartTime; /* CPU time at start of literal */ int Ticks, /* calls of TryArgs() */ TicksCheck; /* point to check time again */ /* Examine possible variable assignments for next literal using relation R. If CountOnly specified, this will only set the number of them in R->NTrialArgs; otherwise, it will evaluate the possible arguments */ void ExploreArgs(Relation R, Boolean CountFlag) /* ----------- */ { int MaxArgs=1; Var V; CountOnly = CountFlag; if ( CountOnly ) { R->NTrialArgs = 0; } else { R->NTried = 0; } if ( R == Target && ! AnyPartialOrder ) return; if ( Predefined(R) ) { if ( R == EQVAR ) { ExploreEQVAR(); } else if ( R == EQCONST ) { ExploreEQCONST(); } else if ( R == GTVAR ) { ExploreGTVAR(); } else if ( R == GTCONST ) { ExploreGTCONST(); } return; } if ( CountOnly ) { /* Carry out a preliminary feasibility check */ for ( V = 1 ; MaxArgs <= 1E7 && V <= R->Arity ; V++ ) { MaxArgs *= EstimatePossibleArgs(R->Type[V]); } if ( MaxArgs > 1E7 ) { Verbose(2) { printf("\t\t\t\t[%s: too many possibilities]\n", R->Name); } R->NTrialArgs = 0; return; } } else { Ticks = 0; TicksCheck = 10; StartTime = CPUTime(); } TryArgs(R, 1, Current.MaxVar, 0, 0, 0, true, false); } int EstimatePossibleArgs(int TNo) /* -------------------- */ { int Sum=1, V; ForEach(V, 1, Current.MaxVar) { if ( Compatible[Variable[V]->Type][TNo] ) Sum++; } return Sum; } /* Determine whether a key is acceptable for the relation being explored. Note that keys are packed bit strings with a 1 wherever there is an unbound variable */ Boolean AcceptableKey(Relation R, int Key) /* ------------- */ { int i; if ( ! R->NKeys ) return true; ForEach(i, 0, R->NKeys-1) { if ( (R->Key[i] | Key) == R->Key[i] ) return true; } return false; } /* See whether a potential literal is actually a repeat of a literal already in the clause (with perhaps different free variables) */ Boolean Repetitious(Relation R, Var *A) /* ----------- */ { Literal L; Var V, MaxV; int i, a, N; MaxV = Target->Arity; ForEach(i, 0, NLit-1) { L = NewClause[i]; if ( L->Rel == R && SameArgs(R->Arity, A, Current.MaxVar, L->Args, MaxV, i+1) ) { return true; } if ( L->Sign ) { N = L->Rel->Arity; ForEach(a, 1, N) { if ( (V = L->Args[a]) > MaxV ) MaxV = V; } } } return false; } Boolean Mentioned(Var V, int First) /* --------- */ { int i, a, N; Literal L; ForEach(i, First, NLit-1) { L = NewClause[i]; N = L->Rel->Arity; ForEach(a, 1, N) { if ( L->Args[a] == V ) return true; } } return false; } /* Check whether two aruments are identical up to substitution of free variables */ Boolean SameArgs(int N, Var *A1, int MV1, Var *A2, int MV2, int LN) /* -------- */ { int a; ForEach(a, 1, N) { if ( ( A1[a] <= MV1 ? A2[a] != A1[a] : ( A2[a]-MV2 != A1[a]-MV1 || Mentioned(A2[a], LN) ) ) ) { return false; } } return true; } /* Find arguments for predefined relations */ void ExploreEQVAR() /* ------------ */ { Var V, W; ForEach(V, 1, Current.MaxVar-1) { if ( Barred[V] ) continue; Arg[1] = V; ForEach(W, V+1, Current.MaxVar) { if ( Barred[W] ) continue; if ( Compatible[Variable[V]->Type][Variable[W]->Type] ) { if ( CountOnly ) { EQVAR->NTrialArgs++; } else { Arg[2] = W; EvaluateLiteral(EQVAR, Arg, EQVAR->Bits, Nil); EQVAR->NTried++; } } } } } void ExploreEQCONST() /* -------------- */ { Var V; int T, i, n; Const C; Boolean *VarBound; Literal L; /* Find variables that have bound values */ VarBound = AllocZero(Current.MaxVar+1, Boolean); ForEach(i, 0, NLit-1) { L = NewClause[i]; if ( L->Rel == EQCONST && L->Sign ) { VarBound[L->Args[1]] = true; } } ForEach(V, 1, Current.MaxVar) { if ( Barred[V] || VarBound[V] ) continue; T = Variable[V]->Type; if ( n = Type[T]->NTheoryConsts ) { Arg[1] = V; ForEach(i, 0, n-1) { if ( CountOnly ) { EQCONST->NTrialArgs++; } else { C = Type[T]->TheoryConst[i]; SaveParam(&Arg[2], &C); EvaluateLiteral(EQCONST, Arg, EQCONST->Bits, Nil); EQCONST->NTried++; } } } } free(VarBound); } void ExploreGTVAR() /* ------------ */ { Var V, W; ForEach(V, 1, Current.MaxVar-1) { if ( Barred[V] || ! Variable[V]->TypeRef->Continuous ) continue; Arg[1] = V; ForEach(W, V+1, Current.MaxVar) { if ( Barred[W] || Variable[W]->Type != Variable[V]->Type ) continue; if ( CountOnly ) { GTVAR->NTrialArgs++; } else { Arg[2] = W; EvaluateLiteral(GTVAR, Arg, GTVAR->Bits, Nil); GTVAR->NTried++; } } } } void ExploreGTCONST() /* -------------- */ { Var V; float Z=MISSING_FP; ForEach(V, 1, Current.MaxVar) { if ( Barred[V] || ! Variable[V]->TypeRef->Continuous ) continue; if ( CountOnly ) { GTCONST->NTrialArgs++; } else { Arg[1] = V; SaveParam(&Arg[2], &Z); EvaluateLiteral(GTCONST, Arg, GTCONST->Bits, Nil); GTCONST->NTried++; } } } /* Generate argument lists starting from position This. In the partial argument list Arg[1]..Arg[This-1], HiVar is the highest variable (min value MaxVar) FreeVars is the number of free variable occurrences MaxDepth is the highest depth of a bound variable Key gives the key so far TryMostGeneral is true when we need to fill all remaining argument positions with new free variables. RecOK is true when a more general argument list has been found to satisfy RecursiveCallOK(), so this must also. Return false if hit time limit. */ Boolean TryArgs(Relation R, int This, int HiVar, int FreeVars, int MaxDepth, int Key, Boolean TryMostGeneral, Boolean RecOK) /* ------- */ { Var V, W, MaxV; Boolean Prune, UselessSameVar; int NewFreeVars, NewMaxDepth, CopyKey; float TimeSpent; /* This version contains a time cutout to prevent too much effort begin invested in a single literal. Unfortunately, direct monitoring of time is too expensive (in system time and overhead) so a more circuitous method that calls CPUTime() rarely is used */ if ( ! CountOnly ) { if ( Ticks > TicksCheck ) { if ( (TimeSpent = CPUTime() - StartTime) > MAXTIME ) { return false; } else if ( TimeSpent > 0.001 * MAXTIME ) { TicksCheck += 0.01 * Ticks * MAXTIME / TimeSpent; } else { TicksCheck *= 10; } } Ticks++; } /* Try with all remaining positions (if any) as new free variables */ NewFreeVars = R->Arity - This + 1; if ( TryMostGeneral && HiVar + NewFreeVars <= MAXVARS /* enough variables */ && FreeVars < This-1 /* at least one bound */ && ( ! NewFreeVars || MaxDepth < MAXVARDEPTH ) ) { CopyKey = Key; ForEach(V, This, R->Arity) { Arg[V] = W = HiVar + (V - This + 1); CopyKey |= 1<Type = R->Type[V]; Variable[W]->TypeRef = R->TypeRef[V]; } if ( AcceptableKey(R, CopyKey) && ( R != Target || RecOK || (RecOK = RecursiveCallOK(Arg)) ) ) { if ( CountOnly ) { R->NTrialArgs++; } else if ( ! Repetitious(R, Arg) ) { EvaluateLiteral(R, Arg, R->Bits, &Prune); R->NTried++; if ( Prune && NewFreeVars ) { Verbose(3) printf("\t\t\t\t(pruning subsumed arguments)\n"); return true; } } } } if ( This > R->Arity ) return true; /* Now try substitutions recursively */ MaxV = ( Predefined(R) ? HiVar : This < R->Arity && HiVar < MAXVARS ? HiVar+1 : HiVar ); for ( V = 1 ; V <= MaxV && BestLitGain < MaxPossibleGain ; V++ ) { if ( V <= Current.MaxVar ) { if ( Barred[V] ) continue; NewMaxDepth = Max(MaxDepth, Variable[V]->Depth); NewFreeVars = FreeVars; } else { NewMaxDepth = MaxDepth; NewFreeVars = FreeVars+1; } if ( V > HiVar ) { Variable[V]->Type = R->Type[This]; Variable[V]->TypeRef = R->TypeRef[This]; Key |= 1<ArgNotEq[ ArgPair(This,W) ]; } if ( UselessSameVar || V <= HiVar && ! Compatible[Variable[V]->Type][R->Type[This]] || NewMaxDepth + (NewFreeVars > 0) > MAXVARDEPTH || R->BinSym && This == 2 && V < Arg[1] ) { continue; } Arg[This] = V; if ( ! TryArgs(R, This+1, Max(HiVar, V), NewFreeVars, NewMaxDepth, Key, V <= HiVar, RecOK) ) return false; } return true; } /******************************************************************************/ /* */ /* This group of routines has responsibility for evaluating a proposed */ /* literal. There are many aspects that are checked simultaneously: */ /* */ /* * whether the literal is determinate */ /* * whether this literal would result in a completed clause */ /* * whether this literal would produce too many tuples */ /* * pruning, both of this literal and of any specialisations of it */ /* * new variables that duplicate existing variables */ /* - for all tuples */ /* - for pos tuples (determinate literals) */ /* * all new variables being bound to constants on pos tuples */ /* * gain computation (including weak literal sequence check) */ /* * adjusting records of best literals so far */ /* */ /* The principles underlying this routine are: */ /* */ /* * No literal may introduce a variable that duplicates an existing */ /* variable (since the same effect could be obtained with a more */ /* specific literal). */ /* * No determinate literal may introduce a new variable that is */ /* the same as an existing variable on pos tuples (since the more */ /* specific literal would also be determinate). */ /* * Exploration of a literal can cease as soon as it is clear that */ /* the literal will not be used. In some cases, it is also possible*/ /* to exclude other literals subsumed by this. Such pruning is */ /* tied to the calculation of gain and determinacy, and would need */ /* to be altered if these are changed. */ /* */ /* The various counts have components with the following meanings: */ /* */ /* Pos pos tuples */ /* Neg neg tuples */ /* Tot all tuples */ /* */ /* T pertaining to the unnegated literal R(A) */ /* F pertaining to ~R(A) */ /* M missing value (so neither) */ /* */ /* Now number of tuples in current state */ /* Orig number of tuples in original state */ /* New referring to state if use R(A) or ~R(A) */ /* */ /******************************************************************************/ int OrigTPos, /* orig pos tuples with extensions, R(A) */ OrigTTot, OrigFPos, /* ditto, ~R(A) */ OrigFTot, NowTPos, /* current pos tuples with extensions, R(A) */ NowTTot, NowFPos, /* ditto, ~R(A); NewFPos is identical */ NowFNeg, NowFTot, /* calculated for brevity at end */ NowMPos, /* pos tuples with missing values */ NowMTot, /* pos tuples with missing values */ NewTPos, /* pos tuples in new state, R(A) */ NewTTot, NNewVars, /* number of unbound vars in R(A) */ NConstVars, /* number of constant pseudo-vars */ NDuplicateVars, /* number of duplications so far */ NArgs, /* number of relation arguments */ BestCover, /* coverage of best saveable clause */ MinSaveableCover, /* min coverage if clause saveable */ MaxFPos, PossibleCuts; Var *OldVar, /* old var possibly equal to a new var */ *NewVarPosn, /* argument number of new var */ *ConstVarPosn; /* new vars with unchanging values */ Tuple FirstBinding; /* check for consts masquerading as new vars */ Boolean Allocate = true, NegatedLiteralOK, /* ~R(A) permissible */ *DifferOnNegs, /* corresponding pair not identical */ *FirstOccurrence, /* first time variable appears in args */ PossibleT, /* R(A) is a candidate */ PossibleF, /* ~R(A) is a candidate */ Determinate; /* R(A) is determinate */ float MinUsefulGain, /* min gain to affect outcome */ MinPos, /* min pos tuples to achieve MinUsefulGain */ BestAccuracy, /* accuracy of best saveable clause */ MaxFNeg, /* max FNeg tuples to avoid pruning ~R(A) */ NewClauseBits; /* if add literal to clause */ /* Examine literals R(A) and ~R(A) (if appropriate) */ void EvaluateLiteral(Relation R, Var *A, float LitBits, Boolean *Prune) /* --------------- */ { Boolean Abandoned, RealDuplicateVars=false, WeakT, WeakF, SavedSign; Var V, W; int i, j, Coverage, Size; float PosGain, NegGain, Gain, CurrentRatio, Accuracy, Extra; Verbose(3) { putchar('\t'); PrintComposedLiteral(R, true, A); } if ( Prune ) *Prune = false; Extra = LitBits - Log2(NLit+1.001-NDetLits); NewClauseBits = ClauseBits + Max(0, Extra); PrepareForScan(R, A); if ( R == GTCONST ) { /* Find best threshold and counts in one go */ FindThreshold(A); if ( PossibleCuts > 0 ) LitBits += Log2(PossibleCuts); Determinate = Abandoned = false; NDuplicateVars = NConstVars = 0; } else if ( (Abandoned = TerminateScan(R, A)) && NewTTot <= MAXTUPLES /* not because out of room for tuples */ && NNewVars /* new vars, so potential for pruning */ && Current.NPos - (NowFPos+NowMPos) < MinPos /* R(A) has insuff gain */ ) { /* Check for possible pruning of more specific literals */ if ( NegatedLiteralOK ) { /* A more specific ~R(A) will match more tuples. In order to prune, we must be sure that the current ~R(A) matches enough neg tuples to ensure that the gain is not interesting. Assume all pos tuples other than those known to have missing values would be matched by a more specific ~R(A) */ MaxFPos = Current.NPos - NowMPos; MaxFNeg = NegThresh(MaxFPos, MaxFPos); CheckForPrune(R, A); *Prune = NowFNeg > MaxFNeg; } else { /* Can prune only when a more specific literal than R(A) could not be saveable */ *Prune = OrigTPos < MinSaveableCover; } } NowFTot = NowFPos + NowFNeg; PossibleT &= NowTPos > 0; PossibleF &= NowFPos > 0; Verbose(3) { printf(" %d[%d/%d]", NowTPos, NewTPos, NewTTot); if ( NegatedLiteralOK || Abandoned ) { printf(" [%d/%d]", NowFPos, NowFTot); } printf(" "); } if ( Abandoned ) { Verbose(3) { printf(" abandoned"); if ( OutOfWorld ) printf(" ^"); printf("(%d%%)\n", (100 * (NowTTot+NowFTot+NowMTot)) / Current.NTot); } return; } ForEach(i, 0, NDuplicateVars-1) { V = A[ NewVarPosn[i] ]; W = OldVar[i]; if ( W > Current.MaxVar ) W = A[ W-Current.MaxVar ]; /* special */ if ( NowTPos || ! DifferOnNegs[i] ) { Verbose(3) printf(" %s%s%s", Variable[W]->Name, ( DifferOnNegs[i] ? "=+" : "=" ), Variable[V]->Name); } RealDuplicateVars |= ! DifferOnNegs[i]; } Verbose(3) { if ( NewTPos > 1 ) { ForEach(i, 0, NConstVars-1) { V = A[ j=ConstVarPosn[i] ]; printf(" %s=", Variable[V]->Name); if ( Variable[V]->TypeRef->Continuous ) { printf("%g", FP(FirstBinding[j])); } else { printf("%s", ConstName[FirstBinding[j]]); } } } } if ( Determinate ) { /* Check whether determinacy has been violated */ Determinate = ! NDuplicateVars && NConstVars < NNewVars; Verbose(3) printf(" [%s]", Determinate ? "Det" : "XDet"); } /* Now assess gain if applicable. Any literal that introduces a duplicate variable is unacceptable (the more specific literal would give the same result. A literal R(A) that introduces a new variable that replicates an existing variable on pos tuples is also excluded -- the more specific literal would match the same number of pos tuples and perhaps fewer neg tuples */ PossibleT &= ! NDuplicateVars; if ( RealDuplicateVars || ( ! PossibleT && ! PossibleF ) ) { Verbose(3) printf(" #\n"); return; } /* Due to arithmetic roundoff, ratios rather than gain are used to detect weak literals */ CurrentRatio = Current.NPos/(float) Current.NTot; if ( PossibleT ) { if ( OrigTPos == OrigTTot && OrigTPos == StartClause.NPos ) { PosGain = MaxPossibleGain; } else { PosGain = Worth(NowTPos, NewTPos, NewTTot, NNewVars-NConstVars); } WeakT = NowFTot <= 0 || NewTPos / (NewTTot+1E-3) <= 0.9999 * CurrentRatio; } else { PosGain = 0.0; } if ( PossibleF ) { if ( OrigFPos == OrigFTot && OrigFPos == StartClause.NPos ) { NegGain = MaxPossibleGain; } else { NegGain = Worth(NowFPos, NowFPos, NowFTot, 0); } WeakF = NowTTot <= 0 || NowFPos / (NowFTot+1E-3) <= 0.9999 * CurrentRatio; } else { NegGain = 0.0; } Verbose(3) { printf(" gain %.1f", PosGain); if ( NegatedLiteralOK ) printf(",%.1f", NegGain); } /* Weak literal sequence check */ if ( NWeakLits >= MAXWEAKLITS && ! Determinate && ( ! PossibleT || WeakT ) && ( ! PossibleF || WeakF ) ) { Verbose(3) printf(" (weak)\n"); return; } Verbose(3) putchar('\n'); /* Would the addition of this literal to the clause create the best saved clause so far? */ if ( PossibleT && ( ! PossibleF || OrigTPos / (float) OrigTTot > OrigFPos / (float) OrigFTot ) ) { SavedSign = 1; Accuracy = OrigTPos / (float) OrigTTot; Coverage = OrigTPos; } else if ( PossibleF ) { SavedSign = 0; Accuracy = OrigFPos / (float) OrigFTot; Coverage = OrigFPos; } else { Accuracy = 0; } if ( Accuracy >= AdjMinAccuracy-1E-3 && ( Accuracy > BestAccuracy || Accuracy == BestAccuracy && Coverage > BestCover ) ) { if ( ! AlterSavedClause ) { AlterSavedClause = AllocZero(1, struct _poss_lit_rec); } AlterSavedClause->Rel = R; AlterSavedClause->Sign = SavedSign; AlterSavedClause->Bits = LitBits; AlterSavedClause->WeakLits = 0; AlterSavedClause->TotCov = ( SavedSign ? OrigTTot : OrigFTot ); AlterSavedClause->PosCov = ( SavedSign ? OrigTPos : OrigFPos ); Size = R->Arity+1; if ( HasConst(R) ) Size += sizeof(Const) / sizeof(Var); AlterSavedClause->Args = Alloc(Size, Var); memcpy(AlterSavedClause->Args, A, Size*sizeof(Var)); } /* Compute gains and save if appropriate */ Gain = Max(PosGain, NegGain); if ( Determinate && Gain < DETERMINATE * MaxPossibleGain && GoodDeterminateLiteral(R, A, LitBits) ) { return; } if ( PosGain > 1E-3 && ( ! SavedClause || SavedClauseAccuracy < .999 || ! WeakT ) ) { ProposeLiteral(R, true, A, NowTTot, LitBits, OrigTPos, OrigTTot, PosGain, WeakT); } if ( NegGain > 1E-3 && ( ! SavedClause || SavedClauseAccuracy < .999 || ! WeakF ) ) { ProposeLiteral(R, false, A, NowFTot, LitBits, OrigFPos, OrigFTot, NegGain, WeakF); } } /* Initialise variables for scan. NOTE: this assumes that Current.BaseInfo and MaxPossibleGain have been set externally. */ void PrepareForScan(Relation R, Var *A) /* -------------- */ { int i, j, PossibleVarComps; Var V, W, VP; /* First time through, allocate arrays */ if ( Allocate ) { Allocate = false; PossibleVarComps = MAXARGS * MAXVARS + (MAXARGS * (MAXARGS-1) / 2); OldVar = Alloc(PossibleVarComps, Var); NewVarPosn = Alloc(PossibleVarComps, Var); ConstVarPosn = Alloc(MAXARGS+1, Var); DifferOnNegs = Alloc((MAXARGS+1)*(MAXVARS+1), Boolean); FirstOccurrence = Alloc(MAXVARS+MAXARGS, Boolean); FirstBinding = Alloc(MAXARGS+1, Const); } OrigTPos = 0; OrigTTot = 0; OrigFPos = 0; OrigFTot = 0; NowTPos = 0; NowTTot = 0; NowFPos = 0; NowFNeg = 0; NowMPos = 0; NowMTot = 0; NewTPos = 0; NewTTot = 0; NDuplicateVars = NNewVars = NConstVars = 0; NArgs = R->Arity; memset(FirstOccurrence, true, Current.MaxVar+NArgs); OutOfWorld = false; ForEach(i, 1, NArgs) { if ( (V = A[i]) > Current.MaxVar && FirstOccurrence[V] ) { NNewVars++; FirstOccurrence[V] = false; ConstVarPosn[NConstVars++] = i; ForEach(W, 1, Current.MaxVar) { if ( ! Compatible[Variable[W]->Type][R->Type[i]] ) continue; NewVarPosn[NDuplicateVars] = i; OldVar[NDuplicateVars] = W; DifferOnNegs[NDuplicateVars] = false; NDuplicateVars++; } } } /* New variables shouldn't replicate each other, either */ ForEach(i, 0, NConstVars-2) { VP = ConstVarPosn[i]; V = A[VP]; ForEach(j, i+1, NConstVars-1) { W = ConstVarPosn[j]; if ( ! Compatible[Variable[V]->Type][R->Type[W]] ) continue; NewVarPosn[NDuplicateVars] = W; OldVar[NDuplicateVars] = Current.MaxVar+VP; /* special */ DifferOnNegs[NDuplicateVars] = false; NDuplicateVars++; } } ClearFlags; PossibleT = true; PossibleF = NegatedLiteralOK = ( NEGLITERALS || R == GTVAR || R == GTCONST || ( NEGEQUALS && ( R == EQVAR || R == EQCONST ) ) ); Determinate = NNewVars > 0; /* 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; } /* Set thresholds for pos tuples */ MinPos = MinUsefulGain / Current.BaseInfo - 0.001; /* Now check coverage required for a saveable clause that would pass the MDL criterion. Don't worry about long saveable clauses. */ if ( AlterSavedClause ) { BestCover = AlterSavedClause->PosCov; BestAccuracy = BestCover / (float) AlterSavedClause->TotCov; } else { BestCover = SavedClauseCover; BestAccuracy = SavedClauseAccuracy; } if ( NLit < 5 ) { MinSaveableCover = BestCover+1; while ( Encode(MinSaveableCover) <= NewClauseBits ) MinSaveableCover++; } else { MinSaveableCover = StartDef.NPos; } } /* Make a pass through the tuples, terminating if it becomes clear that neither R(A) or ~R(A) can achieve the minimum useful gain. Since all pos tuples appear first in the tuple sets, thresholds for NewTNeg and NowFNeg can be set when the first neg tuple is encountered. */ #define TermTest(Cond, Test)\ if ( Cond && Test && ! Determinate ) {\ Cond = false; if ( ! PossibleT && ! PossibleF ) return true; } Boolean TerminateScan(Relation R, Var *A) /* ------------- */ { Tuple *TSP, Case; Boolean BuiltIn=false, FirstNegTuple=true; int RN, MaxCover, OrigPos=0; Const X2; float NewTNegThresh, NowFNegThresh; if ( Predefined(R) ) { BuiltIn = true; RN = (int) R->Pos; if ( HasConst(R) ) { GetParam(&A[2], &X2); } else { X2 = A[2]; } } for ( TSP = Current.Tuples ; Case = *TSP++ ; ) { if ( FirstNegTuple && ! Positive(Case) ) { /* Encoding length checks */ PossibleT &= Encode(OrigTPos) > NewClauseBits; PossibleF &= Encode(OrigFPos) > NewClauseBits; if ( ! PossibleT && ! PossibleF ) { Verbose(3) { printf(" MDL prune %d,%d", OrigTPos, OrigFPos); } return true; } /* Set thresholds now that NowTPos and NowFPos are known */ NewTNegThresh = ( NNewVars && BestLitGain < 1E-2 ? MAXTUPLES : NegThresh(NowTPos, NewTPos) ); NowFNegThresh = NegThresh(NowFPos, NowFPos); FirstNegTuple = false; } if ( MissingValue(R, A, Case) ) { NowMTot++; if ( Positive(Case) ) NowMPos++; NFound = 0; } else if ( BuiltIn ? Satisfies(RN, A[1], X2, Case) : Join(R->Pos, R->PosIndex, A, Case, NArgs, false) ) { /* R(A) is barred if it would introduce an out-of-world constant. Note: can't use TermTest() since check for Determinate does not matter */ if ( OutOfWorld ) { PossibleT = false; if ( ! PossibleF ) return true; } /* Extensions of this tuple from R(A) */ CheckNewVars(Case); NowTTot++; NewTTot += NFound; TermTest(PossibleT, NewTTot > MAXTUPLES); if ( Positive(Case) ) { NowTPos++; NewTPos += NFound; /* If all remaining pos tuples go to NowFPos, are there sufficient to make ~R(A) viable? Note: do not abandon ~R(A) if it could lead to a saveable clause (assuming all remaining original pos tuples are covered by ~R(A)) */ MaxCover = OrigFPos + (Current.NOrigPos - OrigPos); if ( MaxCover < MinSaveableCover ) { TermTest(PossibleF, Current.NPos - (NowTPos + NowMPos) < MinPos-1E-3); } } else { /* We already know the final number of NewTPos tuples. Are there now enough NewTNeg tuples to make the gain of R(A) insufficient? (Note: since R(A) matches a neg tuple, don't have to worry about saveable clause.) */ TermTest(PossibleT, (NewTTot - NewTPos) > NewTNegThresh+1E-3); } if ( ! TestFlag(Case[0]&Mask, TrueBit) ) { SetFlag(Case[0]&Mask, TrueBit); OrigTTot++; if ( Positive(Case) ) { OrigTPos++; if ( ! TestFlag(Case[0]&Mask, FalseBit) ) OrigPos++; } } } else { if ( Positive(Case) ) { NowFPos++; /* If all remaining pos tuples go to NowTPos, are there sufficient to make R(A) viable? Note: don't kill R(A) if it could lead to a saveable clause when all remaining original pos tuples covered by R(A) */ MaxCover = OrigTPos + (Current.NOrigPos - OrigPos); if ( MaxCover < MinSaveableCover ) { TermTest(PossibleT, Current.NPos - (NowFPos + NowMPos) < MinPos-1E-3); } } else { NowFNeg++; /* We already know the final number of NowFPos tuples. Are there already enough NowFNeg tuples to make the gain of ~R(A) insufficient? (As above saveability not relevant.) */ TermTest(PossibleF, NowFNeg > NowFNegThresh+1E-3); } if ( ! TestFlag(Case[0]&Mask, FalseBit) ) { SetFlag(Case[0]&Mask, FalseBit); OrigFTot++; if ( Positive(Case) ) { OrigFPos++; if ( ! TestFlag(Case[0]&Mask, TrueBit) ) OrigPos++; } } } Determinate &= ( Positive(Case) ? NFound == 1 : NFound <= 1 ); } return false; } /* If there are unbound variables, try to satisfy the pruning criterion for more specific literals. A more specific negated literal will cover more tuples; NowFNeg must be great enough so that, if all positive tuples were covered by ~R(A), the gain would still be too low. */ void CheckForPrune(Relation R, Var *A) /* ------------- */ { Tuple *TSP, Case; int RemainingNeg; RemainingNeg = (Current.NTot - Current.NPos) - (NowMTot - NowMPos) - (NowTTot - NowTPos) - NowFNeg; for ( TSP = Current.Tuples + (NowMTot+NowTTot+NowFPos+NowFNeg) ; Case = *TSP++ ; ) { if ( Positive(Case) || MissingValue(R, A, Case) ) { continue; } if ( ! Join(R->Pos, R->PosIndex, A, Case, NArgs, true) ) { NowFNeg++; /* See if have found enough */ if ( NowFNeg > MaxFNeg ) break; } RemainingNeg--; /* See whether not enough left */ if ( NowFNeg + RemainingNeg <= MaxFNeg ) break; } } /* Check new variables for non-utility, specifically * replicating existing variables on all or pos tuples * all being bound to constants on pos tuples */ void CheckNewVars(Tuple Case) /* ------------ */ { Var P; Const OldVarVal; int i, j, Col; for ( i = 0 ; i < NDuplicateVars ; i++ ) { if ( ! Positive(Case) && DifferOnNegs[i] ) continue; P = OldVar[i]; if ( P <= Current.MaxVar ) OldVarVal = Case[P]; Col = NewVarPosn[i]; for ( j = 0 ; j < NFound ; j++ ) { if ( Found[j][Col] == ( P <= Current.MaxVar ? OldVarVal : Found[j][P-Current.MaxVar] ) ) { continue; } if ( Positive(Case) ) { NDuplicateVars--; for ( j = i ; j < NDuplicateVars ; j++ ) { NewVarPosn[j] = NewVarPosn[j+1]; OldVar[j] = OldVar[j+1]; DifferOnNegs[j] = DifferOnNegs[j+1]; } i--; } else { DifferOnNegs[i] = true; } break; } } /* Check for new vars bound to constants */ if ( NConstVars ) { if ( ! NowTTot ) { memcpy(FirstBinding, Found[0], (NArgs+1)*sizeof(Const)); } ForEach(i, 0, NConstVars-1) { Col = ConstVarPosn[i]; for ( j = 0 ; j < NFound ; j++ ) { if ( FirstBinding[Col] == Found[j][Col] ) continue; NConstVars--; for ( j = i ; j < NConstVars ; j++ ) { ConstVarPosn[j] = ConstVarPosn[j+1]; } i--; break; } } } } /* Compute the maximum number N1 of neg tuples that would allow P1 pos tuples (P orig pos tuples) to give a gain >= threshold. The underlying relation is P * (Current.BaseInfo + log(P1/(P1+N1)) >= MinUsefulGain where N1 is adjusted by the sampling factor. NOTE: This is the inverse of the gain calculation in Worth. If one is changed, the other must be modified accordingly */ float NegThresh(int P, int P1) /* --------- */ { return P <= 0 ? 0.0 : SAMPLE * (P1+1) * (exp(LN2 * (Current.BaseInfo - MinUsefulGain/P)) - 1); } /* Compute aggregate gain from a test on relation R, tuple T. The Basic gain is the number of positive tuples * information gained regarding each; but there is a minor adjustment: - a literal that has some positive tuples and no gain but introduces one or more new variables, is given a slight gain */ float Worth(int N, int P, int T, int UV) /* ----- */ { float G, TG; TG = N * (G = Current.BaseInfo - Info(P, T)); if ( G < 1E-3 && N && UV ) { return 0.0009 + UV * 0.0001; /* very small notional gain */ } else { return TG; } } /* The ratio P/T is tweaked slightly to (P+1)/(T+1) so that, if two sets of tuples have the same proportion of pos tuples, the smaller is preferred. The reasoning is that it is easier to filter out all neg tuples from a smaller set. If you don't like this idea and change it back to P/T, NegThresh must be changed also */ float Info(int P, int T) /* ---- */ { /* Adjust total T to take account of sampling */ T = (int)((float)(T-P) / SAMPLE) + P; return Log2(T+1) - Log2(P+1); } Boolean MissingVal(Relation R, Var *A, Tuple T) /* ---------- */ { register Var i, V; ForEach(i, 1, R->Arity) { V = A[i]; if ( V <= Current.MaxVar && Unknown(V, T) ) return true; } return false; } Boolean Unknown(Var V, Tuple T) /* ------- */ { return ( Variable[V]->TypeRef->Continuous ? FP(T[V]) == MISSING_FP : T[V] == MISSING_DISC ); } /* See whether a case satisfies built-in relation RN */ Boolean Satisfies(int RN, Const V, Const W, Tuple Case) /* --------- */ { switch ( RN ) { case 0: /* EQVAR */ NFound = ( Case[V] == Case[W] ); break; case 1: /* EQCONST */ NFound = ( Case[V] == W ); break; case 2: /* GTVAR */ NFound = ( FP(Case[V]) > FP(Case[W]) ); break; case 3: /* GTCONST */ NFound = ( FP(Case[V]) > FP(W) ); break; default: exit(0); } return NFound; } /* The following stuff calculates thresholds for GTCONST relations. The pos and neg tuples are sorted separately, then merged. The current value is acceptable as a threshold unless it is in the middle of a run of tuples of the same sign or a run of the same value */ float BestGain, BestThresh; int BestTPos, BestTTot; void FindThreshold(Var *A) /* ------------- */ { Tuple *ScanPos, *ScanNeg, Case; float PosVal, NegVal, ThisVal, PrevVal=(-1E30); Var V; int ThisSign, NextSign, Signs=0, i; V = A[1]; BestGain = -1E10; PossibleCuts = 0; NowMPos = MissingAndSort(V, 0, Current.NPos-1); NowMTot = NowMPos + MissingAndSort(V, Current.NPos, Current.NTot-1); NowTPos = Current.NPos - NowMPos; NowTTot = Current.NTot - NowMTot; ScanPos = &Current.Tuples[NowMPos]; ScanNeg = &Current.Tuples[Current.NPos + (NowMTot - NowMPos)]; PosVal = ( NowTPos ? FP(((*ScanPos)[V])) : 1E30 ); NegVal = ( NowTTot > NowTPos ? FP(((*ScanNeg)[V])) : 1E30 ); while ( NowTTot >= 1 ) { if ( PosVal <= NegVal ) { NowTPos--; NowTTot--; ScanPos++; ThisVal = PosVal; PosVal = ( NowTPos ? FP(((*ScanPos)[V])) : 1E30 ); ThisSign = 1; } else { NowTTot--; ScanNeg++; ThisVal = NegVal; NegVal = ( NowTTot > NowTPos ? FP(((*ScanNeg)[V])) : 1E30 ); ThisSign = 2; } if ( ThisVal == PrevVal ) { Signs |= ThisSign; } else { Signs = ThisSign; PrevVal = ThisVal; PossibleCuts++; } NextSign = ( PosVal == NegVal ? 3 : PosVal < NegVal ? 1 : 2 ); if ( NowTTot && ThisVal != PosVal && ThisVal != NegVal && (Signs | NextSign) == 3 ) { PossibleCut(ThisVal); } } PossibleCuts--; /* Fix up all required counts */ if ( BestGain >= 0 ) { NewTPos = NowTPos = BestTPos; NewTTot = NowTTot = BestTTot; NowFPos = Current.NPos - NowTPos - NowMPos; NowFNeg = (Current.NTot - Current.NPos) - (NowTTot - NowTPos) - (NowMTot - NowMPos); SaveParam(&A[2], &BestThresh); Verbose(3) printf("%g", BestThresh); /* Now determine coverage of original tuples */ ClearFlags; OrigTPos = OrigTTot = OrigFPos = OrigFTot = 0; ForEach(i, 0, Current.NTot-1) { Case = Current.Tuples[i]; ThisVal = FP(Case[V]); if ( ThisVal == MISSING_FP ) continue; if ( ThisVal > BestThresh ) { if ( ! TestFlag(Case[0]&Mask, TrueBit) ) { SetFlag(Case[0]&Mask, TrueBit); OrigTTot++; if ( Positive(Case) ) OrigTPos++; } } else { if ( ! TestFlag(Case[0]&Mask, FalseBit) ) { SetFlag(Case[0]&Mask, FalseBit); OrigFTot++; if ( Positive(Case) ) OrigFPos++; } } } /* Encoding length checks */ PossibleT &= Encode(OrigTPos) > NewClauseBits; PossibleF &= Encode(OrigFPos) > NewClauseBits; } else { NewTPos = NowTPos = Current.NPos; NewTTot = NowTTot = Current.NTot; NowFPos = NowFNeg = 0; PossibleT = PossibleF = false; } } void PossibleCut(float C) /* ----------- */ { float TGain, FGain, Better; TGain = Worth(NowTPos, NowTPos, NowTTot, 0); FGain = Worth(Current.NPos-NowTPos-NowMPos, Current.NPos-NowTPos-NowMPos, Current.NTot-NowTTot-NowMTot, 0); Better = Max(TGain, FGain); if ( Better > BestGain ) { BestGain = Better; BestThresh = C; BestTPos = NowTPos; BestTTot = NowTTot; } } /* Count missing values and sort the remainder */ Tuple Hold; #define Swap(V,A,B) { Hold = V[A]; V[A] = V[B]; V[B] = Hold; } int MissingAndSort(Var V, int Fp, int Lp) /* -------------- */ { int i, Xp; /* Omit and count unknown values */ Xp = Fp; ForEach(i, Fp, Lp) { if ( FP(Current.Tuples[i][V]) == MISSING_FP ) { Swap(Current.Tuples, Xp, i); Xp++; } } Quicksort(Current.Tuples, Xp, Lp, V); return Xp - Fp; } void Quicksort(Tuple *Vec, int Fp, int Lp, Var V) /* --------- */ { register int Middle, i; register float Thresh; if ( Fp < Lp ) { Thresh = FP(Vec[ (Fp+Lp)/2 ][V]); /* Isolate all items with values < threshold */ Middle = Fp; for ( i = Fp ; i <= Lp ; i++ ) { if ( FP(Vec[i][V]) < Thresh ) { if ( i != Middle ) Swap(Vec, Middle, i); Middle++; } } /* Sort the lower values */ Quicksort(Vec, Fp, Middle-1, V); /* Extract all values equal to the threshold */ for ( i = Middle ; i <= Lp ; i++ ) { if ( FP(Vec[i][V]) == Thresh ) { if ( i != Middle ) Swap(Vec, Middle, i); Middle++; } } /* Sort the higher values */ Quicksort(Vec, Middle, Lp, V); } } /******************************************************************************/ /* */ /* Routines to control search. The search for clauses is basically */ /* greedy, but a limited number of alternative possibilities is */ /* kept on hand */ /* */ /******************************************************************************/ Boolean FirstSave; /* flag for printing */ /* 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 */ void ProposeLiteral(Relation R, Boolean TF, Var *A, int Size, float LitBits, int OPos, int OTot, float Gain, Boolean Weak) /* -------------- */ { PossibleLiteral Entry; int i, j, ArgSize; /* See where this literal would go. Other things being equal, prefer an unnegated literal - regarding "<=" as unnegated */ i = NPossible; while ( i > 0 && ( Gain > Possible[i]->Gain + 1E-3 || 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; ArgSize = (R->Arity+1)*sizeof(Var); if ( HasConst(R) ) ArgSize += sizeof(Const); Entry->Gain = Gain; Entry->Rel = R; Entry->Sign = TF; memcpy(Entry->Args, A, ArgSize); Entry->Bits = LitBits; Entry->NewSize = Size; Entry->PosCov = OPos; Entry->TotCov = OTot; Entry->WeakLits = ( Weak ? NWeakLits+1 : 0 ); } /* 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; if ( ! NPossible ) return Nil; FirstSave = true; ForEach(i, 2, NPossible) { if ( Possible[i]->Gain >= MINALTFRAC * Possible[1]->Gain ) { Remember(MakeLiteral(i), Possible[i]->PosCov, Possible[i]->TotCov); } } return MakeLiteral(1); } Literal MakeLiteral(int i) /* ----------- */ { int ArgSize; Literal L; L = AllocZero(1, struct _lit_rec); L->Rel = Possible[i]->Rel; L->Sign = Possible[i]->Sign; L->Bits = Possible[i]->Bits; L->WeakLits = Possible[i]->WeakLits; ArgSize = (L->Rel->Arity+1)*sizeof(Var); if ( HasConst(L->Rel) ) ArgSize += sizeof(Const); L->Args = Alloc(ArgSize, Var); memcpy(L->Args, Possible[i]->Args, ArgSize); 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 */ void Remember(Literal L, int OPos, int OTot) /* -------- */ { int i, j; Alternative Entry; float InfoGain; InfoGain = OPos * (Info(StartClause.NPos, StartClause.NTot) - Info(OPos, OTot)); /* See where this entry would go */ for ( i = NToBeTried ; i && ToBeTried[i]->Value < InfoGain ; i-- ) ; if ( i >= MAXALTS ) { FreeLiteral(L); 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 ) pfree(Entry->UpToHere); Entry->UpToHere = Alloc(NLit+2, Literal); memcpy(Entry->UpToHere, NewClause, (NLit+1)*sizeof(Literal)); Entry->UpToHere[NLit] = L; Entry->UpToHere[NLit+1] = Nil; Entry->Value = InfoGain; Verbose(1) { if ( FirstSave ) { putchar('\n'); FirstSave = false; } printf("\tSave "); PrintLiteral(L); printf(" (%d,%d value %.1f)\n", OPos, OTot, InfoGain); } } Boolean Recover() /* ------- */ { int i; Clause C; Alternative Entry; if ( SavedClause || ! NToBeTried || MAXRECOVERS-- < 1 ) return Nil; Entry = ToBeTried[1]; C = ToBeTried[1]->UpToHere; Verbose(1) { printf("\nRecover to "); PrintClause(Target, C); } ForEach(i, 2, NToBeTried) { ToBeTried[i-1] = ToBeTried[i]; } ToBeTried[NToBeTried] = Entry; NToBeTried--; RecoverState(C); CheckOriginalCaseCover(); ExamineVariableRelationships(); return true; } void FreeLiteral(Literal L) /* ----------- */ { pfree(L->Args); if ( L->ArgOrders ) pfree(L->ArgOrders); pfree(L); } void FreeClause(Clause C) /* ---------- */ { Clause CC; for ( CC = C ; *CC ; CC++ ) { FreeLiteral(*CC); } pfree(C); } /******************************************************************************/ /* */ /* Routines for processing determinate literals */ /* */ /******************************************************************************/ Boolean GoodDeterminateLiteral(Relation R, Var *A, float LitBits) /* ---------------------- */ { int MaxSoFar, PreviousMax, This, i, j; Var V; Literal L; Boolean SensibleBinding=false; /* See whether this determinate literal's bound variables were all bound by determinate literals on the same relation */ ForEach(j, 1, R->Arity) { SensibleBinding |= ( A[j] <= Target->Arity ); } MaxSoFar = Target->Arity; for ( i = 0 ; ! SensibleBinding && i < NLit ; i++ ) { if ( ! NewClause[i]->Sign ) continue; PreviousMax = MaxSoFar; ForEach(j, 1, NewClause[i]->Rel->Arity) { if ( (V = NewClause[i]->Args[j]) > MaxSoFar ) MaxSoFar = V; } if ( NewClause[i]->Rel != R || NewClause[i]->Sign != 2 ) { ForEach(j, 1, R->Arity) { SensibleBinding |= ( A[j] <= MaxSoFar && A[j] > PreviousMax ); } } } if ( ! SensibleBinding ) { Verbose(3) { printf("\tall vars bound by determinate lits on same relation\n"); } return false; } /* Record this determinate literal */ This = NLit + NDeterminate; if ( This && This%100 == 0 ) { Realloc(NewClause, This+100, Literal); } L = NewClause[This] = AllocZero(1, struct _lit_rec); L->Rel = R; L->Sign = 2; L->Bits = LitBits; L->Args = Alloc(R->Arity+1, Var); memcpy(L->Args, A, (R->Arity+1)*sizeof(Var)); NDeterminate++; return true; } void ProcessDeterminateLiterals(Boolean AllWeak) /* -------------------------- */ { int PrevMaxVar, i, j, l, m; Literal L; Var V; Boolean Unique, Changed; PrevMaxVar = Current.MaxVar; Verbose(1) printf("\nDeterminate literals\n"); ForEach(l, 1, NDeterminate) { L = NewClause[NLit++]; Verbose(1) { putchar('\t'); PrintLiteral(L); } Changed = PrevMaxVar != Current.MaxVar; /* Rename free variables */ ForEach(i, 1, L->Rel->Arity) { if ( L->Args[i] > PrevMaxVar ) { L->Args[i] += Current.MaxVar - PrevMaxVar; if ( L->Args[i] > MAXVARS ) { Verbose(1) printf("\t\tno more variables\n"); NLit--; MonitorWeakLits(AllWeak); return; } } } if ( Changed ) { Verbose(1) { printf(" ->"); PrintLiteral(L); } Changed = false; } if ( L->Rel == Target ) AddOrders(L); FormNewState(L->Rel, true, L->Args, Current.NTot); /* Verify that new variables introduced by this determinate literal don't replicate new variables introduced by previous determinate literals. [Note: new variables checked against old variables in EvaluateLiteral() ] */ for ( i = Current.MaxVar+1 ; i <= New.MaxVar ; ) { Unique = true; for ( j = PrevMaxVar+1 ; Unique && j <= Current.MaxVar ; j++ ) { Unique = ! SameVar(i, j); } if ( Unique ) { i++; } else { j--; Verbose(1) { printf(" %s=%s", Variable[i]->Name, Variable[j]->Name); } ShiftVarsDown(i); ForEach(V, 1, L->Rel->Arity) { if ( L->Args[V] == i ) L->Args[V] = j; else if ( L->Args[V] > i ) L->Args[V]--; } Changed = true; } } /* If no variables remain, delete this literal */ if ( Current.MaxVar == New.MaxVar ) { Verbose(1) printf(" (no new vars)"); NLit--; ForEach(m, 1, NDeterminate-l) { NewClause[NLit+m-1] = NewClause[NLit+m]; } FreeTuples(New.Tuples, true); } else { /* This determinate Literal is being kept in the clause */ if ( Changed ) { Verbose(1) { printf(" ->"); PrintLiteral(L); } } AcceptNewState(L->Rel, L->Args, Current.NTot); NDetLits++; if ( L->Rel == Target ) NoteRecursiveLit(L); } Verbose(1) putchar('\n'); } MonitorWeakLits(AllWeak); } /* See whether variable a is always the same as variable b in all positive tuples of the new state */ Boolean SameVar(Var A, Var B) /* ------- */ { Tuple *TSP, Case; for ( TSP = New.Tuples ; Case = *TSP++; ) { if ( Positive(Case) && Case[A] != Case[B] ) return false; } /* If same, delete any negative tuples where different */ for ( TSP = New.Tuples ; Case = *TSP; ) { if ( ! Positive(Case) && Case[A] != Case[B] ) { *TSP = New.Tuples[New.NTot-1]; New.NTot--; New.Tuples[New.NTot] = Nil; } else { TSP++; } } return true; } void ShiftVarsDown(int s) /* ------------- */ { Tuple *TSP, Case; Var V; New.MaxVar--; for ( TSP = New.Tuples ; Case = *TSP++ ; ) { ForEach(V, s, New.MaxVar) { Case[V] = Case[V+1]; } } ForEach(V, s, New.MaxVar) { Variable[V]->Type = Variable[V+1]->Type; Variable[V]->TypeRef = Variable[V+1]->TypeRef; } } /******************************************************************************/ /* */ /* Routines for controlling recursive definitions. The basic idea */ /* is to keep track of partial orders between variables (using */ /* either predefined or discovered constant orders) and to ensure */ /* that there is an ordering of all recursive literals that will */ /* guarantee termination. See Cameron-Jones and Quinlan, IJCAI'93 */ /* */ /******************************************************************************/ /* Examine relationships among variables: LHSVar <,=,>,# anyvar and anyvar = anyvar */ void ExamineVariableRelationships() /* ---------------------------- */ { Var V, W; Const VVal, WVal; Ordering X, ThisX; Tuple *Scan, Case; int *TypeOrder; Boolean FirstTime=true; /* First reset all partial orders */ ForEach(V, 1, Target->Arity) { memset(PartialOrder[V], '#', Current.MaxVar+1); PartialOrder[V][V] = '='; } ForEach(V, 1, Current.MaxVar-1) { if ( Variable[V]->TypeRef->Continuous ) continue; if ( V <= Target->Arity ) { TypeOrder = Target->TypeRef[V]->CollSeq; } ForEach(W, V+1, Current.MaxVar) { if ( Variable[W]->TypeRef->Continuous || ! Compatible[Variable[V]->Type][Variable[W]->Type] ) continue; for ( X = 0, Scan = Current.Tuples ; X != '#' && *Scan ; Scan++ ) { Case = *Scan; if ( (VVal = Case[V]) == (WVal = Case[W]) ) { ThisX = '='; } else if ( V > Target->Arity || ! Variable[V]->TypeRef->Ordered || ! Variable[W]->TypeRef->Ordered ) { ThisX = '#'; } else { ThisX = ( TypeOrder[VVal] < TypeOrder[WVal] ? '<' : '>' ); } if ( ! X ) { X = ThisX; } else if ( X != ThisX ) { X = '#'; } } if ( X != '#' ) { Verbose(2) { if ( FirstTime ) { printf("\t\tNote"); FirstTime = false; } printf(" %s%c%s", Variable[V]->Name, X, Variable[W]->Name); } } if ( X == '=' ) Barred[W] = true; /* Record partial order for recursive literals. If polarity is fixed, treat > as # */ if ( V <= Target->Arity && X != '#' ) { ThisX = PartialOrder[V][W] = X; AnyPartialOrder |= ThisX == '<' || ThisX == '>'; if ( W <= Target->Arity ) { ThisX = PartialOrder[W][V] = X == '<' ? '>' : X == '>' ? '<' : '='; AnyPartialOrder |= ThisX == '<' || ThisX == '>'; } } } } Verbose(2) putchar('\n'); } /* Vet proposed arguments for recursive literal. Uses a mapping from ThisOrder x Cell to ThisOrder */ Boolean RecursiveCallOK(Var *A) /* --------------- */ { int i, j, k, N, NRowLeft, Count, NRow, BestCount, BestCol; Ordering *ThisCall, ThisOrder, BestOrder, Cell; Boolean SomeInequality=false, ColOrder[100]; static Ordering **Map=Nil; static Boolean *ColLeft, *RowLeft; if ( ! AnyPartialOrder ) return false; if ( ! Map ) { N = (int) '>'; /* max of '#', '<', '>', '=' */ Map = Alloc(N+1, Ordering *); /* We want the final value for a column to be '=' if it contains only '=' entries '<' if it contains only '<' and/or '=' entries '>' if it contains only '>' and/or '=' entries and '#' otherwise */ Map['='] = Alloc(N+1, Ordering); Map['<'] = Alloc(N+1, Ordering); Map['>'] = Alloc(N+1, Ordering); Map['#'] = Alloc(N+1, Ordering); Map['=']['='] = '='; Map['=']['<'] = '<'; Map['=']['>'] = '>'; Map['=']['#'] = '#'; Map['<']['='] = '<'; Map['<']['<'] = '<'; Map['<']['>'] = '#'; Map['<']['#'] = '#'; Map['>']['='] = '>'; Map['>']['<'] = '#'; Map['>']['>'] = '>'; Map['>']['#'] = '#'; Map['#']['='] = '#'; Map['#']['<'] = '#'; Map['#']['>'] = '#'; Map['#']['#'] = '#'; ColLeft = Alloc(MAXARGS+1, Boolean); RowLeft = Alloc(1001, Boolean); /* assume <1000 recursive lits! */ } N = Target->Arity; memset(ColLeft, true, N+1); NRow = NRowLeft = NRecLitClause + NRecLitDef; memset(RowLeft, true, NRow+1); /* First need to establish ordering constraints for these arguments. (Skip this if A is nil, called from pruning routines) */ if ( A ) { ThisCall = RecursiveLitOrders[0]; ForEach(i, 1, N) { if ( A[i] > Current.MaxVar ) { ThisCall[i] = '#'; } else { ThisCall[i] = PartialOrder[i][A[i]]; SomeInequality |= ThisCall[i] == '<' || ThisCall[i] == '>'; } } if ( ! SomeInequality ) return false; } else { NRowLeft--; RowLeft[0] = false; } /* Check for a possible ordering by * finding a column that has only (< or >) and = orders * delete rows containing (< or >) * continue until no rows remain */ /* This routine is also invoked during the pruning phase, when some literals have been (perhaps temporarily) removed from the most recent clause. Their orderings are marked as inactive; these are treated as if already covered */ ForEach(j, NRecLitDef+1, NRow) { if ( RecursiveLitOrders[j][0] ) { RowLeft[j] = false; NRowLeft--; } } /* Find the initial column ordering constraints */ ForEach(k, 1, N) { ColOrder[k] = ( Target->TypeRef[k]->FixedPolarity ? '>' : '=' ); } while( NRowLeft >= 0 ) { BestCol = BestCount = 0; ForEach(k, 1, N) { if ( ! ColLeft[k] ) continue; Count = 0; ThisOrder = ColOrder[k]; for ( j = 0 ; ThisOrder != '#' && j <= NRow ; j++ ) { if ( ! RowLeft[j] ) continue; Cell = RecursiveLitOrders[j][k]; if ( Cell != '=' ) Count++; ThisOrder = Map[ThisOrder][Cell]; } if ( ThisOrder != '#' && Count > BestCount ) { BestCount = Count; BestCol = k; BestOrder = ThisOrder; } } if ( ! BestCol ) { /* Recursive Call Not OK */ return false; } /* Process best column */ ForEach(j, 0, NRow) { if ( RowLeft[j] && RecursiveLitOrders[j][BestCol] != '=' ) { RowLeft[j] = false; NRowLeft--; } } ColLeft[BestCol] = false; /* Make sure the same type is treated consistently */ ForEach(k, 1, N) { if ( k != BestCol && Target->TypeRef[k] == Target->TypeRef[BestCol] ) { ColOrder[k] = BestOrder; } } } return NRowLeft < 0; } /* Add argument order information for recursive literal. Note: this must be performed before calling NewState so that new variables are correctly given ordering # */ void AddOrders(Literal L) /* --------- */ { Var V, W; /* Allocate ordering and mark as active */ if ( ! L->ArgOrders ) { L->ArgOrders = Alloc(Target->Arity+1, Ordering); L->ArgOrders[0] = 0; } ForEach(V, 1, Target->Arity) { W = L->Args[V]; L->ArgOrders[V] = ( W <= Current.MaxVar ? PartialOrder[V][W] : '#' ); } } /* Keep track of argument orders for recursive literals. (The first cell is reserved for testing) */ void NoteRecursiveLit(Literal L) /* ---------------- */ { static int RecLitSize=0; int i; NRecLitClause++; i = NRecLitDef + NRecLitClause; if ( i >= RecLitSize ) { RecLitSize += 100; Realloc(RecursiveLitOrders, RecLitSize, Ordering *); } RecursiveLitOrders[i] = L->ArgOrders; } /* Given tuples T with index TIX, find the tuples that satisfy the column and same-value constraints on case C. Leave the tuples in Found with their number in NFound */ /* NB: Foil spends a large proportion of its execution time in this single routine. For that reason, the code has been written for speed (on a DECstation), even though this has reduced its clarity. If using different hardware, it would probably be worth rewriting this */ int FoundSize = 0; Boolean Join(Tuple *T, Index TIX, Var *A, Tuple C, int N, Boolean YesOrNo) /* ---- */ { static int *Pair, /* Pair[i], Pair[i+1] are paired variables */ *Contin, /* Contin[i] is a continuous variable that must have the given value */ **Next; /* Next[i] = next tuple obeying ith constraint */ static Boolean *Checked; int *MaxPair, /* highest pair of same variables */ *PairPtr, *MaxContin, /* highest continuous variable */ *ContinPtr, MaxCol=0, /* highest column constraint */ MaxNo=0, /* index numbers in relation */ **NextPtr, **LastNext, V, Val, i, j; Boolean NoCols; Tuple Candidate; /* Allocate arrays first time through */ if ( ! FoundSize ) { Pair = Alloc(2*(MAXVARS+1), int); Next = Alloc(MAXVARS+1, int *); Checked = Alloc(MAXVARS+1, Boolean); Contin = Alloc(MAXVARS+1, int); FoundSize = 20000; Found = Alloc(FoundSize+1, Tuple); } MaxPair = Pair; MaxContin = Contin; NFound = 0; OutOfWorld = false; /* Set the column constraints and find pairs of free variables that must be the same */ memset(Checked+1, 0, N); ForEach(i, 1, N) { /* If this variable is bound, record a constraint; otherwise see if it is the same as another unbound variable */ if ( (V = A[i]) <= Current.MaxVar && (Val = C[V]) != UNBOUND ) { if ( Variable[V]->TypeRef->Continuous ) *MaxContin++ = i; else if ( ! (Next[MaxCol++] = TIX[i][Val]) ) return false; } else if ( ! Checked[i] ) { ForEach(j, i+1, N) { if ( A[j] == V ) { *MaxPair++ = i; *MaxPair++ = j; Checked[j] = true; } } } } NoCols = MaxCol-- <= 0; LastNext = Next + MaxCol; while ( true ) { /* Advance all columns to MaxNo */ for ( NextPtr = Next ; NextPtr <= LastNext ; ) { while ( **NextPtr < MaxNo ) (*NextPtr)++; MaxNo = **NextPtr++; } if ( MaxNo == FINISH || NoCols && ! T[MaxNo] ) { Found[NFound] = Nil; return (NFound > 0); } else if ( NoCols || MaxNo == *Next[0] ) { /* Found one possibility -- check same variable constraints */ Candidate = T[MaxNo]; for ( PairPtr = Pair ; PairPtr < MaxPair && Candidate[*PairPtr] == Candidate[*(PairPtr+1)] ; PairPtr += 2 ) ; for ( ContinPtr = Contin ; ContinPtr < MaxContin && Candidate[*ContinPtr] == C[ A[*ContinPtr] ] ; ContinPtr++ ) ; if ( PairPtr >= MaxPair && ContinPtr >= MaxContin ) { if ( YesOrNo ) return true; if ( NFound >= FoundSize ) { FoundSize += 20000; Realloc(Found, FoundSize+1, Tuple); } Found[NFound++] = Candidate; /* Check for falling off the end of the (closed) world */ for ( i = 1 ; ! OutOfWorld && i <= N ; i++ ) { if ( Candidate[i] == OUT_OF_RANGE ) { OutOfWorld = true; Found[NFound] = Nil; return true; } } } MaxNo++; } } } #include #include extern int VERBOSITY; /* Protected memory allocation routines on call for memory which is not allocated rather than let program continue erroneously */ void *pmalloc(unsigned arg) /* ------- */ { void *p; p = (void *) malloc(arg); if( p || !arg ) return p; printf("\n*** malloc erroneously returns NULL\n"); exit(1); } void *prealloc(void * arg1, unsigned arg2) /* -------- */ { void *p; if ( arg1 == Nil ) return pmalloc(arg2); p = (void *)realloc(arg1,arg2); if( p || !arg2 ) return p; printf("\n*** realloc erroneously returns NULL\n"); exit(1); } void *pcalloc(unsigned arg1, unsigned arg2) /* ------- */ { void *p; p = (void *)calloc(arg1,arg2); if( p || !arg1 || !arg2 ) return p; printf("\n*** calloc erroneously returns NULL\n"); exit(1); } void pfree(void *arg) { if ( arg ) free(arg); } float CPUTime() { struct rusage usage; getrusage(RUSAGE_SELF, &usage); return (usage.ru_utime.tv_sec + usage.ru_stime.tv_sec) + (usage.ru_utime.tv_usec + usage.ru_stime.tv_usec) / 1E6; } /******************************************************************************/ /* */ /* All the stuff for trying possible next literals, growing clauses */ /* and assembling definitions */ /* */ /******************************************************************************/ int FalsePositive, FalseNegative; void FindDefinition(Relation R) /* -------------- */ { int Size, i, TargetPos, FirstDefR; Target = R; NCl = 0; printf("\n----------\n%s:\n", R->Name); /* Reorder the relations so that the target relation comes first */ FirstDefR = ( RelnOrder[2] == GTVAR ? 4 : 2 ); for ( TargetPos = FirstDefR ; RelnOrder[TargetPos] != Target ; TargetPos++ ) ; for ( i = TargetPos ; i > FirstDefR ; i-- ) { RelnOrder[i] = RelnOrder[i-1]; } RelnOrder[FirstDefR] = Target; /* Generate initial tuples and make a copy */ OriginalState(R); StartClause = StartDef; Size = StartDef.NTot+1; StartClause.Tuples = Alloc(Size, Tuple); memcpy(StartClause.Tuples, StartDef.Tuples, Size*sizeof(Tuple)); NRecLitDef = 0; FalsePositive = 0; FalseNegative = StartDef.NPos; R->Def = Alloc(100, Clause); while ( StartClause.NPos ) { if ( ! (R->Def[NCl] = FindClause()) ) break; R->Def[NCl++][NLit] = Nil; if ( NCl % 100 == 0 ) { Realloc(R->Def, NCl+100, Clause); } NRecLitDef += NRecLitClause; } 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); pfree(StartClause.Tuples); pfree(StartDef.Tuples); /* Restore original relation order */ for ( i = FirstDefR ; i < TargetPos ; i++ ) { RelnOrder[i] = RelnOrder[i+1]; } RelnOrder[TargetPos] = Target; } Clause FindClause() /* ---------- */ { Tuple Case, *TSP; InitialiseClauseInfo(); GrowNewClause(); /* Now that pruning includes addition of implicit equalities, should try even when there is a single RHS literal */ PruneNewClause(); /* Make sure accuracy criterion is satisfied */ if ( ! NLit || Current.NOrigPos+1E-3 < AdjMinAccuracy * Current.NOrigTot ) { if ( NLit ) { Verbose(1) printf("\nClause too inaccurate (%d/%d)\n", Current.NOrigPos, Current.NOrigTot); } pfree(NewClause); return Nil; } FalsePositive += Current.NOrigTot - Current.NOrigPos; FalseNegative -= Current.NOrigPos; /* Set flags for positive covered tuples */ ClearFlags; for ( TSP = Current.Tuples ; Case = *TSP ; TSP++ ) { if ( Positive(Case) ) { SetFlag(Case[0]&Mask, TrueBit); } } if ( Current.Tuples != StartClause.Tuples ) { FreeTuples(Current.Tuples, true); } /* Copy all negative tuples and uncovered positive tuples */ StartClause.NTot = StartClause.NPos = 0; for ( TSP = StartClause.Tuples ; Case = *TSP ; TSP++ ) { if ( ! Positive(Case) || ! TestFlag(Case[0]&Mask, TrueBit) ) { StartClause.Tuples[StartClause.NTot++] = Case; if ( Positive(Case) ) StartClause.NPos++; } } StartClause.Tuples[StartClause.NTot] = Nil; StartClause.NOrigPos = StartClause.NPos; StartClause.NOrigTot = StartClause.NTot; StartClause.BaseInfo = Info(StartClause.NPos, StartClause.NTot); Current = StartClause; Verbose(1) { printf("\nClause %d: ", NCl); PrintClause(Target, NewClause); } return NewClause; } void ExamineLiterals() /* --------------- */ { Relation R; int i, Relns=0; NPossible = NDeterminate = 0; MaxPossibleGain = Current.NPos * Current.BaseInfo; /* If this is not the first literal, review coverage and check variable orderings, identical variables etc. */ if ( NLit != 0 ) { CheckOriginalCaseCover(); ExamineVariableRelationships(); } AvailableBits = Encode(Current.NOrigPos) - ClauseBits; Verbose(1) { printf("\nState (%d/%d", Current.NPos, Current.NTot); if ( Current.NTot != Current.NOrigTot ) { printf(" [%d/%d]", Current.NOrigPos, Current.NOrigTot); } printf(", %.1f bits available", AvailableBits); if ( NWeakLits ) { Verbose(2) printf(", %d weak literal%s", NWeakLits, Plural(NWeakLits)); } printf(")\n"); Verbose(4) PrintTuples(Current.Tuples, Current.MaxVar); } /* Find possible literals for each relation */ ForEach(i, 0, MaxRel) { R = RelnOrder[i]; ExploreArgs(R, true); if ( R->NTrialArgs ) Relns++; } /* Evaluate them */ AlterSavedClause = Nil; Verbose(2) putchar('\n'); for ( i = 0 ; i <= MaxRel && BestLitGain < MaxPossibleGain ; i++ ) { R = RelnOrder[i]; if ( ! R->NTrialArgs ) continue; R->Bits = Log2(Relns) + Log2(R->NTrialArgs+1E-3); if ( NEGLITERALS || Predefined(R) ) R->Bits += 1.0; if ( R->Bits - Log2(NLit+1.001-NDetLits) > AvailableBits ) { Verbose(2) { printf("\t\t\t\t[%s requires %.1f bits]\n", R->Name, R->Bits); } } else { ExploreArgs(R, false); Verbose(2) printf("\t\t\t\t[%s tried %d/%d] %.1f secs\n", R->Name, R->NTried, R->NTrialArgs, CPUTime()); } } } void GrowNewClause() /* ------------- */ { Literal L; int i, OldNLit; Boolean Progress=true; float Accuracy, ExtraBits; while ( Progress && Current.NPos < Current.NTot ) { ExamineLiterals(); /* If have noted better saveable clause, record it */ if ( AlterSavedClause ) { Realloc(SavedClause, NLit+2, Literal); ForEach(i, 0, NLit-1) { SavedClause[i] = NewClause[i]; } SavedClause[NLit] = AllocZero(1, struct _lit_rec); SavedClause[NLit+1] = Nil; SavedClause[NLit]->Rel = AlterSavedClause->Rel; SavedClause[NLit]->Sign = AlterSavedClause->Sign; SavedClause[NLit]->Args = AlterSavedClause->Args; SavedClause[NLit]->Bits = AlterSavedClause->Bits; SavedClause[NLit]->WeakLits = 0; SavedClauseCover = AlterSavedClause->PosCov; SavedClauseAccuracy = AlterSavedClause->PosCov / (float) AlterSavedClause->TotCov; Verbose(1) { printf("\n\tSave clause ending with "); PrintLiteral(SavedClause[NLit]); printf(" (cover %d, accuracy %d%%)\n", SavedClauseCover, (int) (100*SavedClauseAccuracy)); } pfree(AlterSavedClause); } if ( NDeterminate && BestLitGain < DETERMINATE * MaxPossibleGain ) { ProcessDeterminateLiterals(true); } else if ( NPossible ) { /* At least one gainful literal */ NewClause[NLit] = L = SelectLiteral(); if ( ++NLit % 100 == 0 ) Realloc(NewClause, NLit+100, Literal); ExtraBits = L->Bits - Log2(NLit-NDetLits+1E-3); ClauseBits += Max(ExtraBits, 0); Verbose(1) { printf("\nBest literal "); PrintLiteral(L); printf(" (%.1f bits)\n", L->Bits); } /* Check whether should regrow clause */ if ( L->Rel != Target && AllLHSVars(L) && Current.MaxVar > Target->Arity && ! AllDeterminate() ) { OldNLit = NLit; NLit = 0; ForEach(i, 0, OldNLit-1) { if ( AllLHSVars(NewClause[i]) ) { NewClause[NLit++] = NewClause[i]; } } NewClause[NLit] = Nil; RecoverState(NewClause); Verbose(1) { printf("\n[Regrow clause] "); PrintClause(Target,NewClause); } GrowNewClause(); return; } NWeakLits = L->WeakLits; if ( L->Rel == Target ) AddOrders(L); NewState(L, Current.NTot); if ( L->Rel == Target ) NoteRecursiveLit(L); } else { Verbose(1) printf("\nNo literals\n"); Progress = Recover(); } } NewClause[NLit] = Nil; /* Finally, see whether saved clause is better */ CheckOriginalCaseCover(); Accuracy = Current.NOrigPos / (float) Current.NOrigTot; if ( SavedClause && ( SavedClauseAccuracy > Accuracy || SavedClauseAccuracy == Accuracy && SavedClauseCover > Current.NOrigPos || SavedClauseAccuracy == Accuracy && SavedClauseCover == Current.NOrigPos && CodingCost(SavedClause) < CodingCost(NewClause) ) ) { Verbose(1) printf("\n[Replace by saved clause]\n"); RecoverState(SavedClause); CheckOriginalCaseCover(); } } InitialiseClauseInfo() /* -------------------- */ { Var V; /* Initialise everything for start of new clause */ NewClause = Alloc(100, Literal); Current = StartClause; NLit = NDetLits = NWeakLits = NRecLitClause = 0; NToBeTried = 0; AnyPartialOrder = false; ClauseBits = 0; ForEach(V, 1, Target->Arity) { Variable[V]->Depth = 0; Variable[V]->Type = Target->Type[V]; Variable[V]->TypeRef = Target->TypeRef[V]; } memset(Barred, false, MAXVARS+1); SavedClause = Nil; SavedClauseAccuracy = SavedClauseCover = 0; MAXRECOVERS = MAXALTS; } Boolean SameLiteral(Relation R, Boolean Sign, Var *A) /* ----------- */ { Var V, NArgs; if ( R != AlterSavedClause->Rel || Sign != AlterSavedClause->Sign ) { return false; } NArgs = ( HasConst(R) ? 1 + sizeof(Const) : R->Arity); ForEach(V, 1, NArgs) { if ( A[V] != AlterSavedClause->Args[V] ) return false; } return true; } Boolean AllLHSVars(Literal L) /* ---------- */ { Var V; ForEach(V, 1, L->Rel->Arity) { if ( L->Args[V] > Target->Arity ) return false; } return true; } /* See whether all literals in clause are determinate */ Boolean AllDeterminate() /* -------------- */ { int i; ForEach(i, 0, NLit-2) { if ( NewClause[i]->Sign != 2 ) return false; } return true; } /* Find the coding cost for a clause */ float CodingCost(Clause C) /* ---------- */ { float SumBits=0, Contrib; int Lits=0; while ( *C ) { Lits++; if ( (Contrib = (*C)->Bits - Log2(Lits)) > 0 ) SumBits += Contrib; C++; } return SumBits; } /******************************************************************************/ /* */ /* Routines for evaluating a definition on a case. Used both during */ /* pruning and when testing definitions found */ /* */ /******************************************************************************/ #define HighestVar Current.MaxVar /* must be set externally! */ Boolean RecordArgOrders = false; /* flag set by prune */ Const *Value = Nil; /* current variable bindings */ Boolean CheckRHS(Clause C) /* -------- */ { Relation R; Tuple Case, *Bindings, *Scan; Literal L; int i, N; Var *A, V, W; Const KVal, *CopyValue; float VVal, WVal; Ordering ThisOrder, PrevOrder; Boolean SomeOrder=false; if ( ! (L = C[0]) ) return true; R = L->Rel; A = L->Args; N = R->Arity; /* If literal marked inactive, ignore */ if ( A[0] ) return CheckRHS(C+1); /* Record types of unbound variables */ ForEach(i, 1, N) { V = A[i]; if ( Value[V] == UNBOUND ) Variable[V]->TypeRef = R->TypeRef[i]; } /* Check for missing values */ if ( MissingValue(R, A, Value) ) return false; /* Adjust ordering information for recursive literals if required */ if ( RecordArgOrders && R == Target ) { ForEach(V, 1, N) { W = A[V]; if ( Value[W] == UNBOUND ) { ThisOrder = '#'; } else { if ( Variable[V]->TypeRef->Continuous ) { VVal = FP(Value[V]); WVal = FP(Value[W]); } else { VVal = Variable[V]->TypeRef->CollSeq[Value[V]]; WVal = Variable[V]->TypeRef->CollSeq[Value[W]]; } ThisOrder = ( VVal < WVal ? '<' : VVal > WVal ? '>' : '=' ); } PrevOrder = L->ArgOrders[V]; if ( PrevOrder != ThisOrder ) { L->ArgOrders[V] = ( ! PrevOrder ? ThisOrder : '#' ); } ThisOrder = L->ArgOrders[V]; SomeOrder |= ( ThisOrder == '<' || ThisOrder == '>' ); } if ( ! SomeOrder ) { return RecordArgOrders = false; } } /* Various possible cases */ if ( Predefined(R) ) { if ( HasConst(R) ) { GetParam(&A[2], &KVal); } else { KVal = A[2]; } return Satisfies((int)R->Pos, A[1], KVal, Value) == (L->Sign != 0) && CheckRHS(C+1); } if ( ! L->Sign ) { return ( ! Join(R->Pos, R->PosIndex, A, Value, N, true) ) && CheckRHS(C+1); } if ( ! Join(R->Pos, R->PosIndex, A, Value, N, false) ) return false; /* Each tuple found represents a possible binding for the free variables in A. Copy them (to prevent overwriting on subsequent calls to Join) and try them in sequence */ Bindings = Alloc(NFound+1, Tuple); memcpy(Bindings, Found, (NFound+1)*sizeof(Tuple)); CopyValue = Alloc(MAXVARS+1, Const); memcpy(CopyValue, Value, (HighestVar+1)*sizeof(Const)); Scan = Bindings; /* Check rest of RHS */ while ( Case = *Scan++ ) { ForEach(i, 1, N) { V = L->Args[i]; if ( Value[V] == UNBOUND ) Value[V] = Case[i]; } if ( CheckRHS(C+1) ) { pfree(Bindings); memcpy(Value, CopyValue, (HighestVar+1)*sizeof(Const)); pfree(CopyValue); return true; } memcpy(Value, CopyValue, (HighestVar+1)*sizeof(Const)); } pfree(Bindings); pfree(CopyValue); return false; } Boolean Interpret(Relation R, Tuple Case) /* --------- */ { int i; ForEach(i, 1, R->Arity) { Variable[i]->TypeRef = R->TypeRef[i]; } InitialiseValues(Case, R->Arity); for ( i = 0 ; R->Def[i] ; i++ ) { if ( CheckRHS(R->Def[i]) ) return true; } return false; } void InitialiseValues(Tuple Case, int N) /* ---------------- */ { int i; if ( ! Value ) { Value = Alloc(MAXVARS+1, Const); } ForEach(i, 1, N) { Value[i] = Case[i]; } ForEach(i, N+1, MAXVARS) { Value[i] = UNBOUND; } } /******************************************************************************/ /* */ /* Stuff for pruning clauses and definitions. Clauses are first */ /* `quickpruned' to remove determinate literals that introduce unused */ /* variables; if this causes the definition to become less accurate, */ /* these are restored. Then literals are removed one at a time to */ /* see whether they contribute anything. A similar process is */ /* followed when pruning definitions: clauses are removed one at a */ /* time to see whether the remaining clauses suffice */ /* */ /******************************************************************************/ extern Boolean RecordArgOrders; /* for interpret.c */ #define MarkLiteral(L,X) { (L)->Args[0]=X;\ if ((L)->ArgOrders) (L)->ArgOrders[0]=X;} /* See whether literals can be dropped from a clause */ void PruneNewClause() /* -------------- */ { int Errs, i, j, k; Boolean *Used, Changed=false; Literal L, LL; Var V; Errs = Current.NOrigTot - Current.NOrigPos; Used = Alloc(MAXVARS+1, Boolean); Verbose(2) { printf("\nInitial clause (%d errs): ", Errs); PrintClause(Target, NewClause); } /* Save arg orderings for recursive literals and promote any literals of form A=B or B=c to immediately after B appears in the clause */ ForEach(i, 0, NLit-1) { L = NewClause[i]; if ( L->Sign && ( L->Rel == EQVAR || L->Rel == EQCONST ) ) { V = ( L->Rel == EQVAR ? L->Args[2] : L->Args[1] ); if ( V > Target->Arity ) { ForEach(j, 1, i) { LL = NewClause[j-1]; if ( LL->Sign && Contains(LL->Args, LL->Rel->Arity, V) ) { break; } } } else { j = 0; } for ( k = i ; k > j ; k-- ) { NewClause[k] = NewClause[k-1]; } NewClause[j] = L; } else if ( L->Rel == Target ) { L->SaveArgOrders = Alloc(Target->Arity+1, Ordering); memcpy(L->SaveArgOrders, L->ArgOrders, (Target->Arity+1)*sizeof(Ordering)); } } /* Look for unexpected relations V=W or V=c */ CheckVariables(); /* Check for quick pruning of apparently useless literals */ if ( QuickPrune(NewClause, Target->Arity, Used) ) { if ( SatisfactoryNewClause(Errs) ) { Verbose(3) printf("\tAccepting quickpruned clause\n"); Changed = true; } else { /* Mark all literals as active again */ ForEach(i, 0, NLit-1) { MarkLiteral(NewClause[i], 0); } } } Changed |= RedundantLiterals(Errs); /* Remove unnecessary literals from NewClause */ if ( Changed ) { for ( i = 0 ; i < NLit ; ) { L = NewClause[i]; if ( L->Args[0] ) { FreeLiteral(L); NLit--; ForEach(j, i, NLit-1) { NewClause[j] = NewClause[j+1]; } } else { i++; } } NewClause[NLit] = Nil; RenameVariables(); /* Need to recompute partial orders and clause coverage */ RecoverState(NewClause); CheckOriginalCaseCover(); } else { /* Restore arg orders */ ForEach(i, 0, NLit-1) { L = NewClause[i]; if ( L->Rel == Target ) { memcpy(L->ArgOrders,L->SaveArgOrders, (Target->Arity+1)*sizeof(Ordering)); pfree(L->SaveArgOrders); } } } pfree(Used); } /* Look for unexpected equivalences of variables or variables with unchanging values. If found, insert pseudo-literals into the clause so that redundant literals can be pruned */ void CheckVariables() /* -------------- */ { Var A, B; ForEach(A, 1, Current.MaxVar) { if ( TheoryConstant(Current.Tuples[0][A], Variable[A]->TypeRef) && ConstantVar(A, Current.Tuples[0][A]) ) { if ( ! Known(EQCONST, A, 0) ) { Insert(A, EQCONST, A, Current.Tuples[0][A]); } } else { ForEach(B, A+1, Current.MaxVar) { if ( Compatible[Variable[A]->Type][Variable[B]->Type] && IdenticalVars(A,B) && ! Known(EQVAR, A, B) ) { Insert(B, EQVAR, A, B); } } } } } /* See whether a constant is a theory constant */ Boolean TheoryConstant(Const C, TypeInfo T) /* -------------- */ { int i; if ( T->Continuous ) return false; ForEach(i, 0, T->NTheoryConsts-1) { if ( C == T->TheoryConst[i] ) return true; } return false; } /* Check for variable with constant value */ Boolean ConstantVar(Var V, Const C) /* ----------- */ { Tuple Case, *TSP; for ( TSP = Current.Tuples ; Case = *TSP++; ) { if ( Positive(Case) && Case[V] != C ) return false; } return true; } /* Check for identical variables */ Boolean IdenticalVars(Var V, Var W) /* ------------- */ { Tuple Case, *TSP; for ( TSP = Current.Tuples ; Case = *TSP++; ) { if ( Positive(Case) && ( Unknown(V, Case) || Case[V] != Case[W] ) ) return false; } return true; } /* Make sure potential literal isn't already in clause */ Boolean Known(Relation R, Var V, Var W) /* ----- */ { int i; Literal L; ForEach(i, 0, NLit-1) { L = NewClause[i]; if ( L->Rel == R && L->Sign && L->Args[1] == V && ( ! W || L->Args[2] == W ) ) { return true; } } return false; } /* Insert new literal after V first bound */ void Insert(Var V, Relation R, Var A1, Const A2) /* ------ */ { int i=0, j; Literal L; if ( V > Target->Arity ) { ForEach(i, 1, NLit) { L = NewClause[i-1]; if ( L->Sign && Contains(L->Args, L->Rel->Arity, V) ) break; } } /* Insert literal before NewClause[i] */ if ( ++NLit % 100 == 0 ) Realloc(NewClause, NLit+100, Literal); for ( j = NLit ; j > i ; j-- ) { NewClause[j] = NewClause[j-1]; } L = AllocZero(1, struct _lit_rec); L->Rel = R; L->Sign = true; L->Bits = 0; if ( R == EQVAR ) { L->Args = AllocZero(3, Var); L->Args[1] = A1; L->Args[2] = A2; } else { L->Args = AllocZero(2+sizeof(Const), Var); L->Args[1] = A1; SaveParam(L->Args+2, &A2); } NewClause[i] = L; Verbose(2) { printf("\tInsert literal "); PrintSpecialLiteral(R, true, L->Args); printf("\n"); } } /* Check for variable in argument list */ Boolean Contains(Var *A, int N, Var V) /* -------- */ { int i; ForEach(i, 1, N) { if ( A[i] == V ) return true; } return false; } /* Remove determinate literals that introduce useless new variables (that are not used by any subsequent literal) */ Boolean QuickPrune(Clause C, Var MaxBound, Boolean *Used) /* ---------- */ { Var V, NewMaxBound; Literal L; Boolean SomeUsed=true, Changed=false; if ( (L = C[0]) == Nil ) { ForEach(V, 1, MaxBound) Used[V] = false; return false; } L->Args[0] = 0; NewMaxBound = MaxBound; if ( L->Sign ) { ForEach(V, 1, L->Rel->Arity) { if ( L->Args[V] > NewMaxBound ) NewMaxBound = L->Args[V]; } } Changed = QuickPrune(C+1, NewMaxBound, Used); if ( L->Sign == 2 ) { SomeUsed = false; ForEach(V, MaxBound+1, NewMaxBound) { SomeUsed = Used[V]; if ( SomeUsed ) break; } } if ( ! SomeUsed && C[1] ) { /* Mark this literal as inactive */ MarkLiteral(L, 1); Verbose(3) { printf("\tQuickPrune literal "); PrintLiteral(L); putchar('\n'); } Changed = true; } else ForEach(V, 1, L->Rel->Arity) { Used[L->Args[V]] = true; } return Changed; } Boolean SatisfactoryNewClause(int Errs) /* --------------------- */ { Boolean RecursiveLits=false, ProForma; Literal L; int i, ErrsNow=0; /* Prepare for redetermining argument orders */ ForEach(i, 0, NLit-1) { if ( (L = NewClause[i])->Args[0] ) continue; if ( L->Rel == Target ) { RecursiveLits = true; memset(L->ArgOrders, 0, Target->Arity+1); } } /* Scan case by case, looking for too many covered neg tuples */ RecordArgOrders = RecursiveLits; ForEach(i, StartDef.NPos, StartDef.NTot-1) { InitialiseValues(StartDef.Tuples[i], Target->Arity); if ( CheckRHS(NewClause) && ++ErrsNow > Errs || RecursiveLits && ! RecordArgOrders ) { RecordArgOrders = false; return false; } } /* If satisfactory and recursive literals, must also check pos tuples covered to complete arg order information */ for ( i = 0 ; i < StartDef.NPos && RecordArgOrders ; i++ ) { InitialiseValues(StartDef.Tuples[i], Target->Arity); ProForma = CheckRHS(NewClause); } /* Now check that recursion still well-behaved */ return ( RecursiveLits ? RecordArgOrders && RecursiveCallOK(Nil) : true ); } /* Rename variables in NewClause */ void RenameVariables() /* --------------- */ { Var *NewVar, Next, SaveNext, V; int l, i; Literal L; NewVar = AllocZero(MAXVARS+1, Var); Next = Target->Arity+1; ForEach(l, 0, NLit-1) { if ( (L=NewClause[l])->Args[0] ) continue; SaveNext = Next; ForEach(i, 1, L->Rel->Arity) { V = L->Args[i]; if ( V > Target->Arity ) { if ( ! NewVar[V] ) NewVar[V] = Next++; L->Args[i] = NewVar[V]; } } /* New variables appearing in negated lits are still free */ if ( ! L->Sign ) { Next = SaveNext; ForEach(V, 1, MAXVARS) if ( NewVar[V] >= Next ) NewVar[V] = 0; } } pfree(NewVar); } /* Omit the first unnecessary literal. This version prunes from the end of the clause; if a literal can't be dropped when it is examined, it will always be needed, since dropping earlier literals can only increase the number of minus tuples getting through to this literal */ Boolean RedundantLiterals(int ErrsNow) /* ----------------- */ { int i, j; Boolean Changed=false; Literal L; /* Check for the latest literal, omitting which would not increase the number of errors. Note: checking last literal is reinstated since clause may contain errors */ for ( i = NLit-1 ; i >= 0 ; i-- ) { L = NewClause[i]; if ( L->Args[0] || EssentialBinding(i) ) { continue; } MarkLiteral(L, 1); if ( SatisfactoryNewClause(ErrsNow) ) { Verbose(3) { printf("\t\t"); PrintLiteral(L); printf(" removed\n"); } Changed = true; } else { Verbose(3) { printf("\t\t"); PrintLiteral(L); printf(" essential\n"); } MarkLiteral(L, 0); /* If this literal is V=W, where W is a non-continuous variable bound on the RHS of the clause, substitute for W throughout and remove the literal */ if ( L->Rel == EQVAR && L->Sign && L->Args[2] > Target->Arity && ! Variable[L->Args[2]]->TypeRef->Continuous ) { ForEach(j, i, NLit-1) { NewClause[j] = NewClause[j+1]; } NLit--; ReplaceVariable(L->Args[2], L->Args[1]); } } } return Changed; } /* Can't omit a literal that is needed to bind a variable appearing in a later negated literal relation, or whose omission would leave a later literal containing all new variables */ #define NONE -1 #define MANY 1000000 Boolean EssentialBinding(int LitNo) /* ---------------- */ { int i, j, b, *UniqueBinding; Boolean Needed=false, Other; Literal L; Var V, NArgs; /* UniqueBinding[V] = NONE (if V not yet bound) = i (if V bound only by ith literal) = MANY (if V bound by more than one literal) */ UniqueBinding = Alloc(MAXVARS+1, int); ForEach(V, 1, MAXVARS) { UniqueBinding[V] = ( V <= Target->Arity ? MANY : NONE ); } for ( i = 0 ; i < NLit && ! Needed ; i++ ) { if ( (L = NewClause[i])->Args[0] ) continue; NArgs = L->Rel->Arity; if ( i > LitNo ) { if ( Predefined(L->Rel) || ! L->Sign ) { ForEach(j, 1, NArgs) { Needed |= UniqueBinding[L->Args[j]] == LitNo; } } else { Other = false; ForEach(j, 1, NArgs) { b = UniqueBinding[L->Args[j]]; Other |= b != NONE && b != LitNo; } Needed = ! Other; } if ( Needed ) { Verbose(/*3*/2) { printf("\t\t"); PrintLiteral(NewClause[LitNo]); printf(" needed for binding "); PrintLiteral(NewClause[i]); putchar('\n'); } } } if ( L->Sign ) { /* Update binding records for new variables */ ForEach(j, 1, NArgs) { V = L->Args[j]; if ( UniqueBinding[V] == NONE ) { UniqueBinding[V] = i; } else if ( UniqueBinding[V] != i ) { UniqueBinding[V] = MANY; } } } } pfree(UniqueBinding); return Needed; } /* Substitute for variable in clause */ void ReplaceVariable(Var Old, Var New) /* --------------- */ { int i, a; Literal L; Boolean Bound=false; ForEach(i, 0, NLit-1) { L = NewClause[i]; if ( L->Sign || Bound ) { ForEach(a, 1, L->Rel->Arity) { if ( L->Args[a] == Old ) { L->Args[a] = New; Bound = true; } } } } } /* See whether some clauses can be dispensed with */ void SiftClauses() /* ----------- */ { int i, j, Covers, Last, Retain=0, Remove=0; Boolean *Need, *Delete; if ( ! NCl ) return; Delete = AllocZero(NCl, Boolean); Need = AllocZero(NCl, Boolean); Current.MaxVar = HighestVarInDefinition(Target); while ( Retain+Remove < NCl ) { /* See if a clause uniquely covers a pos tuple */ for ( i = 0 ; i < StartDef.NPos && Retain < NCl ; i++ ) { Covers = 0; for ( j = 0 ; j < NCl && Covers <= 1 && Retain < NCl ; j++ ) { if ( Delete[j] ) continue; InitialiseValues(StartDef.Tuples[i], Target->Arity); if ( CheckRHS(Target->Def[j]) ) { Covers++; Last = j; } } if ( Covers == 1 && ! Need[Last] ) { Verbose(3) { printf("\tClause %d needed for ", Last); PrintTuple(StartDef.Tuples[i], Target->Arity, Target->TypeRef, false); } Need[Last] = true; Retain++; } } if ( Retain == NCl ) break; /* Remove the latest unneeded clause */ Last = -1; ForEach(i, 0, NCl-1) { if ( ! Need[i] && ! Delete[i] ) Last = i; } if ( Last == -1 ) break; Delete[Last] = true; Remove++; } if ( Retain < NCl ) { Verbose(1) printf("\nDelete clause%s\n", Plural(NCl - Retain)); Retain = 0; ForEach(i, 0, NCl-1) { if ( Delete[i] ) { Verbose(1) { printf("\t"); PrintClause(Target, Target->Def[i]); FreeClause(Target->Def[i]); } } else { Target->Def[Retain++] = Target->Def[i]; } } Target->Def[Retain] = Nil; } pfree(Delete); pfree(Need); } /* Find highest variable in any clause */ Var HighestVarInDefinition(Relation R) /* ---------------------- */ { Var V, HiV; Literal L; Clause C; int i; HiV = R->Arity; for ( i = 0 ; R->Def[i] ; i++ ) { for ( C = R->Def[i] ; L = *C ; C++ ) { if ( L->Sign ) { ForEach(V, 1, L->Rel->Arity) { if ( L->Args[V] > HiV ) HiV = L->Args[V]; } } } } return HiV; } /******************************************************************************/ /* */ /* Routines concerned with discovering a plausible ordering of the */ /* constants of each type. There are three phases: */ /* * finding possible orderings on pairs of relation arguments */ /* * finding a partial ordering that satisfies as many of these */ /* as possible */ /* * selecting a constant ordering consistent with the partial */ /* ordering */ /* */ /******************************************************************************/ Boolean **Table=Nil; /* partial order for target type */ int TTN, /* target type number */ NC, /* size of target type */ *TTCollSeq, /* collation sequence */ NArgOrders = 0, /* number of possible arg orders */ MaxConsistent; /* max consistent arg orders */ ArgOrder *ArgOrderList = Nil; /* Find ordering for constants of each type */ void OrderConstants() /* -------------- */ { int i, j; Boolean **PO; Tuple *NLT; ForEach(TTN, 1, MaxType) { if ( Type[TTN]->FixedPolarity ) continue; NC = Type[TTN]->NValues; TTCollSeq = Type[TTN]->CollSeq; Verbose(3) printf("\nOrdering constants of type %s\n",Type[TTN]->Name); if ( ! Table ) Table = AllocatePartOrd(MaxConst); FindArgumentOrders(); if ( NArgOrders == 0 ) { Type[TTN]->Ordered = false; Verbose(3) printf("\t\tunordered\n"); continue; } else { Type[TTN]->Ordered = true; } /* Assemble in Table the partial order consistent with the maximum number of arg orders */ MaxConsistent = 0; PO = AllocatePartOrd(NC); ClearPartOrd(PO); Verbose(3) printf("\tFinding maximal consistent set\n"); FindConsistentSubset(0, 0, PO); FreePartOrd(PO, NC); /* Sort constants on number of entries in partial order; resolve ties in favour of the initial constant order */ NLT = Alloc(NC, Tuple); ForEach(i, 0, NC-1) { NLT[i] = Alloc(2, Const); NLT[i][0] = Type[TTN]->Value[i]; FP(NLT[i][1]) = CountEntries(i+1) + i / (float) NC; } Quicksort(NLT, 0, NC-1, 1); /* Change collation sequence and print message */ Verbose(3) printf("\tFinal order:\n\t\t"); ForEach(i, 0, NC-1) { j = NLT[i][0]; Type[TTN]->CollSeq[j] = i+1; Verbose(3) printf("%s ", ConstName[j]); pfree(NLT[i]); } Verbose(3) putchar('\n'); pfree(NLT); } if ( Table ) FreePartOrd(Table, MaxConst); ForEach(i, 0, NArgOrders-1) { pfree(ArgOrderList[i]); } pfree(ArgOrderList); } /* Find potential orderings between pairs of arguments of each relation for type TTN */ void FindArgumentOrders() /* ------------------ */ { int i; Relation R; ForEach(i, 0, MaxRel) { R = RelnOrder[i]; if ( Predefined(R) || R->Arity < 2 ) continue; ExamineArgumentPairs(R, true, R->Pos); if ( R->Neg ) { ExamineArgumentPairs(R, false, R->Neg); } } } /* Find potential orderings between pairs of arguments of R where relevant to the type under investigation */ void ExamineArgumentPairs(Relation R, Boolean Sign, Tuple *TP) /* -------------------- */ { int FirstArg, SecondArg; Verbose(3) printf("\tChecking arguments of %s%s\n", Sign ? "" : "~", R->Name); ForEach(FirstArg, 1, R->Arity-1) { if ( ! Compatible[R->Type[FirstArg]][TTN] ) continue; ForEach(SecondArg, FirstArg+1, R->Arity) { if ( ! Compatible[R->Type[SecondArg]][TTN] ) continue; Verbose(3) printf("\t\targuments %d,%d ", FirstArg, SecondArg); ClearPartOrd(Table); if ( ConsistentClosure(Table, TP, FirstArg, SecondArg) ) { Verbose(3) printf("are consistent\n"); AddArgOrder(R, Sign, FirstArg, SecondArg); } else { Verbose(3) printf("are not consistent\n"); } } } } /* Investigate args A and B of a set of tuples TP. See whether each pair of constants is consistent with TP; if so, add and form closure */ Boolean ConsistentClosure(Boolean **PO, Tuple *TP, Var A, Var B) /* ----------------- */ { Const K, L; int i, j; while( *TP ) { K = (*TP)[A]; L = (*TP)[B]; TP++; if ( K == MISSING_DISC || K == OUT_OF_RANGE || L == MISSING_DISC || L == OUT_OF_RANGE ) continue; /* Not consistent if either constant missing from type or if current pair in conflict with existing table */ if ( (i = TTCollSeq[K]) == 0 || (j = TTCollSeq[L]) == 0 || ! AddPair(PO, i, j) ) { return false; } } return true; } /* Note partial order between A and B; add to table if not already there and generate closure. Return false if the table is no longer consistent */ Boolean AddPair(Boolean **PO, int A, int B) /* ------- */ { int i, j; if ( PO[A][B] ) return true; /* already there */ else if ( A == B || PO[B][A] ) return false; /* not consistent */ ForEach(i, 1, NC) { if ( i == A || PO[i][A] ) { ForEach(j, 1, NC) { if ( j == B || PO[B][j] ) { if ( PO[j][i] ) return false; PO[i][j] = true; } } } } return true; } void AddArgOrder(Relation R, Boolean Sign, int A1, int A2) /* ----------- */ { ArgOrder AO; if ( NArgOrders % 100 == 0 ) { ArgOrderList = Realloc(ArgOrderList, NArgOrders+100, ArgOrder); } ArgOrderList[NArgOrders++] = AO = Alloc(1, struct _arg_ord_rec); AO->Rel = R; AO->Sign = Sign; AO->A1 = A1; AO->A2 = A2; AO->In = 0; } /* Routines for constant partial order tables */ Boolean **AllocatePartOrd(int Size) /* --------------- */ { Boolean **PO; int i; PO = Alloc(Size+1, Boolean *); ForEach(i, 1, Size) { PO[i] = Alloc(Size+1, Boolean); } return PO; } void FreePartOrd(Boolean **PO, int Size) /* ----------- */ { int i; ForEach(i, 1, Size) { pfree(PO[i]); } pfree(PO); } void ClearPartOrd(Boolean **PO) /* ------------ */ { int i; ForEach(i, 1, NC) { memset(PO[i], false, NC+1); } } void CopyPartOrd(Boolean **To, Boolean **From) /* ----------- */ { int i; ForEach(i, 1, NC) { memcpy(To[i], From[i], (NC+1)*sizeof(Boolean)); } } void FindConsistentSubset(int Included, int TryNext, Boolean **PO) /* -------------------- */ { Boolean **CopyPO; ArgOrder AO; Tuple *Entries; int i; if ( Included > MaxConsistent ) { /* Note best consistent partial order so far */ CopyPartOrd(Table, PO); MaxConsistent = Included; Verbose(3) { printf("\t\tbest so far"); ForEach(i, 0, NArgOrders-1) { AO = ArgOrderList[i]; if ( AO->In ) { printf(" %s%s:", AO->Sign ? "" : "~", AO->Rel->Name); if ( AO->In == 1 ) { printf("%d>%d", AO->A1, AO->A2); } else { printf("%d>%d", AO->A2, AO->A1); } } } putchar('\n'); } } if ( TryNext >= NArgOrders || Included + (NArgOrders - TryNext) <= MaxConsistent ) { return; } AO = ArgOrderList[TryNext]; Entries = AO->Sign ? AO->Rel->Pos : AO->Rel->Neg; CopyPO = AllocatePartOrd(NC); CopyPartOrd(CopyPO, PO); if ( ConsistentClosure(PO, Entries, AO->A1, AO->A2) ) { AO->In = 1; FindConsistentSubset(Included+1, TryNext+1, PO); } /* Do not have to try both polarities of first argument ordering */ if ( Included > 0 ) { CopyPartOrd(PO, CopyPO); if ( ConsistentClosure(PO, Entries, AO->A2, AO->A1) ) { AO->In = -1; FindConsistentSubset(Included+1, TryNext+1, PO); } } CopyPartOrd(PO, CopyPO); AO->In = 0; FindConsistentSubset(Included, TryNext+1, PO); FreePartOrd(CopyPO, NC); } int CountEntries(int K) /* ------------ */ { int i, Sum=0; ForEach(i, 1, NC) { if ( Table[K][i] ) Sum++; } return Sum; }