# Tag Info

In your case, the simplest solution may be to use SAT. Your first clause includes $x \le 0.25$ and $x > 0.91$. This means that there are five regions of interest for the variable $x$, which we identify with boolean variables: $X_1 \equiv x \in(-\infty, 0.25)$, $X_2 \equiv x = 0.25$, $X_3 \equiv x \in (0.25, 0.91)$, $X_4 \equiv x = 0.91$, $X_5 \equiv x \in ... 3 Some SAT solvers and SMT solvers offer an interface that lets you push clauses, and then later pop/retract them and push some new ones. You could explore to see whether this offers a speedup in your situation. There are no guarantees, and the only way to tell is to try it. 2 Yes, you could solve this with a SMT solver that supports linear real arithmetic. However SMT supports more general inequalities where you can have linear sums of variables (e.g.,$2a+3x \le 5.7$) instead of simple comparisons between a single variable and a constant (e.g.,$a \le 1.6$), so it might be more powerful than you need, so if you don't have any ... 2 First, you need to figure out the semantics of your language: does divide-by-zero cause the program to abort/halt/throw an exception, or does execution proceed and the divide-by-zero returns a NaN? If it causes the program to halt, then you should not try to represent$\bot$values. Instead, treat division as a conditional statement, that first tests ... 1 Your answers to (a) and (c) are correct. To tell whether (b) is correct we need a precise notion of expressiveness. The issue is that propositional logic and first-order logic have totally different semantics: their notions of "model" are valuation and structure respectively. When two logics use the same notion of "model" we can ... 1 If the constraints you have are of the form$a < b$and$a=b$(i.e., only unconditional inequality constraints), you can model them with a directed graph: each node represents a variable, and an edge$v \to w$corresponds to the inequality$v < w$. Then you can answer queries by doing a straightforward reachability check. (If you see the equality$v=...