Improvement on Octogonal Method

In Deepak's method[1], when there is some constraint present at the verification condition (VC) generating position, the algorithm takes that constraint into consideration eagerly. This may result in a problem that the constraint might not be hit, like an infinite loop for instance. However, this constraint still enlarges the feasible domain of the octagon, which makes the generated VC weaker than the optimal one.

In order to address this problem, I make such a consideration lazy, which means that first apply the quantifier elimination method without constraints, and then compare the result with the constraints. Let U be the generated VC without constraints, and  P be the set of constraints (it can be test conditions or conditionals), if we can achieve that
                              \[ U \rightarrow P. \]
Then we can know that P will not be hit, which implies that we can ignore these constraints and U is right the final VC we want.

The original method is in P. If we consider to apply the two possible branches, i.e. either involve the constraints or not, at each position, then the method will be exponential. With my improvement, it's still exponential in worst case. But if I'm able to reduce the process of add constraints P back into U if necessary in constant time, then we can achieve an algorithm which can generate stronger program invariants but still in polynomial time.


---------------------------------
References:

[1] Kapur, Deepak, et al. "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants." Automated Reasoning and Mathematics. Springer Berlin Heidelberg, 2013. 189-228.