%{ #include #include #include #include "mis.h" #include "order.h" #include "gram.c" #include "mis.c" #include "allocator.c" #include "order.c" %} %token INT REAL WORD SUBCASE PERM TAKE_TWO_OUT_OF MIS TOTAL ANY GIVES CHOICE CONSTANT NOT END OMITTED AT_LEAST WITH_OTHERS CALLS NUMBER SPECIAL REGorSUBDOM CANONICAL COMMON TWO_OF_LAST_THREE AND REDUCED UNION EACH A_NEIGHBOUR A_COMMON_NEIGHBOUR NEIGHBOURS EDGE DEGREE LPAR RPAR LCURLY RCURLY LSQUARE RSQUARE COMMA SEMICOLON COLON EOF EQUAL LT LE GT PLUS DASH STAR EXPO A B G ALPHA ARROW %% file : fileheader {initpowers();} caselist END { /* The interval should end at the last possible subcase */ checkfinal($3.subcase); printf("terminated with %i errors\n",errorcount); return; }; fileheader : sort INT {size=$2.ival; bound= Nhood? size==4?c4:size==5?c5:size==6?c6:c7 : size==4?a4:a5; } ; sort : DEGREE {Nhood=true;} | TAKE_TWO_OUT_OF {Nhood=false;} ; caselist : /* A case or caselist has an attribute "subcase" a pointer to the (last in the list) subcase struct */ caselist case { $$.subcase=$2.subcase; /* last in list */ /* The two intervals should be adjacent */ checkfollows($1.subcase,$2.subcase); } | case { $$.subcase=$1.subcase; /* The interval should start at the first possible subcase */ checkinitial($$.subcase); } ; case : caseheader casetreatment {$$.subcase=$2.subcase; checkinterval($$.subcase);} ; caseheader : SUBCASE NUMBER INT COLON ; optdegree : DEGREE | ; casetreatment : /* a casetreatment has an attribute "subcase" a pointer to the graph structure */ graphheader reasonnottreated {$$.subcase=$2.subcase;} | graph PERM COLON permu GIVES graph algorithm { validperm($4.permutation); checkperm($1.subcase,$4.permutation,$6.subcase); $$.subcase=$1.subcase; } ; permu : /* a (partial) permutation has an attribute "permutation", a pointer to the vector containing the permutation */ permu INDEX ARROW INDEX { (*$1.permutation)[$2.ival]=$4.ival; $$.permutation=$1.permutation; } | INDEX ARROW INDEX { permptr p=(permptr)malloc(sizeof(vector)); int i; for (i=1;i<=size;i++) (*p)[i]=unknown; (*p)[$1.ival]=$3.ival; $$.permutation=p; } ; INDEX : /* an integer in [1..size]; attribute "ival" is its value */ INT {$$.ival=$1.ival; Assert(inrange($1.ival), "bad index value");} ; Bvertex : B INDEX { $$.ival=$2.ival; } ; algorithm : CALLS {first=true; clearcoverage();} callslist total {Assert(approx($3.rval,$4.rval),"total differs from list"); Assert($4.rval<=bound,"time exceeds claimed bound"); checkcoverage(pointer); } | CALLS SPECIAL {checkspecial(pointer);} ; reasonnottreated : NOT REGorSUBDOM graphdetails {checkregdom($3.subcase); $$.subcase=$3.subcase;} | NOT CANONICAL based PERM COLON permu graphdetails {$$.subcase=$7.subcase; validperm($6.permutation); checknotcanon($7.subcase,$6.permutation,$3.ival);} ; based : /* does fact that subcase is not canonical depend on (i) just the edges, (ii) edges and degrees or (iii) also common neighbour information? */ LPAR EDGE RPAR {$$.ival=1;} | LPAR EDGE DEGREE RPAR {$$.ival=2;} | {$$.ival=3;} ; graph : graphheader graphdetails {$$.subcase=$2.subcase;}; graphdetails : /* attribute "subcase" is pointer to graph structure */ degrees SEMICOLON adjacencies { $$.subcase=pointer; Assert(indx==size,"wrong number of degrees"); Assert(rowindx==size+1&&columnindx==1, "wrong number of adjacency items"); checkgraph(pointer); }; graphheader : sort optdegree INT COLON {indx=0; columnindx=2;rowindx=1; pointer=(subcaseptr)malloc(sizeof(subcase)); /* prepare to read graph */ }; degrees : degrees degree | degree ; degree : INT COMMA INT {pointer->degree[++indx]=$1.ival; pointer->extdegree[indx]=$3.ival;} | ANY {pointer->degree[++indx]=unknown; pointer->extdegree[indx]=unknown;} ; adjacencies: adjacencies adjacency {nextcell();} | adjacency {nextcell();} ; adjacency : /* adjacency (0 or 1) and common neighbour information can be e.g. 2-4 a range from 2 to 4 or 2[4] exactly 2 and maximum possible was 4 or absent: no information alternatively "*" means no information at all */ INT LPAR INT DASH INT RPAR {pointer->adj[rowindx][columnindx]=$1.ival; pointer->mincommon[rowindx][columnindx]=$3.ival; pointer->maxcommon[rowindx][columnindx]=$5.ival; pointer->theomaxcommon[rowindx][columnindx]=$5.ival;} | INT LPAR INT LSQUARE INT RSQUARE RPAR {pointer->adj[rowindx][columnindx]=$1.ival; pointer->mincommon[rowindx][columnindx]=$3.ival; pointer->maxcommon[rowindx][columnindx]=$3.ival; pointer->theomaxcommon[rowindx][columnindx]=$5.ival;} | INT LPAR RPAR {pointer->adj[rowindx][columnindx]=$1.ival; pointer->mincommon[rowindx][columnindx]=unknown; pointer->maxcommon[rowindx][columnindx]=unknown; pointer->theomaxcommon[rowindx][columnindx]=unknown;} | STAR LPAR RPAR {pointer->adj[rowindx][columnindx]=unknown; pointer->mincommon[rowindx][columnindx]=unknown; pointer->maxcommon[rowindx][columnindx]=unknown; pointer->theomaxcommon[rowindx][columnindx]=unknown;} ; callslist : /* attribute "rval" is sum of timing values */ callslist call {$$.rval=$1.rval+$2.rval;} | call {$$.rval=$1.rval;} ; call : LPAR INT RPAR COLON MIS subgraph timing {resetbuffer();} {if ($7.ival>=0) Assert($6.ival==$7.ival, "invalid power used in timing analysis"); $$.rval=$7.rval; if (first) { if (Nhood) Assert(order(Chosen)==1 && (Achosen || Bichosen && Bi==1), "first recursive call must be G-A or G-B1"); first=false; } } ; subgraph : /* attribute "ival" is number of vertices removed */ LPAR G minus chosen minus neighbours minus rejected forced RPAR {vertexset All; $$.ival=$4.ival+$6.ival+$8.ival+$9.ival; CalcDegrees(Chosen,Neighbours,Rejected,pointer,Degree); CopyVertexset(Chosen,&All); merge(&All,Neighbours,pointer); merge(&All,Rejected,pointer); merge(&All,$9.vertexset,pointer); Assert(order(&All)==$$.ival,"sets overlap?"); checkconsistent(&All,pointer); } ; chosen : vertexset {$$.vertexset=$1.vertexset; $$.ival=$1.ival; Chosen=$$.vertexset; checkchosen(Chosen,pointer); Assert(order($1.vertexset)==$$.ival,"chosen size incorrect");} ; neighbours : vertexset {$$.vertexset=$1.vertexset; $$.ival=$1.ival; Neighbours=$$.vertexset; checkneighbours(Chosen,Neighbours,pointer); } rejected : vertexset {$$.vertexset=$1.vertexset; $$.ival=$1.ival; Rejected=$$.vertexset; checkreject(Chosen,Rejected,pointer); } forced : forceout forcein { merge($1.vertexset,$2.vertexset,pointer); $$.vertexset=$1.vertexset; $$.ival=$1.ival+$2.ival; Assert(order($$.vertexset)==$$.ival, "forced in and exclusions overlap?"); } | forceout {$$.vertexset=$1.vertexset; $$.ival=$1.ival;} | forcein {$$.vertexset=$1.vertexset; $$.ival=$1.ival;} | { $$.vertexset=0; $$.ival=0; } ; forceout : minus INT COMMON NEIGHBOURS Bvertex WITH_OTHERS { int x=$5.ival,y,z; Assert(order(Chosen)==0,"2 out of last 3 not forced"); Assert(TwoB(),"no guarantee of 2 B vertices"); vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); clearvertexset(VSP); y=x==size-2?size-1:size-2; z=x==size?size-1:size; /* assign the common neighbours arbitrarily to y and z so that each has a positive number */ VSP->commonneighbour[x][y]=1; VSP->commonneighbour[x][z]=$2.ival-1; $$.vertexset=VSP; $$.ival=$2.ival; checklast(3,x,y,z,Chosen,Neighbours,Rejected); /* The forced out vertices are the common neighbours of B[x] and B[y] and those of B[x] and B[z] but we must avoid double counting of any overlap */ Assert($$.ival==pointer->mincommon[x][y]+pointer->mincommon[x][z] -pointer->maxcommon[y][z], "wrong number of common neighbours"); } | minus INT COMMON NEIGHBOURS Bvertex AND Bvertex /* common external neighbours of the two Bvertices are forced out but we must not count any which are already excluded because they are also adjacent to B[Bi] */ { vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); int maxtriplecommon=pointer->maxcommon[Bi][$5.ival]maxcommon[Bi][$7.ival]? pointer->maxcommon[Bi][$5.ival]:pointer->maxcommon[Bi][$7.ival]; Assert(order(Chosen)==1,"1 out of last 2 not forced"); Assert(TwoB(),"no guarantee of 2 B vertices"); clearvertexset(VSP); VSP->commonneighbour[$5.ival][$7.ival]=$2.ival; $$.vertexset=VSP; $$.ival=$2.ival; checklast(2,$5.ival,$7.ival,0,Chosen,Neighbours,Rejected); Assert($$.ival==pointer->mincommon[$5.ival][$7.ival]-maxtriplecommon, "wrong number of common neighbours"); } | minus INT COMMON NEIGHBOURS TWO_OF_LAST_THREE LPAR Bvertex AND Bvertex RPAR { vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); Assert(order(Chosen)==0,"2 out of last 3 not forced"); Assert(TwoB(),"no guarantee of 2 B vertices"); clearvertexset(VSP); VSP->commonneighbour[$7.ival][$9.ival]=$2.ival; $$.vertexset=VSP; $$.ival=$2.ival; checklast(3,$7.ival,$9.ival,0,Chosen,Neighbours,Rejected); Assert($$.ival==pointer->mincommon[$7.ival][$9.ival], "wrong number of common neighbours"); } ; forcein : minus INT NEIGHBOURS LPAR blist RPAR REDUCED DEGREE INT {vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); int numvertices=$5.ival, numneighbours=$2.ival; clearvertexset(VSP); while (numvertices>1) { VSP->neighbourinmis[$5.Bset[numvertices]]=1; numvertices--; numneighbours--; } VSP->neighbourinmis[$5.Bset[1]]=numneighbours; $$.vertexset=VSP; checkforcedin(Chosen,VSP,Neighbours,Rejected,pointer); $$.ival=$2.ival; } ; vertexset : /* an expression representing a set of vertices; attributes are: "vertexset" a pointer to the set struct and "ival" the size of the set (probably superfluous but an extra check against counting same vertex twice); nonterminals "vertex"and "vertices" have same attributes. */ LCURLY vertices RCURLY {$$.vertexset=$2.vertexset; $$.ival=$2.ival;} | vertex {$$.vertexset=$1.vertexset; $$.ival=$1.ival;} ; vertices : vertex {$$.vertexset=$1.vertexset; $$.ival=$1.ival;} | vertex and vertices { merge($1.vertexset,$3.vertexset,pointer); $$.vertexset=$1.vertexset; /*free($3.vertexset);*/ $$.ival=$1.ival+$3.ival; } | { vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); clearvertexset(VSP); $$.vertexset=VSP; $$.ival=0; } ; and : COMMA | PLUS ; vertex : /* a simple expression representing one or more vertices */ A { vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); clearvertexset(VSP); VSP->Av=true; $$.vertexset=VSP; $$.ival=1; } | Bvertex { vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); clearvertexset(VSP); VSP->Bv[$1.ival]=true; $$.vertexset=VSP; $$.ival=1; } /* In the last two cases the set is of INT (external) neighbours of a specified B vertex; in all cases the B vertex is chosen and so its neighbours are not in the independent set. */ | INT NEIGHBOURS Bvertex { vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); clearvertexset(VSP); VSP->neighbournotinmis[$3.ival]=$1.ival; $$.vertexset=VSP; $$.ival=$1.ival; } | AT_LEAST INT NEIGHBOURS Bvertex { vertexsetptr VSP=(vertexsetptr)myalloc(sizeof(vertexset)); clearvertexset(VSP); VSP->neighbournotinmis[$4.ival]=$2.ival; $$.vertexset=VSP; $$.ival=$2.ival; } ; blist : /* A list of B vertices; attributes are: "ival" the number of vertices in the list; "Bset" an array containing the indices of the B vertices (in positions [1..ival]) */ Bvertex {$$.ival=1; $$.Bset[1]=$1.ival;} | blist COMMA Bvertex { int j; $$.ival=$1.ival+1; $$.Bset[$$.ival]=$3.ival; for (j=1;j<$$.ival;j++) { Assert($1.Bset[j]!=$3.ival,"duplicates in B vertex list"); $$.Bset[j]=$1.Bset[j]; } } ; timing : /* the claimed bound on the timing for a single recursive call; e.g. "a5 (2 out of 5 : neighbours of B1)*alpha^-8=0.1974847706" meaning that the claimed bound is a5*alpha^-8 and (1) in the coefficient (a5) which means that two out of five vertices are to be included in the independent set, the five vertices are the neighbours of B[1]; (2) 8 vertices are removed from the graph for this call; (3) the numerical value of a5*alpha^-8 is 0.1974847706. Condition (1) will be checked internally in the coefficient, condition (2) will be checked later using the value 8 which is returned as the value of attribute "ival", condition (3) is checked here and the value (0.1974847706) returned as attribute "rval". */ COLON coefficient power EQUAL REAL {$$.ival=$3.ival;$$.rval=$5.rval; Assert(approx($5.rval,$2.rval*poweralpha[$3.ival]),"arithmetic"); } | COLON power EQUAL REAL /* no coefficient */ {$$.ival=$2.ival;$$.rval=$4.rval; Assert(approx($4.rval,poweralpha[$2.ival]),"arithmetic"); } | /* this call can be omitted because the independent set is to contain more than INT neighbours of vertex B[i] but this is impossible */ OMITTED COLON text Bvertex text INT text {$$.ival=-1;$$.rval=0; checkomitclaim(pointer,$4.ival,Rejected); } ; coefficient : /* A coefficient or constant has two attributes: "constant" a pointer to the constant struct (will be left in variable "constant" to be checked later for compatibility with justification given), "rval" the numerical value of the constant */ constant {constant=$1.constant;} LPAR comment COLON justification RPAR STAR {$$.rval=$1.rval;} ; constant : CONSTANT {$$.rval=$1.rval;$$.constant=$1.constant;} | power {$$.rval=$1.rval; $$.constant=$1.ival==1 ? constle2 : constd1; /* constant alpha^-1 is valid if a vertex has degree <= 1; alpha^-2 is valid if it has degree exactly 1 */ Assert($1.ival==1 || $1.ival==2, "impossible power of alpha used as coefficient"); } ; justification : /* A justification has no attributes; it checks that the information given justifies the coefficient stored in variable "constant". */ Bvertex /* this Bvertex will have low degree in the subgraph */ {Assert(constant->sort==1 || constant->sort==4, "wrong justification type"); Assert(!(Chosen->Bv[$1.ival] || Neighbours->Bv[$1.ival] || Rejected->Bv[$1.ival]), "low degree vertex not in rec. call graph"); if (constant->sort==1) Assert(Degree[$1.ival]<=constant->n,"degree doesn't match"); else Assert(Degree[$1.ival]==constant->n && mindegree[$1.ival]>0, "degree might be zero"); } | A_NEIGHBOUR Bvertex /* there must be a neighbour of this Bvertex which has low degree in the subgraph */ {int j; Assert(constant->sort==1, "wrong justification type"); Assert(Nhood,"no information about neighbours'degrees"); Assert(pointer->degree[$2.ival]==size,"wrong size"); /* there is a vertex Bj not adjacent to $2 and with degree d; so, by the choice of A, $2 had a neighbour of degree <= d and so now <=d-1 */ for (j=1; j<=size; j++) if (j!=$2.ival && !pointer->adj[j][$2.ival] && pointer->degree[j]==1+constant->n) break; Assert(j<=size,"no Bj found with necessary degree"); } | Bvertex AND Bvertex /* these are the last two Bvertices remaining and one must be included in the independent set to have a total of two B[i] in the set */ { Assert(Bichosen && !Bjchosen,"should be only one B chosen"); Assert(TwoB(),"cannot rely on 2 B vertices"); Assert(constant->sort==2,"wrong justification type"); Assert(constant->n==1,"no justification for two conditions"); checkexplicit(2,$1.ival,$3.ival,0,constant, Chosen, Neighbours, Rejected); } | Bvertex COMMA Bvertex AND Bvertex /* these are the last three Bvertices remaining and two must be included in the independent set to have a total of two B[i] in the set */ { Assert(constant->sort==2 || constant->sort==3, "wrong justification type"); Assert(constant->n==1,"no justification for two conditions"); Assert(TwoB(),"cannot rely on 2 B vertices"); checkexplicit(3,$1.ival,$3.ival,$5.ival,constant, Chosen, Neighbours, Rejected); if (constant->sort==3) /* not a triangle */ Assert(!(pointer->adj[$1.ival][$3.ival] && pointer->adj[$1.ival][$5.ival] && pointer->adj[$5.ival][$3.ival]),"triangle"); } | NEIGHBOURS Bvertex /* this Bvertex is rejected and so two of its neighbours must be in the independent set */ { Assert(constant->n==1,"no justification for two conditions"); checkxoutofycondition(constant,pointer,Rejected,$2.ival,1); } | NEIGHBOURS EACH Bvertex AND Bvertex /* The two Bvertices are both rejected and so must have two neighbours in the independent set; they have no common neighbours in the subgraph */ { Assert(constant->n==2,"justification for two conditions"); checkxoutofycondition(constant,pointer,Rejected,$3.ival,1); checkxoutofycondition(constant,pointer,Rejected,$5.ival,2); Assert(!pointer->maxcommon[$3.ival][$5.ival], "two x-out-of-y conditions may refer to non disjoint sets"); } | UNION NEIGHBOURS Bvertex AND Bvertex /* The two Bvertices are non-adjacent and both rejected (but adjacent to two chosen B vertices); if no external neighbour of either is in an independent set, Bi and Bj can be replaced in the independent set by these two; So, one of their combined external neighbours can be assumed to be in the independent set. */ { checkunion($3.ival,$5.ival,constant,pointer, Chosen, Neighbours, Rejected); } | NEIGHBOURS Bvertex AND LCURLY Bvertex COMMA Bvertex RCURLY /* Two x-out-of-y conditions; the first on the external neighbours of the first Bvertex, the second one out of the other two Bvertices; (these two sets are necessarily disjoint). */ { Assert(constant->n==2,"justification for two conditions"); checkxoutofycondition(constant,pointer,Rejected,$2.ival,2); checkexplicit(2,$5.ival,$7.ival,0,constant, Chosen, Neighbours, Rejected); } ; comment : /* no semantic content: reminder of meaning of coefficient inserted to make file readable by humans */ WORD comment | INT comment | DEGREE comment | NOT comment | AND comment | LE comment | EQUAL comment | ; power : /* alpha^-i: attributes are "ival"=i and "rval"the numeric value */ ALPHA EXPO minus INT {$$.ival=$4.ival;$$.rval=poweralpha[$4.ival];} ; total : TOTAL EQUAL REAL {$$.rval=$3.rval;} ; minus : DASH ; text : /* no semantic content: non-reserved words inserted to make file readable by humans */ WORD text | ; %% #include #include #include "lex.yy.c" main() { setupconstants(); yyparse(); } yyerror(char *s) { printf ("%s line number %i\n",s,line); }