Home

Welcome to the Leon wiki!

Description of resident topic branches

topic/condition-abduction

Implements synthesis by condition-abduction, relies on insynth, allows synthesis of more complicated programs.

topic/hornclause-generation

Based on Ravi's fork. Converts numerical Leon programs to Horn clauses automatically.

topic/extern

Allows proper Evaluator calls to functions annotated with @extern, Leon will rely on scalac-generated bytecode and with bridge them. Solver reasoning for @extern functions are limited to their specification (body treated as chooses).