A Choice-Point Library for Backtrack Programming.
Pierre‐Etienne Moreau · 1998
Implementing a compiler for a language with nondeterministic features is known to be a difficult task. This paper presents two new functions setChoicePoint and fail that extend the C language to efficiently handle choice point management. Originally, these two functions were designed to compile the ELAN strategy language. However, they can be used by programmers for general programming in C. We illustrate their use by presenting the classical 8-queens problem and giving some experimental results. Algorithms and implementation techniques are sufficiently detailed to be easily modified and re-implemented. 1 Introduction In the area of formal specifications, rewriting techniques have been developed for two main applications: prototyping algebraic specifications of user-defined data types and theorem proving related to program verification. In this context we are interested in nondeterministic computation and deduction. Term rewriting is nondeterministic in the sense that there may be sev...