// Header for the chk8 programs

GLOBAL {
 relspace: ug   // Space for the relation nodes
 relspacep      // Position of next relation node
 relspaceupb    // Upb of relspace

 relv           // Vector of relations, bounds 1..reln
 reln           // Number of relations
 relvupb        // Upb of relv

 maxid          // New var ids are in the range 1..maxnewid

 refs           // refs!id is list of each relation using id
 refcount       // refcount!id is the length of refs!id

 varinfo        // information about each id
                // varinfo!i = -2  was used in only one relation
                // varinfo!i = -1  nothing known about vi
                // varinfo!i =  0  vi = 0
                // varinfo!i =  1  vi = 1
                // varinfo!i =  2*id    if vi=vid
                // varinfo!i =  2*id+1  if vi=~vid

 id2orig        // mapping from old to new id
                // id2orig!0 is zero or the parent mapping vector
 origid         // function to find the original id using id2orig

 //old2new        // mapping from old to new id

 relstack       // Stack of relations that have recently changed
 relstackp      // Top of relstack -- points to latest item pushed
 relstackupb    // Upb of relstack

 tracing        // Cause trace output to be generated


 // Boolean matrices
 matn           // (=maxid) Size of matrix
 matnw          // Number of 32-bit words in a row

 mata           //  vi ->  vj
 matb           //  vi -> ~vj
 matc           // ~vi ->  vj
 matd           // ~vi -> ~vj

 // The matrices before the latest changes
 mataprev       //  vi ->  vj
 matbprev       //  vi -> ~vj
 matcprev       // ~vi ->  vj
 matdprev       // ~vi -> ~vj

// Functions in chk8
 rdrels         // Read relations in from a given file
 rdhex          // Read a hex number, ignoring comments
 rdnum          // Read a decimal number, ignoring comments
 
 wrrels         // Write relations out to file
 wrrel          // Write a relation out to file

 // Functions in module trans1
 trans1          // trans1 module

 exchargs          // Exchange arguments i and j in a relation
 ignorearg         // remove argument i assuming it is unconstrained
 standardise       // Sort relation arguments and remove duplicates

 split             // Attempt to split a relation into two

 // Functions in module apfns
 apfns             // apfns module

 apnot             // Negate argument i in a relation

 apset1            // Apply  ai  =   1
 apset0            // Apply  ai  =   0
 apeq              // Apply  ai  =  aj
 apne              // Apply  ai ~=  aj

 apimppp           // Apply  ai ->  aj
 apimppn           // Apply  ai -> ~aj
 apimpnp           // Apply ~ai ->  aj
 apimpnn           // Apply ~ai -> ~aj

 // Functions in module apvar
 apvar             // apvar module

 ignorevar         // eliminate an ignorable varible from a relation

 apvarset1            // Apply  vi  =   1 to all relations
 apvarset0            // Apply  vi  =   0 to all relations
 apvareq              // Apply  vi  =  vj to all relations
 apvarne              // Apply  vi ~=  vj to all relations

 apvarimppp           // Apply  vi ->  vj to all relations
 apvarimppn           // Apply  vi -> ~vj to all relations
 apvarimpnp           // Apply ~vi ->  vj to all relations
 apvarimpnn           // Apply ~vi -> ~vj to all relations

 // Functions in module trans2
 tests           // tests module

 findimps

 // Functions in module bmat
 bmat            // bmat module

 bm_setmatsize
 bm_mkmat
 bm_clrmat
 bm_warshall
 bm_setbitpp
 bm_setbitpn
 bm_setbitnp
 bm_setbitnn
 bm_setvar0
 bm_setvar1
 bm_setvareq
 bm_setvarne
 bm_setbit
 bm_prmat
 bm_findnewinfo


 // Functions in module engine
 engine           // engine module

 explore          // Apply the recursive explore algorithm

 // Functions in module utils
 utils            // utils module

 bug              // Report programming bug

 pairblks
 freepairs
 mk2
 unmk2

 ch
 token
 lexval
 
 rdrels
 wrrels
 formlists
 length

 wrvars

 pushrel          // Push a relation onto the relstack
 poprel           // Pop an item off the relstack

 rmref            // remove ref to a relation for a specified variable

 andrelbits1
 andrelbits2
 andrelbits4
 andrelbits8v

 // Functions in module debug
 debug            // utils module

 check1           // Debugging functions
 check2
 check3
 check4
 check5
 check6
 check7
 check8
 check9
 check10
 check11
 check12
}

MANIFEST {
 // Relation node fields
 r_w0=0; r_w1; r_w2; r_w3; r_w4; r_w5; r_w6; r_w7
 r_v0;   r_v1; r_v2; r_v3; r_v4; r_v5; r_v6; r_v7
 r_instack  // TRUE if this relation is in relstack
 r_weight   // Cumulative variable use counts
 r_varcount // Number variables -- unused ones are zero
 r_numb     // Relation number
 r_upb

 relnmax=1000
 //relspaceupb=relnmax*r_upb

 // rdrels symbols
 s_eof=1
 s_var
 s_bits
}

