N:integer        := 0
V:array<integer> := make_array(N,integer,-1)
D:array<set>     := make_array(N,set,{})
CD:array<set>    := make_array(N,set,{})
C:set            := {}

CHECKS:integer   := 0
NODES:integer    := 0

CONSISTENT:boolean := true

[stats() : void
 -> list("nodes",NODES,"checks",CHECKS)]

[reset(i:integer) : void
 -> V[i]  := -1,
    CD[i] := copy(D[i])]
//
// reset a variable
//

[reset() : void
 -> CHECKS := 0,
    NODES  := 0,
    CONSISTENT := true,
    for i in (1 .. N) reset(i)]
//
// reset everything
//

[look(i:integer) : void
 -> list(i,V[i],CD[i],D[i])]
//
// look at the ith variable, showing its
// index, value, and domain
//

[look() : boolean
 -> for i in (1 .. N) printf("\n~S",look(i)),
    CONSISTENT]
//
// look at everything
//

[getRelation(h:integer,i:integer,c:set) : set
 -> {z in c | (z[2] = h & z[3] = i)}]

[check(c:tuple,x:integer,y:integer) : boolean
 -> //[4] check(~S,~S,~S) // c,x,y,
    let l := list{c[k] | k in (4 .. length(c))} /+ list(x,y)
    in apply(c[1],l)]
//
// This now allows us binary constraints that involve
// more than just 2 arguments. For example, nqueens
// need to know rows and columns for two positions.
// We can now also produce extensional constraints as 
// sets of goods or nogoods
//

[check(h:integer,x:integer,i:integer,y:integer,c:set) : boolean
 -> let f := getRelation(h,i,c)
    in (if (size(f) = 0) 
          true           // no relation exists, therefore compatible
        else
            (//[3] check(~S, v[~S] = ~S & v[~S] = ~S) ~S// f[1][1],h,x,i,y,check(f[1],x,y),
             CHECKS := CHECKS + 1,
             check(f[1],x,y)))]
//
// Is it compatible for variable v[h] to take the value x
// and variable v[i] to take the value y, given the constraints
// C, where each constraint (f,j,k) in C is call(f,v[j],v[k])
//

[arcCons(d:array<set>,c:tuple) : set
 -> let s := {},
        i := c[2],
        j := c[3]
    in (for x in d[i]
        let supported := false
        in (for y in d[j]
             (supported := check(c,x,y),
              if supported return()),
            if not(supported) s := s U set(x)),
         s)]

[localArcCons(d:array<set>,c:tuple,w:integer) : set
 -> //[3] localArcCons(~S,~S) // c,w,
    arcCons(d,c)]
//
// opportunity to specialise this with resepect to c
//

[enqueue(i:integer,delta:set,q:set,constraints:set) : set
 -> // enqueue(~S,~S) // i,delta,
    for c in {z in constraints | z[3] = i}
     for w in delta
       q := q U set(tuple(c,w)),
     q]
//
// d[i] has lost the values delta
// add to the q tuples (c,w) where
//  - the constraint c is the constraint C_k,i
//  - w is in delta
//

[ac5(d:array<set>,constraints:set) : boolean
 -> //[3] ac5(~S) // constraints,
    let Q := {}
    in (for c in constraints
         let delta := arcCons(d,c),
             i := c[2]
         in (d[i] := difference(d[i],delta),
             Q := enqueue(i,delta,Q,constraints)),
        //[3] ------ // ,
        //[3] Q = ~S// Q,
        while (Q != {})
         (let t := Q[1],
              c := t[1],
              w := t[2],
              i := c[2],
              delta := localArcCons(d,c,w)
          in (delete(Q,t),
              Q := enqueue(i,delta,Q,constraints),
              //[3] Q = ~S// Q,
              d[i] := difference(d[i],delta)))),
        CONSISTENT]