Tutorial

1.1 Loading a Program

This first chapter is a short tutorial that introduces the major concepts gradually. It contains enough information for a reader familiar with other object-oriented language to start practicing with claire. Each aspect of the language will be detailed in a further chapter. All the examples that are shown here should be available as part of the standard claire system so that you should not need to type the longer examples.

The first step that must be mastered to practice with claire is to learn how to invoke the compiler or the interpreter. Notice that you may obtain a warning if you load claire and no file « init.cl » is found in your current directory. You can ignore this message for a while, then you may use such a file to store some of your favorite settings. You are now ready to try our first program. This program simply prints the release number of the claire system that you are using.

main() -> printf("claire release ~A\n", release())

You must first save this line on a file, using your favorite text editor (e.g. emacs). Let us now assume that this one-line program is in a file release.cl.  Using a file that ends with .cl is not mandatory but is strongly advised.

When you invoke the claire executable, you enter a loop called a top-level[1]. This loop prompts for a command with the prompt "claire>" and returns the result of the evaluation with a prompt "[..]". The number inside the brackets can be used to retrieve previous results (this is explained in the last appendix). Here we assume that you are familiar with the principle of a top-level loop; otherwise, you may start by reading the description of the claire top-level in the Appendix C. To run our program, we enter two commands at the top-level. The first one load("release") loads the file that we have written and returns true to say that everything went fine. The second command main() invokes the method (in claire a procedure is called a method) that is defined in this file.

% claire

claire> load("release")

eval[1] true

claire> main()

eval[2] claire release 4.0.4 

claire> q

%

Each claire program is organized into blocks, which are surrounded by parentheses, and definitions such as class and method definition. Our program has only one definition of the method main. The declaration main() tells that this method has no parameters, the expression after the arrow  -> is the definition of the method. Here it is just a printf statement, that prints its first argument (a format string) after inserting the other arguments at places indicated by the control character ~ (followed by an option character which can be A,S,I). This is similar to a C printf, except that the place where the argument release()  must be inserted in the control string is denoted with ~S. There is no need to tell the type of the argument for printf, claire knows it already. We also learn from this example that there exist a pre-defined method release() that returns some version identification, and that you exit the top-level by typing q (^D also works).

In this example, release() is a system-defined method[2]. The list of such methods is given in the second appendix. When we load the previous program, it is interpreted (each instruction becomes a claire object that is evaluated). It can also be compiled (through the intermediate step of C++ code generation). To compile a program, one must place it into a module, which plays a double role of a compilation unit and namespace. The use of modules will be explained later on.

Let us now write a second program that prints the first 11 Fibonacci numbers. We will now assume that you know how to load and execute a program, so we will only give the program file. The following example defines the fib(n) function, where fib(n) is the n-th Fibonacci number.

fib(n:integer) : integer
    -> (if (n < 2) 1 else fib(n - 1) + fib(n - 2))

main() -> (for i in (0 .. 10) printf("fib(~S) = ~S\n",i,fib(i)))

From this simple example, we can notice many interesting rules for writing method in claire. First, the range of a method is introduced by the "typing" character ":". The range is mandatory if the function returns a useful result since the default range is void, which means that no result is expected. Conditionals in claire use a traditional if construct (Section 3.3), but the iteration construct "for" is a set iteration. The expression for x in S e(x) evaluates the expression e(x) for all values x in the set S. There are many kinds of set operators in claire (Section 3.1); (n .. m) is the interval of integers between n and m.

Obviously, this program is very naive and is not the right way to print a long sequence of Fibonacci numbers, since the complexity of fib(n) is exponential. We can compute the sequence using two local variables to store the previous values of fib(n - 1) and fib(n - 2).  The next example illustrates such an idea and the use of let, which is used to introduce a list of local variables. Notice that they are local variables, whose scope is only the instruction after the keyword in. Also notice that a variable assignment uses the symbol :=, as in PASCAL, and the symbol = is left for equality.

