QSynthesis documentation

QSynthesis is a Python API to perform Greybox synthesis of bitvector expressions. The base synthesis algorithm is based on both a blackbox I/O based approach comparing solely input-to-output pairs to perform the synthesis, but also a whitebox AST search to synthesize sub-expressions (if the root expression cannot be synthesized all at once). Also, instead of deriving possible candidates on each expressions to synthesize, QSynthesis relies on pre-computated expressions stored in a database. The database keeps the mapping of an expression and its associated output vector representing its behavior on a set of inputs. Given a bitvector expression to synthesize, finding a candidate can thus be performed in near O(1) as the lookup is the lookup cost in database. With the structure used (Google Level-DB) the cost is thus Log(N) with N the number of entries in the database.

Python API