search

souffle-lang / souffle

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.
http://souffle-lang.github.io/
Universal Permissive License v1.0
916 stars 207 forks source link

Incorrect results with the synthesiser #1578

Closed tytus-metrycki closed 4 years ago

tytus-metrycki commented 4 years ago

I believe that the following program produces correct results with the interpreter, but incorrect when the synthesizer is used.

Program

.type Tree = [x: number, y: TreeX]
.type TreeX = [x: Tree, y: unsigned, z: Tree]

.decl TreeHeight(t:Tree, height:unsigned) 
TreeHeight([0,[nil, 0, nil]],0).
TreeHeight([1,[left,(h+1),right]], (h+1)) :- 
   TreeHeight(left,h),
   TreeHeight(right,h),
   h < 1.
.output TreeHeight(IO="stdout")

Interpreter (correct result)

---------------
TreeHeight
===============
[0, [nil, 0, nil]]  0
[1, [[0, [nil, 0, nil]], 1, [0, [nil, 0, nil]]]]    1
===============

Synthesiser (incorrect result)

---------------
TreeHeight
===============
[0, [nil, 0, nil]]  0
===============
tytus-metrycki commented 4 years ago

The example can be further simplified to

.type Tree = [x: number, y: TreeX]
.type TreeX = [x: Tree, y: unsigned, z: Tree]

.decl TreeHeight(t:Tree, height:unsigned) 
TreeHeight([0,[nil, 0, nil]],0).
TreeHeight([1,[left,1,right]], 1) :- 
   TreeHeight(left,0),
   TreeHeight(right,0).
.output TreeHeight(IO="stdout")
SamArch27 commented 4 years ago

Hey @darth-tytus!

I've simplified it down to:

.decl TreeHeight(x:number, height:unsigned)
TreeHeight(0,0).
TreeHeight(1,1) :-
   TreeHeight(left,0).
.output TreeHeight(IO="stdout")