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.

Overview

Welcome!

This is the official repository for the Soufflé language project. The Soufflé language is similar to Datalog (but has terms known as records), and is frequently used as a domain-specific language for analysis problems.

License: UPL CI-Tests codecov

Features of Soufflé

  • Efficient translation to parallel C++ of Datalog programs (CAV'16, CC'16)

  • Efficient interpretation using de-specialization techniques (PLDI'21)

  • Specialized data structure for relations (PACT'19, PPoPP'19, PMAM'19) with optimal index selection (VLDB'18)

  • Extended semantics of Datalog, e.g., permitting unbounded recursions with numbers and terms

  • Simple component model for Datalog specifications

  • Recursively defined record types/ADTs (aka. constructors) for tuples

  • User-defined functors

  • Strongly-typed types for safety

  • Subsumption

  • Aggregation

  • Choice Construct (APLAS'21)

  • Extended I/O system for relations (including SQLITE3 interfaces)

  • C++/SWIG interfaces

  • Provenance/Debugging (TOPLAS'20)

  • Profiling tools

How to get Soufflé

Use git to obtain the source code of Soufflé.

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

Build instructions can be found here.

Legacy code

If you have written code for an older version of Souffle, please use the command line flag --legacy. Alternatively, please add the following line to the start of your source-code:

.pragma "legacy"

Issues and Discussions

Use either the issue list for

  • bug reporting

  • enhancements

  • documentation

  • proposals

  • releases

  • compatibility issues

  • refactoring.

or use the discussions bulletin board to engage with other community members and for asking questions you’re wondering about.

How to contribute

Issues and bug reports for Souffle are found in the issue list. This list is also where new contributors may find extensions / bug fixes to work on.

To contribute in this repo, please open a pull request from your fork of this repository. The general workflow is as follows.

  1. Find an issue in the issue list.

  2. Fork the souffle-lang/souffle repo.

  3. Push your changes to a branch in your forked repo.

  4. Submit a pull request to souffle-lang/souffle from your forked repo.

Our continuous integration framework enforces coding guidelines with the help of clang-format and clang-tidy.

For more information on building and developing Souffle, please read the developer tutorial.

Home Page

Documentation

Contributors

Issues

License

For academics

If you use our work, please cite our work. A list of publications can be found here. The main publications are:

  • Herbert Jordan, Bernhard Scholz, Pavle Subotić: Souffle: On Synthesis of Program Analyzers. CAV 2016.
  • Bernhard Scholz, Herbert Jordan, Pavle Subotić, Till Westmann: On fast large-scale program analysis in Datalog. CC 2016: 196-206
Comments
  • Potential deadlock in Souffle

    Potential deadlock in Souffle

    Hello,

    I think I have encountered several cases where Souffle falls into a deadlock and continues executing without producing anything at all. This seems to be independent of the analysis I am running but I can share with you both the analysis code and the facts I'm using. Right now I keep running the same analysis over over with -j 16. It is supposed to run in about 20-22 mins with maximum memory consumed 30GB.

    The analysis executable produced sometimes crashes with bad allocation (the error is related to read and write locks) and other times seems to fall into a deadlock, with the memory unchanged for hours and 1600% CPU usage. We used gdb to check where it is stuck and here it is:

    $ gdb /home/anantoni/Development/cache/souffle-analyses/fully-guided-context-sensitive/37dc31dec70d2a418f1ec2ddd9512ace022c92f4eb37364dc58ed0d0227818f1 13602GNU gdb (GDB) Fedora 8.0.1-36.fc27 (gdb) bt #0 0x0000000000435984 in souffle::OptimisticReadWriteLock::start_read() () #1 0x00000000005942be in souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::insert(souffle::ram::Tuple<int, 4ul> const&, souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::btree_operation_hints<1u>&) () #2 0x00000000005948f7 in souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::insert(souffle::ram::Tuple<int, 4ul> const&, souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::btree_operation_hints<1u>&) () #3 0x00000000005948f7 in souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::insert(souffle::ram::Tuple<int, 4ul> const&, souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::btree_operation_hints<1u>&) ()

    Thanks in advance, Anastasis

    bug - identified 
    opened by anantoni 39
  • guide about how to write parallelizable datalog rules

    guide about how to write parallelizable datalog rules

    Hello, Is there any documentation that tells how to design datalog rules that helps souffle compiler to synthesize parallel evaluator? I wrote a control flow analysis in souffle datalog that has many rules, but unfortunately souffle did not manage to parallelize it enough. I'd like to refactor my code and make it more parallel and faster. My CFA code: https://github.com/grin-compiler/ghc-grin/tree/d7aebb21fd78eda7f86a85868f79d36a071038de/lambda-grin/souffle-datalog

    Thanks!

    question 
    opened by csabahruska 34
  • WIP: Cmake port

    WIP: Cmake port

    This is a WIP but it's already useful.

    If you know cmake, this should be straightforward to use. I will update the README once closer to being finished.

    For the uninitiated, see here or just follow the below:

    1. cmake >= 3.15 required
    2. In your srcdir, run cmake -S . -B <build_dir> or cmake -S . -B <build_dir> -D<option>=<value> if you want to control settings (documented in the root CMakeFile.txt). You can also use ccmake <build_dir> after to see which options are set.
    3. The run cmake --build <build_dir> [-j16] and souffle will build
    4. To run tests, cd <build_dir>; ctest [-j16] or even just cmake --build <build_dir> [-j16] --target test

    I've made sure the compilation flags are the same on Linux 32/64. You can run both cmake and ctest with --verbose to see compile lines or test executions. Not all the tests are done yet - all the unit tests are included but not all of the positive/negative souffle tests are done.

    A few notes on improvements:

    1. It's not automake ;). No need for bootstrap/configure
    2. In general, I think the make structure is cleaner. Right now, the source layout is still automake compatible since I want the two to live side-by-side but there is some room for improvement
    3. Clear targets which can be built. See cmake --build <build_dir> --target help to see what's available
    4. Testing is improved; all tests are named (so they can be run by name using ctest -R/--tests-regex or by label, e.g. cmake -L/--label-regex. It's now possible to e.g. run just the "interpreted" tests so that testing turnaround is improved. --rerun-failed is your friend, too.
    5. I broke out each test into four phases - setup, test, compare stderr/out, compare out files. That way it's easier to spot which part of the test failed. That's why you will now see about 4x more tests.
    6. The build is now out-of-source by default and it's possible/easier to have e.g. a release and a debug build side-by-side. Just configure into two separate build dirs.
    7. Support from editors (including Intellisense) such as VS Code, CLion and Visual Studio.

    There are also performance advantages. On my machine, there are the build/test times:

    automake, with -j4: clean build: 3:12.24 total

    cmake, with -j4: clean build: 1:55.35 total (This actually does more since it also builds the unit tests)

    There's still some work to be done; there is a list of TODO's in the root CMakeFile.txt.

    I would appreciate it if someone could give this a spin on Ubuntu/MacOS to see if there are any issues.

    opened by TomasPuverle 29
  • WIP: Support for Python bindings using pybind

    WIP: Support for Python bindings using pybind

    TODO before review:

    Python code features:

    • [x] Finish exposing all current existing interfaces
      • [ ] Symbol table. Interface TBD.
      • [ ] Record table. Interface TBD.
    • [x] Handle aux/primary arity, provenance and whether or not it needs to be handled/exposed
    • [ ] Handle records
    • [ ] Synthesize named tuples for UDTs
    • [ ] Support for writing functors in Python (see #1831)
    • [ ] Support wrapping of Python objects in Souffle programs

    Infra work Items:

    • [ ] Make python support conditional
    • [ ] Update infra containers to add poetry/nox
    • [ ] Linting
    • [ ] Mypy
    • [ ] More complete nox runner
    • [ ] Finish test coverage
    • [ ] Documentation
    • [ ] Doctests
    • [ ] Update README to install poetry and nox
    • [ ] Improve distcheck for Python code
    opened by TomasPuverle 25
  • MSVC support, CI github Actions `windows-2019`

    MSVC support, CI github Actions `windows-2019`

    This is a work-in-progress to support the build of Souffle on native Windows with Visual Studio.

    Current achievement:

    • build on Github Actions with windows-latest.
    • tests are disabled, they all fail in ctest currently, I did not investigate.

    Fixes Main fixes include:

    • must use signed integer loop variable in OMP parallel for.
    • must explicit many integer conversions.
    • must not use dynamically sized array, use unique pointers instead.
    • must replace gnu builtins with equivalent msvc builtins.

    Other changes:

    • getopt / getopt_long no standard on Windows, wrote a replacement function to avoid introducing third-party licensed code.
    • some compilation options.
    opened by quentin 22
  • Incorrect result in compiler mode?

    Incorrect result in compiler mode?

    Hi guys,

    Consider the following program:

    .decl graph(from:number, to:number)
    .decl eql(a: number, b: number)
    .decl rel(a: number, b: number) btree_delete
    .decl C(x:number) btree_delete
    .decl D(x:number, y:number)
    .decl E(x:number, y:number) btree_delete
    .decl a__(a:number, b:number) 
    
    .output a__ // Output node
    
    graph(1, 2).
    graph(1, 3).
    graph(3, 4).
    graph(2, 5).
    graph(4, 6).
    graph(5, 6).
    graph(6, 7).
    
    eql(x,x) :- eql(x,_); eql(_,x).
    eql(x,y) :- eql(y,x).
    eql(x,z) :- eql(x,y), eql(y,z).
    rel(1, 2).
    rel(1, 3).
    eql(x, x) :- rel(x, _).
    eql(2, 3).
    rel(a, b) <= rel(c, d) :- eql(a, c), eql(b, d), a <= c, b <= d.
    
    C(1).
    D(1, 1).
    C(x1) <= C(x2) :- D(x1, x2), x1 <= x2.
    
    E(1,1).
    E(1,2).
    E(_, x1) <= E(_, x2) :- x1 <= x2.
    
    a__(b, c) :- graph(g, b), !rel(b, d), C(c), E(d, a).
    

    When I run the above program in compiler mode, I get the following result for the relation a__:

    $ souffle_59260/src/souffle -w -c orig_rules.dl && cat a__.csv
    2	1
    3	1
    4	1
    5	1
    6	1
    7	1
    

    However, if I add a subgoalE(d, e) in rule a__ to get the a__(b, c) :- graph(g, b), !rel(b, d), C(c), E(d, a), E(d, e)., the result of a__ should not change. But running the following program computes an empty result for a__.

    
    .decl graph(from:number, to:number)
    .decl eql(a: number, b: number)
    .decl rel(a: number, b: number) btree_delete
    .decl C(x:number) btree_delete
    .decl D(x:number, y:number)
    .decl E(x:number, y:number) btree_delete
    .decl a__(a:number, b:number) 
    
    .output a__ // Output node
    
    graph(1, 2).
    graph(1, 3).
    graph(3, 4).
    graph(2, 5).
    graph(4, 6).
    graph(5, 6).
    graph(6, 7).
    
    eql(x,x) :- eql(x,_); eql(_,x).
    eql(x,y) :- eql(y,x).
    eql(x,z) :- eql(x,y), eql(y,z).
    rel(1, 2).
    rel(1, 3).
    eql(x, x) :- rel(x, _).
    eql(2, 3).
    rel(a, b) <= rel(c, d) :- eql(a, c), eql(b, d), a <= c, b <= d.
    
    C(1).
    D(1, 1).
    C(x1) <= C(x2) :- D(x1, x2), x1 <= x2.
    
    E(1,1).
    E(1,2).
    E(_, x1) <= E(_, x2) :- x1 <= x2.
    
    a__(b, c) :- graph(g, b), !rel(b, d), C(c), E(d, a), E(d, e).
    
    $ souffle_59260/src/souffle -w -c orig_rules.dl && cat a__.csv
    
    

    FYI, Running both programs in interpreter mode returns:

    2	1
    3	1
    4	1
    5	1
    6	1
    7	1
    

    I am using the latest commit: 592605c21c6b0af9a971499ad9c6a147302184b1

    bug - identified 
    opened by bertram-gil 21
  • Integrate SWIG Interface and improve c++ interface

    Integrate SWIG Interface and improve c++ interface

    This pull request is aimed to solve issue #573 to enhance Souffle with the implementation of a program interface with SWIG through integrating the work done for the issue as well as adding tests for it. Its aim is to allow other languages to interface Souffle using SWIG. Current supported languages for the SWIG interface is Java and Python. Documentation can be found on https://github.com/chadgavin/souffle/wiki/SWIG.

    This pull request is also aimed to solve issue #1075 to fix the tuple insertion bug. A tuple can now only be inserted to a relation which has the same arity and variable type. In addition, SouffleInterface.h is commented and documented by using Doxygen. Documentation can be found on https://github.com/chadgavin/souffle/wiki/C---Interface.

    opened by detljh 21
  • Segfault when requesting tuple provenance

    Segfault when requesting tuple provenance

    When requesting the provenance of a tuple, Souffle encounters a segmentation fault. The test case is attached. I have encountered this behavior both with the latest release and the repository head.

    andersen.zip

    To reproduce, run souffle -t explain -F . -D - rules.dl, and request the provenance of pt("v7", "v1").

    bug - identified 
    opened by r-mukund 20
  • error when installing: fatal error: 'ast/BranchDeclaration.h' file not found

    error when installing: fatal error: 'ast/BranchDeclaration.h' file not found

    I am trying to install souffle on OSX 11.6.

    I am following the build directions listed here.
    However, I am getting the following error when run cmake --build build -j8:

    In file included from ~/repos/souffle/src/parser/ParserDriver.cpp:32:
    ./parser/parser.yy:68:14: fatal error: 'ast/BranchDeclaration.h' file not found
        #include "ast/BranchDeclaration.h"
    

    I also attempted install using homebrew as described here. When running brew install --HEAD souffle-lang/souffle/souffle, I receive the error

    ==> cmake --build build --target install
    Last 15 lines from ~/Library/Logs/Homebrew/souffle/03.cmake:
    /tmp/souffle-20211015-55340-1cu7kzf/src/include/souffle/utility/json11.h:290:14: error: expected unqualified-id
        if (std::isfinite(value)) {
                 ^
    /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX11.3.sdk/usr/include/math.h:155:5: note: expanded from macro 'isfinite'
        ( sizeof(x) == sizeof(float)  ? __inline_isfinitef((float)(x))       \
        ^
    15 errors generated.
    make[2]: *** [src/CMakeFiles/libsouffle.dir/ast/analysis/ProfileUse.cpp.o] Error 1
    make[1]: *** [src/CMakeFiles/libsouffle.dir/all] Error 2
    make[1]: *** Waiting for unfinished jobs....
    [ 45%] Linking CXX executable test_brie
    [ 45%] Linking CXX executable souffleprof
    [ 45%] Built target test_brie
    [ 45%] Built target souffleprof
    make: *** [all] Error 2
    

    Even after following the instructions to update the command line tools.

    help wanted 
    opened by wdduncan 19
  • Correct reporting of line numbers

    Correct reporting of line numbers

    After the latest additions, I get errors and warnings of the form: Variable ?lastFld only occurs once in file analysis.dl at line 2966 on a file of only 2000 lines. I'm not sure if this is due to wave (suspect not, since I don't use preprocessor directives in that file, but it could be, since I've run into other wave issues without using preprocessor directives) or if it's an issue with the support of multiple heads of rules.

    bug - identified 
    opened by yanniss 19
  • C-Preprocessor

    C-Preprocessor

    At the moment we rely on cpp to convert Datalog input programs with macros to programs without macros. The conversion is done in main.cpp. The popen() function invokes the cpp and returns a FILE handle on the converted program.

    Unfortunately, various systems use different cpp versions/implementations. As a consequence, the behaviour of the macro expansion is not consistent.

    My suggestion is to replace cpp with boost's wave library. This library implements a C-Preprocessor and can be added to the Souffle source code. Souffle has a UPL license. Hence I feel that using BOOST with a BSD style license should work (i.e. in general, I believe we cannot add code that has a GPL style license).

    bug - identified enhancement 
    opened by b-scholz 19
  • A problem about subsumption.

    A problem about subsumption.

    Hi,

    Consider the following program:

    .decl a(A:number)
    a(1).
    a(2).
    a(A1)<=a(A2):-A1<A2.
    a(A1)<=a(A2):-A1>A2.
    .output a
    

    Souffle has empty result on this program.

    The following program is equivalent to this program:

    .decl a(A:number)
    a(1).
    a(A+1):-a(A), A<2.
    a(A1)<=a(A2):-A1<A2.
    a(A1)<=a(A2):-A1>A2.
    .output a
    

    Souffle has the following result:

    ---------------
    a
    A
    ===============
    1
    ===============
    

    Whether they should have equal results, Or maybe I'm wrong to write subsumption like this.

    I have another small question, when dealing with subsumption, should it be treated as a separate rule?

    The current version of Souffle I use is 3cd802d.

    opened by DerZc 0
  • Fix complexity analysis

    Fix complexity analysis

    The complexity analysis was ignoring intrinsics operations that can contain functor calls. It had an impact on the reordering of conditions that would move a functor call too early when it is within an intrinsic operation.

    fix #2373

    opened by quentin 1
  • Insufficient checking on unground variable

    Insufficient checking on unground variable

    Hi,

    Consider the following program:

    .type typeHejh = symbol
    .type typeMrgs = unsigned
    .type typeAiik = symbol
    
    .decl tdfw(A:float, B:float, C:float)
    .decl hhxs(A:typeHejh, B:typeAiik, C:number, D:typeAiik)
    .decl vxeo(A:typeHejh, B:symbol, C:number, D:typeAiik, E:typeAiik, F:typeHejh)
    
    hhxs("40uD340uD3", "40uD3", 4, "40uD3").
    tdfw(10.712999999999999, 16.931999999999999, 10.712999999999999).
    
    vxeo(E, C, F, D, C, D) :- tdfw(B, max(A,7.179), --A), hhxs(D, C, F, E).
    
    .output vxeo
    

    This program would hang. I guess it was caused by the unground variable A, but the grammar checker did not find this. If I write this rule b(A):-tdfw(B, max(A,7.179), --A), the grammar can find this error.

    The souffle version is 3cd802d, I tried with some older version, also have this issue.

    opened by DerZc 0
  • Eliminate nondeterminism in Condition ordering

    Eliminate nondeterminism in Condition ordering

    Conditions were sorted nondeterministically in during both the MakeIndex and ReorderConditions RAM transforms. This updates both to use std::stable_sort and eliminates use of pointer comparison to sort Conditions.

    When building incremental builds of ddisasm with --generate-many, these changes significantly reduce the number of object files to recompile when a trivial change is made (with the change I am making in my particular configuration, it drops from rebuilding 18 compilation units down to two).

    opened by adamjseitz 1
  • Fix source locations with `--no-preprocessor` and add a virtual file system layer to the parser

    Fix source locations with `--no-preprocessor` and add a virtual file system layer to the parser

    This change fixes source locations with --no-preprocessor and introduces a light virtual file system layer to the parser.

    By default the parser sees the real file system (through RealFileSystem). But it is also possible to present any other object that implements the new FileSystem interface. For intance the OverlayFileSystem combines multiple stacked virtual file-system objects (à-la Docker).

    Adds a test that demonstrate the use of vfs with the libsouffle.

    opened by quentin 1
  • Drop clause if it contains an impossible BinaryConstraint

    Drop clause if it contains an impossible BinaryConstraint

    Some BinaryConstraint atoms can be determined to be impossible during synthesis. This PR introduces a transform to eliminate clauses containing such impossible atoms.

    These kinds of atoms are not likely to be written directly, but can easily arise with inlined code.

    In ddisasm (with a small work-in-progress change to take greater advantage of this), across its various arch configurations, Souffle generates between 5.0% and 12% fewer lines of C++ with this patch. This yields build time improvements of 2.5% - 10% depending on arch configuration and compiler.

    This is my first attempt at adding a transformer pass, so please apply additional scrutiny.

    opened by adamjseitz 2
Releases(2.3)
  • 2.3(May 14, 2022)

    Synopsis

    • Auto-scheduler for rules (SamArch27)
    • Better scheduling heuristic (julienhenry)
    • Improved component system (quentin)
    • Improved type-system for record alias (quentin)
    • Introducing include directives (quentin)
    • Optional use of libffi (quentin)
    • New packaging mechanism using souffle-lang.github.io (XiaowenHu96, mmcgr)
    • Misc fixes and refactoring (langston-barrett, aeflores, pnwamk, quentin, b-scholz, XiaowenHu96, OlivierHamel, cwarden, mbid, davidwzhao, cmuellner, luc-tielen)

    What's Changed

    • Fix issue #2176 by @XiaowenHu96 in https://github.com/souffle-lang/souffle/pull/2178
    • Do not print newline after functor declaration by @mbid in https://github.com/souffle-lang/souffle/pull/2179
    • Fix github action by @XiaowenHu96 in https://github.com/souffle-lang/souffle/pull/2180
    • fixes unsigned range souffle-lang/souffle#2182 by @quentin in https://github.com/souffle-lang/souffle/pull/2184
    • fix missing header in synthesized profiled program by @quentin in https://github.com/souffle-lang/souffle/pull/2186
    • Allow URI Filenames for SQLite Input and Output by @cwarden in https://github.com/souffle-lang/souffle/pull/2177
    • update dominance example by @XiaowenHu96 in https://github.com/souffle-lang/souffle/pull/2192
    • fix souffle-compile argument parsing by @pnwamk in https://github.com/souffle-lang/souffle/pull/2191
    • control libffi dependency with SOUFFLE_USE_LIBFFI by @quentin in https://github.com/souffle-lang/souffle/pull/2188
    • alias-type on record and adt types by @quentin in https://github.com/souffle-lang/souffle/pull/2197
    • enable sqlite3 URI filename capabilty by @quentin in https://github.com/souffle-lang/souffle/pull/2199
    • Fix -Wparentheses warning in synthesized C++ code by @luc-tielen in https://github.com/souffle-lang/souffle/pull/2202
    • MSVC support, CI github Actions windows-2019 by @quentin in https://github.com/souffle-lang/souffle/pull/2098
    • emit missing '\n' in cpp includes by @pnwamk in https://github.com/souffle-lang/souffle/pull/2206
    • Subsumption fix for issue #2189 by @b-scholz in https://github.com/souffle-lang/souffle/pull/2204
    • cleanup Windows CI trigger by @quentin in https://github.com/souffle-lang/souffle/pull/2210
    • Clean up relation generation for provenance in synthesiser and interpreter by @davidwzhao in https://github.com/souffle-lang/souffle/pull/2208
    • Cleanup defunct delta-based SIPs by @langston-barrett in https://github.com/souffle-lang/souffle/pull/2212
    • separate symbol table interface from implementation by @quentin in https://github.com/souffle-lang/souffle/pull/2200
    • fix type system when a record's field is an alias type by @quentin in https://github.com/souffle-lang/souffle/pull/2219
    • Fix#2223 by @b-scholz in https://github.com/souffle-lang/souffle/pull/2224
    • Allow populating and reading ADTs in souffle::tuple interface by @aeflores in https://github.com/souffle-lang/souffle/pull/2183
    • Subsumption Example by @b-scholz in https://github.com/souffle-lang/souffle/pull/2216
    • improve behaviour of inheritance by @quentin in https://github.com/souffle-lang/souffle/pull/2220
    • fix examples by @quentin in https://github.com/souffle-lang/souffle/pull/2234
    • Fix segfault in souffleprof related to "@new" relations by @langston-barrett in https://github.com/souffle-lang/souffle/pull/2230
    • Not adding -g flag when compiled with NDEBUG by @XiaowenHu96 in https://github.com/souffle-lang/souffle/pull/2238
    • Fix #2190: Magicset bug by @b-scholz in https://github.com/souffle-lang/souffle/pull/2241
    • Subsumptive clauses crash when dominated and dominating heads are identical. by @b-scholz in https://github.com/souffle-lang/souffle/pull/2240
    • update to vcpkg 2022.03.10 by @quentin in https://github.com/souffle-lang/souffle/pull/2242
    • Don't apply RemoveRelationCopies transformer to EQRELs by @langston-barrett in https://github.com/souffle-lang/souffle/pull/2244
    • Auto-Scheduler for Soufflé by @SamArch27 in https://github.com/souffle-lang/souffle/pull/2237
    • Fix profiler cost estimate by @OlivierHamel in https://github.com/souffle-lang/souffle/pull/2245
    • Fix segfault in ~ProfileEventSingleton by @langston-barrett in https://github.com/souffle-lang/souffle/pull/2226
    • Remove ProfileSips by @SamArch27 in https://github.com/souffle-lang/souffle/pull/2251
    • Disable pragma2 test on Linux by @cmuellner in https://github.com/souffle-lang/souffle/pull/2252
    • Update/correct/standardise version and license text by @mmcgr in https://github.com/souffle-lang/souffle/pull/2254
    • Fix deb file creation by @mmcgr in https://github.com/souffle-lang/souffle/pull/2255
    • Fixed auto-scheduler for recursive rules using Selinger w/ vector by @SamArch27 in https://github.com/souffle-lang/souffle/pull/2258
    • Add release debs/rpms to souffle-lang.github.io/ppa by @mmcgr in https://github.com/souffle-lang/souffle/pull/2261
    • delta-max-bound sips heuristic by @julienhenry in https://github.com/souffle-lang/souffle/pull/2260
    • fact-like rule using functor by @quentin in https://github.com/souffle-lang/souffle/pull/2262
    • fix test: getopt_long returns an int by @quentin in https://github.com/souffle-lang/souffle/pull/2264
    • Fix#2257 by @b-scholz in https://github.com/souffle-lang/souffle/pull/2267
    • eqrel: Simplify insertAll by @langston-barrett in https://github.com/souffle-lang/souffle/pull/2268
    • add support for include in datalog scanner by @quentin in https://github.com/souffle-lang/souffle/pull/2270
    • Prepare changelog for Release V2.3 by @b-scholz in https://github.com/souffle-lang/souffle/pull/2272

    New Contributors

    • @mbid made their first contribution in https://github.com/souffle-lang/souffle/pull/2179
    • @pnwamk made their first contribution in https://github.com/souffle-lang/souffle/pull/2191

    Full Changelog: https://github.com/souffle-lang/souffle/compare/2.2...2.3

    Source code(tar.gz)
    Source code(zip)
    sha512sum.txt(513 bytes)
    x86_64-fedora-34-souffle-2.3-Linux.rpm(2.48 MB)
    x86_64-oraclelinux-8-souffle-2.3-Linux.rpm(2.61 MB)
    x86_64-ubuntu-2004-souffle-2.3-Linux.deb(3.87 MB)
  • 2.2(Jan 17, 2022)

    • Subsumption clauses, e.g., A(x1) <= A(x2) :- x1 <= x2 (@julienhenry, @b-scholz)
    • IR and build improvements (@OlivierHamel, @langston-barrett, @quentin, @b-scholz, @aeflores, @cmuellner, @broffra, @rahlk, @yihozhang, @trofi)
    • Refactoring of type analysis (@tytus-metrycki)
    • Improved packaging (@XiaowenHu96, @quentin, @uxhg, @cwarden)
    • Improved loading of DLLs (@quentin)
    • Type annotation printer (@hide-kawabata)
    • Performance improvements for eqrel (@langston-barrett, @kevzhumba)
    Source code(tar.gz)
    Source code(zip)
    sha512sum.txt(679 bytes)
    x86_64-centos-8-souffle-2.2-Linux.rpm(2.44 MB)
    x86_64-fedora-34-souffle-2.2-Linux.rpm(2.34 MB)
    x86_64-ubuntu-2004-souffle-2.2-Linux.deb(3.63 MB)
    x86_64-ubuntu-2104-souffle-2.2-Linux.deb(3.68 MB)
  • 2.1(Aug 19, 2021)

    • Choice domain (@XiaowenHu96)
    • Proper treatment of escape codes in symbol constants (@lyxell)
    • CSV output has rfc4180 flag for delimiters (@quentin)
    • Fix UDF syntax (@TomasPuverle)
    • Add no_magic/no_inline relational qualifiers (@sharon-wang)
    • Retire $; replace by autoinc() (@b-scholz)
    • Suppress file errors with -w flag (@b-scholz)
    • Re-implementation of the ast-to-ram translator (@azreika)
    • Added Cmake PORT support (@XiaowenHu96, @quentin
    • GitHub Action (@XiaowenHu96, @quentin, @XiaowenHu96, @b-scholz, @lyxell,@quentin,@OlivierHamel)
    • Debian Packaging and CodeCov support in GitHub Action/Cmake (@phao5814)
    • Lock-free record/symbol tables (@quentin)
    • Interpreter refactoring / fixing (@XiaowenHu96)
    • Type Analysis Refactoring (@azreika, @tytus-metrycki)
    • New SIPS strategy (@langston-berrett)
    • Refactor AST & RAM & Provenance (@TomasPuverle, @b-scholz, @azreika)
    • RAM Optimisation (@SamArch27)
    • Multiple library flag (@mclements)
    • Added “max-bound-delta” SIPS (@langston-barrett)
    • General Fixes and improvements (@b-scholz, @csabahruska, @julienhenry, @langston-berrett, @mmcgr, @TomasPuverle, @quentin,@XiaowenHu96)
    • Add fuzzing scripts with AFL and Radamsa (@langston-barrett)

    Download Debian packages from here: https://packagecloud.io/souffle-lang/souffle

    Install Souffle on Mac using brew: https://github.com/souffle-lang/homebrew-souffle

    Source code(tar.gz)
    Source code(zip)
  • 2.0.2(Sep 25, 2020)

    • Fix OSX user library paths (mmcgr)
    • Fix concurrent profling (mmcgr)
    • Fix indirect index use (aeflores)
    • Fix 'as' type conversion (darth-tytus)
    • Fix output of hint statistics (azreika)
    • Implement Record/ADT user-defined functors (darth-tytus)
    • Optimise ADT encoding (darth-tytus)
    • Added limitsize directive (b-scholz)
    • Add heuristic-based clause reordering (azreika)
    • Enhanced Magic Set transformation (azreika)
    • Restructuring for readability and maintainability (b-scholz, mmcgr)
    Source code(tar.gz)
    Source code(zip)
    souffle-2.0.2.md5(36 bytes)
    souffle-2.0.2.pkg(2.13 MB)
    souffle_2.0.2-1_amd64.deb(1.38 MB)
    souffle_2.0.2-1_amd64.md5(36 bytes)
  • 2.0.1(Jul 29, 2020)

    • Stop overmaterialising aggregate bodies (rdowavic)
    • Parallelise aggregate computation (rdowavic)
    • Add JSON IO (GaloisNeko)
    • Extend program minimiser (azreika)
    • Use greater precision for floating point output (mmcgr)
    • Fix duplicated symbols with multiple souffle object files (luc-tielen)
    • Fix multithreaded, interpreted, provenance (taipan-snake)
    • Fix provenance constraint explanation (taipan-snake)
    • Fix path detection for souffle tools (mmcgr)
    • Fix output directory use (mmcgr)
    Source code(tar.gz)
    Source code(zip)
    souffle-2.0.1.md5(36 bytes)
    souffle-2.0.1.pkg(2.54 MB)
    souffle_2.0.1-1_amd64.deb(1.46 MB)
    souffle_2.0.1-1_amd64.md5(36 bytes)
  • 2.0.0(Jun 30, 2020)

    • Added --legacy flag to allow use of legacy options (darth-tytus)
    • Added --show [...] flag to show various extra bits of information for debugging/optimising (lyndonhenry)
    • Query interface for provenance (yuli6313)
    • Removed MPI support (b-scholz)
    • Removed bddbddb and logicblox converters (b-scholz)
    • Removed checkpointed evaluation (b-scholz)
    • Extended inlining support (azreika)
    • Added AST debug output for final 'optimised datalog' (mmcgr)
    • Added RAM debug output (b-scholz)
    • Updated man pages (darth-tytus/mmcgr)
    • Fixes for AST/RAM printing (mmcgr)
    • More useful debug output (mmcgr)
    • Much more useful debug output (ohamel-softwaresecure)
    • Interpreted souffle performance improvements (XiaowenHu96)
    • Improved version output (mmcgr)
    • Added support for floats and unsigned ints (darth-tytus)
    • Improved testing (yuli6313/mmcgr)
    • Added support for Record I/O (darth-tytus)
    • Simplified error and warning messages (mmcgr)
    • Added bitshift operators (ohamel-softwaresecure)
    • Added support for polymorphic constants (darth-tytus)
    • Improved aggregate performance (rdowavic)
    • Added support for as(arg, type) (darth-tytus)
    • Extensive refactoring of AST, RAM, utilities, and other bits (b-scholz and others)
    • Improve Program Minimiser(azreika)
    • Unrestricted number of columns per relation (before set to 64) (SamArch27)
    • Generative functors (ohamel-softwaresecure)
    • Refactor parser (ohamel-softwaresecure)
    • Various bugfixes
    Source code(tar.gz)
    Source code(zip)
    souffle-2.0.0.md5(36 bytes)
    souffle-2.0.0.pkg(2.51 MB)
    souffle_2.0.0-1_amd64.deb(1.42 MB)
    souffle_2.0.0-1_amd64.md5(36 bytes)
  • 1.7.0(Nov 29, 2019)

    • Rewrote Interpreter for enhanced performance (XiaowenHu96,HerbertJordan)
    • Add SWIG interface (detljh,chadgavin,honghyw)
    • Improved C++ interface and documentation (detljh,chadgavin,honghyw)
    • C++ interface allows specification of thread count (mmcgr)
    • Added RAM analysis to debug report (b-scholz)
    • New provenance instrumentation storing subproof heights (ssallinger)
    • Compiles with MSVC (brianfairservice)
    • Provenance interface supports querying results (yuli6313)
    • Removed mpi support
    • C++17 used for synthesised code
    • Performance enhancements
    • Bug fixes
    Source code(tar.gz)
    Source code(zip)
    souffle-1.7.0.md5(36 bytes)
    souffle-1.7.0.pkg(2.96 MB)
    souffle_1.7.0-1_amd64.deb(1.39 MB)
    souffle_1.7.0-1_amd64.md5(36 bytes)
  • 1.6.0(Jul 26, 2019)

    • Low Level Machine Interpreter for improved non-synthesised performance (XiaowenHu96,HerbertJordan)
    • Provenance support for negation and equivalence relations (taipan-snake)
    • New semantics for RAM (b-scholz)
    • Stratified RAM Analysis interfaces (b-scholz)
    • New RAM Transformations: expand/collapsing conditions of filters, hoisting of conditions, index transformation to utilize index operations, if-conversions (converting scans to existence operations if possible), Choice conversion, hoisting aggregates, and parallelization (dcol97)
    • Meta-transformers for RAM (sequence/loop/conditional) (b-scholz)
    • Add RAM transform support to debug report (rdowavic)
    • Enable complex aggregates (rdowavic)
    • Memory use improvements (mmcgr)
    • Allow input pipes for datalog (maweki)
    • Allow arbitrary argument length formax/min/cat functors (azreika)
    • AST optimisations (azreika)
    • Add user-defined libraries for functors (mmcgr)
    • Added -l parameter for functor libraries and -L for functor library paths (mmcgr)
    • Added --interpreter[LVM|RAMI] parameter for interpreter choice (XiaowenHu96)
    • Improved code documentation (dcol97)
    • Refactoring for maintainability and readability (mmcgr)
    • Performance enhancements
    • Bug fixes
    Source code(tar.gz)
    Source code(zip)
    souffle-1.6.0.md5(36 bytes)
    souffle-1.6.0.pkg(2.57 MB)
    souffle_1.6.0-1_amd64.deb(1.25 MB)
    souffle_1.6.0-1_amd64.md5(36 bytes)
  • 1.5.0(Jan 18, 2019)

    • Rewritten code generation (taipan-snake)
    • Improved Provenance via generated data structures (taipan-snake)
    • Profile cpu & memory usage (mmcgr)
    • Enhanced profiler graphs (mmcgr)
    • Productivity measures in profiler (mmcgr)
    • General profiler enhancements (mmcgr)
    • Added support for non-x86 platforms (mmcgr)
    • Improve compilation speed (mmcgr)
    • Bash autocompletion (mmcgr)
    • Extended verbose mode (azreika/mmcgr)
    • Reorder atoms to optimise evaluation speed (azreika)
    • Profile-guided atom reordering (azreika)
    • Various AST optimisations (azreika)
    • User defined functors (b-scholz)
    • Bug fixes
    Source code(tar.gz)
    Source code(zip)
  • 1.4.0(Sep 4, 2018)

    • improved parallel performance (HerbertJordan)
    • improved operators hints in btree (HerbertJordan)
    • extended progress logging in verbose mode (mmcgr)
    • added to_string and to_number functors (b-scholz)
    • live profiler (mmcgr)
    • changed profile output format to json (mmcgr)
    • profile output is less indeterminate (mmcgr)
    • profiler tracks memory and cpu usage during execution (mmcgr)
    • profiler tracks load/store times (mmcgr)
    • multiple input directives (mmcgr)
    • handle failed input less terminally (mmcgr)
    • MPI engine (lyndonhenry)
    • Bug fixes
    Source code(tar.gz)
    Source code(zip)
    souffle-1.4.0.md5(36 bytes)
    souffle-1.4.0.pkg(1.94 MB)
    souffle_1.4.0-1_amd64.deb(968.52 KB)
    souffle_1.4.0-1_amd64.md5(36 bytes)
  • 1.3.1(May 28, 2018)

    • Added more feedback in verbose mode (azreika/mmcgr)
    • Fixed and enhanced 64 bit domain support (mmcgr/cfallin)
    • Improved debug report (azreika)
    • Enhanced profiler (atom frequency, bug fixes) (mmcgr)
    • Hashmap support (HerbertJordan,65linesofcode)
    • Enhanced provenance tools (taipan-snake)
    • Performance enhancements (azreika)
    • Bug fixes (mmcgr, azreika)
    • Fix parallel profiler logging
    Source code(tar.gz)
    Source code(zip)
    souffle-1.3.1.md5(36 bytes)
    souffle-1.3.1.pkg(1.78 MB)
    souffle_1.3.1-1_amd64.deb(987.24 KB)
    souffle_1.3.1-1_amd64.md5(36 bytes)
  • 1.3.0(May 24, 2018)

  • 1.2.0(Oct 4, 2017)

  • 1.1.0(Mar 30, 2017)

    • Configurable I/O System with more options and support for new language extensions (mmcgr).
    • Support of equivalence relation using union/find data-structures (pnappa)
    • New profiling tool rewritten in C++ with HTML/Javascript output (DominicRomanowski).
    • Replacing the Boost C-prepocessor wave by mcpp (pnappa)
    • Adding ternary functors (b-scholz)
    • JNI interface (psubotic)
    • Memory optimisations (lyndonhenry)
    • Numerous bug fixes.
    Source code(tar.gz)
    Source code(zip)
    souffle-1.1.0.md5(36 bytes)
    souffle-1.1.0.pkg(808.78 KB)
    souffle_1.1.0-1_amd64.deb(571.79 KB)
    souffle_1.1.0-1_amd64.md5(36 bytes)
Owner
The Soufflé Project
The Soufflé Project
weggli-native a "native" C API for Google's weggli

weggli-native a "native" C API for Google's weggli

Trail of Bits 3 Jul 13, 2022
A library in Rust for theorem proving with Intuitionistic Propositional Logic.

Prop Propositional logic with types in Rust. A library in Rust for theorem proving with Intuitionistic Propositional Logic. Supports theorem proving i

AdvancedResearch 48 Jan 3, 2023
Logimu: Circuit & logic gate simulator

Logimu: Circuit & logic gate simulator The main goal of Logimu is to simulate large circuits at a high speed. Features Live simulation Embed other cir

David Hoppenbrouwers 4 Nov 20, 2022
A Rust library that implements the main lightning logic of the lipa wallet app.

lipa-lightning-lib (3L) Warning This library is not production ready yet. Build Test Start Nigiri Bitcoin: nigiri start --ln The --ln flag is not stri

lipa 9 Dec 15, 2022
Propositional logic evaluator and rule-based pattern matcher

Plogic Propositional logic evaluator and pattern transformer written in Rust. Plogic evaluates logic expressions in a REPL (Read, Execute, Print, Loop

Jan 17 Nov 25, 2022
Implementation of the WebUSB specification in Rust.

Implementation of the WebUSB specification in Rust.

Divy Srivastava 38 Dec 4, 2022
This contract is to provide vesting account feature for the both cw20 and native tokens, which is controlled by a master address

Token Vesting This contract is to provide vesting account feature for the both cw20 and native tokens, which is controlled by a master address. Instan

yys 7 Oct 7, 2022
Extracting react native app source code from apk file.

extract-myreact Extracting React Native app source code from apk file.

Aan 3 Oct 5, 2022
Waits until the exit code of a program is zero

Waitz A rust utility to wait that a program exits with 0. You need to wait for something to start up and don't know when it finishes?

Max Strübing 15 Apr 10, 2022
A program written in pure Rust to query music info from mpd and display it in a notification.

musinfo A program written in pure Rust to query music info from mpd and display it in a notification. Note: Cover art is expected to be placed at /tmp

Cpt.Howdy 10 Aug 16, 2022
Wait Service is a pure rust program to test and wait on the availability of a service.

Wait Service Wait Service is a pure rust program to test and wait on the availability of a service.

Magic Len (Ron Li) 3 Jan 18, 2022
A program written in Rust, that allows the user to find the current location of the International Space Station and see it on a map.

ISS Location ViewFinder A program written in Rust, that allows the user to find the current location of the International Space Station and see it on

Suvaditya Mukherjee 2 Nov 8, 2021
✨ Safe, global singletons initialized at program start

✨ magic_static Safe, global singletons initialized at program start. Usage Simply add magic_static as a dependency in your Cargo.toml to get started:

William 5 Nov 8, 2022
Noir Pay - Fork of the Light Protocol Program for local testing / optimisation.

Noir Pay v0 Built on Light Protocol Noir Pay will be directly built ontop of the Light Protocol SDK and provide users with a beautifully simple privat

0xNico 1 Feb 12, 2022
Program a Raspberry Pi Pico with pure Rust

pi-pico-rs Program a Raspberry Pi Pico with pure Rust. Get Started Install the latest version of Rust and the thumbv6m-none-eabi target. This is the p

Gerald Nash 5 Jul 29, 2022
A simple program for handling Ethiopian calendar dates.

Mek’ut’erīya A simple program for handling Ethiopian calendar dates. Installation cargo install --git https://github.com/frectonz/mek-ut-er-ya If you

Fraol Lemecha 15 Dec 20, 2022
A bare metal STM32F103C8T6/STM32F103 MCU program written in pure Rust

A bare metal (register level) STM32F103C8T6/STM32F103 MCU program written in pure Rust without any IDE, SDK, HAL or library, and no assembly code, the only tool required is the Rust compiler.

Hema Shushu 105 Dec 18, 2022
Rust program to monitor Windows 10 Registry keys for changes or modifications.

RegMon This Rust program monitors changes to multiple registry keys in Windows 10 and writes the changes to a text file. It also periodically sends a

0x44F 3 Jan 16, 2023
A tool of generating and viewing dice roll success distributions.

AZDice A GUI tool for generating and visualising dice roll probability distributions. Aims Intended to help people trying to get game balance just rig

null 13 Mar 2, 2021