Fix bug in bound variables check; add regression tests (#25)

* Fix bug in bound variables check; add regression tests * Expand tests; reformat. --------- Co-authored-by: Ulrik Rasmussen <[email protected]> Co-authored-by: Aaron Bembenek <[email protected]>
HarvardPL · Nov 6, 2024 · 4e25a86 · 4e25a86
1 parent bcc8c75
commit 4e25a86
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 1 deletion.
diff --git a/src/main/java/edu/harvard/seas/pl/abcdatalog/ast/validation/DatalogValidator.java b/src/main/java/edu/harvard/seas/pl/abcdatalog/ast/validation/DatalogValidator.java
@@ -216,8 +216,18 @@ public DatalogValidationException visit(NegatedAtom atom, DatalogValidationExcep
       }
     }
 
+    for (Variable v : new HashSet<>(boundVars)) {
+      Term t = subst.get(v);
+      if (t instanceof Variable) {
+        boundVars.add((Variable) t);
+      }
+    }
+
     for (Variable x : possiblyUnboundVars) {
-      if (!boundVars.contains(x) && !(subst.get(x) instanceof Constant)) {
+      Term t;
+      if (!boundVars.contains(x)
+          && !((t = subst.get(x)) instanceof Constant)
+          && !(boundVars.contains(t))) {
         throw new DatalogValidationException(
             "Every variable in a rule must be bound, but "
                 + x

diff --git a/src/test/java/edu/harvard/seas/pl/abcdatalog/engine/ExplicitUnificationTests.java b/src/test/java/edu/harvard/seas/pl/abcdatalog/engine/ExplicitUnificationTests.java
@@ -150,4 +150,14 @@ public void testBinaryDisunificationFail2() throws DatalogValidationException {
     test("p(X) :- q(X), Y!=_. q(a).", "p(X)?", "");
     throw new DatalogValidationException();
   }
+
+  @Test
+  public void testVariablesBoundByUnifiers1() throws DatalogValidationException {
+    test("p(X, Y) :- q(Z, W), X = Z, W = Y. q(a, b).", "p(a, b)?", "p(a, b).");
+  }
+
+  @Test
+  public void testVariablesBoundByUnifiers2() throws DatalogValidationException {
+    test("p(X, Y) :- q(Z, W), Z = A, B = W, X = A, B = Y. q(a, b).", "p(a, b)?", "p(a, b).");
+  }
 }