Design and implementation of a modular interface to integrateCLP and tabled execution
Joaquín Arias · 2015
Logic programming (LP) is a family of high-level programming languages which provides high expressive power. With LP, the programmer writes the properties of the result and / or executable specifications instead of detailed computation steps. Logic programming systems which feature tabled execution and constraint logic programming have been shown to increase the declarativeness and efficiency of Prolog, while at the same time making it possible to write very expressive programs. Tabled execution avoids infinite failure in some cases, while improving efficiency in programs which repeat computations. CLP reduces the search tree and brings the power of solving (in)equations over arbitrary domains. Similarly to the LP case, CLP systems can also benefit from the power of tabling. Previous implementations which take ful advantage of the ideas behind tabling (e.g., forcing suspension, answer subsumption, etc. wherever it is necessary to avoid recomputation and terminate whenever possible) did not offer a simple, well-documented, easy-to-understand interface. This would be necessary to make the integratation of arbitrary CLP solvers into existing tabling systems possible. This clearly hinders a more widespread usage of the combination of both facilities. In this thesis we examine the requirements that a constraint solver must fulfill in order to be interfaced with a tabling system. We propose and implement a framework, which we have called Mod TCLP, with a minimal set of operations (e.g., entailment checking and projection) which the constraint solver has to provide to the tabling engine. We validate the design of Mod TCLP by a series of use cases: we re-engineer a previously existing tabled constrain domain (difference constraints) which was connected in an ad-hoc manner with the tabling engine in Ciao Prolog; we integrateHolzbauer’s CLP(Q) implementationwith Ciao Prolog’s tabling engine; and we implement a constraint solver over (finite) lattices. We evaluate its performance with several benchmarks that implement a simple abstract interpreter whose fixpoint is reached by means of tabled execution, and whose domain operations are handled by the constraint over (finite) lattices, where TCLP avoids recomputing subsumed abstractions.---ABSTRACT---La programacion logica con restricciones (CLP) y la tabulacion son extensiones de la programacion logica que incrementan la declaratividad y eficiencia de Prolog, al mismo tiempo que hacen posible escribir programasmas expresivos. Las implementaciones anteriores que integran completamente ambas extensiones, incluyendo la suspension de la ejecucion de objetivos siempre que sea necesario, la implementacion de inclusion (subsumption) de respuestas, etc., en todos los puntos en los que sea necesario para evitar recomputaciones y garantizar la terminacion cuando sea posible, no han proporcionan una interfaz simple, bien documentada y facil de entender. Esta interfaz es necesaria para permitir integrar resolutores de CLP arbitrarios en el sistema de tabulacion. Esto claramente dificulta un uso mas generalizado de la integracion de ambas extensiones. En esta tesis examinamos los requisitos que un resolutor de restricciones debe cumplir para ser integrado con un sistema de tabulacion. Proponemos un esquema (y su implementacion), que hemos llamadoMod TCLP, que requiere un reducido conjunto de operaciones (en particular, y entre otras, entailment y proyeccion de almacenes de restricciones) que el resolutor de restricciones debe ofrecer al sistema de tabulacion. Hemos validado el diseno de Mod TCLP con una serie de casos de uso: la refactorizacion de un sistema de restricciones (difference constraints) previamente conectado de un modo ad-hoc con la tabulacion de Ciao Prolog; la integracion del sistema de restricciones CLP(Q) de Holzbauer; y la implementacion de un resolutor de restricciones sobre reticulos finitos. Hemos evaluado su rendimiento con varios programas de prueba, incluyendo la implementacion de un interprete abstracto que alcanza su punto fijo mediante el sistema de tabulacion y en el que las operaciones en el dominio son realizadas por el resolutor de restricciones sobre reticulos (finitos) donde TCLP evita la recomputacion de valores abstractos de las variables ya contenidos en llamadas anteriores.