3 ms·

What is the engine satisfying?

• fooker 3y ago
  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.
  • bjourne 3y ago
    But what variable assignment is being SATisfied?
    • fooker 3y ago
      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.
      • programmer_dude 3y ago
        This does not answer the question. I think people here know how equations work. But what's the "x" in the article?
        • fooker 3y ago
          Think of cpu instructions as functions. x is the set of inputs to an instruction.
      • bjourne 3y ago
        I see. The goal is to find some x s.t f(x)!=g(x).