Blog

Here are the two code snippets that I presented in class that come from the *Decision Procedures* text:

```
if(!a && !b) h();
else
if(!a) g();
else f();
```

```
if(a) f();
else
if(b) g();
else h();
```

They represent what an optimizer might do when compiling code. We would like to show that these snippets are the same for every input. Specifically, we would like to check the *validity* of the optimization. I gave you the first step in translating the code into a form appropriate for checking using Z3:

```
if ~a /\ ~b then h
else
if ~a then g
else f
```

```
if a then f
else
if b then g
else h
```

Here we replaced C-like constructions `&&`

and `!`

with logical equivalents and replaced funnction calls with uninterpreted functions. We can also replace the `if`

statements using the following equivalence:

```
(if x then y else z) == (x /\ y) \/ (~x /\ z)
```

You are to do this last transformation to generate a logical expression and check that logical expression for validity in Z3. This will tell is if the optimization is correct.