main()
  ->  let n := 2, f_n-1 := 1, f_n-2 := 1 in
    (   printf("fib(0) = 1 \nfib(1) = 1\n"),
        while (n < 10)
            let f_n := f_n-1 + f_n-2 in
              ( printf("fib(~S) = ~S \n",n,f_n),
                  n := n + 1, f_n-2 := f_n-1, f_n-1 := f_n)  )

Note that we used f_n-1 and f_n-2 as variable names. Almost any character is allowed within identifiers (all characters but separators, '/', '#' and @). Hence, x+2 can be the name of an object whereas the expression denoting an addition is x + 2. Blank spaces are always mandatory to separate identifiers. Using x+2 as a variable name is not a good idea, but being able to use names such as *% that include “arithmetic” characters is quite useful.

Warning:  claire’s  syntax is intended to be fairly natural for C programmers, with expressions that exist  both
                in CLAIRE and C having the same meaning. There are two important exceptions to this rule: the    
                choice of  := for assignment and = for equality, and the absence  of special status for  characters
              +, *, -, etc. Minor differences include the use of & and | for boolean operations and % for
                membership.

A more elegant way is to use a table fib[n], as in the following version of our program.

fib[n:integer] : integer :=  1

main()
  ->  (for i in (2 .. 10) fib[i] := fib[i - 1] + fib[i - 2],
    for i in (0 .. 10) printf("fib(~S) = ~S\n",i,fib[i]) )

An interesting feature of claire is that the domain of a table is not necessarily an interval of integers. It can actually be any type, which means that tables can be seen as "extended dictionaries" (Section 5.1). On the other hand, when the domain is a finite set, claire allows the user to define an "initial value" using the := keyword, as for a global variable assignment. For instance, the ultimate version of our program could be written as follows (using the fact that intervals are enumerated from small to large).

fib[n:(0 .. 10)] : integer := (if (n < 2) 1 else fib[n - 1] + fib[n - 2])

main() -> (for i in (0 .. 10) printf("fib(~S) = ~S\n",i,fib[i]))

Let us now write a file copy program. We use two system functions getc(p) and putc(p) that respectively read and write a character c on an input/output port p. A port is an object usually associated with a file from the operating system. A port is open with the system function fopen(s1,s2)  where s1 is the name of the file (a string) and s2 is another string that controls the way the port is used (cf. Section 6.1; for instance "w" is for writing and "r" is for reading).

copy(f1:string,f2:string)
  -> let p1 := fopen(f1,"r"),
        p2 := fopen(f2,"w"),
        c := ' ' in
    (use_as_output(p2),
    while (c != EOF) (c := getc(p1), putc(c,p2)),
    fclose(f1), fclose(f2) )

Let us now write a program that copies a program and automatically indents it. Printing with indentation is usually called pretty-printing, and is offered as a system method in claire: pretty_print(x) pretty-prints on the output port. All claire instructions are printed so that they can be read back. In the previous example, we have used two very basic read/write methods (at the character level) and thus we could have written a very similar program using C. Here we use a more powerful method called read(p) that reads one instruction on the port p (thus, it performs the lexical & syntactical analysis and generate the claire objects that represents instructions). Surprisingly, our new program is very similar to the previous one.

copy&indent(f1:string,f2:string)
  -> let p1 := fopen(f1,"r"),
        p2 := fopen(f2,"w"),
        c := unknown in
    ( use_as_output(p2),
      while (c != eof)
        pretty_print(c := read(p1)),
      fclose(p1), fclose(p2) )

Module organization is a key aspect of software development and should not be mixed with the code. Modules’ definitions are placed in the init.cl file which is loaded automatically by the interpreter or the compiler. It is also possible to put module definitions in a project file, and to load this file explicitly.

  ;; modules definitions
  phone_application :: module(   part_of = claire,
                          made_of = list(“phone”))
  phone_database :: module(part_of = phone_application)

The statement part_of = y inside the definition of a module x says that x is a new child of the module y. We can then call load(phone_application) to load the file in the phone_application namespace. This is achieved through the slot made_of that contains the list of files that we want to associate with the module (cf. Part 6).

