Description

The algorithm used in the Arith tactic cannot solve general sets of linear inequalities over the integers, though such problems are abundant (for example when doing array bounds checking). Solving linear inequalities over the integers is a strictly harder problem than over the rationals: polynomial time algorithms are known for the solving linear inequalities over the rationals, but integer linear programming is NP complete  .

The SupInf tactic is uses the Sup-Inf method of Bledsoe  [1] for solving integer inequalities. While method is only complete for the rationals, not the integers, it does work well in practice for the integers. Todd Wilson [6] has written a reference version of SupInf.

The basic algorithm considers a conjunction of inequalities where the are linear expressions over the rationals in variables and determines whether or not there exists an assignment of values to the that satisfies the conjunction. The algorithm works by determining upper and lower bounds for each of the variables in turn --- hence the name `sup-inf'. The bound calculations are always conservative, so that if some upper bound is strictly below some lower bound, then the conjunction is unsatisfiable.

Shostak  [5] showed that the calculated bounds are the best possible, and hence that the algorithm is complete for the rationals. He proposed a simple modification that made the algorithm return an explicit satisfying assignment when the conjunction is satisfiable.

When used over the integers, the Sup-Inf algorithm is sound, but not complete; if there is no satisfying assignment over the rationals, then there is also none over the integers. However, there are cases when the algorithm finds a rational-valued satisfying assignment even though none exists that is integer valued. There are standard techniques for restoring completeness, but it has been both Shostak's and our experiences to date that examples for which the algorithm is incomplete are rare in practice.

The procedure implemented currently does the following:

1. Takes a goal g and extracts a logical expression P built from the logical connectives , the order relations on the integers and <, and the equality relation = on the integers, such that if is not satisfiable, then the goal g is true. If the goal has the form

   

   where the are all instances of the relations over the integers involving expressions over the integer variables , then has form

   

2. The expression is put into disjunctive normal form. Occurrences of = and < relations are eliminated in favour of . Where possible, ='s are eliminated by substitution rather than splitting into inequalities.

3. The left-hand argument of each is moved to right-hand side and the integer expressions are put into a sum of products normal form. Each product has any constant coefficient brought out to the left of the product.

4. Each distinct non-linear expression is generalized to a new rational variable. These non-linear expressions might involve and , as well as integer-valued functions (for example, the list length function). The arithmetic expressions are now all linear.

5. Each disjunct is augmented with extra arithmetic information suitably normalized that comes from various sources including:
   1. typing of variables and generalized non-linear expressions. If variable i has type , then can be added.
   2. arithmetic property lemmas. An example is a lemma stating that the length of two lists appended is the sum of the lengths of each list.
   This augmentation is in general a recursive procedure; the inferred arithmetic propositions can themselves contain variables and non-linear expressions about which further information can be inferred.

6. The Sup-Inf algorithm is run on each disjunct. If none is satisfiable, then the original goal is true. If a satisfying assignment is found, then it is returned to the user as a counter-example.

7. When no disjunct is satisfiable, the procedure creates several well-formedness subgoals. Some of these check the well-formedness of the arithmetic expressions in the conclusion of the original goal g. Others check that the arithmetic property lemmas can be instantiated as the procedure assumed they could be.

The inference of arithmetic properties from typing and from property lemmas greatly increases the procedure's usefulness.

Unlike most other tactics, but like the arith rule which

SupInf largely supercedes, SupInf's inferences are not refined down to primitive rule level, so Nuprl's soundness now depends on the soundness of a core part of SupInf's implementation.