, If min = max, because the linear programming solver is correct, then min is the only possible value for X within the constraint C. Hence X = min ? C is satisfiable

, Otherwise, because of the convexity of C, the half sum (min + max)/2 is a possible value for X within the constraint C. Hence X = (min + max)/2 ? C is satisfiable

, Then because of the convexity of C, min + 1 is a possible value for X within the constraint C (while we don't know for min). So X = min + 1 ? C is satisfiable, X is bounded by min but not bounded from above

, X is bounded by max but not bounded from below. Then by convexity max ? 1 is a possible value for X. The constraint X = max ? 1 ? C is satisfiable

. Otherwise, C is satisfiable and X is not bounded within C, 0 is a possible value for X, and the constraint X = 0 ? C is satisfiable

, So in all cases, the equation returned by the algorithm is indeed a solution for X of the input constraint C

, Grounding In Figure 5, we present an algorithm that grounds some variables while ensuring that the subspace it defines intersects with all positive atoms. First we need the projection of a constraint onto a variable

A. R. Bradley, Z. Manna, and H. B. Sipma, What's decidable about arrays, Proc. of VMCAI'06, vol.3855, pp.427-442, 2006.
DOI : 10.1007/11609773_28
URL : http://theory.stanford.edu/~sipma/papers/avmcai06.pdf

D. Chan, Constructive negation based on the completed database, ICLP/SLP, pp.111-125, 1988.

W. Craig, Three uses of the herbrand-gentzen theorem in relating model theory and proof theory, J. Symb. Log, vol.22, issue.3, pp.269-285, 1957.

A. Dovier, E. Pontelli, and G. Rossi, A necessary condition for constructive negation in constraint logic programming, Inf. Process. Lett, vol.74, issue.3-4, pp.147-156, 2000.

J. P. Gallagher and M. Bruynooghe, The derivation of an algorithm for program specialisation, New Generation Comput, vol.9, issue.3/4, pp.305-334, 1991.

G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey, Failure tabled constraint logic programming by interpolation, TPLP, vol.13, issue.4-5, pp.593-607, 2013.

C. Holzbaur, OFAI clp(q,r) manual, edition 1.3.3, 1995.

J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages and Computation, 1979.

J. Jaffar and J. Lassez, Constraint Logic Programming, Proc. of 14th Annual ACM Symp. on Principles of Programming Languages, pp.111-119, 1987.

J. Jaffar and M. J. Maher, Constraint logic programming: A survey, Journal of Logic Programming, vol.19, pp.503-581, 1994.
DOI : 10.1016/0743-1066(94)90033-7
URL : https://doi.org/10.1016/0743-1066(94)90033-7

J. Jaffar, M. J. Maher, K. Marriott, and P. J. Stuckey, The semantics of constraint logic programs, Journal of Logic Programming, vol.37, issue.1-3, pp.1-46, 1998.

J. Jaffar, V. Murali, and J. A. Navas, Boosting concolic testing via interpolation, ESEC/SIGSOFT FSE, pp.48-58, 2013.

J. Jaffar, A. E. Santosa, and R. Voicu, An interpolation method for CLP traversal, CP, vol.5732, pp.454-469, 2009.

J. W. Lloyd, Foundations of Logic Programming, 1987.

K. Marriott and P. J. Stuckey, Programming with Constraints: An Introduction, 1998.

F. Mesnard, ´. E. Payet, and G. Vidal, Concolic testing in logic programming, TPLP, vol.15, issue.4-5, pp.711-725, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01451690

F. Mesnard, ´. E. Payet, and G. Vidal, On the completeness of selective unification in concolic testing of logic programs, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01451698

P. Refalo and P. Van-hentenryck, CLP(R lin ) revised, Proc. of the Joint International Conf. and Symposium on Logic Programming, pp.22-36, 1996.

T. Ströder, F. Emmes, P. Schneider-kamp, J. Giesl, and C. Fuhs, A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog, LOPSTR'11, vol.7225, pp.237-252, 2011.

P. J. Stuckey, Negation and constraint logic programming, Inf. Comput, vol.118, issue.1, pp.12-33, 1995.