TCHR: a framework for tabled CLP

TL;DR

TCHR is a high-level framework that combines Constraint Handling Rules with tabled Logic Programming, enabling easier development of applications like program analysis and model checking, with customizable performance controls.

Contribution

It introduces TCHR, a novel, lightweight framework integrating CHR with tabled CLP, facilitating application-specific constraint domains and answer set compaction techniques.

Findings

Framework simplifies development of tabled CLP applications

Supports instantiation with new constraint domains

Includes a novel technique for compacting answer sets

Abstract

Tabled Constraint Logic Programming is a powerful execution mechanism for dealing with Constraint Logic Programming without worrying about fixpoint computation. Various applications, e.g in the fields of program analysis and model checking, have been proposed. Unfortunately, a high-level system for developing new applications is lacking, and programmers are forced to resort to complicated ad hoc solutions. This papers presents TCHR, a high-level framework for tabled Constraint Logic Programming. It integrates in a light-weight manner Constraint Handling Rules (CHR), a high-level language for constraint solvers, with tabled Logic Programming. The framework is easily instantiated with new application-specific constraint domains. Various high-level operations can be instantiated to control performance. In particular, we propose a novel, generalized technique for compacting answer sets.