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

Assertion error in ast2ram: "variable not grounded" (functor example) #2474

Open aaronbembenek opened 8 months ago

aaronbembenek commented 8 months ago

I tried this program

root@d769dccd107c:~# cat broken.dl
.type Pair = [x:number, y:number]
.functor mypair():Pair stateful

.decl P(x:number, y:number)
P(x, y) :- [x, y] = @mypair().
.output P

and got this assertion error:

root@d769dccd107c:~# souffle broken.dl
souffle: /root/souffle-mirror/src/ast2ram/seminaive/ValueTranslator.cpp:48: virtual souffle::Own<souffle::ram::Expression> souffle::ast2ram::seminaive::ValueTranslator::visit_(souffle::type_identity<souffle::ast::Variable>, const souffle::ast::Variable&): Assertion `index.isDefined(var.getName()) && "variable not grounded"' failed.
Aborted

I used the most recent version of Souffle:

root@d769dccd107c:~# souffle --version
----------------------------------------------------------------------------
Version: 2.4.1-19-gd8049888d
Word size: 32 bits
Options enabled: ffi openmp ncurses sqlite zlib
----------------------------------------------------------------------------
Copyright (c) 2016-22 The Souffle Developers.
Copyright (c) 2013-16 Oracle and/or its affiliates.
All rights reserved.
============================================================================

This might be the same underlying issue as #2213.

Unlike #2294 and #2318, there are no explicit inline qualifiers in this example.

quentin commented 8 months ago

Hi, It is a current limitation of Soufflé: ADT and record values returned by a user-defined functor cannot get destructed into sub-parts. The semantics checker does not catch this limitation and eventually you get this assertion error.

Alternatively you can do this:

.decl Q(p:Pair)
Q(p) :- p = @mypair().
P(x,y) :- Q([x,y]).

I have a fix that is part of an ongoing work, although I cannot tell yet when it will land in master.

aaronbembenek commented 8 months ago

Thanks for your response! I will work around it for now :)