SMT Encodings

Currently the SMT encoding of NV consists of two different modules, a translation to constraints of the functional language, and a translation to constraints of the stable routes problem. For each of these two, there are two alternative encodings currently, explained below.

SmtExpr Encodings

SmtExpr Boxed Encoding

Prerequisites: Renaming, Inlining, Record unrolling, Map unrolling

The boxed encoding is essentially a straightforward translation from NV to SMT-LIB expressions. It uses the datatype theory, so option types and tuples are translated to custom SMT datatypes for options and pairs.

• Easy to implement.
• Readable SMT query.
• Slow performance. The datatype theory in Z3 seems much slower than Integers+Booleans.

SmtExpr Unboxed Encoding

Prerequisites: Renaming, Inlining, Record unrolling, Map unrolling,Option Unboxing, Tuple Flattening

The key idea here is to eliminate all instances of complex types such as tuples and options, and to reduce the SMT encoding to just Integers and Booleans. To achieve that, we use the option unboxing (roughly for a value of type option[T], None is translated to (false, default_value T) and Some x is translated to (true, x)) and tuple flattening transformations (roughly does two things: 1. all variables of tuple type are converted to a normal form, i.e. x : int * int ~> (fst x, snd x) and 2. it flattens tuples ((1,2),3) ~> (1,2,3)). With these transformations, the compiler to SMT essentially has to deal either with single values or with lists of values where we just have to lift the translation code and not the resulting SMT code.

• Fast queries
• Relying on less SMT theories
• More stress on normalization due to lot of auxiliary variables and blow-up in the size of expressions
• More complicated implementation.

Smt Encodings

Smt Classic Encoding

This is based on the encoding of Minesweeper. Intuitively, we create the following SMT variables:

• For each node u, a variable label(u) that denotes the solution of that node.
• For each link (u,v), a variable trans_in(u,v) that denotes the input message to be transformed and a variable trans_res(u,v) that denotes the result of that transformation.
• For each node u, a variable x(v,u) for each neighbor v that sends a routing message, and a variable merge_res(v,u) for each merge operation.
• For each node u, a variable init(u) denoting the initial attribute.

And then add the constraints to capture the SRP semantics:

• trans_in(u,v) = label(u), i.e. the input message over edge u,v is the solution of u.
• trans_res(u,v) = [| (trans (u,v)).body|], i.e. the result variables for the transfer function are constrained by the expression of the transfer function.
• x(v,u) = trans_res(u,v), i.e. the incoming messages to node v are the results of the transfer function that was applied over the link (u,v).
• merge_res(u,x,y) = [| (merge u).body.body |] (takes two arguments, so we apply body twice)
• label(u)= fold (fun acc v -> merge_res(u,x(v,u),acc)) (incoming_messages(u)) init(u)

where [| trans(u,v) |] roughly means partially evaluate and then translate to SMT constraints with one of the two methods explained above.

Finally, we translate the assertion function for each node to SMT constraints, and for each assertion we associate an input variable assert_in(u) with the input (the solution of node u) and an SMT variable assert_result(u) with the result of the assertion function on this node. We require that:

• [|assert_in(u)|] = label(u)
• [|assert_result(u)|] = false, i.e. the solver tries to find an assignment to the network variables that violate the assertion. If it fails, then our network is safe (or does not converge).

Smt Functional Encoding

The idea here is to leverage the flexibility of NV and the ability to do partial evaluation and other transformations to simplify the problem as much as possible before feeding it to the SMT solver. In particular, instead of building the SRP semantics as above (by using SMT variables), we would like to build NV expressions that captures the SRP semantics, simplify them and then feed them the solver. In particular, we create a symbolic NV variable for each node's solution (call it label(u)) and an NV expression for each node:

exp(u) merge u (trans (v1,u) label(v1)) (merge u (trans (v2,u) label(v2)... init(u)))

We then add a constraint that: [|label(u)|] = |exp(u)|] i.e. after partial evaluation the smt variable that corresponds to label(u) should be equal to that expression. Notice, that in this encoding there is much more room for normalization to reduce the size of the expression.

As of right now, this encoding doesn't work with the unboxed SmtExpr encoding: Consider the unboxed version of merge, it's going to be a function of the form merge u x1 x2... y1 y2.. To apply this function to the incoming messages (i.e. the transfer function), these must be in tuple normal-form. That is, they should be an expression of the form (e1,e2,...). Otherwise, if it was an expression such as match ... with ... we would not be able to bring to a tuple normal form and do the application. Hence we need an extra transformation to do this.

Performance (updated)

After fixing a couple bugs in the normalization process, functional encoding works again. We cannot yet do the unboxed encoding though and hence SMT performance suffers from this.

TODO: Add some benchmarks.

TODOs

Going forward these are obvious avenues to explore:

• Reduce the size of the expression to be encoded. NV expressions blow up a lot due to the way record projections and map operations work (through match statements which use long lists of variables/patterns). There are at least two ways to improve upon this:
  • The unboxed encoding with a bit more work from the normalizer can do this. For instance a record projection x.f is translated to a tuple projection match x with | (..,f,..) -> ... An unboxed version would look like: match (x0,x1,...) -> | (..,f,..) -> .. and hence with some extra effort from the normalizer we can reduce this trivial match away. These are still not for free.
  • [Recommended] Introduce (tuple) projection functions as primitives. Then the boxed version can translate them directly to their SMT equivalent (theory of datatypes has projection functions for the tuples) and the unboxed version can trivially erase them. That would be neat to have.
• Fix the unboxed version, because it enables more reductions as seen above and because the SMT solver seems to be faster when constrained to Bool+Int theory. I implemented the tuple normal-form transformation (all expressions of type TTuple are ETuple) but the size of even the smallest networks is huge and it does not scale. Hence the initial plan to do this won't work, however we can try something else: Create the SRP expressions with a boxed encoding, do some partial normalization, unbox them and then do so more partial normalization. This might be a bit complicated, but it does not require the tuple normal-form translation so the size will be kept down.