souffle 语法

概述:

souffle 中的主要语言元素是关系声明（relations）、事实(facts)、规则（rurle）、指令(instruction)。

关系（relations）：

关系是一组有序元组（x1,…Xk）,其中每个元素xi是由属性类型表示的数据域的成员。

1

.decl A(x:number, y:number)

上式定义了A包含数对的关系。第一个属性被命名为x, 第二个属性被命名为y。属性具有由标识符指定的类型，标识符跟在属性后面的冒号后。在上式中，x和y都是number类型。souflfle的类型检查器将会使用关系的属性来推断变量的类型。

类型（types）:

Souffle 包含四种原始类型：

  • 符号类型：symbol
  • 数字类型：number
  • 无符号类型：unsigned
  • 浮点数类型：float
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

.decl Name(n: symbol)
Name("Hans").
Name("Gretl").

.decl Translate(n: symbol , o: number)
.output Translate
Translate(x,ord(x)) :- Name(x).

.decl Magic(x:number, y:unsigned, z:float)
Magic(-1,1,2.718).
.output Magic

事件（facts）:

事件是无条件成立的条款；它们是有规则头，但是没有规则体。

1
2
3
4

.decl A(x:number, y:number)  // declaration of relation A
A(1,2).                      // facts of relation A
A(2,3).
.output A

关系A有两个事件：A(1,2). 和 A(2,3).

注：事件可以使用输入指令（.input）进行加载。

规则（rules）:

规则是一个子句，它有一个谓词作为头部，一个或者多个文字在主体中。文字可以是谓词，否定谓词或约束。

1
2
3
4
5
6
7
8
9

.decl edge(x:number, y:number)
edge(1,2).
edge(2,3).

.decl path(x:number, y:number)
.output path

path(x, y) :- edge(x, y). // 规则（约束）
path(x, y) :- path(x, z), edge(z, y).

示例

代码示例

1
2
3
4
5
6
7
8
9

.decl edge(x:number, y:number)
edge(1,2).
edge(2,3).

.decl path(x:number, y:number)
.output path

path(x, y) :- edge(x, y).
path(x, y) :- path(x, z), edge(z, y).

以上的规则为：如果存在表x,y 即 edge(x,y) ,则可以推导出path(x,y) ; 如果存在边edge(z, y)和路径path(x, z) 那么就存在路径path(x,y).

输出结果

1
2
3

1       2
1       3
2       3

解析

  1. A(1, 2) => B(1, 2); A(2, 3) => B(2, 3)
  2. A(1, 2) , B(2, 3) => B(1, 3)

综上可得：B(1, 2) B(2, 3) B(1, 3)