#include #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() */ 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 LogComb(n,r) (LogFact[n] - LogFact[r] - LogFact[(n)-(r)]) #define Except(n,e) ((n) ? (1.1*(Log2(n) + LogComb(n, e))) : 0.0) #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) /* 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 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 */ /******************************************************************************/ /* */ /* 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); /* 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 PrintDefinition(Relation R); /* literal.c */ void ExploreArgs(Relation R, Boolean CountFlag); Boolean AcceptableKey(Relation R, int Key); void ExploreEQVAR(); void ExploreEQCONST(); void ExploreGTVAR(); void ExploreGTCONST(); void TryArgs(Relation R, int This, int HiVar, int FreeVars, int MaxDepth, int Key, Boolean TryMostGeneral, Boolean RecOK); /* 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, float LitBits); 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); void FindThreshold(Var *A, float LitBits); 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, Boolean RSign, 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, int NMV); void CheckOriginalCaseCover(); void FreeTuples(Tuple *TT, Boolean TuplesToo); /* determinate.c */ Boolean GoodDeterminateLiteral(Relation R, Var *A); 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 BetterSaveableClause(); Boolean SameLiteral(Relation R, Boolean Sign, Var *A); Boolean AllLHSVars(Literal L); Boolean AllDeterminate(); /* prune.c */ void PruneNewClause(); Boolean QuickPrune(Clause C, Var MaxBound, Boolean *Used); Boolean SatisfactoryNewClause(int Errs); void RenameVariables(); Boolean RedundantLiterals(int ErrsNow); Boolean EssentialBinding(int LitNo); 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);