souffle egglog 2

README.md

Compile the library. I got the various build arguments from souffle-compile. You can also run this in interpreter mode.

../../souffle/build/src/souffle add2.dl -lunionfind -o out -j4
time ./out -j4

add.dl

#define NUM(x) as(x, number)
#define FIND(x) as(@findNode(NUM(x)), Id)
#define UFIND(x,y,z) as(@constfind(@unionNodes(NUM(x), NUM(y)), NUM(z)), Id)
.functor findNode(number):number 
.functor constfind(number,number):number // find second argument, ignores first
.functor unionNodes(number,number):number // performs union, returns 0
.type Id = Add {x : Id, y : Id}
         | Num {n : number}

.decl add(x : Id, y : Id, c : Id) btree_delete
.decl num(x : number, c : Id) // btree_delete

// comm-add
add(UFIND(xy, yx, x), FIND(y), FIND(xy)) :- add(y, x, yx),
 xy = $Add(FIND(x), FIND(y)).
// yx = $Add(FIND(y), $Add(FINDx))

// assoc-add
add(UFIND(xy_z, x_yz, xy), FIND(z), FIND(x_yz)),
add(FIND(x), FIND(y), FIND(xy))
:- // it's ludicrous this is the best way to do this.
add(y, z, yz1), add(x, yz, _x_yz), FIND(yz1) = FIND(yz),
//x_yz = $Add(x,$Add(y,z))),
//xy = $Add(FIND(x), FIND(y)), xy_z = $Add(FIND(xy), FIND(z)).
x_yz = FIND($Add(x,FIND($Add(y,z)))),
//x_yz = FIND($Add(x,FIND(yz))),
xy = $Add(FIND(x), FIND(y)), xy_z = $Add(FIND(xy), FIND(z)).

// congruence
add(UFIND(a,b,x), FIND(y), FIND(a)) :- add(x, y, a), add(x, y, b), a != b.

// num(n, FIND(a)) :- num(n, a), num(n, b), a != b.

// populate eql
//num(n, FIND(c)) :- num(n, c).
//add(FIND(x), FIND(y), FIND(z)) :- add(x,y,z).
//add(x,y,$Add(x,y)) :- add(x,y,_z).

// If there are bads, subsumption isn't strong enough?
add(x, y, z) <= add(FIND(x), FIND(y), FIND(z)) :- true.

// insert an expression 1 + 2 + 3
.decl add_prep(x : Id, y : Id, c : Id)
num(1, $Num(1)).
num(2, $Num(2)).
add_prep($Num(2), $Num(1), $Add($Num(2), $Num(1))).
add_prep($Num(x + 1), id, $Add($Num(x + 1), id)),
 num(x + 1, $Num(x + 1))
 :-
 add_prep($Num(x), _, id),
 x < 8.

add(x, y, c) :- add_prep(x, y, c).

// Summary statistics

// Count Enodes
.decl cnt(c : number)
cnt(c) :- c=count : { add(_, _, _) }.
.output cnt(IO=stdout)

// Equivalence classes
.decl eq(n : Id)
eq(x) :- add(x,_,_), x = FIND(x).
eq(y) :- add(_,y,_), y = FIND(y).
eq(z) :- add(_,_,z), z = FIND(z).

// unnormalized entries 
.decl bad(n : Id, y : Id)
bad(x, FIND(x)) :- add(x,_,_), x != FIND(x).
bad(y, FIND(y)) :- add(_,y,_), y != FIND(y).
bad(z, FIND(z)) :- add(_,_,z), z != FIND(z).
.output bad

.decl cbad(c : number) 
cbad(c) :- c=count : { bad(_,_) }.
.output cbad(IO=stdout)

.decl ceq(c : number) 
ceq(c) :- c=count : { eq(_) }.
.output ceq(IO=stdout)

compile.sh

/usr/bin/c++ -march=native -fopenmp -O3 -DUSE_NCURSES -DUSE_LIBZ -DUSE_SQLITE -fopenmp \
    -std=c++17 -o unionlib.o -c -fPIC unionlib.cpp \
    -I../../souffle/build/src/../include -I../../souffle/build/src/include \
    -I../../souffle/build/src/../include/souffle/swig -I../../souffle/build/src/include/souffle/swig \
    -I/home/philip/Documents/prolog/souffle/src/include
g++ -shared -o libunionfind.so unionlib.o 

unionlib.cpp

#include <cstdint>
#include "souffle/CompiledSouffle.h"
#include "souffle/datastructure/UnionFind.h"



extern "C" {

souffle::SparseDisjointSet<int32_t> ds = souffle::SparseDisjointSet<int32_t>(); 

int32_t unionNodes(int32_t x, int32_t y){
    ds.unionNodes(x,y);
    return 0;
}
int32_t findNode(int32_t x){
    return ds.findNode(x);
}
int32_t constfind(int32_t x, int32_t y){
    return ds.findNode(y);
}

}