Our next program is a very simplified phone directory. The public interface for that program is a set of two methods store(name, phone) and dial(name). We want all other objects and methods to be in a different namespace, so we place these definitions into the module called phone_application. We also use comments that are defined in claire as anything that in on the same line after the character ‘;’ or after the characters ‘//’ as in C++.

  // definition of the module
  begin(phone_application)

  // value is a table that stores the phone #
  private/value_string[s:string] : string

  // lower returns the lower case version of a string
  // (i.e. lower("aBcD") = "abcd")
  lower(s:string) : string
  -> let s2 := copy(s) in
    (  for i in (1 .. length(s))
            (if (integer!(s2[i]) % (integer!('A') .. integer!('Z'))
                s2[i] := char!(integer!(s2[i]) + 32))
      s2)

  claire/store(name:string,phone:string)
    -> (value_string[lower(name)] := phone)

  claire/dial(name:string) : string   // returns the phone #
    -> value_string[lower(name)]

  end(phone_application)

This example illustrates many important features of modules. Modules are first-class objects; the statement begin(x) tells CLAIRE to use the namespace associated with the module x. We may later return to the initial namespace with end(x). When begin(x) has been executed, any new identifier that is read will belong to the new namespace associated with x. This has an important consequence on the visibility of the identifier, since an identifier lower defined in a module phone_application is only visible (i.e. can be used) in the module phone_application itself or its descendents. Otherwise, the identifier must be qualified (phone_application/lower) to be used. There are two ways to escape this rule: first, an identifier can be associated to any module above the currently active module, if it is declared with the qualified form. Secondly, when an identifier is declared with the prefix private/, it becomes impossible to access the identifier using the qualified form. For instance, we used private/value to forbid the use of the table (in the claire sense) anywhere but in the descendents of the module phone_application

The previous example may be placed in any file and loaded at any time. However, the preferred way to write the code associated with a module is to place it in one of the files that have been identified in the made_of slot (here, “phone.cl”). These files may be loaded inside a module's namespace using the load(m:module) method, without any explicit use of begin/end. For instance, we could remove the first and last lines in the previous example and put the result in the file phone.cl.

Appendix C shows the command-line syntax for invoking CLAIRE. For the time being, it is useful to know that claire –f <file> invokes claire and loads the file <file>. Also, claire –m <module> is similar but loads the module <module> which is defined in the init.cl file.

[1]  In the following we assume that CLAIRE is invoked in a workstation/PC environment using a command shell. You must first find out how to invoke the CLAIRE system in your own environment.

[2] The release is a string « 4.X.Y » and the version is a float X.Y, where X is the version number and Y the revision number. The release number in this book (4) should be the same as the one obtained with your system. Changes among different version numbers should not affect the correctness of this documentation.

1.2 Objects and Classes

Our next example is a small pricing program for hi-fi Audio components[1]. The goal of the program is to manage a small database of available material, to help build a system by choosing the right components (according to some constraints) and compute the price.

We start by defining our class hierarchy:

  component <: thing(price:integer, brand:string)
  amplifier <: component( power:integer, input:integer,
                                ohms:set[{4,8}])
  speaker <: component(maxpower:integer, ohm:{4,8})
  headphone <: component(maxpower:integer,  ohm:{4,8})
  musical_source <: component(sensitivity:integer)
  CDplayer <: musical_source(laser_beams:(1 .. 3))
  turntable <: musical_source()
  tuner <: musical_source()
  B :: thing() C :: thing()  nodolby :: thing()
  tape <: musical_source(dolby:{nodolby,B,C})
  stereo <: object( sources:set[musical_source],
                amp:amplifier,
                out:set[speaker U headphone],
                warranty:boolean = false)

Now that we have defined the taxonomy of all the objects in our hive world, we can describe the set of all models actually carried by our store. These are defined by means of instances of those classes.

  amp1 :: amplifier(power = 120, input = 4, ohms = {4,8},
                price = 400, brand = "Okyonino")
  amp2 :: amplifier(power = 40, input = 2, ohms = {4},
                price = 130, brand = "Cheapy")
  tuner1 :: tuner( sensitivity = 10, price = 200, brand = "Okyonino")
  tuner2 :: tuner( sensitivity = 30, price = 80, brand = "Cheapy")
  CD1 :: CDplayer( sensitivity = 3, price = 300,
                laser_beams = 3, brand = "Okyonino")
  CD2 :: CDplayer( sensitivity = 7, price = 180,
                laser_beams = 2, brand = "Okyonino")
  CD3 :: CDplayer( sensitivity = 15, price = 110,
                laser_beams = 1, brand = "Cheapy")
  t1 :: tape(  sensitivity = 40, price = 70,
            dolby = nodolby, brand = "Cheapy")
  s1 :: speaker(   ohm = 8, maxpower = 150,
                price = 1000, brand = "Magisound")
  s2 :: speaker(   ohm = 8, maxpower = 80,
                price = 400, brand = "Magisound")
  s3 :: speaker(   ohm = 4, maxpower = 40,
                price = 150, brand = "Cheapy")
  ph :: speaker(ohm = 4, maxpower = 40, price = 50, brand = "Okyonino")
    etc ...

Now that we have defined some components with their technical features, we can manipulate them and define some methods. For example, we can compute the total price of a stereo as the sum of the prices of all its components. We first need an auxiliary method that computes the sum of a list of integers.

  sum(s:list[integer]) : integer
    -> let n := 0 in (for y in s n :+ y, n)

  total_price(s:stereo) : integer
        -> sum(list{x.price | x in s.sources U set(s.amp) U s.out})

  InventoryTotal:integer :: 0

Note here the use of set image (we consider the list of all x.price  for all x in the following set: the union of s.sources, {s.amp}  and s.out ). Also, we introduce a global variable InventoryTotal, of range integer and value 0. If we want to keep some “specials” which are sets of components for which the price is less than the sum of its components, we may use a table to store them:

  discount[s:set[component]] : integer := 0
  discount[{amp1,s1}] := 1200
  discount[{amp1,CD1}] := 600

To find the best price of a set of components, we now write a more sophisticated method that tries to identify the best subsets that are on sale. This is a good example of CLAIRE’s programming style (if we assume that size(s) is small and that discount contains thousands of tuples).

 [best_price(s:set[component]) : integer
  -> let p := 100000 in
    (if (size(s) = 0) p := 0
        else if (size(s) = 1) p := price(s[1])
        else for s2 in set[s]      ;; decompose s = s2 U ...
          let x := size(s2),
              p2 := (if (x > 1) discount[s2]
                    else if (x = 1) price(s2[1])
                    else 0)  in
          (if (p2 > 0) p :min (p2 + best_price(difference(s,s2)))),
      p) ]

Notice that we use some syntactical sugar here:  p :min x is equivalent to p := (p min x). This works with any other operation (such as +).

[1] All brands and product names are totally fictitious.

1.3 Rules

We now want to do some reasoning about stereo systems. We start by writing down the rules for matching components with one another. We want a signal to be raised whenever one of these rules is violated. Hence we create the following exception:

  technical_problem <: exception(s:string)

A rule is defined by a condition and a conclusion (using a pattern rule(condition => conclusion) ). The condition is the combination of an event pattern and a Boolean expression. The event pattern tells when  the Boolean expression should be checked, in case of success the conclusion is evaluated. Here are some simple rules that will raise exceptions when some technical requirements are not met.

  compatibility1() :: rule(
    st.speaker :add sp & not(sp.ohms % st.amplifier.ohms) )
    => technical_problem(s = "conflict speakers-amp"))

  compatibility2() :: rule(
    st.sources :add x & size(st.sources) > st.amp.inputs
    => technical_problem(s = "too many sources"))

  compatibility3() :: rule(
      (st.out :add x) & x.maxpower < st.amp.power
      => technical_problem(s = "amp to strong for the speakers"))

