Lab for Automated Reasoning and Analysis LARA

COMFUSY: COMplete FUnctional SYnthesis

Comfusy is a tool for synthesizing executable code from specifications in linear integer arithmetic and constraints on sets of objects.

Comfusy works as a plugin for the Scala compiler. Comfusy was developed and tested with the version 2.7.7 of Scala (*not* the more recent 2.8.* or 2.9.* releases).

Examples

  • Browse through the examples here: examples

Using Synthesis to Generate and Compile Code

(The following assumes that the plugin Jar file is called synthesis-plugin.jar and is in the current directory.)

  • Compile your code with

scalac -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar YourFile.scala

  • Run your code with

scala -classpath synthesis-plugin.jar YourObject

Using Synthesis in the Interpreter

You can also use the plugin in the Scala interpreter (REPL) directly. Start scala with:

scala -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar

then type:

import synthesis.Definitions._

then try for instance:

scala> val answer = choose((x: Int) => x > 41)

…and you will get:

<console>:7: Synthesis predicate has multiple solutions for variable assignment:
  Solution 1: x = 42
  Solution 2: x = 43
       val answer = choose((x: Int) => x > 41)
                    ^
answer: Int = 42

Notes on using Z3 for additional compile-time checks

By default, the plugin tries to run Z3 to check that calls to the choose function have a (unique) solution, and warns the user if this is not always the case (the warnings include counter-examples). It also checks if pattern-matching expressions are exhaustive (no input value can fall through all the cases), and if all cases are reachable (no case is subsumed by the cases above it).

* The command the plugin tries to run is z3 -smt -m -in, so make sure Z3 is in the path and that it accepts these arguments (this may depend on the version you have). We currently do not support any other solver.

* You can disable these checks by compiling the code with the command:

scalac -Xplugin:synthesis-plugin.jar -classpath synthesis-plugin.jar -P:synthesis:nowarnings YourFile.scala

(Comfusy parses Z3 models to produce a warning; versions of Z3 more recent than 2.18 may not output the proper format.)

On YouTube

Comfusy has been used to synthesize a part of computation used to generate the following Happy New Year 2010 Video (see the making-of at 0:47).

People

The people involved in the development of Comfusy are, in alphabetical order: Viktor Kuncak, Mikaël Mayer, Ruzica Piskac and Philippe Suter.

 
comfusy.txt · Last modified: 2013/10/16 18:27 by mikael.mayer