Quick fix: Prohibit negated variables from being guarded by aggregate…

…d variables

src/main/scala/datalog/execution/JoinIndexes.scala

@@ -36,6 +36,7 @@ case class GroupingJoinIndexes(varIndexes: Seq[Seq[Int]],
  * @param edb - for rules that have EDBs defined on the same predicate, just read
  * @param atoms - the original atoms from the DSL
  * @param cxns - convenience data structure tracking how many variables in common each atom has with every other atom.
+ * @param negationInfo - information needed to build the complement relation of negated atoms: for each term, either a constant or a list of pairs (relationid, column) of the ocurrences of the variable in the rule (empty for anonynous variable)
  */
 case class JoinIndexes(varIndexes: Seq[Seq[Int]],
                        constIndexes: mutable.Map[Int, Constant],
@@ -92,23 +93,19 @@ object JoinIndexes {
         case _ => if (a.negated) PredicateType.NEGATED else PredicateType.POSITIVE
       , a.rId))
 
-    val typeHelper = body.flatMap(a => a.terms.map(* => !a.negated))
-
     val bodyVars = body
-      .flatMap(a => a.terms)      // all terms in one seq
+      .flatMap(a => a.terms.zipWithIndex.map((t, i) => (t, (a.negated, a.isInstanceOf[GroupingAtom] && i >= a.asInstanceOf[GroupingAtom].gv.length))))  // all terms in one seq
       .zipWithIndex               // term, position
-      .groupBy(z => z._1)         // group by term
+      .groupBy(z => z._1._1)      // group by term
       .filter((term, matches) =>  // matches = Seq[(var, pos1), (var, pos2), ...]
         term match {
           case v: Variable =>
-            matches.map(_._2).find(typeHelper) match
-              case Some(pos) =>
-                variables(v) = pos
-              case None =>
-                if (v.oid != -1)
-                  throw new Exception(s"Variable with varId ${v.oid} appears only in negated rules")
-                else
-                  ()
+            val wrong = v.oid != -1 && matches.exists(_._1._2._1) && matches.forall(x => x._1._2._1 || x._1._2._2)  // Var occurs negated and all occurrences are either negated or aggregated
+            if wrong then
+              throw new Exception(s"Variable with varId ${v.oid} appears only in negated atoms (and possibly in aggregated positions of grouping atoms)")
+            else
+              if (v.oid != -1)
+                variables(v) = matches.find(!_._1._2._1).get._2
             !v.anon && matches.length >= 2
           case c: Constant =>
             matches.foreach((_, idx) => constants(idx) = c)
@@ -147,7 +144,9 @@ object JoinIndexes {
     )
 
 
-    val variables2 = body.filterNot(_.negated).flatMap(a => a.terms.zipWithIndex.collect{ case (v: Variable, i) if !v.anon => (v, i) }.map((v, i) => (v, (a.rId, i)))).groupBy(_._1).view.mapValues(_.map(_._2))
+    val variables2 = body.filterNot(_.negated).flatMap(a =>
+      a.terms.zipWithIndex.collect{ case (v: Variable, i) if !v.anon => (v, i) }.map((v, i) => (v, (a.rId, i)))
+    ).groupBy(_._1).view.mapValues(_.map(_._2))
 
     val negationInfo = body.filter(_.negated).map(a =>
       a.hash -> a.terms.map{

src/test/scala/test/StratifiedNegationTests.scala

@@ -1,6 +1,6 @@
 package test
 
-import datalog.dsl.{Constant, Program, __, not}
+import datalog.dsl.{Constant, Program, __, not, groupBy, AggOp}
 import datalog.execution.*
 import datalog.storage.DefaultStorageManager
 
@@ -18,7 +18,7 @@ class StratifiedNegationTests extends munit.FunSuite {
     t(x, y) :- e(x, y)
     t(x, z) :- (t(x, y), e(y, z))
 
-    interceptMessage[java.lang.Exception]("Variable with varId 0 appears only in negated rules") {
+    interceptMessage[java.lang.Exception]("Variable with varId 0 appears only in negated atoms (and possibly in aggregated positions of grouping atoms)") {
       tc(x, y) :- not(t(x, y)) // x and y are not limited.
     }
   }
@@ -35,7 +35,7 @@ class StratifiedNegationTests extends munit.FunSuite {
     t(x, y) :- e(x, y)
     t(x, z) :- (t(x, y), e(y, z))
 
-    interceptMessage[java.lang.Exception]("Variable with varId 2 appears only in negated rules") {
+    interceptMessage[java.lang.Exception]("Variable with varId 2 appears only in negated atoms (and possibly in aggregated positions of grouping atoms)") {
       tc(x, y) :- (e(x, y), !e(x, z), !e(x, z))
     }
   }
@@ -52,4 +52,18 @@ class StratifiedNegationTests extends munit.FunSuite {
       p.solve(e.id)
     }
   }
+
+  test("stratified negation with aggregation") {
+    val p = Program(new StagedExecutionEngine(new DefaultStorageManager()))
+    val a = p.relation[Constant]("a")
+    val b = p.relation[Constant]("b")
+    val x, y = p.variable()
+
+    a("A", 1) :- ()
+    a("B", 2) :- ()
+
+    interceptMessage[java.lang.Exception]("Variable with varId 0 appears only in negated atoms (and possibly in aggregated positions of grouping atoms)") {
+      b(x) :- (!a(__, x), groupBy(a(__, y), Seq(), AggOp.SUM(y) -> x))
+    }
+  }
 }