Lesson 13: Program Synthesis

[sampsyo]

The tasks for the program synthesis lesson are extremely open-ended: just do something interesting on top of the basic synthesizer that we built in class!

[zzzDavid]

My implementation is here.

Tiny SuperOptimizer

Tiny SuperOptimizer is a program synthesis tool that generates a minimum Bril program from an input Python function.

Introduction

The idea of implementing a superoptimizer comes from this paper. Given an instruction set, the superoptimizer finds the shortest program to compute a function.

Demo

Tiny SuperOptimizer takes a Python function as input, for example:

def f(x, y):
    a = x * 2 + y
    b = a * 5
    c = b * (128 // 4)
    return c

The tiny superoptimizer takes in the function and arg names as input, synthesize the minimum program and convert to Bril's json form:

tree, holes = superoptimize(f, ['x', 'y'])
converter = to_bril(tree, holes)
print(converter.bril_prog)

The result looks like this:

$ python main.py | bril2txt

@main(x: int, y: int) {
  v20: int = const 160;
  v1: int = mul v20 y;
  v12: int = const 6;
  v0: int = shl x v12;
  v0: int = add v0 v1;
  print v0;
}

As the result, the output program is a simplified version of the input Python function. A print instruction is added to display the result.

Implementation

The idea of synthesizing a minimum program is traversing the search space of n instructions, with n ranging from 1 to a preset maximum number of instruction.

The optimizer enumerates all combinations of instruction choices and formulate a proof problem for each program.
For each enumerated program in the search space, it uses hole variables to encode the operands. The optimizer uses Z3 SMT solver to solve the proof problem, and keep traversing and increasing n until the solver outputs a valid solution.

There are four steps:

1. Build an AST for the Python function, and create a Z3 expression from the AST.
2. Start from n=1 and enumerate all possible programs in the search space, formulate a problem for each.
3. Increase n until Z3 outputs a valid solution or reaches the maximum of n.
4. Convert the output program to Bril's json format.

The two key parts of the process are generating operand choice encodings and enumerating all cases in the search space.

Encode operand choices

The operand of an instruction can be one of the following situations:

• one of the input variables
• a constant (a hole that we want to fill)
• the result of a previous operation.

We the instruction set to binary operations, thus The optimizer encode the operand as either one of the input variables or a constant. For example, with three inputs x0, x1, and x2, The optimizer encode the operand as:

(h2 ? (h1 ? x2 : (h0 ? x1 : x0)) : h3)

h0 and h1 select one of the input variables, and h2 select between input variables and a constant h3.

Generate the search space

With the operand encoded, The optimizer can enumerate all operation combinations given the number of instruction n.
Specifically, the implementation is here: sample(n, vars).

Discussion

We limit the "instruction set" to a small group of binary operations:

# set of operations used in superoptimization
# sorted by computation cost, from low to high
self.ops = ['<<', '>>', '+', '-', '*', '/']

And the optimizer chooses operations with cheaper computation cost over the expensive ones.

Even though the scope of problem is limited, the search space still grows exponentially when n increases. For the above example, the optimizer finds a solution in about 3 seconds, while more complex input function may take tens of minutes to yield a solution.

[5hubh4m]

I don't think bril has shift left and shift right instructions.

[zzzDavid]

You are right, that's why bril2txt works but brilli doesn't. We can imagine bril with a bit operation extension for this to work, which should be straightforward to implement. Otherwise it won't be much fun just generating the mul from *.

[sampsyo]

Wow; this is super cool!!!! I really like the idea of building a instruction-based synthesizer. This is far outside the scope of the original assignment, but I would love to know how this turns out for bigger programs… 3 seconds is pretty fast, so how big can we go? Even stealing some examples from existing superoptimizer papers would be terribly interesting. I'd be happy to provide more guidance if this is something you're interested in continuing to hack on in the future. 😃

With respect to bitwise operations, maybe Bril needs a new official extension to cover those…

[alaiasolkobreslin]

Code is here

Implementation

I followed James Bornholt's Rosette tutorial. I defined a simple AST containing if statements, some arithmetic operations, and some equality operations. The AST also contains square which squares a number and absolute which takes the absolute value. I also wrote an interpreter and defined an "expression hole" as any expression composed of the provided terminals:

(define (??expr terminals)
  (define a (apply choose* terminals))
  (define b (apply choose* terminals))
  (choose*  a
            b
            (neg a)
            (plus a b)
            (minus a b)
            (mul a b)
            (div a b)
            (square a)
            (absolute a)
            (eq a b)
            (lt a b)
            (gt a b)))

We can then define a sketch and assert that the interpreted sketch is always equal to the interpreted concrete expression. Then calling evaluate on the sketch yields an equivalent expression. For example, if I wanted to get an equivalent if expression for an absolute value expression, I could write:

(define-symbolic x integer?)
(define-symbolic i j integer?)  ; get access to constants
(define sketch1
  (iffy (??expr (list x i j)) x (??expr (list x i j))))

(define M
  (synthesize
    #:forall (list x)
    #:guarantee (assert (= (interpret sketch1) (interpret (absolute x))))))

(evaluate sketch1 M)

which results in the expression (iffy (lt -1 x) x (neg x)). Note that when I replace one of the lines above with:

(define sketch1
  (iffy (??expr (list x i j)) (??expr (list x i j)) (??expr (list x i j))))

I get (iffy (eq 1 x) (square x) (absolute x)), which is technically correct, but not the expression I was looking for.

Evaluation

Rosette was able to synthesize some simple expressions. Another example that worked was trying to synthesize a multiplication expression equivalent to a square expression:

(define-symbolic y integer?)
(define-symbolic a b integer?)
(define sketch2
  (mul (??expr (list y a b)) (??expr (list y a b))))

(define N
  (synthesize
    #:forall (list y)
    #:guarantee (assert (= (interpret sketch2) (interpret (square y))))))

(evaluate sketch2 N)

which resulted in the expression (mul y y).

There were many sketches that Rosette got tripped up on. At first I included an arithmetic shift operation in the AST and tried synthesizing a multiplication expression equivalent to a left shift of 2, but Rosette said the sketch was unsatisfiable. I even tried something as simple as (mul 2 (mul 2 e)) and tried to get an equivalent multiplication expression (expecting (mul 4 e)), but Rosette also said this was unsatisfiable.

Discussion

Using Rosette was surprisingly challenging to use. When a sketch is unsatisfiable, Rosette responds with the same error message every time:

application: not a procedure;
 expected a procedure that can be applied to arguments
  given: (unsat)

which doesn't really help me find the issue. So I still have no idea why it was struggling with shift operations and simple multiplication.

[sampsyo]

Super cool that you got Rosette up and running and doing what you want! I'm a little surprised by those simple examples that were reportedly unsatisfiable… I am sure there is a deeper story there (i.e., a "bug" to be fixed) if it's doing that rather than just timing out. But I'm at a loss as to exactly what!

Anyway, even if there is a much deeper well to debugging Rosette here, I'm glad you were able to get started with it. If you're curious, I'd be happy to try to dive in and help figure out where the roadblock is for these examples.

[JonathanDLTran]

Summary

Code

I used the sketch builder from https://github.com/sampsyo/minisynth/blob/master/ex2.py, and built off this sketching program.

To add extra features, I considered adding comparison operators like less than, less than equal, greater than, greater than equal, equals and not equals. I then implemented these in ex2.py.

I also added test sketches to see whether a solution could be synthesized for the holes. These included examples using the less than and greater than equals operator to check whether the sketch worked properly.

To do something different, I also added in simple structures that resemble for loops. These are the forplus, forminus, and fortimes loops. The gist is that forplus x += n1 inrange n2 will add n1 to x for n2 number of times. This is defined similarly for the expressions forminus and fortimes.

I unfortunately was not able to get fortimes to work the way I wanted to, perhaps because I had to convert bitvectors to ints and then back to bitvectors. Besides this though, forminus and forplus seem to work approrpriately and can be used to synthesize simple iteration.

In terms of test cases, for these small, contrived examples, the solver can find a solution relatively quickly. Most of the test cases are not very large, and the time to solve the sketch is minuscule. Even for the test case named large.txt, the time to solve the sketch is relatively quick, though this may be because the expression with holes is still syntactically similar to the expression without holes.

As a whole, this lesson was fairly straightforward given the code in ex2.py was already complete when I started with it. Adding on more elements was fairly simple, modulo some problems figuring out types in z3, which were quickly fixed by looking at the z3 documentation. Overall, I think synthesis seems remarkable, in that a program can be built without human intervention. I do have trouble seeing it being used in commonplace applications because it seems to scale poorly on larger sketch programs.

[sampsyo]

Neat; sounds pretty cool!! I can imagine that BV-to-int-to-BV conversions would really trip up the solver. I honestly don't even know to what degree these are supported—when converting too much between theories, often solvers like Z3 will just say "unknown" instead of SAT or UNSAT. Cool idea to hack in support for loops though!

[andrewb1999]

I added strings to the language in ex2. Here is my code.

Implementation

I added support for escaped strings in the lark parser and removed some of the math operations to simplify the implementation for now. This language supports string replace, strToInt, intToStr, and substring functions. Unfortunately these functions can't be implemented naturally to work in both the interpretation and z3 goal cases, so I had to specialize the interp function to build to right z3 objects. The python bindings support all of these functions directly so I didn't have to do any encoding myself. Holes can be either strings or integers depending on their location in a "function" call.

Testing

I wrote a few example sketches, here is a subset of them:

"abcd" + x
replace(h1, "e", x)

101
strToInt(intToStr(10) + h1)

"abcd"
substr("zxyabcddsls", h1, h2)

All of the sketches I wrote were able to be easily solved by z3, but there were a few times I made mistakes in how I wrote the sketch which caused z3 to never finish.

Discussion

I found Z3 pretty easy to use. Honestly, the more challenging part of this assignment was modifying the parser. Lark is fairly easy to use but I haven't used it before so I made some silly mistakes at first that didn't give errors that were easy to debug.

[sampsyo]

Wow, pretty rad! The theory of strings in SMT is still a pretty experimental/exotic one, so I'm glad you were able to bend it to your will for a few examples. Nice work!

[atucker]

My code is here.

Implementation

Lacking the insight into bit operations necessary to make good sketches, I instead opted to extend the program synthesis assignment by performing program synthesis by brute forcing over the space of possible sketches, up to a fixed depth of 5. It only searches over programs that use the bit operators (<<, >>, &, |) as well as addition and subtraction.

Adding or and and

I added the or and and operations, in keeping with the idea that the program synthesis would be looking for easier ways of doing more complicated operations. This was very straightforward when using the architecture suggested in Adrian's Tutorial.

Managing the sketch space

I wrote a class called Forest to manage the abstract syntax trees that I was brute forcing through. The main important thing here is that I didn't want to re-add trees that I had already explored, so I made an add method that was a NOOP if it had already seen a tree's string. I also separated the commutative operations from the non-commutative operations, and only added one copy rather than adding t1 op t2 and t2 op t1, and I created a canonical representation by sorting the two arguments by their representation string.

For convenience, I also separated the concern of finding new nodes to add to the sketch tree from the concern of combining the two nodes for each operation.

The main way that it explores the sketches is by use of the function expand_top, which takes a node then looks through every other node that it's seen of equal or lesser depth, and combines it with every operation. Since we start the frontier expansion from the root nodes of a single variable, we do all the depth n nodes before doing all the depth n+1 nodes.

Making it go faster

At first, I wanted to do something where the program would, before calling z3, try to check for equality on a smaller number of inputs. It was going to be really great because I was going to keep track of how many programs each input disproved so that I could try the most informative ones first. But then I realized that this was a confused notion that I had gotten from the super optimization discussion -- you can't actually disprove a sketch with a single input, so that was that idea.

Instead, I noticed that an earlier version of my code when I only added an x or new hole to the top of the tree was finding solutions faster than my new and improved version which explored the space of possible sketches more thoroughly. So I broke my search into two steps -- one which used the old version of the exploration, and one which used the new version of the exploration.

The forest implementation actually handled this pretty nicely, since if a node was already seen then it can't get readded to the frontier, but it does still exist in the tree cache, and so it's available for getting added to the tree.

Testing

I mostly tested this synchronously in an ipython notebook while I was writing the code, but I added some test cases too.

A few tests just run through the examples from the synthesis tutorial, and then a few other ones show the brute forcing results.

So for example, for x*12, after searching through >900 trees it finds:

   sketch: (((x + x) + x) << h79)
synthesis: (((x + x) + x) << 2)

Or it manages to do the "variable or hole?" analysis that the tutorial mentions for x * 9:

   sketch: ((x << h1) + x)
synthesis: ((x << 3) + x)

Other times it finds something pretty obvious, like it's answer for x * 3:

   sketch: ((x + x) + x)
synthesis: ((x + x) + x)

It doesn't really have a cost model right now, so there's no actual guarantee that the new version is faster. Just that it doesn't use *.

Overall this was pretty fun! Z3 definitely feels like magic, though watching my computer grind through the brute forces definitely made me realize that it's not actually doing things that quickly.

[sampsyo]

Really really interesting; I like this idea! The basic notion of searching over the space of sketches, and then solving the sketches, reminds me quite a bit of metasketches. You might enjoy reading their solution to the same basic problem.

you can't actually disprove a sketch with a single input, so that was that idea.

Good point; you can't even really run a sketch with a single input. (Unless you do some sort of symbolic interpretation, which might defeat the purpose of getting a fast early rejection.)

Anyway, super cool reframing of the synthesis problem here!

[chhzh123]

In this task, I implemented a simple solver for polynomial factorization on the integer set . The code is here, which partly reuses the Ex2 program.

Firstly I added power support (a^b) to the language, so that the users can type the polynomial they want to factorize in a text file. We can consider the following polynomial,
,
if
,
then we can rewrite in this form
.
Those are the variables we want to solve.

After my synthesizer reads in the original polynomial, it will automatically construct the above expression based on the largest exponent of the polynomial. The polynomial factoring problem then becomes finding the solution of .

Since I used ^ as the power operator in the language, but for Python ^ represents XOR, we need to add paratheses to ensure the precedence relationship is correct. (I spent lots of time debugging here :(

Finally, the synthesizer works as expected. I show three non-trivial examples below, all of which prove the correctness of my synthesizer. However, when the exponent term is greater than 3, it has already taken more than 20 minutes to get the solution on my M1 MacBook.

// example 1
((2 * (x ^ 2)) - (9 * x)) - 5
((1 * x) + -5) * ((2 * x) + 1)
// example 2
(((x ^ 3) + (6 * (x ^ 2))) + (11 * x)) + 6
(((1 * x) + 1) * ((1 * x) + 2)) * ((1 * x) + 3)
// example 3
((((x ^ 4) + (x ^ 3)) - (19 * (x ^ 2))) + (11 * x)) + 30
((((1 * x) + 1) * ((1 * x) + -2)) * ((1 * x) + 5)) * ((1 * x) + -3)

In the first place, I wanted to implement the general factorization algorithm as the one shown in Mathematica, but it becomes very complicated when the roots of the polynomial are in complex space . Since Z3 is actually not a general symbolic solver, the search space is too large for it to deal with more complex factorization problems.

[sampsyo]

This is a really cool application-domain idea, @chhzh123! I can imagine something like this being actually useful, even if it is outperformed by more specialized covers for this exact problem (as used in Mathematica). Like, maybe it could work for equations that are not strictly polynomials or something. Very neat!

[andreyyao]

Synthia!

For this assignment I collaborated with @charles-rs. The code is here.

Extending the language

We started off with the complete sketch(including the ternary operator) from Adrian's tutorial. We first extended the language to have some bitwise operators, like |, ^, and &, as well as boolean negation, and bitwise inversion. We also included comparison operators !=, ==, <, and >, which mean that we can write down some slightly more interesting examples, such as

x * y
x == h1 ? y : x * y

This synthesizes a "better" (kind of?) version of multiplication that does a check, and maybe just returns y (that is, when x == 1). We have another similar example with 0 instead of y, that will figure out the condition x == 0.

We had to extend the interpreter as well, as we wanted the only type of values in the program to be BitVects (16 bits). Thus even comparisons return bitvectors instead of booleans, so we have to simulate them with the Z3 "if then else" expressions, with an example being z3.If(lhs < rhs, BitVectVal(1, 16), BitVectVal(0, 16)). Other than that, the interpreter extensions were quite straightforward. Lark is quite intuitive to use as well.

Craters

Our main extension over the original sketch was actually not the bitwise operators and comparisons, but rather augmented holes. The tutorial pointed out (which I still think is like magic) that by using a conditional like h1 ? x : h2 the SMT solver Z3 can conditionally switch between bounded variable x and constant h2 by choosing whether to put 0 into h1. However it would be tedious to write this every single time in the source code. While originally variables whose names start with h are considered holes, we invented a new kind of hole, that is variables names starting with hh. In this post we will refer to them as craters. In the place of craters, Z3 can put either quantified variables or bitvector constants. Meanwhile variables with a single leading h like hehe can still only be filled with constants.

However, due to the limitations of Z3, this was not trivial to implement. Here's the workflow. After constructing Z3 trees expr1, expr2 from the Lark parse trees tree1, tree2, we pass expr2 into a few postprocessing steps.

• dig_holes calls expand on each uninterpreted variable it sees.
• expand(var, plain_vars) takes in a list of quantified variables plain_vars. It looks at var which is a Z3 uninterpreted variable and checks if it's a crater, i.e. if its name starts with "hh". If not, it returns the var unchanged. If var is a crater, it "expands" the var into what we call a "crater tree", a nested conditional switch between an ordinary hole and the list of plain variables. An example tree looks like this(but with bitvects): if(hh#x != 0, if(hh#y != 0, hh#num, x), y). Here x and y are the quantified(plain) variables and hh#num is the ordinary hole. Hashtags are to prevent clashing names.
• Now we feed expr2 for Z3 to solve. It will return a model model which we then turn into a mapping from free variable names to their solved Z3 values.
• fill_holes(tree, model) takes expr2 and model and produces a new model, which assigns values to the original craters(which were previously expanded away). We first define a helper function fold_cond(t), which takes in the root of a crater tree t and then "constant fold" away the nested conditional branches based on values in model. This gives back a single result which is either an uninterpreted quantified variable or a constant. Then we call helper(t) which traverses expr2 and finds all the crater tree roots. For each crater root(i.e. "hh2#z") it retrieves the original crater name c(i.e. "hh2"), call fold_cond on the root, and the add a mapping from c to the result of fold_cond to new_model. Finally, we copy all the ordinary hole values(constants) from model to new_model and return new_model.
• Finally, we pretty print expr2 using pretty and new_model.

Experiments

We were able to implement some interesting bit-manipulation hacks and other mathy simplifications.

Quadratic

cat sketches/quadratic.txt 
x * x + y * y + z * z + 2 * x * y + 2 * y * z + 2 * x * z
(hh1 + hh2 + hh3) * (hh3 + hh1 + hh2)

python3 src/util.py < sketches/quadratic.txt
((((((x * x) + (y * y)) + (z * z)) + ((2 * x) * y)) + ((2 * y) * z)) + ((2 * x) * z))
(((z + x) + y) * ((y + z) + x))
{'hh1': z, 'hh2': x, 'hh3': y}

Sign

cat sketches/sign.txt
(x < 0) ? -1 : 0
- (hh < h)

python3 src/util.py < sketches/sign.txt
((x < 0) ? -1 : 0)
-(x < 0)
{'h': 0, 'hh': x}

min

cat sketches/min.txt 
(x < y) ? x : y
hh1 ^ ((hh2 ^ hh3) & - (hh4 < hh5))

python3 src/util.py < sketches/min.txt
((x < y) ? x : y)
(y ^ ((y ^ x) & -(x < y)))
{'hh1': y, 'hh2': y, 'hh3': x, 'hh4': x, 'hh5': y}

Challenges

Setting up emacs for python was confusing.

Also Z3 switches the order of operands without permission, like a != b has b as the first child, sometimes. That was a PAIN to debug.

[sampsyo]

This is really really cool!! I like the idea of making craters first-class citizens, which is kind of their ultimate destiny, instead of something weird and hacky you have to put into the sketch itself. Awesome work taking this idea to its logical conclusion—the examples are pretty nifty and brain-teasery.

[andreyyao]

The examples are indeed very clever, but we should mention that we didn't come up with them! They come from here.

[sampsyo]

Ah, neato! That explains it.

[5hubh4m]

(Is) Program Synthesis (Possible?)

Work done by @ayakayorihiro, @anshumanmohan, and @5hubh4m. Our code is here.

Language Extension

We played around with implementing floats in the language. This was as simple as replacing z3.BitVec with z3.FloatSingle, and try to let Z3 synthesize polynomial factorizations for us. However, this turned out to be non-trivial because (1) it took too long to find models; and (2) weird floating point semantics. For instance Z3 could synthesize holes for the expression a *x * x + b * x + c == ?? * x * x + ?? * x + ?? but not for a *x * x + b * x + c == ?? * (x - ??) * (x - ??).

So we abandoned this and settled down on another language extension which was a straightforward expansion of the language: a switch expression.

expr ! default : num1 -> value1, num2 -> value2, ...

which evaluates the expression expr and compares it to numbers num1, num2, ... and returns the corresponding value; and default otherwise.

We extend the minisynth parser, interpreter, and the Z3 expression builder to support this.

Synthesis

Our problem statement is a bit different from class. Instead of synthesizing holes, we aim to find efficient lookup tables for entire expressions ("functions" of single-variables) which we represent as a large switch expression the values of which we leave as holes, and then let Z3 synthesize them for our expression. Additionally we add a pruning step, where we compress the lookup table by removing redundant entries if they match the default case.

Examples

$> echo "x * x" | python3 synthesis.py
x ! 0 : 1 -> 1, 2 -> 4, 3 -> 9, 4 -> 16, 5 -> 25, 6 -> 36, 7 -> 49, 8 -> 64, <omitted ...>

$>  echo "3 * x * x + 2 * x + 23" | python3 synthesis.py
x ! 23 : 1 -> 28, 2 -> 39, 3 -> 56, 4 -> 79, 5 -> 108, 6 -> 143, 7 -> 184, 8 -> 231,  <omitted ...>

$> echo "(x + 1) / (x + 1)" | python3 synthesis.py
x ! 1 : 255 -> 255

The last case is interesting because in Z3, all functions are total; so even division by 0 is defined, and so we see the weird result in case of 255.

An Interesting Case of Z3 and BitVectors

We implemented comparison operators <, >.. and so on as well. We were trying to synthesize lookup tables intelligently, for instance, for the expression x < 8 ? x * x : 0; which we were hoping would be something like x ! 0 : 1 -> 1, 2 -> 4, ... , 7 -> 49 however we got this huge expression.

x ! 0 : 1 -> 1, 2 -> 4, 3 -> 9, 4 -> 16, 5 -> 25, 6 -> 36, 7 -> 49, 129 -> 1, 130 -> 4, 131 -> 9, 132 -> 16, 133 -> 25, 134 -> 36, 135 -> 49, 136 -> 64, 137 -> 81, 138 -> 100, 139 -> 121, 140 -> 144, 141 -> 169, 142 -> 196, 143 -> 225, 145 -> 33, 146 -> 68, 147 -> 105, 148 -> 144, 149 -> 185, 150 -> 228, 151 -> 17, 152 -> 64, 153 -> 113, 154 -> 164, 155 -> 217, 156 -> 16, 157 -> 73, 158 -> 132, 159 -> 193, 161 -> 65, 162 -> 132, 163 -> 201, 164 -> 16, 165 -> 89, 166 -> 164, 167 -> 241, 168 -> 64, 169 -> 145, 170 -> 228, 171 -> 57, 172 -> 144, 173 -> 233, 174 -> 68, 175 -> 161, 177 -> 97, 178 -> 196, 179 -> 41, 180 -> 144, 181 -> 249, 182 -> 100, 183 -> 209, 184 -> 64, 185 -> 177, 186 -> 36, 187 -> 153, 188 -> 16, 189 -> 137, 190 -> 4, 191 -> 129, 193 -> 129, 194 -> 4, 195 -> 137, 196 -> 16, 197 -> 153, 198 -> 36, 199 -> 177, 200 -> 64, 201 -> 209, 202 -> 100, 203 -> 249, 204 -> 144, 205 -> 41, 206 -> 196, 207 -> 97, 209 -> 161, 210 -> 68, 211 -> 233, 212 -> 144, 213 -> 57, 214 -> 228, 215 -> 145, 216 -> 64, 217 -> 241, 218 -> 164, 219 -> 89, 220 -> 16, 221 -> 201, 222 -> 132, 223 -> 65, 225 -> 193, 226 -> 132, 227 -> 73, 228 -> 16, 229 -> 217, 230 -> 164, 231 -> 113, 232 -> 64, 233 -> 17, 234 -> 228, 235 -> 185, 236 -> 144, 237 -> 105, 238 -> 68, 239 -> 33, 241 -> 225, 242 -> 196, 243 -> 169, 244 -> 144, 245 -> 121, 246 -> 100, 247 -> 81, 248 -> 64, 249 -> 49, 250 -> 36, 251 -> 25, 252 -> 16, 253 -> 9, 254 -> 4, 255 -> 1

Which happens because of how signed arithmetic is defined for z3.BitVec(_, 8) which means that 129 < 8 is evaluated to True.

However, we get the "expected" program for the following expression:

$> echo "x < 8 ? (x >= 0 ? x * x : 0) : 0" | python3 synthesis.py
x ! 0 : 1 -> 1, 2 -> 4, 3 -> 9, 4 -> 16, 5 -> 25, 6 -> 36, 7 -> 49

[sampsyo]

Pretty nifty idea! It's interesting that this necessitated an after-the-fact simplification step to get it to give you what you wanted. Some of your examples remind me of the sorcerer's apprentice in Fantasia, as solvers and synthesis in general often do. Pretty cool!

The floating-point thing is indeed tricky. About this example:

For instance Z3 could synthesize holes for the expression a *x * x + b * x + c == ?? * x * x + ?? * x + ?? but not for a *x * x + b * x + c == ?? * (x - ??) * (x - ??).

I think your problem there is that distributivity does not hold for floating-point numbers (the way it does for real numbers). A way around this, if you're curious, would be to use the SMT theory of nonlinear real arithmetic, which obeys the laws that you want.

[5hubh4m]

For floats, we also tried to solve z3.Abs(expr1 - expr2) < 1e-3 instead of expr1 == expr2 to no avail.

[sampsyo]

Indeed, unfortunately, I think it's possible to find counter-examples to lots of laws with surprisingly large errors. We can find violations of distributivity with Z3, for example:

import z3


def solve(phi):
    s = z3.Solver()
    s.add(phi)
    s.check()
    return s.model()


if __name__ == '__main__':
    sort = z3.Float16()

    x = z3.FP('x', sort)
    y = z3.FP('y', sort)
    z = z3.FP('z', sort)

    expr1 = x * (y + z)
    expr2 = x * y + x * z

    delta = z3.FP('delta', sort)
    phi = z3.And((delta == expr1 - expr2), (delta > 0.1))

    print(solve(phi))

Z3 tells me:

$ python3 foo.py
[z = -1.0009765625*(2**6),
 y = -1.75*(2**-1),
 x = -1.6396484375*(2**6),
 delta = 1*(2**2)]

That's for half-precision, of course—full- and double-precision counter-examples are harder to find (i.e., Z3 doesn't return instantly on my machine), but I bet they exist. They certainly do for slightly smaller epsilons.

[5hubh4m]

That. is. insane. I knew FP was inaccurate but this is kinda wild! Thanks for the example!!

[tonyjie]

Boolean Expression Simplifier

The code is here

I change the original ex2 program to a Boolean Expression Simplifier: with the input of an boolean expression, it would return a simplified version. This is similar to what K-map would do.

The searching phase is an iterative process, like what superoptimizer would do.

How to use & Testcases

• one term has 2 variables: AB + AB' = A

cat test/2_var.txt
# (a and b) or (a and not b)
python bool_simplify.py < test/2_var.txt

Output is as follows

Original boolean expression:
(a and b) or (a and not b)

Simplified expression:
Or(And(a))

• one term has 3 variables: ABC + ABC' + A'BC + AB'C = AC + AB + BC

cat test/3_var.txt
# (a and b and c) or (a and b and not c) or (not a and b and c) or (a and not b and c)
python bool_simplify.py < test/3_var.txt

Output is as follows:

Original boolean expression:
((((a and b) and c) or ((a and b) and not c)) or ((not a and b) and c)) or ((a and not b) and c)

Simplified expression:
Or(And(a, c), And(a, b), And(b, c))

• one term has 4 variables: A'BC'D' + ABC'D' + A'B'C'D + A'B'CD + AB'C'D + AB'CD = BC'D' + B'D

cat test/4_var.txt
# (not a and b and not c and not d) or (a and b and not c and not d) or (not a and not b and not c and d) or (not a and not b and c and d) or (a and not b and not c and d) or (a and not b and c and d)
python bool_simplify.py < test/4_var.txt

Output is as follows:

Original boolean expression:
(((((((not a and b) and not c) and not d) or (((a and b) and not c) and not d)) or (((not a and not b) and not c) and d)) or (((not a and not b) and c) and d)) or (((a and not b) and not c) and d)) or (((a and not b) and c) and d)

Simplified expression:
Or(And(b, Not(c), Not(d)),
   And(Not(b), c, d),
   And(Not(b), Not(c), d))

Note that the simplified expression is BC'D' + B'CD + BC'D, which is not the most simplified expression. This is a limitation of current implementation due to Z3 solver.

Implementation

• Add support for boolean expression.

  3 ops: and, or, not are added. I use z3.Bool(name) for each variable and z3.And(), z3.Or(), z3.Not() to build z3 expressions.

• Build template expression with holes.

  This is implemented in def get_match_template_expr. I list all the possible and terms with a hole variable, and or them together.

  E.g. vars includes 3 variables: a, b, c. Template expr would be:

  (a*h111) + (a'*h112) + (b*h121) + (b'*h122) + (c*h131) + (c'*h132) 
  + (a*b*h211) + (a*b'*h212) + (a'*b*h213) + (a'*b'*h214) + (a*c*h221) + (a*c'*h222) + (a'*c*h231) * (a'*c'*232)
  + (a*b*c*h311) + ........'
  

  Then use z3.Solver to solve these holes (True or False).

• Get final simplified boolean expression.

  This is implemented in def get_simplified_expr(). Given the values of solved holes, print the simplified boolean expression.

Limitation

Can't guarantee to find the most simplified version due to the naive usage of Z3 solver, shown in the testcases test/4_var.txt. Z3 solver would search and find one correct answer and stop searching for more. So the result is simplified, but might not be the most simplified version.

[sampsyo]

Neato!! This is pretty cool and seems like a legitimately useful application. It's interesting to see how integral the post-processing get_simplified_expr step is to obtaining the minimized outputs you were looking for.

And you make a good point about minimality. Like the synthesizer we built in class, this one doesn't have a notion of "larger" or "smaller" expressions and just finds some equivalent one. It's interesting to think about what it would take to try to find the smallest expression… presumably it would need either multiple SMT queries or something like Z3's support for MaxSAT optimization problems.

[orkosinha]

My extension adds let expressions to the Basic Calculator grammar.

Adding let expressions required passing in another parameter to the interp function which allowed variables to be defined, stored, and removed such that lookup is able to find those variables in the correct context.

As an extension to the example used in class

let x = 1 in let x = 2 in y * x
y << h1

checked whether variables were scoped correctly.'

let expressions work by updating the variable store with the evaluated definition, evaluating the expression following the in, and then removing the variable from the store.

[sampsyo]

Alright; seems perfectly good! Did the let interpretation work exactly the same as how you'd write it for a normal interpreter? Or did you have to do anything special for the synthesis setting?

[gsvic]

Sets

I implemented a version of the example in the tutorial that supports sets. My code can be found here. In summary, given an input set S and an expression of the form E = S1 operator S2, where the operator can be either intersect, union or diff will calculate an expression E that will be equal to S.

Operators

I have added support for the following operators

• Intersection (insersect)
• Union (union)
• Difference (diff)

An example expression could be the following.
{1, 5, 10} union {8, 9}

or

{1, 5, 10} diff {5}

Tests

I provided three examples, one for each of the set operators that I added. Those are the following:

Intersect

{2, 5}
{h1, h2, h3} intersect {h4, h5, h6

Result: {'3', '2', '5'} intersect {'2', '5', '4'}

Union

{2, 5}
{h1, h2} union {h3, h4}

Result: {'2'} union {'2', '5'}

Difference

{2, 5, 100}
{h1, h2, h3, h4} diff {h6, h7, h8}

Result: {'2', '100', '5', '6'} diff {'3', '6', '4'}

Comments

It was a little bit tricky to integrate this to the already existing synthesizer, so I did some core modifications in the parser in order to support the set operations, but now it supports only those.

[sampsyo]

Interesting! I wasn't able to follow the link to your code (it's a 404; did you forget to push?), but to satisfy my curiosity: did you end up using an SMT theory of sets, or did you come up with your own encoding?

I can't exactly explain why, but these synthesized examples are kinda fun to stare at (and imagine how I would synthesize them if I were an SMT solver).

[gsvic]

Hi @sampsyo! So, I realized that I merged the PR so I accidentally deleted the branch of the link, but my code can be found here. So, I did not use any SMT theory, but I used Z3's set operations (e.g. z3.SetUnion) and then I followed the logic of your example in order to synthesize and compute the holes. The line in which I am using Z3 set operations is the following: https://github.com/gsvic/CornellCS6120/blob/main/synthesis/sethesyzer.py#L32

[sampsyo]

Ah, got it—in fact, that is using the SMT theory. (Using constructors like EmptySet and operators like SetUnion means you're invoking the theory of sets.)

[gsvic]

Yeah, I did not expressed it the right way, so the answer is yes :)

[michaelmaitland]

Code is here.

Summary

I followed and extended James Bornholt's tutorial on Building a Program Synthesizer. I chose to extend the DSL in the tutorial with minus and div.
I chose to extend with these constructs to see what would happen with regard to synthesis when we add multiple ways to do the same thing into the language. For example, we all know that subtraction can be implemented using addition of negative integers. How does this impact synthesis? How does the synthesizer know which constructs to synthesize?

Implementation

I basically added on all the same steps that James did in the tutorial but with my new and extended DSL. This was quite straightforward.

Evaluation

I played around to see if it would generate the same program for the example he synthesized. What was interesting is that it gave back a different program! It was an equivalent program. I'm not sure why this happened though. I ran the both my version and his version many times and kept getting back the same answers. So it seems deterministic for each example but we are unable to decipher why a DSL with additional constructs acts deterministically different.

I wonder the impact of this in the real world. I assume that it has to do with Z3 magic behind the scenes and satisfying in different manners. But does this have real impact on synthesis?

I also played around testing some other programs to make sure I could in fact synthesize programs with division and subtraction.

One thing I also thought about was that division on CPU is slow. One optimization is to use optimizations to replace the division with a faster sequence of instructions. I wonder how difficult it would be to extend my code to do something like this

[sampsyo]

Sounds cool! How hard did you find it working with Rosette (presumably for the first time)?

I played around to see if it would generate the same program for the example he synthesized. What was interesting is that it gave back a different program! It was an equivalent program. I'm not sure why this happened though.

This can certainly happen! In my experience, Z3 is deterministic in the sense that running it twice on the same input gives me the same answer, but it's not exactly "stable", in the sense that different versions of Z3 or different setups on different machines will give me different answers. (In the case of SAT, of course—it's not like it can't make up its mind about whether something is SAT or UNSAT!) Like, my little in-class example of x ÷ 7 = 6 gives me 42 on most machines but 43 or whatever on some (because we're doing integer arithmetic).

One optimization is to use optimizations to replace the division with a faster sequence of instructions. I wonder how difficult it would be to extend my code to do something like this

Seems like this should "just work", right? In the same way that we synthesized stuff like x << 3 for x * 8, it seems like you could probably synthesize x >> 3 for x ÷ 8. Maybe you already tried that?