We can now use our system (applying the rules on the small database) to look for consistent systems. For example, suppose that I want to buy speakers that fit my amp (for instance, amp1): we will try several possibilities to fill the slot out  of my stereo and will watch whether they raise an exception or not. In order for the rule to be triggered, we need to tell which changes in the database are relevant to rule triggering. Here, modifications on the relation out  trigger the evaluation of the concerned rules.

  my_system :: stereo(amp = amp1)
  (exists(sp in speaker |
    (try (my_system.out :add sp, true)
      catch technical_problem
        (//[0] rejects ~S because ~A // sp, exception!().s,
          my_system.out :delete sp,
          false))),

If we want to successively choose the speakers, the CD player, the tape, etc.. We cannot guarantee that if a choice does not immediately raise an exception, there will always exist a solution in the end. Thus, we need to make some hypothetical reasoning: we suppose one branch of the choice contains a solution, and we backtrack on failure. The conclusions that had been drawn during the hypothesis need to be undone. To do so, we can declare that some relations in the database are stored in a special way such that one can go back to a previous state. Such states of the database (versions) are called worlds. The methods choice()  and backtrack()  respectively create a new world (i.e., create a choice point) and return to the previous one. The command store(out)  means that the graph of the relation out  will be stored in that special way adapted to the world mechanism. In this example, we create the list of all possible (bringing no conflict according to the rules) stereos with two different musical sources.

store(out)

all_possible_stereos() : list[stereo]
  -> let solutions := list<stereo>() , syst:stereo := stereo() in
      (for a in amplifier
        (syst.amp := a,
          for sp in speaker  try
            (choice(),
            syst.out := set(sp),
            for h in headphone try
              (choice(),
                syst.out :add h,
                for s1 in musical_source try
                  (choice(),
                  syst.sources := set(s1),
                  for s2 in {s in musical_source |
                              owner(s) != owner(s1) & s.price < s1.price} try
                      (choice(),
                      syst.sources :add s2,
                      solutions :add copy(syst),
                      backtrack())

         catch technical_problem backtrack(),
                backtrack())
              catch technical_problem backtrack(),
              backtrack())
          catch technical_problem backtrack(),
          backtrack())
    catch technical_problem  backtrack()),
    solutions) 

This method explores the tree of all possibilities for stereos and returns the list of all the valid ones.

Here is a last example of a method that returns the list of all possible stereos, classified by increasing prices. The same thing could be done with other criteria of choice.

price_order(s1:stereo, s2:stereo) : boolean -> (total_price(s1) <= total_price(s2))

cheapest() : list[stereo] ->
  let l := all_possible_stereos() in sort(price_order @ stereo, l) ]

