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 (CHECKS := CHECKS + 1,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])
//

[revise(d:array<set>,c:tuple,i:integer,j:integer) : boolean
 -> //[3] revise(~S): d[~S] = ~S, d[~S] = ~S// c,i,d[i],j,d[j],
    let revised := false
    in (for x in copy(d[i])
        (let supported := false
         in (for y in d[j]
              (if check(c,x,y)
                 (supported := true,
                  return())),
              if not(supported)
                (delete(d[i],x),
                 revised := true))),
         CONSISTENT := d[i] != {},
         //[3] revised(~S): d[~S] = ~S// c,i,d[i],
         //[3] ---------//,
         revised)]

[ac3(d:array<set>,constraints:set) : boolean
 -> //[3] ac3(~S) // constraints,
    let Q := copy(constraints)
    in (while (Q != {} & CONSISTENT)
        let c := Q[1],
            i := c[2],
            j := c[3]
        in (delete(Q,c),
            if revise(d,c,i,j)
               Q := Q U {z in constraints | z[3] = i})),
    CONSISTENT]