Implementation Details

The solver is written using two novel software tools --- the APTS transformational programming system [16] and the high-level language SETL2 [96] --- each having special features that the solver exploits. The front-end to the constraint solver engine is an APTS program that reads the Erep program and type checks it. For example, we check that only lines participate in angle constraints. If there are no obvious type errors, the Erep program is transformed into an equivalent Erep specification in a normal form in which only distance and angle constraints are allowed. For example, incidence constraints are translated to zero-distance constraints. The specification of the orientation of lines in angle constraints is also regularized. Relations representing a constraint graph are then extracted from the Erep program and are exported via a foreign interface to a SETL2 program that implements the main algorithmic part of the solver.

The use of such novel systems as APTS and SETL2 is motivated by the special needs of our project. A major part of our research is the discovery and implementation of complex, nonnumerical algorithms. Our goal of high performance based on a new algebraic approach to constraint solving entails deep graph-theoretic analysis of implicit dependencies between constraints, and complex graph traversals based on such analysis. A wide variety of techniques seem available to us, but proper evaluation requires extensive labor-intensive computational experiments. Using these tools has allowed us to implement our algorithms with surprising speed. In the future we also hope to make use of a promising new technology for mechanically transforming prototype SETL2 programs into high performance C code [16].

The special syntactic, semantic, and transformational capabilities of APTS are also well suited to a flexible, experimental development of a logical framework with an evolving Erep language and corresponding solver. Like systems such as Centaur [6]. the Synthesizer Generator [82], and Refine [81], APTS has a single uniform formalism for lexical analysis, syntactic analysis, and pretty-printing. However, the semantic formalism in APTS has several advantages over the more conventional attribute grammar approach [55] that is used in the Synthesizer Generator. APTS uses a logic-based approach to semantics in which semantic rules that define relations are written in a Datalog-like language [14] but with the full expressive power of Prolog. These rules are written independently of the individual grammar productions and without reference to the parse tree structure. They define relations over a rich assortment of primitive and constructed domains, and have the brevity and convenience of unrestricted circular attribute grammars. We are not aware of any implementation that allows a comparable unrestricted circularity.