1.4 Worlds & Hypothetical Reasoning

We shall conclude this tutorial with a classical SUDOKU example, since it illustrates the benefits of built-in hypothetical reasoning in CLAIRE using the “world mechanism” (cf. Section 5.3).

The first part of our last program describes the Sudoku data structures: cells, grid and cell sets. Cells are straightforward, defined by x,y coordinates and value, which is the integer between 1 and 9 that we need to find. A grid is simply a 9 x 9 matrix of cells. The only subtlety of our data model is the explicit representation of lines, column and 3x3 squares as subsets of cells called CellSets (with a unique property: each digit must appear exactly once in each such set).

We notice that we declare value and count to be defeasible slots (cf. Section 5) which will enable hypothetical reasoning (to search for the solution). We also create an “event” property (countUpdate) to be used with a rule.

// data structure

Cell <: object

CellSet <: object

// cell from a 9 x 9 Sudoku grid

Cell[x,y] <: object(x:integer,

                 y:integer,

                    possible:list<boolean>,  // list of possible values for the cell

                 count:integer = 9,   // number of possible value

                 value:integer = 0,   // assigned value to the cell (0 = none)

                 line:CellSet,        // the line to which the cell belongs

                 column:CellSet,      // same for column …

                 square:CellSet)      // one of the 9 3x3 squares

// a set of cells: line, column, square that holds the AllDiff constraint

CellSet[cells] <: object(cells:list<Cell>,          // cells that belong to the set

                         counts:list<integer>)      // a possible value counter

// two defeasible slots for hypothetical reasoning, but possible uses direct store

