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
903 stars 198 forks source link

ADTs with negation #2448

Closed gilbert closed 9 months ago

gilbert commented 9 months ago

Hi, relatively new to Datalog here. I'm trying to write a rule that "collapses" a specific branch when the rule encounters it.

However, when I try to use negation to match the rest of the cases, I get Error: Ungrounded ADT branch. Is there a way to do this without pattern matching every other case manually, or am I taking the wrong approach? Thank you!

.type MyType
  = A { id: symbol }
  | B { id: symbol }
  | C { id: symbol }
  | D { id: symbol }

.decl foo(n: number, mytype: MyType)
// Definition omitted; working properly

.decl bar(n: number, mytype: MyType)

bar(n, mtype) :-
  foo(n, $A(id)),
  foo(n+1, mtype).

bar(n, mtype) :-
  foo(n, mtype),
  mtype != $A(_).  // Error occurs here
quentin commented 9 months ago

Duplicate of #2315 Hi, the question is discussed in the issue above.

gilbert commented 9 months ago

My search was not as thorough as I thought it was. Thanks!