ArrayStoreException: Polynomial

[DavePearce]

The following generates an ArrayStoreException:

assert:
    forall (int item, int[] items):
        if:
            forall(int j):
                items[j] == 0
        then:
            forall(int j):
                items[j] == 0

The exact error is:

Caused by: java.lang.ArrayStoreException: wyal.lang.WyalFile$Expr$Polynomial
    at wytp.proof.util.AbstractProofRule.construct(AbstractProofRule.java:190)
    at wytp.proof.util.AbstractProofRule.construct(AbstractProofRule.java:179)
    at wytp.proof.rules.ExhaustiveQuantifierInstantiation.instantiateQuantifier(ExhaustiveQuantifierInstantiation.java:232)
    ...

Essentially, the problem happens during "construction" when we end up substituting a known term (e.g. x) for a polynomial (e.g. y+1). The problem is that you end up with a polynomial being assigned into an array of polynomial terms (and that don't fit).

Ideas

The above raises the obvious and important question: can we live without Expr.Polynomial ?

To answer this, we need to consider where the polynomial is used:

• Normal Forms (see #68). Of course, Polynomial provides a normal form representation of arithmetic expressions.
• Proof Rules. Operations on Polynomials (e.g. isConstant(), add(), subtract(), negate(), etc). are used within various proof rules.

Currently, the main rules that use Polynomial operations are: CongruenceClosure, InequalityIntroduction, ExhaustiveQuantifierInstantiation. They are also used within `Formulae.simplify().

[DavePearce]

Removing Polynomial

If we remove Polynomial, what do we need to do to replace it? We need the simplification rules to work on general Expr.Add and Expr.Mul nodes. Various rewrite rules such as:

(ADD x (ADD y z)) ===> (ADD x y z)

(ADD x) ===> x

(MUL 2 (ADD 1 x)) ===> (ADD (MUL 2 1) (MUL 2 x))

From a Proof.Rule we need to be able to simplify expressions (i.e. move them into normal form) after applying operations. For example, subtracting one side of an equation from another.