Skip to content

souffle-lang/souffle-lib

Repository files navigation

C libraries for Souffle

Introduction

Souffle is a capable Datalog implementation which allows for relatively easy integration with C functions. This library defines a set of functors for using some of the C math and datetime (timestamp) functions in Souffle.

By default, Souffle is compiled with C int32_t and float for the number and float types, respectively. Souffle can also be configures to use int64_t and double for those types by using ./configure --enable-64bit-domain. We have used autoconf and configure to allow for these differences.

Setup

The setup of the library may be as simple as:

make clean && make
configure: creating ./config.status
config.status: creating math.dl
configure: creating ./config.status
config.status: creating math.dl
config.status: creating test.dl
configure: creating ./config.status
config.status: creating math.dl
config.status: creating test.dl
config.status: creating datetime.cpp
g++ -shared -fPIC datetime.cpp -o libfunctors.so

In the following examples, we have used test examples that are in the same directory as the library files and assume that there is no other libfunctors.so or libfunctors.dylib file. For using the library from another folder, you may need to change:

  1. The -L argument to be the library directory to use the datetime functions.
  2. The paths for the included souffle-lib library Datalog files.
  3. If you have your own compiled shared library that is also called libfunctors.so or or libfunctors.dylib, then you will need to rename one of the shared libraries and use the -l argument.

Math functions

The C99 math function names differ for float and double arguments. We have provided for each in math_32.dl and math_64.dl, respectively. These files provide documentation on the calls (which call the C functions of the same names). We have also provided the math.dl file, which is configured to switch between math_32.dl and math_64.dl.

As a simple example and assuming a 64-bit configuration, we have the following Souffle test_64.dl file (we could also have used the test.dl file, which is configured to switch between test_32.dl and test_64.dl):

#include "math_64.dl"

.decl Summary(label: symbol, y: float)
Summary("to_float(\"NaN\")", to_float("NaN")) :- true.
Summary("@exp(NaN)", @exp(to_float("NaN"))) :- true.
Summary("@exp(1.0)", @exp(1.0)) :- true.
Summary("@log(@exp(1.0))", @log(@exp(1.0))) :- true.
.output Summary

This reads in the functor definitions, declares a Summary relationship, and calculates some values. The code to run this in the interpreter may be as simple as souffle -lm test_64.dl or in the compiler using souffle -c -lm test_64.dl. However, when libm is an ld script, this code will not work for the Souffle interpreter. To address this case, we have provided a bash script lib_ldscript for transforming the library arguments when there is an ld script. As an example:

souffle -D- `lib_ldscript -lm` test_64.dl
---------------
Summary
label	y
===============
to_float(\"NaN\")	-0
@exp(NaN)	1
@exp(1.0)	2.7182818284590451
@log(@exp(1.0))	1
===============

As a reminder, the -D- argument sends the output values to stdout rather than to files.

Datetime (timestamps)

This library also defines a small set of functors for using some of the C date-time functions. Documentation is available in the datetime.dl file. Note that the datetime.cpp file has been configured to use either int32_t or int64_t integer types. As a simple example, we have the following Souffle test_datetime.dl file:

#include "datetime.dl"

.decl Times(timestamp:timestamp)
.decl Test(operator:symbol, timestamp:timestamp, result:symbol)

Times(@from_date("1970-01-01")) :- true.
Times(@from_date_time("1970-01-02 00:00:00")) :- true.
Times(@to_timestamp("03/01/1970", "%d/%m/%Y")) :- true.
Times(@localtimestamp()) :- true.
Times(@from_date("")) :- true.

Test("@to_days	", timestamp, to_string(@to_days(timestamp))) :- Times(timestamp).
Test("@to_date", timestamp, @to_date(timestamp)) :- Times(timestamp).
Test("@to_date_time", timestamp, @to_date_time(timestamp)) :- Times(timestamp).
Test("@from_timestamp", timestamp, @from_timestamp(timestamp,"%d/%m/%Y")) :- Times(timestamp).
Test("@age	", timestamp1, to_string(@age(timestamp1,timestamp2))) :-
    Times(timestamp1), Times(timestamp2), timestamp1>timestamp2.

.output Test

This reads in the functor definitions, declares relationships for times and test results, and calculates test results for each of the times. The code to run this in the interpreter is souffle test.dl or, in the compiler, souffle -c test.dl. As an example:

souffle -D- test_datetime.dl