/ocelot

A synthesis-enabled solver for relational logic

Primary LanguageRacketBSD 2-Clause "Simplified" LicenseBSD-2-Clause

Ocelot

Build Status

Ocelot provides an embedding of relational logic in Rosette, a solver-aided programming language. Ocelot enables both verification and synthesis of relational logic expressions.

Installation

From the Racket package server

Run:

raco pkg install ocelot

From Source

Clone this respository, enter its directory, and run:

raco pkg install

Getting started

Open the Ocelot documentation:

raco docs ocelot