Termination properties of actual Prolog systems with constraints are fragile and difficult to analyse. The lack of the occurs-check, moded and overloaded arithmetical evaluation via is 2 and the occasional nontermination of finite domain constraints are all sources for invalidating termination results obtained by current termination analysers that rely on idealized assumptions. In this paper, we present solutions to address these problems on the level of the underlying Prolog system. Improved unification modes meet the requirements of norm based analysers by offering dynamic occurs-check detection. A generalized finite domain solver overcomes the shortcomings of conventional arithmetic without significant runtime overhead. The solver offers unbounded domains, yet propagation always terminates. Our work improves Prolog's termination and makes Prolog a more reliable target for termination and type analysis. It is part of SWI-Prolog since version 5.6.50.
SICStus Prolog @cite_13 was the first system to generalize finite domain constraints without sacrificing correctness. It uses small integers for domains but signals domain overflows as representation errors and not as silent failures.
@cite_13
2012741612
We describe the design and implementation of a finite domain constraint solver embedded in a Prolog system using an extended unification mechanism via attributed variables as a generic constraint interface. The solver is essentially a scheduler for indexicals, i.e. reactive functional rules encoding local consistency methods performing incremental constraint solving or entailment checking, and global constraints, i.e. general propagators which may use specialized algorithms to achieve a higher degree of consistency or better time and space complexity.