summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorWei Tang <i@null.tl>2015-09-09 12:25:17 +0800
committerWei Tang <i@null.tl>2015-09-09 12:25:17 +0800
commit19cba1848b0f1df433dae7b4a901f97e6e4fb88f (patch)
tree6ce54bf47f679be9fd9faab7c1e4297156fa3ae6
parent266c0a4758f47ab3ae039aac974644a48c049e8e (diff)
downloadmm-19cba1848b0f1df433dae7b4a901f97e6e4fb88f.tar.gz
mm-19cba1848b0f1df433dae7b4a901f97e6e4fb88f.tar.bz2
Fix disj: False does not count as success
-rw-r--r--mm.rkt11
1 files changed, 8 insertions, 3 deletions
diff --git a/mm.rkt b/mm.rkt
index be83911..e90d533 100644
--- a/mm.rkt
+++ b/mm.rkt
@@ -311,13 +311,18 @@
((fresh (s1 s2)
(== `(== ,s1 ,s2) predicate)
(unifyo s1 s2 parent out)))
- ((fresh (s1 s2 o1 o2)
+ ((fresh (s1 s2 o1 o2 t1 t2)
(== `(disj ,s1 ,s2) predicate)
(conde
((predicatifyo s1 pattern-assoc parent fresh-next
- fresh-next-out out o1))
+ fresh-next-out t1 o1))
((predicatifyo s2 pattern-assoc parent fresh-next
- fresh-next-out out o2)))))
+ fresh-next-out t2 o2)))
+ (conde
+ ((== t1 #f) (== t2 #f) (== #t #f))
+ ((=/= t1 #f) (== t2 #f) (== out t1))
+ ((== t1 #f) (=/= t2 #f) (== out t2))
+ ((=/= t1 #f) (=/= t2 #f) (conde ((== out t1)) ((== out t2)))))))
((fresh (s1 s2 o1 o2 fresh-next-tmp tmp)
(== `(conj ,s1 ,s2) predicate)
(predicatifyo s1 pattern-assoc parent fresh-next