store(value,count)

// event that signals an update on counts for value v

countUpdate :: property(domain = CellSet, range = (1 .. 9))

// creates a cell

makeCell(a:integer,b:integer) : Cell

  -> Cell(x = a, y = b, possible = list<boolean>{true | i in (1 .. 9)}, value = 0)

// A sudoku grid

Grid <: object(cells:list<Cell>,

               lines:list<CellSet>,

               columns:list<CellSet>,

               squares:list<CellSet>)

// useful for debug

nth(g:Grid,i:(1 .. 9),j:(1 .. 9)) : Cell -> some(c in g.cells | c.x = i & c.y = j)

// creates a grid

makeGrid() : Grid

  -> let g := Grid() in

   (for i in (1 .. 9)

     for j in (1 .. 9) g.cells :add makeCell(i,j),

   for i in (1 .. 9)

     let li := list<Cell>{c in g.cells | c.x = i},

         cs := CellSet(cells = li, counts = list<integer>{9 | i in (1 .. 9)}) in

        (g.lines :add cs,

         for c in li c.line := cs),

    for j in (1 .. 9)

    let co := list<Cell>{c in g.cells | c.y = j},

         cs := CellSet(cells = co, counts = list<integer>{9 | i in (1 .. 9)}) in

      (g.columns :add cs,

        for c in co c.column := cs),

  for k1 in (1 .. 3)

     for k2 in (1 .. 3)

       let sq := list<Cell>{c in g.cells | abs(3 * k1 - c.x - 1) <= 1 &

                                            abs(3 * k2 - c.y - 1) <= 1},

               cs := CellSet(cells = sq, counts = list<integer>{9 | i in (1 .. 9)}) in

          (g.squares :add cs,

              for c in sq c.square := cs),

      g)

