Search

In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints (ℒ|⋅|) to a decision procedure for ℒ|⋅| extended with set terms denoting finite integer intervals (ℒ[]). In ℒ[] interval limits can be integer linear terms including unbounded variables. These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for ℒ[] it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the {log} ('setlog') tool. The paper includes a case study based on the elevator algorithm showing that {log} can automatically discharge all its invariance lemmas, some of which involve intervals. [ABSTRACT FROM AUTHOR]

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) [ABSTRACT FROM AUTHOR]

This paper introduces an instantiation of the constraint logic programming scheme called CLP(PolyFD) in which variables take values from finite subsets of the integers and constraints are expressed as equalities, inequalities, and disequalities of polynomials with integer coefficients. Such constraints, which we call polynomial constraints over finite domains, can be treated effectively by means of a specific solver under the assumption that initial approximations of the domains of variables are available. The proposed solver deals with constraints in a canonical form and it uses the modified Bernstein form of polynomials to detect the satisfiability of constraints. The solver is complete and a preliminary assessment of its performance is reported. [ABSTRACT FROM AUTHOR]