Permalink
Browse files

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.
  • Loading branch information...
namin authored and swannodette committed Jan 4, 2013
1 parent 2f38577 commit fb489298417c643fdd03efbf6951e998e6821910
@@ -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)
@@ -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))))
+ ())))
@@ -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

0 comments on commit fb48929

Please sign in to comment.