We now define a few rules that capture the reasoning about possible values for each cells. The first rule is triggered when we select a value for a cell. We disable the counters associated with the three “cell sets” of the cell (its line, its column and its 3x3 neighbor square) and the value v that got picked : the assignment of 0 to the counter tells that it is no longer necessary since the value v was used for these “CellSets”. We then propagate the information that, since v was picked, all other values that were still possible for this cell are no longer possible (using the “noLonger” method. Last, we propagate to the three CellSets the fact that v is not allowed any more, using the “forbid” method. This method main ambition is to remove v for the “c.possible” list of possible value (using the store defeasible update which is explained in chapter 5), and then to maintain the “counters” associated with the cellsets. However, there is a trick: there are other rules, and it is possible that some of the inferences yield contradictory conclusion. Therefore, when we remove a possible value, we must make sure that it has not been picked as the current value by some other action. If this is the case, we raise a “contradiction”, a special kind of CLAIRE exception.
The second rule is much simpler: when there is only one possible value for a cell, we can deduce that the cell must contain this value The third rule is triggered by the “updateCount” event, which occurs when we change the counter associated with a CellSet (in the “oneLess” method). This rule (r3) says that when a counters reaches 1, we may assign this value to the only cell in the CellSet which is still a candidate.

// first propagation rule

r1() :: rule(

  c.value := v => (store(c.line.counts,v,0),    // disable counts[v] since v was found !

                      store(c.column.counts,v,0),

                      store(c.square.counts,v,0),

                   for v2 in (1 .. 9)            // for all values v2 that were still OK

                     (if (v != v2 & c.possible[v2]) noLonger(c,v2),

                   for c2 in (c.line.cells but c) forbid(c2,v),  // v is used for c.line

                   for c2 in (c.column.cells but c) forbid(c2,v), // … and c.column

                   for c2 in (c.square.cells but c) forbid(c2,v))))  // … and c.square

// noLonger(c,v2) tells that v2 is no longer a possible value

noLonger(c:Cell,v2:(1 .. 9)) : void

  ->  (store(c.possible,v2,false),       // avoid double count

    oneLess(c.line,v2),           // v2 looses one support cell for c.line

    oneLess(c.column,v2),         // same for c.column

    oneLess(c.square,v2))         // and c.square

// forbid a value

// Attention: if we forbid a value that is assigned, we must raise a contradiction

forbid(c:Cell,v:(1 .. 9))

  -> (//[3] forbid ~S(~A) -> ~A // c,c.value,v,

   if (c.value = v) (//[5] contradiction while propagation //,

                     contradiction!())

   else if (c.value = 0 & c.possible[v])

      (store(c.possible,v,false),

       c.count :- 1,

       oneLess(c.line,v),

       oneLess(c.column,v),

       oneLess(c.square,v)))

// remove a value in a CellSet

oneLess(cs:CellSet,v:(1 .. 9)) : void

  -> let cpos := cs.counts[v] in

   (if (cpos > 0)               // cpos = 0 counter is inactive

      (store(cs.counts,v,cpos - 1), // update the counter

       updateCount(cs,v)))         // creates an event

// second rule : if c.count = 1, the only possible value is certain

r2() :: rule(

  c.count := y & y = 1 =>  c.value := some(y in (1 .. 9) | c.possible[y]))

// third rule (uses the CellSetSupport event) :

// if a value v is possible only in one cell, it is certain

r3() :: rule(

  updateCount(cs,v) & cs.counts[v] <= 1

  => when c := some(c in cs.cells | c.value = 0 & c.possible[v]) in c.value := v

     else contradiction!())

The hard part of the program is the set of rules, because it captures the logic inferences. Solving the puzzle is easy because we may leverage CLAIRE’s built-in hypothetical capabilities, that is, the ability to explore a search tree. To define the search tree, we create a method “findPivot” which select the cell with smallest “support” set of possible values. The exploration of the search tree (solve) is defined recursively:  pick the pivot cell, for each value in the possible set, try to assign this value to the cell and recursively call the solve method. We use the branch(X) control structure (cf. Section 3.6), which creates a “branch” of the search tree and evaluate the CLAIRE expression X within this branch. If X returns true, the search is considered a success and the current state is returned. If X returns false, the search has failed and the branch is removed, that is, CLAIRE returns to its previous state before branch(X) was invoked. Notice that the method solve is only 5 lines long and that it is very easy to modify to accomplish other goals, such as counting the number of solutions to the Sudoku problem.

// finds a cell with a min count (naive heuristic)

[findPivot(g:Grid) : any

  -> let minv := 10, cmin := unknown in

        (for c in g.cells

           (if (c.value = 0 & c.count < minv)

               (minv := c.count, cmin := c)),

         cmin) ]

// solve a sudoku : branch on possible values using a recursive function

// branch(...) does all the work :)

[solve(g:Grid) : boolean

  -> when c := findPivot(g) in

        exists(v in (1 .. 9) |

               (if c.possible[v] branch((c.value := v, solve(g)))

                else false))

  else true]

// show the solution

[see(g:Grid)

  -> printf("\n\t------------------\n"),

  for i in (1 .. 9) printf("\t~I\n",(for j in (1 .. 9) printf("~A ",g[i,j].value))) ]

To play with this program, all we need is a small method that translates an existing Sudoku problem (taken from a magazine, expressed as a list of list of integers, where 0 represents the absence of value).

// create a grid from a problem

[grid(l1:list[list[integer]]) : Grid

   -> let g := makeGrid() in

        (assert(length(l1) = 9),

         for c in g.cells

           let i := c.x, j := c.y, val := l1[i][j] in

             (if (val != 0)  c.value := val),

          g) ]

// example from Yvette

S1 :: grid(list(list(0,3,0,0,9,0,0,1,0),

                list(0,0,7,0,0,0,0,0,6),

                list(0,0,0,0,3,4,0,0,7),

                list(0,0,0,0,0,0,0,0,3),

                list(8,2,1,0,5,0,4,7,9),

                list(9,0,0,0,0,0,0,0,0),

                list(4,0,0,5,2,0,0,0,0),

                list(3,0,0,0,0,0,2,0,0),

                list(0,6,0,0,4,0,0,5,0)))

// this could be entered from the CLAIRE top-level

(solve(S1), see(S1))