I am working on an implementation of Bruno Dutertre's and Leonardo de Moura's paper "A Fast Linear-Arithmetic Solver for DPLL(T)" for SymPy, an open source python library for symbolic computations.
What my code does is check if some set of inequalities (e.g. $x \ge 0$, $x \le -1$) is satisfiable. My question regards a particular trick the paper uses to handle strict inequalities and how to continue using it if I allow inequalities that contain infinity such as $x \ge \infty$.
The trick is used to convert a set of strict and non-strict inequalities over rational numbers into an equisatisfiable set of non-strict inequalities over rational number plus some amount of infinitesimal deltas. For example, $x > 0$ would become $x \ge 0 + 1*\delta$ and $x \ge 0$ would become $ x \ge 0 + 0*\delta$.
A pair $(c, k)$ of $\mathbb Q_\delta$ is denoted by $c+k\delta$ and the following operations and comparison are defined in $\mathbb Q_\delta$:
Screen shot is from the paper. I believe $(c_1, k_1) + (c_1, k_2)$ should be $(c_1, k_1) + (c_2, k_2)$.
The problem is, that since my code allows positive and negative infinity, some bugs occur. Consider for example this problem that came up in testing my code:
$$ y \le r - x \land y \ge r \land x > 0$$
If r is finite, this is not satisfiable. However, if r is positive infinity, then the problem is satisfiable because we can ignore x as it gets eaten up by the infinity. In my code, when r was infinity, the code was wrongly coming to the conclusion that the problem was unsatisfiable.
To resolve this problem I was considering redefining addition when $c_1$ is infinity and $c_2$ is not: in this case $(c_1, k_1) + (c_2, k_2) = (c_1, k_1)$. Does this seem reasonable or will I be breaking addition or causing some other bug by doing this?