fix ungrounded error when destructuring with don't-cares (#2483)

fix ungrounded error when destructuring with don't-cares

Name unnamed variables that appear in record and branch
inits before the resolution of aliases.

fix #2482

After the `ResolveAliasesTransformer`, all  occurences of `t` are replaced with `[ta,_]`, and the groundedness constraint system cannot give a bounded value to `[ta,_]` in the head (`var([ta,_])->0` in the `Solution`).

```
Clause: pred([ta,_],ta) :-
   fact([ta,_]).
Problem:
{
        var([ta,_]) ⇒ var(ta),
        var([ta,_]) ⇒ var(_),
        var(ta) ∧ var(_) ⇒ var([ta,_]),
        var([ta,_]) is true,
        var([ta,_]) ⇒ var(ta),
        var([ta,_]) ⇒ var(_),
        var(ta) ∧ var(_) ⇒ var([ta,_])
}
Solution:
{var(_)->1,var(_)->0,var([ta,_])->1,var([ta,_])->0,var(ta)->1}
```

When you provide an explicit variable for the second part of the record, the constraint system can be solved because the second member of the record has is bound by the variable (`var(_fix)->1` and `var([ta,_fix])->1`):

```
Clause: pred([ta,_fix],ta) :-
   fact([ta,_fix]).
Problem:
{
        var([ta,_fix]) ⇒ var(ta),
        var([ta,_fix]) ⇒ var(_fix),
        var(ta) ∧ var(_fix) ⇒ var([ta,_fix]),
        var([ta,_fix]) is true,
        var([ta,_fix]) ⇒ var(ta),
        var([ta,_fix]) ⇒ var(_fix),
        var(ta) ∧ var(_fix) ⇒ var([ta,_fix])
}
Solution:
{var([ta,_fix])->1,var([ta,_fix])->1,var(ta)->1,var(_fix)->1}
```

To fix this, we need to transform `_` into unique variables before the `ResolveAliasesTransformer`.

src/ast/transform/ResolveAliases.cpp

@@ -34,6 +34,7 @@
 #include "souffle/BinaryConstraintOps.h"
 #include "souffle/utility/FunctionalUtil.h"
 #include "souffle/utility/MiscUtil.h"
+#include "souffle/utility/NodeMapper.h"
 #include "souffle/utility/StreamUtil.h"
 #include "souffle/utility/StringUtil.h"
 #include <algorithm>
@@ -200,6 +201,27 @@ class Equation {
     }
 };
 
+bool nameUnnamedInit(Clause& clause) {
+    int varid = 0;
+    bool changed = false;
+
+    auto namer = nodeMapper<ast::Node>([&](auto&& self, Own<Node> node) -> Own<ast::Node> {
+        if (const auto* unnamed = as<ast::UnnamedVariable>(node)) {
+            changed = true;
+            varid += 1;
+            return mk<ast::Variable>("_<unnamed_" + std::to_string(varid) + ">", unnamed->getSrcLoc());
+        } else {
+            node->apply(self);
+            return node;
+        }
+    });
+
+    visit(clause, [&](RecordInit& rec) { rec.apply(namer); });
+    visit(clause, [&](BranchInit& adt) { adt.apply(namer); });
+
+    return changed;
+}
+
 }  // namespace
 
 Own<Clause> ResolveAliasesTransformer::resolveAliases(const Clause& clause) {
@@ -498,7 +520,7 @@ bool ResolveAliasesTransformer::transform(TranslationUnit& translationUnit) {
     Program& program = translationUnit.getProgram();
 
     // get all clauses
-    std::vector<const Clause*> clauses;
+    std::vector<Clause*> clauses;
     visit(program, [&](const Relation& rel) {
         const auto& qualifiers = rel.getQualifiers();
         // Don't resolve clauses of inlined relations
@@ -510,7 +532,12 @@ bool ResolveAliasesTransformer::transform(TranslationUnit& translationUnit) {
     });
 
     // clean all clauses
-    for (const Clause* clause : clauses) {
+    for (Clause* clause : clauses) {
+        // -- Step 0 --
+        // Name unnamed variables in record and branch inits (souffle-lang/souffle#2482)
+        // This is fine as long as this transformer runs after the semantics checker
+        changed |= nameUnnamedInit(*clause);
+
         // -- Step 1 --
         // get rid of aliases
         Own<Clause> noAlias = resolveAliases(*clause);

tests/semantic/CMakeLists.txt

@@ -274,3 +274,4 @@ positive_test(issue1896)
 positive_test(comp_params)
 positive_test(issue2416)
 positive_test(agg_range)
+positive_test(issue2482)

tests/semantic/issue2482/case_adt.csv

@@ -0,0 +1,2 @@
+$Some(abc, xyz)	some
+$None	none

tests/semantic/issue2482/issue2482.dl

@@ -0,0 +1,30 @@
+.type Rec = [a: symbol, b: symbol]
+.type Adt = Some{a:symbol, b:symbol} | None{}
+
+.decl fact_rec(t:Rec)
+fact_rec(["abc", "xyz"]).
+
+.decl pred_rec(t:Rec, ta:symbol)
+pred_rec(t, ta) :-
+  fact_rec(t),
+  t=[ta, _].
+
+.decl fact_adt(t:Adt)
+fact_adt($Some("abc", "xyz")).
+fact_adt($None()).
+
+.decl pred_adt(t:Adt, ta:symbol)
+pred_adt(t, ta) :-
+  fact_adt(t),
+  t = $Some(ta, _).
+
+.decl case_adt(t:Adt, case:symbol)
+case_adt(t, case) :-
+  fact_adt(t),
+  ( t = $Some(_,_), case = "some"
+  ; t = $None(), case= "none"
+  ).
+
+.output pred_rec()
+.output pred_adt()
+.output case_adt()

tests/semantic/issue2482/pred_adt.csv

@@ -0,0 +1 @@
+$Some(abc, xyz)	abc

tests/semantic/issue2482/pred_rec.csv

@@ -0,0 +1 @@
+[abc, xyz]	abc