From bfc0f5b828593bd9678ec36d5d455484c63be928 Mon Sep 17 00:00:00 2001
From: Nada Amin <namin@alum.mit.edu>
Date: Fri, 4 Jan 2013 12:31:56 +0100
Subject: [PATCH] LOGIC-95: fix some issues with disequality.

1. -relevant-var? is broken for !=c because it compares vars that have
   been rooted with vars that haven't been, when called from udpatec.

2. Because of nested vars, we need to go deeper when recovering vars,
   and only compare ground terms with not= when invoking a !=c
   constraint.

TODO: for 1, we need to rethink how to maintain the constraint map in
face of constraints that change the associations between vars and
constraints.
---
 src/main/clojure/clojure/core/logic.clj            |   24 ++++++++++++--------
 .../clojure/clojure/core/logic/nominal/tests.clj   |   10 ++++++++
 src/test/clojure/clojure/core/logic/tests.clj      |   18 +++++++++++++++
 3 files changed, 43 insertions(+), 9 deletions(-)

diff --git a/src/main/clojure/clojure/core/logic.clj b/src/main/clojure/clojure/core/logic.clj
index 4d9b05a..8f0720d 100644
--- a/src/main/clojure/clojure/core/logic.clj
+++ b/src/main/clojure/clojure/core/logic.clj
@@ -3870,16 +3870,25 @@
     (when sp
       (identical? s sp))))
 
+(defn recover-vars-from-term [x]
+  (let [r (atom #{})]
+    (walk-term x
+      (fn [x]
+        (if (lvar? x)
+          (do (swap! r conj x) x)
+          x)))
+    @r))
+
 (defn recover-vars [p]
   (loop [p (seq p) r #{}]
     (if p
       (let [[u v] (first p)]
-        (if (lvar? v)
-          (recur (next p) (conj r u v))
-          (recur (next p) (conj r u))))
+        (recur (next p)
+          (clojure.set/union
+            r (recover-vars-from-term u) (recover-vars-from-term v))))
       r)))
 
-(declare normalize-store)
+(declare normalize-store ground-term?)
 
 (defn !=c
   ([p] (!=c p nil))
@@ -3897,7 +3906,7 @@
                            vv (walk* a v)]
                        (cond
                          (= xv vv) (recur (next sp) (dissoc p x))
-                         (and (not (lvar? xv)) (not (lvar? vv)) (not= xv vv)) nil
+                         (and (ground-term? xv a) (ground-term? vv a) (not= xv vv)) nil
                          :else (recur (next sp) p)))
                      p))]
            (if p
@@ -3932,9 +3941,6 @@
        IRelevant
        (-relevant? [this s]
          (not (empty? p)))
-       IRelevantVar
-       (-relevant-var? [this x]
-         ((recover-vars p) x))
        IConstraintWatchedStores
        (watched-stores [this] #{::subst}))))
 
@@ -4094,7 +4100,7 @@
                     (let [x (walk s x)]
                       (cond
                         (lvar? x) (throw fk)
-                        (coll? x) (-ground-term? x s)
+                        (tree-term? x) (-ground-term? x s)
                         :else x)))))))]
     (try
       (-ground-term? x s)
diff --git a/src/test/clojure/clojure/core/logic/nominal/tests.clj b/src/test/clojure/clojure/core/logic/nominal/tests.clj
index 609fb89..067f42c 100644
--- a/src/test/clojure/clojure/core/logic/nominal/tests.clj
+++ b/src/test/clojure/clojure/core/logic/nominal/tests.clj
@@ -393,3 +393,13 @@
                (infd x (interval 1 3))
                (== (nom/tie b (nom/tie a x)) (nom/tie c q)))))
         [(nom/tie 'a_0 1) (nom/tie 'a_0 2) (nom/tie 'a_0 3)])))
+
+(deftest test-95-nominal-disequality
+  (is (= (run* [q]
+           (nom/fresh [a b]
+             (fresh [x y]
+               (!= x y)
+               (== (nom/tie a (nom/tie b [b y])) (nom/tie b (nom/tie a [a x])))
+               (== x 'foo)
+               (== [x y] q))))
+        ())))
diff --git a/src/test/clojure/clojure/core/logic/tests.clj b/src/test/clojure/clojure/core/logic/tests.clj
index dec8883..0a3028a 100644
--- a/src/test/clojure/clojure/core/logic/tests.clj
+++ b/src/test/clojure/clojure/core/logic/tests.clj
@@ -947,6 +947,24 @@
              (!= [x 1] [2 y])))
          '((_0 :- (!= (_1 1) (_2 2)))))))
 
+(deftest test-logic-95-disequality-1
+  (is (= (run* [q]
+           (fresh [x y w z]
+             (!= x y)
+             (!= w z)
+             (== z y)
+             (== x 'foo)
+             (== y 'foo)))
+        ())))
+
+(deftest test-logic-95-disequality-2
+  (is (= (run* [q]
+           (fresh [x y w z]
+             (!= x [y])
+             (== x ['foo])
+             (== y 'foo)))
+        ())))
+
 ;; -----------------------------------------------------------------------------
 ;; tabled
 
-- 
1.7.10.4