Ians notes.

0. test examples should be unsat.

Presburger (Cooper)


1.  In get_implicant we need to ensure we have the reduced set of atomic formula
(in particular <= should be eliminated, as well as distinct (c.f. projector_add_literal).)
Also know that we only have Int variables in the fray.

The conjuncts we process from project_literals are of the form:


strict inequality (poly > 0)
non-strict inequality  (poly >= 0)
equality   (poly = 0)
divides    + (k | poly)
divides    - (k | poly)



2. Then given the conjuncts

J0, ..., JN

and uvars

y0, ..., yM0

passed in to project_literals

we need to compute, for a uvar y:

- k = lcm(C) where C  = { c |  c*y occurs in a Ji }

- normalize the coefficients of y to be 1 and add the k-divisibility to the normalized set:

(*) J0_y, ...., JN_y,  k|y

then compute:

- the A[y] set      { e |  either (y < e)  or (y = e - 1)  or (y != e) is a Ji_y }

- the B[y] set      { e |  either (e < y)  or (y = e + 1)  or (y != e) is a Ji_y }

- delta             lcm({ d |  (d|x + e) or (d!|x + e)  is a Ji_y })

Using these we can deterime whether we use the

(-*) The P_{-\infinity} Cooper equivalence

or

(+*) The P_{+\infinity} Cooper equivalence

If |A[y]| < |B[y]| we use the (+*).

If |B[y]| < |A[y]| we use the (-*).

If |B[y]| = |A[y]| we take as smaller the one with the fewer free variables,

if that doesn't decide we pick the first.

Having chosen between (-*) and (+*) we then have to find which disjunct
is true in the model. Note that each disjunct is closely related in form
to the conjunction of (*).

To determine the valid disjunct will require testing validity in the model of:

- 1 <= j <= delta instantiations: P_{-\infinity}[y/j] or P_{+\infinity}[y/j] according to the choice of
(-*) or (+*).

- 1 <= j <= delta, b in |A[y]|  (|B[y]| respectively) instantiations: P[b + (-)j]


This gives rise to a new set of conjuncts and uvars

J0, ..., JN

y0, ..., yM

where M1 < M0  for the process to continue.


4.  The Presburger elimination procedure is based upon the following
fact that can be gleaned from the proof of correctness of Cooper's
algorithm.  In the sequel we have a model A (and an implicit variable
assignment), a variable y, and a set of literals (which are all true
in A) of the following form:

a.  y < U_i                i in I_a

b.  y > L_i                i in I_b

c.  y = S_i                i in I_c

d.  f_i | y + r_i          i in I_d

e.  not( n_i | y + p_i )   i in I_e

Since we are attempting to eliminate y, we assume that I_c is
empty, otherwise we don't have much work to do.

We let:

U  = Min { U_i | i in I_a under the ordering induced by A }

L  = Max { L_i | i in I_b under the ordering induced by A }

delta = lcm { f_i | i in I_d } U { n_i | i in I_e }

Delta = { (f_i | y + r_i)  |  i in I_d } U { not( n_i | y + p_i ) |  i in I_e }

Then:

(*) Delta[y]   iff  Delta[y + c*delta]

So we have three cases:

- I_a and I_b are both empty.

- I_a is empty but I_b is not.

- I_a is not empty.

Choose B as follows: in the first case take B to be 0, in the second case B to be L
and in the third case take B to be U.

In each case we can find a  k  in { 1, ...., delta } such that

Delta[B + k]  in the first two cases, and

Delta[B - k] in the third.

Thus we eliminate y by B + k or B - k according to the nature of the original
set of constraints.