Search code examples
z3smt

Z3: How to best encode a "switch statement"?

I want to create an expression that selects one of a given set of expressions. Given an array of expressions

Expr[] availableExprs = ...;

with statically known length, I want Z3 to select any one of these (like a switch statement). In case the problem is SAT I need a way to find out which of these was selected in the model (its index in the array).

What is the fastest way to encode this?

I considered these approaches so far:

  1. Have an integer restricted to [0, arrayLength) and use ITE to select one of those expressions. The model allows me to extract this integer. Unfortunately, this introduces the integer theory to the model (which previously did not use integers at all).
  2. Have one boolean for each possible choice. Use ITE to select an expression. Assert that exactly one of those booleans is true. This strategy does not need any special theory (I think) but the encoding might be too verbose.
  3. Store the expressions into an array expression and read from that array using an integer. This saves the ITE chain but introduces the array theory.

Clearly, all of these work, but they all seem to have drawbacks. What is the best strategy?

Solution

  • If all you want is to encode is that an element v is in a finite set {e1, ..., en} (with sort U), you can do this using smtlib2 as follows:

    (declare-fun v () U)
(declare-fun p1 () Bool)
...
(assert (= p1 (= v e1)))
(assert (= p2 (= v e2)))
...
(assert (= pn (= v en)))

(assert (or p1 ... pn))

    The variable v will be equal to one of the elements in "the array" of {e1 ... en}. And pi must be true if the selection variable v is equal to ei. This is basically a restatement of Nikolaj's suggestion, but recast for arbitrary sorts.

    Note that multiple pi may be set to true as there is no guarantee ei != ej. If you need to ensure no two elements are both selected, you will need to figure out what semantics you want. If the {e1... en} are already entailed to be distinct, you don't need to add anything. If the "array" elements must be distinct but are not yet entailed to be distinct, you can assert

    (assert (distinct e1 ... en))

    (This will probably be internally expanded to something quadratic in n.) You can instead say that no 2 p variables can be true as once. Note that this is a weaker statement. To see this, suppose v = e1 = 1 and e2 = e3 = 0. Then p1 = true and p2 = p3 = false. The obvious encoding for these constraints is quadratic:

    (assert (or (not pi) (not pj))) ; for all i < j

    If you need a better encoding for this, try taking a look at how to encode "p1+ ... + pn <= 1" in Translating Pseudo-Boolean Constraints into SAT section 5.3. I would only try this if the obvious encoding fails though.