Using parametric set constraints for locating 
errors in CLP programs

This paper introduces a framework of parametric descriptive directional types for Constraint Logic Programming (CLP). It proposes a method for locating type errors in CLP programs, and presents a prototype debugging tool. The main technique used is checking correctness of programs w.r.t. type specifications. The approach is based on a generalization of known methods for proving the correctness of logic programs to the case of parametric specifications. Set constraint techniques are used for formulating and checking verification conditions for (parametric) polymorphic type specifications. The specifications are expressed in a parametric extension of the formalism of term grammars. The soundness of the method is proved, and the prototype debugging tool supporting the proposed approach is illustrated on examples. The paper is a substantial extension of the previous work by the same authors concerning monomorphic directional types.

Download Full-text

Performing fully parallel constraint logic programming on a quantum annealer

Theory and Practice of Logic Programming ◽

10.1017/s1471068418000066 ◽

2018 ◽

Vol 18 (5-6) ◽

pp. 928-949 ◽

Cited By ~ 7

Author(s):

SCOTT PAKIN

Keyword(s):

Logic Programming ◽

Constraint Logic Programming ◽

Logic Programs ◽

Machine Model ◽

Computing Systems ◽

Model Hamiltonian ◽

Constraint Logic Programs ◽

Classical Computing ◽

Specialized Hardware ◽

High Level

AbstractAquantum annealerexploits quantum effects to solve a particular type of optimization problem. The advantage of this specialized hardware is that it effectively considers all possible solutions in parallel, thereby potentially outperforming classical computing systems. However, despite quantum annealers having recently become commercially available, there are relatively few high-level programming models that target these devices. In this article, we show how to compile a subset of Prolog enhanced with support for constraint logic programming into a two-local Ising-model Hamiltonian suitable for execution on a quantum annealer. In particular, we describe the series of transformations one can apply to convert constraint logic programs expressed in Prolog into an executable form that bears virtually no resemblance to a classical machine model yet that evaluates the specified constraints in a fully parallel manner. We evaluate our efforts on a 1,095-qubit D-Wave 2X quantum annealer and describe the approach's associated capabilities and shortcomings.

Download Full-text

Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP

Theory and Practice of Logic Programming ◽

10.1017/s1471068419000383 ◽

2019 ◽

Vol 19 (5-6) ◽

pp. 1107-1123

Author(s):

JOAQUÍN ARIAS ◽

MANUEL CARRO

Keyword(s):

Logic Programming ◽

Abstract Interpretation ◽

Constraint Logic Programming ◽

Additional Cost ◽

Logic Programs ◽

Semantic Equivalence ◽

Constraint Solver ◽

Abstract Domains ◽

Interpretation Algorithm ◽

Branch Switching

AbstractCiaoPP is an analyzer and optimizer for logic programs, part of the Ciao Prolog system. It includes PLAI, a fixpoint algorithm for the abstract interpretation of logic programs which we adapt to use tabled constraint logic programming. In this adaptation, the tabling engine drives the fixpoint computation, while the constraint solver handles the LUB of the abstract substitutions of different clauses. That simplifies the code and improves performance, since termination, dependencies, and some crucial operations (e.g., branch switching and resumption) are directly handled by the tabling engine. Determining whether the fixpoint has been reached uses semantic equivalence, which can decide that two syntactically different abstract substitutions represent the same element in the abstract domain. Therefore, the tabling analyzer can reuse answers in more cases than an analyzer using syntactical equality. This helps achieve better performance, even taking into account the additional cost associated to these checks. Our implementation is based on the TCLP framework available in Ciao Prolog and is one-third the size of the initial fixpoint implementation in CiaoPP. Its performance has been evaluated by analyzing several programs using different abstract domains.

Download Full-text

Failure tabled constraint logic programming by interpolation

Theory and Practice of Logic Programming ◽

10.1017/s1471068413000379 ◽

2013 ◽

Vol 13 (4-5) ◽

pp. 593-607 ◽

Cited By ~ 5

Author(s):

GRAEME GANGE ◽

JORGE A. NAVAS ◽

PETER SCHACHTE ◽

HARALD SØNDERGAARD ◽

PETER J. STUCKEY

Keyword(s):

Logic Programming ◽

Constraint Logic Programming ◽

Logic Programs ◽

Execution Strategy ◽

Speed Up ◽

Constraint Logic Programs

AbstractWe present a new execution strategy for constraint logic programs calledFailure Tabled CLP. Similarly toTabled CLPour strategy records certain derivations in order to prune further derivations. However, our method only learns fromfailed derivations. This allows us to computeinterpolantsrather thanconstraint projectionfor generation ofreuse conditions. As a result, our technique can be used where projection is too expensive or does not exist. Our experiments indicate that Failure Tabling can speed up the execution of programs with many redundant failed derivations as well as achieve termination in the presence of infinite executions.

Download Full-text

Integrating Cardinality Constraints into Constraint Logic Programming with Sets

Theory and Practice of Logic Programming ◽

10.1017/s1471068421000521 ◽

2021 ◽

pp. 1-33

Author(s):

MAXIMILIANO CRISTIÁ ◽

GIANFRANCO ROSSI

Keyword(s):

Logic Programming ◽

Decision Procedure ◽

Software Verification ◽

Empirical Evaluation ◽

Constraint Logic Programming ◽

Theory And Practice ◽

Finite Sets ◽

Cardinality Constraints ◽

Programming Tool ◽

Verification Conditions

Abstract Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool $$\{ log\} $$ provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into $$\{ log\} $$ . The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the $$\{ log\} $$ tool. In turn, the implementation uses Howe and King’s Prolog SAT solver and Prolog’s CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice. Under consideration in Theory and Practice of Logic Programming (TPLP)

Download Full-text