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]