LSign reordered

Abstract

LSign [16] is an elegant domain for analyzing constraint logic programming languages over linear real constraints. Its key conceptual ideas are the abstraction of linear constraints by replacing coefficients by their signs and the use of annotations for preserving multiplicity information on the constraints. Unfortunately, the ordering of abstract constraint stores given in [16] does not capture the intended meaning and makes it impossible to prove the consistency of the abstract operations of LSign. In this paper, we reconsider the domain LSign. Our first contribution is to define a new ordering on abstract constraint stores and to give the meaning of the domain through a monotone concretization function from abstract stores to sets of constraint stores, where a constraint store is a multiset of constraints. Our second contribution is to show that ordering two abstract stores reduces to a matching problem, which can be solved in polynomial time. Our last contribution is to propose a simpler and more precise algorithm for abstract projection and a schema for generating upper bound operations and to prove their consistency.