Merge pull request #2216 from b-scholz/subsumption_example

Subsumption Example

tests/interface/CMakeLists.txt

@@ -7,6 +7,7 @@
 # Make sure that the functor library is built
 add_subdirectory(functors)
 add_subdirectory(graph_coloring)
+add_subdirectory(pathseq)
 
 # swig test which will run python, java or both
 function(SOUFFLE_POSITIVE_FUNCTOR_TEST TEST_NAME)
@@ -153,6 +154,7 @@ function(SOUFFLE_POSITIVE_CPP_TEST TEST_NAME)
 endfunction()
 
 souffle_positive_functor_test(functors CATEGORY interface)
+souffle_positive_functor_test(pathseq CATEGORY interface)
 souffle_positive_functor_test(graph_coloring CATEGORY interface)
 souffle_positive_cpp_test(contain_insert)
 souffle_positive_cpp_test(get_symboltabletype)

tests/interface/pathseq/CMakeLists.txt

@@ -0,0 +1,35 @@
+# Souffle - A Datalog Compiler
+# Copyright (c) 2022 The Souffle Developers. All rights reserved
+# Licensed under the Universal Permissive License v 1.0 as shown at:
+# - https://opensource.org/licenses/UPL
+# - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+add_library(psfunctors SHARED functors.cpp)
+target_include_directories(psfunctors PRIVATE "${CMAKE_SOURCE_DIR}/src/include")
+
+target_compile_features(psfunctors
+                        PUBLIC cxx_std_17)
+
+set_target_properties(psfunctors PROPERTIES CXX_EXTENSIONS OFF)
+set_target_properties(psfunctors PROPERTIES OUTPUT_NAME "functors")
+set_target_properties(psfunctors PROPERTIES WINDOWS_EXPORT_ALL_SYMBOLS ON)
+
+if (NOT MSVC)
+target_compile_options(psfunctors
+                       PUBLIC "-Wall;-Wextra;-Werror;-fwrapv")
+else ()
+  target_compile_options(psfunctors PUBLIC /W3 /WX)
+endif()
+
+if (WIN32)
+  # Prefix all shared libraries with 'lib'.
+  set(CMAKE_SHARED_LIBRARY_PREFIX "lib")
+
+  # Prefix all static libraries with 'lib'.
+  set(CMAKE_STATIC_LIBRARY_PREFIX "lib")
+endif ()
+
+if (SOUFFLE_DOMAIN_64BIT)
+    target_compile_definitions(psfunctors
+                               PUBLIC RAM_DOMAIN_SIZE=64)
+endif()

tests/interface/pathseq/Path.csv

@@ -0,0 +1,26 @@
+n1	n1	[n1, [n2, [n4, [n1, nil]]]]
+n1	n1	[n1, [n3, [n4, [n1, nil]]]]
+n1	n2	[n1, [n2, nil]]
+n1	n3	[n1, [n3, nil]]
+n1	n4	[n1, [n2, [n4, nil]]]
+n1	n4	[n1, [n3, [n4, nil]]]
+n1	n5	[n1, [n2, [n4, [n5, nil]]]]
+n1	n5	[n1, [n3, [n4, [n5, nil]]]]
+n2	n1	[n2, [n4, [n1, nil]]]
+n2	n2	[n2, [n4, [n1, [n2, nil]]]]
+n2	n3	[n2, [n4, [n1, [n3, nil]]]]
+n2	n4	[n2, [n4, nil]]
+n2	n4	[n2, [n4, [n1, [n3, [n4, nil]]]]]
+n2	n5	[n2, [n4, [n5, nil]]]
+n3	n1	[n3, [n4, [n1, nil]]]
+n3	n2	[n3, [n4, [n1, [n2, nil]]]]
+n3	n3	[n3, [n4, [n1, [n3, nil]]]]
+n3	n4	[n3, [n4, nil]]
+n3	n4	[n3, [n4, [n1, [n2, [n4, nil]]]]]
+n3	n5	[n3, [n4, [n5, nil]]]
+n4	n1	[n4, [n1, nil]]
+n4	n2	[n4, [n1, [n2, nil]]]
+n4	n3	[n4, [n1, [n3, nil]]]
+n4	n4	[n4, [n1, [n2, [n4, nil]]]]
+n4	n4	[n4, [n1, [n3, [n4, nil]]]]
+n4	n5	[n4, [n5, nil]]

tests/interface/pathseq/functors.cpp

@@ -0,0 +1,57 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2022, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file functors.cpp
+ *
+ * Implementing a sub-list/prefix check for a list
+ *
+ ***********************************************************************/
+
+#include "souffle/RecordTable.h"
+#include "souffle/SymbolTable.h"
+#include <cassert>
+#include <stack>
+
+extern "C" {
+
+souffle::RamDomain isSubsequence([[maybe_unused]] souffle::SymbolTable* symbolTable,
+        souffle::RecordTable* recordTable, souffle::RamDomain arg1, souffle::RamDomain arg2) {
+    assert(symbolTable && "NULL symbol table");
+    assert(recordTable && "NULL record table");
+
+    std::stack<souffle::RamDomain> stack1, stack2;
+
+    // unwind first node-sequence onto stack1
+    while (arg1 != 0) {
+        const souffle::RamDomain* t = recordTable->unpack(arg1, 2);
+        stack1.push(t[0]);
+        arg1 = t[1];
+    }
+
+    // unwind second node-sequence onto stack2
+    while (arg2 != 0) {
+        const souffle::RamDomain* t = recordTable->unpack(arg2, 2);
+        stack2.push(t[0]);
+        arg2 = t[1];
+    }
+
+    // prefix check
+    while (!stack1.empty() && !stack2.empty()) {
+        auto x = stack1.top(), y = stack2.top();
+        if (x != y) {
+            return 0;
+        }
+        stack1.pop();
+        stack2.pop();
+    }
+    return stack1.empty();
+}
+
+}  // end of extern "C"

tests/interface/pathseq/pathseq.dl

@@ -0,0 +1,58 @@
+// Souffle - A Datalog Compiler
+// Copyright (c) 2022, The Souffle Developers. All rights reserved
+// Licensed under the Universal Permissive License v 1.0 as shown at:
+// - https://opensource.org/licenses/UPL
+// - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+
+//
+// Compute set of acyclic paths using subsumption
+//
+// See Example 2, Fixpoint Iteration with Subsumption in
+// Deductive Databases by G. Koestler et al.,
+// J. of Intelligent Information Systems,
+// 4, 123-148 (1995).
+//
+
+.type node <: symbol
+
+.type node_sequence = [x:node, p:node_sequence]
+
+.functor isSubsequence(node_sequence, node_sequence):number stateful
+
+//
+// Edge set of a directed graph
+//
+.decl Edge(x:node, y:node)
+
+Edge("n1","n2").
+Edge("n1","n3").
+Edge("n2","n4").
+Edge("n3","n4").
+Edge("n4","n1").
+Edge("n4","n5").
+
+//
+// Set of path sequences between node x and y represented as a
+// sequence of nodes of a given length.
+//
+
+.decl Path(x:node, y:node, seq:node_sequence)
+
+// Base case
+Path(x,y,[x,[y,nil]]) :-
+  Edge(x, y).
+
+// Inductive case
+Path(x,z,[x,s]) :-
+  Edge(x,y),
+  Path(y,z,s).
+
+// If the node-sequence of path s1 is a prefix of a
+// node-sequence of path s2, the path of
+// node-sequence s2 subsumes the path of
+// node sequence s1.
+Path(x, y, s1) <= Path (x, y, s2) :-
+ @isSubsequence(s2,s1) = 1.
+
+.output Path