Hacker News Reader

It is common to express denotational semantics as SAT/SMT expressions.

For example, consider a function f(x) = x << 1.

A valid sat semantics for this function is: y == f(x) implies y == 2 * x.

But what variable assignment is being SATisfied?

if f(x) == g(x) is satisfiable, you get one value of x for which f(x) == g(x)

if f(x) != g(x) is satisfiable, you get one value of x for which f(x) != g(x)

Both of these are useful in practice.

This does not answer the question. I think people here know how equations work. But what's the "x" in the article?

Think of cpu instructions as functions.

x is the set of inputs to an instruction.

I see. The goal is to find some x s.t f(x)!=g(x).