Using Real Relaxations During Program Specialization

We propose a program specialization technique for locally stratified CLP(Z) programs, that is, logic programs with linear constraints over the set Z of the integer numbers. For reasons of efficiency our technique makes use of a relaxation from integers to reals. We reformulate the familiar unfold/fold transformation rules for CLP programs so that: (i) the applicability conditions of the rules are based on the satisfiability or entailment of constraints over the set R of the real numbers, and (ii) every application of the rules transforms a given program into a new program with the same perfect model constructed over Z. Then, we introduce a strategy which applies the transformation rules for specializing CLP(Z) programs with respect to a given query. Finally, we show that our specialization strategy can be applied for verifying properties of infinite state reactive systems specified by constraints over Z.