Soufflé Documentation

If you are running code written for an older version of Soufflé, you can enable legacy compatibility using either a command line flag or a source code pragma.

.pragma "legacy"

You can obtain Soufflé in two ways:

1. Packaged Versions: For Ubuntu, Fedora, or Oracle Linux, download a pre-built version from the Releases section.
2. Source Code: Clone the repository using git.

For detailed build instructions, refer to the official build guide.

$ git clone https://github.com/souffle-lang/souffle.git

In the Soufflé AST, a Clause represents a horn clause. It can take two forms:

1. A Fact: A clause with only a head (e.g., X(a, b)).
2. A Rule: A clause with a head and a body (e.g., Y(a, b) :- X(a, b)).

You can construct a clause using various constructors depending on whether you are defining a fact, a rule, or a named clause. You can manipulate the body of the clause by adding literals or setting the entire collection of body literals.

// Example conceptual usage for a rule: Head :- Body1, Body2
// Note: This requires existing Atom and Literal objects
souffle::ast::Clause rule(
    std::move(headAtom), 
    std::move(bodyLiterals), 
    std::move(executionPlan)
);

In Soufflé, you can declare custom functors to extend the language's capabilities. A functor declaration specifies a name, a list of parameter attributes, a return type attribute, and whether the functor is stateful.

Example syntax in Soufflé code:

.functor foo(x:number, y:number):number

The souffle::ast::Node class uses an LLVM-style Run-Time Type Information (RTTI) system. To integrate a new class into the AST hierarchy, you must:

1. Add the class to the NodeKind enum within Node.
2. Implement static bool classof(const Node*) for your class.
3. If the class is final, provide a single enum entry. If it is non-final, provide a range of enums (e.g., NK_T, NK_Child1, ..., NK_LastT) to represent its subtypes.

This allows for safe downcasting and type checking within the Soufflé compiler infrastructure.

The souffle command translates declarative Datalog programs into high-performance C++ code. To compile and execute a program in one step, use the -c or --compile flag. You can also specify input fact directories and output destinations.

Common workflow patterns:

• Compile and run: Use -c to execute the program.
• Direct output: Use -D- to write output relations to stdout.
• Parallel execution: Use -j <N> to run the compiler/interpreter using N threads (use N=auto for system default).

souffle -c program.dl -Ffacts -D- -j20

The souffle-profile tool interactively displays performance profile information for Soufflé programs. It provides three types of views: relation-based, rule-based, and a graphical visualization.

Prerequisite: To use this tool, your Soufflé programs must be compiled with the -p option to generate the necessary profile information files.

If you want to inspect or use the generated code rather than just running the program, use the following flags:

• Generate C++ source: Use -g <FILE> or --generate=<FILE> to write the C++ source code produced from a Datalog file.
• Generate executable: Use -o <FILE> or --dl-program=<FILE> to write the executable program to a file without executing it.

souffle -g output.cpp program.dl

To convert your profiling log into an interactive HTML/JS GUI, use the -j flag. You can optionally specify a custom output filename.

Examples

Generate with default filename:

souffle-profile my_log.log -j

Generate with a specific filename:

souffle-profile my_log.log -j my_custom_report.html

Common ways to invoke the profiler include checking the version, viewing help, or passing a log file for analysis.

souffle-profile -v
souffle-profile -h
souffle-profile <log-file>
souffle-profile -c "help" <log-file>

The getBodyLiterals template allows you to extract literals of a specific type from a clause's body. It iterates through the body and uses as<T> to perform dynamic casting, returning a vector of pointers to the matching literals.

template <typename T, typename C>
std::vector<T*> getBodyLiterals(const C& clause);