search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Minor readability optimisation improvements #138

Closed MattWindsor91 closed 7 years ago

MattWindsor91 commented 7 years ago

This is part of the #136 effort, and adds a few new heuristics to the integer optimisation logic such as

x + 5 + y + 12 -> x + y + 17
x + (y - 5) -> (x + y) - 5
x + 5 <= 6 -> x <= 1
x - 6 > 0 -> x > 6

and so on.

This doesn't do much for us in practice, as most of the problem for #136 is in complex nested Booleans, though it's managed to simplify

    exists ArcFoot:Set<ArcNode> :: (
        acc(ArcFoot) &*&
        (
            ((before_28_1_x in ArcFoot && 1 <= before_28_1_x.count) &&
                ((goal_36_n <= 2) ||
                    (goal_35_x != before_28_1_x) ||
                    (goal_35_x != before_28_1_x) ||
                    ((((goal_36_n - 2) + 1) <= 0) ||
                        (goal_35_x in ArcFoot && ((goal_36_n - 2) + 1) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    (goal_36_n <= 2) ||
                    (goal_35_x != before_28_1_x) ||
                    (goal_35_x != before_28_1_x) ||
                    ((((goal_36_n + (goal_36_n - 2)) + 1) <= 0) ||
                        (goal_35_x in ArcFoot && ((goal_36_n + (goal_36_n - 2)) + 1) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    (goal_36_n <= 2) ||
                    (goal_35_x != before_28_1_x) ||
                    (((goal_36_n + (goal_36_n - 2)) <= 0) ||
                        (goal_35_x in ArcFoot && (goal_36_n + (goal_36_n - 2)) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    (goal_35_x != before_28_1_x) ||
                    (((goal_36_n + 1) <= 0) ||
                        (goal_35_x in ArcFoot && (goal_36_n + 1) <= goal_35_x.count))) &&
                ((goal_35_x != before_28_1_x) ||
                    (goal_36_n <= 2) ||
                    (((goal_36_n - 2) <= 0) ||
                        (goal_35_x in ArcFoot && (goal_36_n - 2) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    ((goal_36_n <= 0) ||
                        (goal_35_x in ArcFoot && goal_36_n <= goal_35_x.count))))
        )
    )

to

    exists ArcFoot:Set<ArcNode> :: (
        acc(ArcFoot) &*&
        (
            ((before_28_1_x in ArcFoot && 1 <= before_28_1_x.count) &&
                ((goal_36_n <= 2) ||
                    (goal_35_x != before_28_1_x) ||
                    (goal_35_x != before_28_1_x) ||
                    ((goal_36_n <= 1) ||
                        (goal_35_x in ArcFoot && (goal_36_n - 1) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    (goal_36_n <= 2) ||
                    (goal_35_x != before_28_1_x) ||
                    (goal_35_x != before_28_1_x) ||
                    (((goal_36_n + goal_36_n) <= 1) ||
                        (goal_35_x in ArcFoot && ((goal_36_n + goal_36_n) - 1) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    (goal_36_n <= 2) ||
                    (goal_35_x != before_28_1_x) ||
                    (((goal_36_n + goal_36_n) <= 2) ||
                        (goal_35_x in ArcFoot && ((goal_36_n + goal_36_n) - 2) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    (goal_35_x != before_28_1_x) ||
                    ((goal_36_n <= -1) ||
                        (goal_35_x in ArcFoot && (goal_36_n + 1) <= goal_35_x.count))) &&
                ((goal_35_x != before_28_1_x) ||
                    (goal_36_n <= 2) ||
                    ((goal_36_n <= 2) ||
                        (goal_35_x in ArcFoot && (goal_36_n - 2) <= goal_35_x.count))) &&
                ((goal_35_x == before_28_1_x) ||
                    ((goal_36_n <= 0) ||
                        (goal_35_x in ArcFoot && goal_36_n <= goal_35_x.count))))
        )
    )
MattWindsor91 commented 7 years ago

Note that the biggest problem we have in the above query is statements of the form

X==Y || X!=Y

which could be blown away with some effort, but making that work in practice might be akin to writing a full blown symbolic evaluator.

septract commented 7 years ago

This looks fine to me.