Linear programming problems are usually solved using the simplex algorithm. While it is easy to encode a constraint system of linear equalities and inequalities as a Parameterized Unit Test for Pex, there is currently no way to tell Pex that we want test inputs that are “minimal” according to a custom objective function. However, Pex can still generate *surprising* feasible solutions.

Let's start with a simple set of linear inequalities that define our problem.

[PexMethod]
public int Test(int x, int y)
{
    // PexAssume is used to add 'constraints' on the input
    // in this case, we simply encode the inequalities in a boolean formula
    PexAssume.IsTrue(
        x + y < 10 & // using bitwise & to avoid introducing branches
        5 * x + 2 * y > 20 &
        -x + 2 * y > 0 &
        x > 0 & y > 0);
    // the profit is returned so that it is automatically logged by Pex
    return x + 4 * y;
}

After running Pex, we get one feasible solution. It is not optimal as expected since we don't apply the simplex algorithm.

Enter overflows

Remember that .Net arithmetic operations will silently overflow unless you execute them in a checked context? Let's push our luck and try to force an overflow by changing x > 0 constraint to x > 1000:

[PexMethod]
public int Test(int x, int y)
{
    PexAssume.IsTrue(
        x + y < 10 &
        5 * x + 2 * y > 20 &
        -x + 2 * y > 0 &
        x > 1000 & y > 0
    );
    return x + 4 * y;
}

Z3, the constraint solver that Pex uses to compute new test inputs, uses bitvector arithmetic to find a surprising solution that fulfills all the inequalities (our profit has just gone of the roof :)).

Z3 is truly an astonishing tool!

Checked context

In order to avoid overflow, one should use a checked context. Let's update the parameterized unit test:

[PexMethod]
public int Test(int x, int y)
{
    checked
    {
        PexAssume.IsTrue(
            x + y < 10 &
            5 * x + 2 * y > 20 &
            -x + 2 * y > 0 &
            x > 0 & y > 0
        );
    }
    return x + 4 * y;
}

In fact, in that case, Pex generates 2 test cases. One test that passes and the other test that triggers an OverflowException (implicit branch).

Stay tuned for more surprising discoveries using Pex.