5

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around. SAT and SMT solvers ...


3

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=...


Only top voted, non community-wiki answers of a minimum length are eligible