Skip to content
forked from QXG2/souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.

Notifications You must be signed in to change notification settings

gangtan/souffle

Repository files navigation

Build Status

Soufflé is a translator of Horn clauses into parallel C++. Soufflé language has similarities to Datalog, and is used as a domain-specific language for analysis problems.

Features of Soufflé

  • Efficient translation to parallel C++ of Datalog programs
  • Extended semantics of Pure Datalog, e.g., permitting unbounded recursions with numbers
  • Simple component model for Datalog specifications
  • Recursively defined record types (aka. constructors) for tuples

To be added

  • Lattice definition
  • Monotone Filter Functions
  • Monotone Functions

Progress

  • ParseDriver, Ast Nodes (done)
  • Ast to Ram translation (almost done, except lattice association)
  • Ram Interpreter and/or Synthesiser (in progress)

see paper "From Datalog to FLIX: A Declarative Language for Fixed Points on Lattices"

How to get Soufflé

Use git to obtain the source code of Soufflé.

$ git clone git@github.com:QXG2/souffle.git

Build instructions can be found here.
basic:

  • use "make -j8" for faster build.
  • use "make doxygen-doc" to create the directory doc/html which will contain the file index.html to view the documentation.
  • In folder "souffle/src/dataflowTest/lattice", try "make" to test the lattice feature.

About

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages

  • C++ 51.2%
  • HTML 36.5%
  • Makefile 9.6%
  • M4 0.9%
  • Yacc 0.7%
  • Shell 0.6%
  • Other 0.5%