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
929 stars 208 forks source link

Issue with `brie` in compiler mode? #2300

Open bertram-gil opened 2 years ago

bertram-gil commented 2 years ago

Hi guys,

Consider the following program:

.decl neg_float(x: float)
.decl a__(a:symbol, b:symbol) 
.decl b__(a:symbol, b:symbol, c:symbol) 
.decl d__(a:number, b:symbol) 
.decl f__(a:number, b:number, c:symbol)
.decl g__(a:number, b:number, c:symbol) 
.decl h__(a:float, b:float) 
.decl i__(a:number, b:number) 
.decl k__(a:number, b:float, c:float) brie
.decl l__(a:number, b:number, c:float) 
.output l__

a__("cn", "xi").
a__("on", "hq").
b__("uv", "yn", "ez").
b__("lg", "oz", "qt").
b__("ng", "oz", "xi").
b__("io", "bs", "oi").
d__(97, "yj").
d__(61, "fs").
d__(47, "on").
g__(86, 86, "tb").
g__(34, 10, "zj").
g__(48, 22, "th").
g__(64, 92, "cc").
i__(63, 7).
i__(9, 52).
i__(48, 24).
i__(5, 18).

neg_float(3.0).
neg_float(-3.5).
neg_float(-x) :- neg_float(x).
h__(a, a) :- neg_float(a).
i__(a, a) :- d__(a, b).
k__(e, b, b) :- h__(b, b), i__(f, d), i__(e, e).
l__(j, j, m) :- b__(c, f, b), f__(d, p, b), f__(d, h, i), g__(e, j, c), h__(m, m).

Running the above program in compiler mode (-c) returns nothing for the relation l__.

$ /souffle/src/souffle -w -c prog.dl && cat l__.csv

Adding a rule l__(a, a, b) :- k__(a, b, c), !k__(a, b, c). should not change the result in l__, but if I run the following program:

.decl neg_float(x: float)
.decl a__(a:symbol, b:symbol) 
.decl b__(a:symbol, b:symbol, c:symbol) 
.decl d__(a:number, b:symbol) 
.decl f__(a:number, b:number, c:symbol)
.decl g__(a:number, b:number, c:symbol) 
.decl h__(a:float, b:float) 
.decl i__(a:number, b:number) 
.decl k__(a:number, b:float, c:float) brie
.decl l__(a:number, b:number, c:float) 
.output l__

a__("cn", "xi").
a__("on", "hq").
b__("uv", "yn", "ez").
b__("lg", "oz", "qt").
b__("ng", "oz", "xi").
b__("io", "bs", "oi").
d__(97, "yj").
d__(61, "fs").
d__(47, "on").
g__(86, 86, "tb").
g__(34, 10, "zj").
g__(48, 22, "th").
g__(64, 92, "cc").
i__(63, 7).
i__(9, 52).
i__(48, 24).
i__(5, 18).

neg_float(3.0).
neg_float(-3.5).
neg_float(-x) :- neg_float(x).
h__(a, a) :- neg_float(a).
i__(a, a) :- d__(a, b).
k__(e, b, b) :- h__(b, b), i__(f, d), i__(e, e).
l__(j, j, m) :- b__(c, f, b), f__(d, p, b), f__(d, h, i), g__(e, j, c), h__(m, m).
l__(a, a, b) :- k__(a, b, c), !k__(a, b, c).

I get:

$ /souffle/src/souffle -w -c prog.dl && cat l__.csv
47  47  -3.5
47  47  -3
61  61  -3.5
61  61  -3
97  97  -3.5
97  97  -3

Note that in interpreter mode, I get an empty result for both programs. I also get an empty result for both programs both in compiler and interpreter mode if I remove brie for the relation k__.

Souffle version I am using: 66b96fd07e7124d0e46bcf7cdc1cc5bf61f54cc3

Please let me know if this is a bug or am I doing something wrong.

b-scholz commented 2 years ago

This is most likely related to Brie data-structure issues. Are you using 32bit or 64Bit as a word size?

bertram-gil commented 2 years ago

My machine specs:

 Operating System: Debian GNU/Linux 10 (buster) 
 Kernel: Linux 5.10.126.1.amd64-smp
 Architecture: x86-64
b-scholz commented 2 years ago

Brie uses bitwise comparison and not floating point comparison. There have been several issues related to this bug. However, it is the same bug. E.g., #2311

Alternatively, there could be a bug in the 64bit version of brie that is still not fixed (but you are using 32bit - so this should not happen).

mingodad commented 2 years ago

Would be nice to have the word size be shown on the help screen, something like:

souffle --help
============================================================================
souffle -- A datalog engine.
Usage: souffle [OPTION] FILE.
----------------------------------------------------------------------------
...
----------------------------------------------------------------------------
Version: 2.3-137-gf2f974194 word-size: 32bits float: 32bits  ///!!!! notice here the extra info
----------------------------------------------------------------------------
Copyright (c) 2016-22 The Souffle Developers.
Copyright (c) 2013-16 Oracle and/or its affiliates.
All rights reserved.
============================================================================
mingodad commented 2 years ago

With this small change we can have the word size on the help screen:

diff --git a/src/main.cpp b/src/main.cpp
index e704fd452..e2e072a06 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -412,7 +412,8 @@ int main(int argc, char** argv) {

         std::stringstream footer;
         footer << "----------------------------------------------------------------------------" << std::endl;
-        footer << "Version: " << PACKAGE_VERSION << "" << std::endl;
+        footer << "Version: " << PACKAGE_VERSION << std::endl;
+        footer << "Word size: " << RAM_DOMAIN_SIZE << " bits" << std::endl;
         footer << "----------------------------------------------------------------------------" << std::endl;
         footer << "Copyright (c) 2016-22 The Souffle Developers." << std::endl;
         footer << "Copyright (c) 2013-16 Oracle and/or its affiliates." << std::endl;

Output:

...
----------------------------------------------------------------------------
Version: 2.3-137-gf2f974194
Word size: 32 bits
----------------------------------------------------------------------------
Copyright (c) 2016-22 The Souffle Developers.
Copyright (c) 2013-16 Oracle and/or its affiliates.
All rights reserved.
============================================================================
b-scholz commented 2 years ago

Can you prepare a pull-request for this?