Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Flexible search #13

Closed
wants to merge 33 commits into from

2 participants

Jamie Brandon David Nolen
Jamie Brandon

Replaces the core stream data-structure with a lazy tree of continuations (ITake becomes ISearchTree).

Adds optional fair conjunction (via bind-fair and all-fair).

Adds new search algorithms: bfs-lazy (the original algorithm), bfs-strict, dfs-lazy, dfs-strict, dfs-par (using fork-join).

Unfortunately, introduces performance regressions for lazy search. For example, for bench/zebrao I see:

  • original branch w/ (run* ...): ~30ms
  • original branch w/ (run 1 ...): ~8.5ms
  • this branch w/ (run* ...): ~25ms
  • this branch w/ (run 1 ...): ~27ms

I suspect that this is simply a missing thunk somewhere but I've run out of time to work on this. Given that laziness is now largely controlled by the search algorithm it may also be worth deprecating the various variants of run.

As a consolation prize:

  • this branch w/ (binding [*search* dfs-par] (run* ...)): ~18ms
David Nolen
Collaborator

I just realized that the reason many tests are failing are probably simply that your version now returns results in a different order. I need to go through the tests and convert many of them to set comparisons.

David Nolen
Collaborator

Excellent, however the usual spiel - I can't merge pull requests for official Clojure projects. I need an enhancement ticket + squashed patch in JIRA, http://dev.clojure.org/jira/browse/LOGIC. I also can only take patches from people that have signed the Contributor Agreement (CA) - http://clojure.org/contributing. Please mail this in, once that's on its way to North Carolina I will happily apply the JIRA patch.

As far as feedback this looks like a fairly small set of changes! To make that even more clear please remove the whitespace changes from the JIRA patch - this is pretty easy to do w/ git if you interactively add the changes via git when creating the patch.

Would love to get this in, this looks like a great step forward for customizable search in core.logic. Thanks much.

Oh and some tests would make me a little bit more confident when applying this :)

Jamie Brandon

I'll send off the CA on Friday.

In the meantime, I poked around at those performance regressions and I'm now wondering if it's just a matter of different search order. In theory bfs-lazy should return results in the same order as master but some of the tests needed changing, so perhaps I've got something swapped around somewhere...

Jamie Brandon

Sent the CA on Friday.

David Nolen
Collaborator

Excellent! Feel free to add a ticket to JIRA w/ attached squashed patch against master.

jamii added some commits
Jamie Brandon jamii Cleanup dev detritus 07a717a
Jamie Brandon jamii Uncomment this test-condu-1, since it seems to pass 169aa5c
Jamie Brandon jamii Merge branch 'master' into flexible-search
Conflicts:
	src/main/clojure/clojure/core/logic.clj
	src/main/clojure/clojure/core/logic/bench.clj
	src/test/clojure/clojure/core/logic/tests.clj
c69c2d8
Jamie Brandon jamii Fix test that relies on inc representation 9f96e56
Jamie Brandon

I wonder if the poor performance in the parallel solver is related to this - https://groups.google.com/forum/#!msg/clojure/48W2eff3caU/qKjFmh3dgvMJ

David Nolen
Collaborator

There's far too much speculation in that thread. Even so, I doubt it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Showing 33 unique commits by 1 author.

Dec 12, 2012
Jamie Brandon jamii First pass at supporting incremental goals 017fee2
Jamie Brandon jamii Explicit tree representation 9be771a
Dec 13, 2012
Jamie Brandon jamii Only return one result per tree node 53849f3
Jamie Brandon jamii Remove trailing whitespace, for the sake of my sanity b012507
Jamie Brandon jamii Remove dead comments b01a8ea
Jamie Brandon jamii Fair conjunction 0d0d4be
Jamie Brandon jamii Replace mplus with choice for the result tree, since the implementati…
…on is always choice anyway.

(This may have broken waiting-streams, but I'm not sure what they do so its hard to tell)
39dc329
Jamie Brandon jamii Make take* slightly lazier af91ba6
Jamie Brandon jamii Add -dec function for tests 0cbbc4a
Jamie Brandon jamii First attempt at parallel solver e2221b7
Dec 17, 2012
Jamie Brandon jamii Clean up the search interface f95870b
Jamie Brandon jamii Add multiple search algorithms 720dce1
Jamie Brandon jamii Remove {:once true} on inc thunks; might actually be useful to run th…
…em multiple times
472ba2d
Jamie Brandon jamii Forgot to update tests with new search functions aceb511
Jamie Brandon jamii Add TODO about ifu 446cf5f
Jamie Brandon jamii Merge branch 'fair-conj3' into parallel-solver
Conflicts:
	src/main/clojure/clojure/core/logic.clj
a341baa
Jamie Brandon jamii Parallel solver 519d75f
Jamie Brandon jamii Remove unnecessary lazy-seq in dfs-lazy 2cf0d85
Jamie Brandon jamii Merge branch 'master' into fair-conj3
Conflicts:
	src/main/clojure/clojure/core/logic.clj
39daac8
Jamie Brandon jamii Correct typo 9e6aaa4
Jamie Brandon jamii Merge branch 'parallel-solver' into flexible-search 0768474
Dec 18, 2012
Jamie Brandon jamii Restore laziness in ifu ad70e25
Jamie Brandon jamii Split ISearchTree into IBranch and ILeaf to avoid problems with nil-v…
…alued leaves
36f613d
Jamie Brandon jamii Remove unnecessary -incs in solver wrappers e94973d
Jamie Brandon jamii Wrap results in lazy-seq to ensure uniform representation (eg some se…
…arch algorithms return nil, others return ())
08acf30
Jamie Brandon jamii Waiting stream has to be a branch, since it may have no children c2bf5a1
Jamie Brandon jamii Use instance? instead of satisfies? (leaf? was a bottleneck) ce00fc3
Jamie Brandon jamii Forgot to update dfs-par in 36f613d 242c454
Jamie Brandon jamii Add test for fair conjunction 33dce78
Dec 27, 2012
Jamie Brandon jamii Cleanup dev detritus 07a717a
Jamie Brandon jamii Uncomment this test-condu-1, since it seems to pass 169aa5c
Jamie Brandon jamii Merge branch 'master' into flexible-search
Conflicts:
	src/main/clojure/clojure/core/logic.clj
	src/main/clojure/clojure/core/logic/bench.clj
	src/test/clojure/clojure/core/logic/tests.clj
c69c2d8
Jamie Brandon jamii Fix test that relies on inc representation 9f96e56
This page is out of date. Refresh to see the latest.
2  project.clj
@@ -18,7 +18,7 @@
18 18 :dependencies [[org.clojure/clojure "1.4.0"]
19 19 [org.clojure/clojurescript "0.0-1535"]
20 20 [org.clojure/google-closure-library "0.0-2029"]
21   - [org.clojure/google-closure-library-third-party "0.0-2029"]
  21 + [org.clojure/google-closure-library-third-party "0.0-2029"]
22 22 [org.clojure/tools.macro "0.1.1"]
23 23 [org.clojure/tools.nrepl "0.2.0-RC1"]
24 24 [com.datomic/datomic-free "0.8.3551" :scope "provided"]]
335 src/main/clojure/clojure/core/logic.clj
@@ -92,11 +92,20 @@
92 92 (defprotocol IBind
93 93 (bind [this g]))
94 94
  95 +(defprotocol IBindFair
  96 + (bind-fair [this g]))
  97 +
95 98 (defprotocol IMPlus
96   - (mplus [a f]))
  99 + (mplus [this that]))
  100 +
  101 +(defprotocol ILeaf
  102 + (value [this] "The value at this leaf"))
  103 +
  104 +(defprotocol IBranch
  105 + (children [this] "The children of this node"))
97 106
98   -(defprotocol ITake
99   - (take* [a]))
  107 +(defn leaf? [thing]
  108 + (instance? clojure.core.logic.ILeaf thing))
100 109
101 110 ;; -----------------------------------------------------------------------------
102 111 ;; soft cut & committed choice protocols
@@ -430,8 +439,8 @@
430 439 :else (FiniteDomain. s (first s) (first (rseq s))))))
431 440
432 441 (defn domain
433   - "Construct a domain for assignment to a var. Arguments should
434   - be integers given in sorted order. domains may be more efficient
  442 + "Construct a domain for assignment to a var. Arguments should
  443 + be integers given in sorted order. domains may be more efficient
435 444 than intervals when only a few values are possible."
436 445 [& args]
437 446 (when (seq args)
@@ -603,7 +612,7 @@
603 612 (multi-interval (interval _lb (dec that))
604 613 (interval (inc that) _ub))
605 614 this))
606   -
  615 +
607 616 (interval? that)
608 617 (let [i this j that
609 618 imin (lb i) imax (ub i)
@@ -620,7 +629,7 @@
620 629 (and (> imax jmax)
621 630 (<= jmin imin)) (interval (inc jmax) imax)
622 631 :else (throw (Error. (str "Interval difference not defined " i " " j)))))
623   -
  632 +
624 633 :else (difference* this that)))
625 634
626 635 IIntervals
@@ -1121,14 +1130,14 @@
1121 1130 (loop [lv v [v vp :as me] (find s v)]
1122 1131 (cond
1123 1132 (nil? me) lv
1124   -
  1133 +
1125 1134 (not (lvar? vp))
1126 1135 (if-let [sv (and (subst-val? vp) (:v vp))]
1127 1136 (if (= sv ::unbound)
1128 1137 (with-meta v (assoc (meta vp) ::unbound true))
1129 1138 sv)
1130 1139 vp)
1131   -
  1140 +
1132 1141 :else (recur vp (find s vp))))
1133 1142 v))
1134 1143
@@ -1157,7 +1166,7 @@
1157 1166
1158 1167 :else (recur vp (find s vp)))))
1159 1168 v))
1160   -
  1169 +
1161 1170 (ext-run-cs [this x v]
1162 1171 (let [x (root-var this x)
1163 1172 xs (if (lvar? v)
@@ -1183,11 +1192,12 @@
1183 1192 IBind
1184 1193 (bind [this g]
1185 1194 (g this))
1186   - IMPlus
1187   - (mplus [this f]
1188   - (choice this f))
1189   - ITake
1190   - (take* [this] this))
  1195 + IBindFair
  1196 + (bind-fair [this g]
  1197 + (g this))
  1198 + ILeaf
  1199 + (value [this]
  1200 + this))
1191 1201
1192 1202 (defn add-attr [s x attr attrv]
1193 1203 (let [x (root-var s x)
@@ -1250,7 +1260,6 @@
1250 1260 ([m cs] (Substitutions. m nil cs nil #{} nil)))
1251 1261
1252 1262 (def empty-s (make-s))
1253   -(def empty-f (fn []))
1254 1263
1255 1264 (defn subst? [x]
1256 1265 (instance? Substitutions x))
@@ -1338,7 +1347,7 @@
1338 1347 (if (-> u clojure.core/meta ::unbound)
1339 1348 (ext-no-check s u (assoc (root-val s u) :v v))
1340 1349 (ext-no-check s u v)))
1341   -
  1350 +
1342 1351 :else nil))
1343 1352
1344 1353 IReifyTerm
@@ -1473,7 +1482,7 @@
1473 1482 s
1474 1483 (unify s u nil))
1475 1484 nil)))
1476   -
  1485 +
1477 1486 (lcons? v)
1478 1487 (loop [u u v v s s]
1479 1488 (if (lvar? u)
@@ -1485,7 +1494,7 @@
1485 1494 (recur (lnext u) (lnext v) s)
1486 1495 nil)
1487 1496 :else (unify s u v))))
1488   -
  1497 +
1489 1498 :else nil))
1490 1499
1491 1500 IReifyTerm
@@ -1571,7 +1580,7 @@
1571 1580 nil)
1572 1581 nil)
1573 1582 (if (seq v) nil s))))
1574   -
  1583 +
1575 1584 (lcons? v) (unify-terms v u s)
1576 1585 :else nil))
1577 1586
@@ -1715,40 +1724,48 @@
1715 1724 ([a g & g-rest]
1716 1725 `(bind* (bind ~a ~g) ~@g-rest)))
1717 1726
  1727 +(defmacro bind-fair*
  1728 + ([a g] `(bind-fair ~a ~g))
  1729 + ([a g & g-rest]
  1730 + `(bind-fair* (bind-fair ~a ~g) ~@g-rest)))
  1731 +
1718 1732 (defmacro mplus*
1719 1733 ([e] e)
1720 1734 ([e & e-rest]
1721   - `(mplus ~e (fn [] (mplus* ~@e-rest)))))
1722   -
1723   -(defmacro -inc [& rest]
1724   - `(fn -inc [] ~@rest))
1725   -
1726   -(extend-type Object
1727   - ITake
1728   - (take* [this] this))
  1735 + `(mplus ~e (mplus* ~@e-rest))))
1729 1736
1730   -;; TODO: Choice always holds a as a list, can we just remove that?
  1737 +(declare choice)
1731 1738
1732   -(deftype Choice [a f]
  1739 +(deftype Choice [left right]
1733 1740 clojure.lang.ILookup
1734 1741 (valAt [this k]
1735 1742 (.valAt this k nil))
1736 1743 (valAt [this k not-found]
1737 1744 (case k
1738   - :a a
  1745 + :left left
  1746 + :right right
1739 1747 not-found))
1740 1748 IBind
1741 1749 (bind [this g]
1742   - (mplus (g a) (fn [] (bind f g))))
1743   - IMPlus
1744   - (mplus [this fp]
1745   - (Choice. a (fn [] (mplus (fp) f))))
1746   - ITake
1747   - (take* [this]
1748   - (lazy-seq (cons (first a) (lazy-seq (take* f))))))
1749   -
1750   -(defn choice [a f]
1751   - (Choice. a f))
  1750 + (choice (bind left g) (bind right g)))
  1751 + IBindFair
  1752 + (bind-fair [this g]
  1753 + (choice (bind-fair left g) (bind-fair right g)))
  1754 + IBranch
  1755 + (children [this]
  1756 + [left right]))
  1757 +
  1758 +(defn choice [left right]
  1759 + (cond
  1760 + (nil? left) right
  1761 + (nil? right) left
  1762 + :else (Choice. left right)))
  1763 +
  1764 +;; TODO: might a binary tree be better?
  1765 +(defmacro choice*
  1766 + ([e] e)
  1767 + ([e & e-rest]
  1768 + `(choice ~e (choice* ~@e-rest))))
1752 1769
1753 1770 ;; -----------------------------------------------------------------------------
1754 1771 ;; MZero
@@ -1757,34 +1774,41 @@
1757 1774 nil
1758 1775 (bind [_ g] nil))
1759 1776
1760   -(extend-protocol IMPlus
1761   - nil
1762   - (mplus [_ f] (f)))
1763   -
1764   -(extend-protocol ITake
  1777 +(extend-protocol IBindFair
1765 1778 nil
1766   - (take* [_] '()))
1767   -
1768   -;; -----------------------------------------------------------------------------
1769   -;; Unit
1770   -
1771   -(extend-type Object
1772   - IMPlus
1773   - (mplus [this f]
1774   - (Choice. this f)))
  1779 + (bind-fair [_ g] nil))
1775 1780
1776 1781 ;; -----------------------------------------------------------------------------
1777 1782 ;; Inc
1778 1783
1779   -(extend-type clojure.lang.Fn
  1784 +(deftype Inc [a restg]
1780 1785 IBind
1781 1786 (bind [this g]
1782   - (-inc (bind (this) g)))
1783   - IMPlus
1784   - (mplus [this f]
1785   - (-inc (mplus (f) this)))
1786   - ITake
1787   - (take* [this] (lazy-seq (take* (this)))))
  1787 + (Inc. a (fn [a2] (bind (restg a2) g))))
  1788 + IBindFair
  1789 + (bind-fair [this g]
  1790 + (Inc. a (fn [a2] (bind (g a2) restg))))
  1791 + IBranch
  1792 + (children [this]
  1793 + (when-let [rest (restg a)]
  1794 + [rest])))
  1795 +
  1796 +(defmacro -inc [a restg]
  1797 + (let [a2 (gensym "a")
  1798 + thunk-body (clojure.walk/prewalk-replace {a a2} restg)
  1799 + thunk `(fn [~a2] ~thunk-body)]
  1800 + `(Inc. ~a ~thunk)))
  1801 +
  1802 +(defn -dec [inc]
  1803 + ((.restg inc) (.a inc)))
  1804 +
  1805 +;; -----------------------------------------------------------------------------
  1806 +;; Return
  1807 +
  1808 +(defrecord Return [value]
  1809 + ILeaf
  1810 + (value [this]
  1811 + value))
1788 1812
1789 1813 ;; =============================================================================
1790 1814 ;; Syntax
@@ -1828,8 +1852,7 @@
1828 1852 [& clauses]
1829 1853 (let [a (gensym "a")]
1830 1854 `(fn [~a]
1831   - (-inc
1832   - (mplus* ~@(bind-conde-clauses a clauses))))))
  1855 + (-inc ~a (choice* ~@(bind-conde-clauses a clauses))))))
1833 1856
1834 1857 (defn- lvar-bind [sym]
1835 1858 ((juxt identity
@@ -1839,24 +1862,63 @@
1839 1862 (mapcat lvar-bind syms))
1840 1863
1841 1864 (defmacro fresh
1842   - "Creates fresh variables. Goals occuring within form a logical
  1865 + "Creates fresh variables. Goals occuring within form a logical
1843 1866 conjunction."
1844 1867 [[& lvars] & goals]
1845 1868 `(fn [a#]
1846   - (-inc
1847   - (let [~@(lvar-binds lvars)]
1848   - (bind* a# ~@goals)))))
  1869 + (-inc a# (let [~@(lvar-binds lvars)]
  1870 + (bind* a# ~@goals)))))
1849 1871
1850 1872 (declare reifyg)
1851 1873
  1874 +(defn bfs-lazy [a]
  1875 + (let [q (java.util.ArrayDeque. [a])]
  1876 + (letfn [(bfs-loop []
  1877 + (when-let [node (.pollFirst q)]
  1878 + (if (leaf? node)
  1879 + (cons (value node) (lazy-seq (bfs-loop)))
  1880 + (do (doseq [child (children node)]
  1881 + (.addLast q child))
  1882 + (recur)))))]
  1883 + (bfs-loop))))
  1884 +
  1885 +(defn bfs-strict [a]
  1886 + (let [q (java.util.ArrayDeque. [a])
  1887 + results (java.util.ArrayDeque.)]
  1888 + (loop []
  1889 + (when-let [node (.pollFirst q)]
  1890 + (if (leaf? node)
  1891 + (.addLast results (value node))
  1892 + (doseq [child (children node)]
  1893 + (.addLast q child)))
  1894 + (recur)))
  1895 + (into nil results)))
  1896 +
  1897 +(defn dfs-lazy [node]
  1898 + (if (leaf? node)
  1899 + (list (value node))
  1900 + (apply concat (map dfs-lazy (children node)))))
  1901 +
  1902 +(defn dfs-strict [node]
  1903 + (let [results (java.util.ArrayDeque.)]
  1904 + (letfn [(dfs-loop [node]
  1905 + (if (leaf? node)
  1906 + (.addLast results (value node))
  1907 + (doseq [child (children node)]
  1908 + (dfs-loop child))))]
  1909 + (dfs-loop node)
  1910 + (into nil results))))
  1911 +
  1912 +(def ^:dynamic *search* bfs-lazy)
  1913 +
1852 1914 (defmacro solve [& [n [x :as bindings] & goals]]
1853 1915 (if (> (count bindings) 1)
1854 1916 `(solve ~n [q#] (fresh ~bindings ~@goals (== q# ~bindings)))
1855   - `(let [xs# (take* (fn []
1856   - ((fresh [~x]
1857   - ~@goals
1858   - (reifyg ~x))
1859   - empty-s)))]
  1917 + `(let [xs# (lazy-seq
  1918 + (*search* ((fresh [~x]
  1919 + ~@goals
  1920 + (reifyg ~x))
  1921 + empty-s)))]
1860 1922 (if ~n
1861 1923 (take ~n xs#)
1862 1924 xs#))))
@@ -1872,7 +1934,7 @@
1872 1934 `(run false ~@goals))
1873 1935
1874 1936 (defmacro run-nc
1875   - "Executes goals until a maximum of n results are found. Does not
  1937 + "Executes goals until a maximum of n results are found. Does not
1876 1938 occurs-check."
1877 1939 [& [n & goals]]
1878 1940 `(binding [*occurs-check* false]
@@ -1898,11 +1960,15 @@
1898 1960 ([] `clojure.core.logic/s#)
1899 1961 ([& goals] `(fn [a#] (bind* a# ~@goals))))
1900 1962
  1963 +(defmacro all-fair
  1964 + ([] `clojure.core.logic/s#)
  1965 + ([& goals] `(fn [a#] (bind-fair* a# ~@goals))))
  1966 +
1901 1967 (defn solutions
1902 1968 ([s g]
1903 1969 (solutions s (lvar) g))
1904 1970 ([s q g]
1905   - (take* ((all g (reifyg q)) s))))
  1971 + (*search* ((all g (reifyg q)) s))))
1906 1972
1907 1973 ;; =============================================================================
1908 1974 ;; Debugging
@@ -1997,14 +2063,13 @@
1997 2063 (queue s (unwrap (apply cs (map #(lvar % false) vs))))))
1998 2064 empty-s (-> u meta ::when))]
1999 2065 (first
2000   - (take*
2001   - (fn []
2002   - ((fresh [q]
2003   - (== u w) (== q u)
2004   - (fn [a]
2005   - (fix-constraints a))
2006   - (reifyg q))
2007   - init-s))))))
  2066 + (*search*
  2067 + ((fresh [q]
  2068 + (== u w) (== q u)
  2069 + (fn [a]
  2070 + (fix-constraints a))
  2071 + (reifyg q))
  2072 + init-s)))))
2008 2073 ([u w & ts]
2009 2074 (if (some #{:when} ts)
2010 2075 (let [terms (take-while #(not= % :when) ts)
@@ -2132,12 +2197,15 @@
2132 2197 (recur b gr))
2133 2198 b)))
2134 2199
2135   - clojure.lang.Fn
  2200 + Inc
2136 2201 (ifa [b gs c]
2137   - (-inc (ifa (b) gs c)))
  2202 + (let [a (.a b)
  2203 + restg (.restg b)]
  2204 + (-inc a (ifa (restg a) gs c))))
2138 2205
2139 2206 Choice
2140 2207 (ifa [b gs c]
  2208 + ;; TODO: should this be (ifu (.left b) gs (delay (ifu (.right b) gs c)))
2141 2209 (reduce bind b gs)))
2142 2210
2143 2211 (extend-protocol IIfU
@@ -2154,14 +2222,15 @@
2154 2222 (recur b gr))
2155 2223 b)))
2156 2224
2157   - clojure.lang.Fn
  2225 + Inc
2158 2226 (ifu [b gs c]
2159   - (-inc (ifu (b) gs c)))
  2227 + (let [a (.a b)
  2228 + restg (.restg b)]
  2229 + (-inc a (ifu (restg a) gs c))))
2160 2230
2161   - ;; TODO: Choice always holds a as a list, can we just remove that?
2162 2231 Choice
2163 2232 (ifu [b gs c]
2164   - (reduce bind (:a b) gs)))
  2233 + (ifu (.left b) gs (delay (ifu (.right b) gs c)))))
2165 2234
2166 2235 (defn- cond-clauses [a]
2167 2236 (fn [goals]
@@ -2176,7 +2245,7 @@
2176 2245 (ifa* ~@(map (cond-clauses a) clauses)))))
2177 2246
2178 2247 (defmacro condu
2179   - "Committed choice. Once the head (first goal) of a clause
  2248 + "Committed choice. Once the head (first goal) of a clause
2180 2249 has succeeded, remaining goals of the clause will only
2181 2250 be run once. Non-relational."
2182 2251 [& clauses]
@@ -2265,7 +2334,7 @@
2265 2334 (= f 'quote)
2266 2335 (if (and (seq? s) (not quoted))
2267 2336 (p->term s vars true)
2268   - p)
  2337 + p)
2269 2338 (= f 'clojure.core/unquote)
2270 2339 (if quoted
2271 2340 (update-pvars! s vars)
@@ -2397,7 +2466,7 @@
2397 2466 (== '() a))
2398 2467
2399 2468 (defn conso
2400   - "A relation where l is a collection, such that a is the first of l
  2469 + "A relation where l is a collection, such that a is the first of l
2401 2470 and d is the rest of l"
2402 2471 [a d l]
2403 2472 (== (lcons a d) l))
@@ -2471,15 +2540,15 @@
2471 2540 ;; =============================================================================
2472 2541 ;; More convenient goals
2473 2542
2474   -(defne membero
  2543 +(defne membero
2475 2544 "A relation where l is a collection, such that l contains x"
2476 2545 [x l]
2477 2546 ([_ [x . tail]])
2478 2547 ([_ [head . tail]]
2479 2548 (membero x tail)))
2480 2549
2481   -(defne appendo
2482   - "A relation where x, y, and z are proper collections,
  2550 +(defne appendo
  2551 + "A relation where x, y, and z are proper collections,
2483 2552 such that z is x appended to y"
2484 2553 [x y z]
2485 2554 ([() _ y])
@@ -2504,7 +2573,7 @@
2504 2573 (let [aseq (drop-while nil? aseq)]
2505 2574 (when (seq aseq)
2506 2575 (choice (first aseq)
2507   - (fn [] (to-stream (next aseq)))))))
  2576 + (to-stream (next aseq))))))
2508 2577
2509 2578 (defmacro def-arity-exc-helper []
2510 2579 (try
@@ -2599,7 +2668,7 @@
2599 2668 ((deref ~'indexes) ~'arity))
2600 2669 (~'add-indexes [~'_ ~'arity ~'index]
2601 2670 (swap! ~'indexes assoc ~'arity ~'index)))
2602   - (defmacro ~'defrel
  2671 + (defmacro ~'defrel
2603 2672 "Define a relation for adding facts. Takes a name and some fields.
2604 2673 Use fact/facts to add facts and invoke the relation to query it."
2605 2674 [~'name ~'& ~'rest]
@@ -2757,7 +2826,7 @@
2757 2826
2758 2827 (defn waiting-stream-check
2759 2828 "Take a waiting stream, a success continuation, and a failure continuation.
2760   - If we don't find any ready suspended streams, invoke the failure continuation.
  2829 + If we don't find any ready suspended streams, invoke the failure continuation.
2761 2830 If we find a ready suspended stream calculate the remainder of the waiting
2762 2831 stream. If we've reached the fixpoint just call the thunk of the suspended
2763 2832 stream, otherwise call mplus on the result of the thunk and the remainder
@@ -2820,8 +2889,8 @@
2820 2889 (fn [] (reuse this argv cache @cache (count start))))]
2821 2890 ;; we have answer terms to reuse in the cache
2822 2891 (let [ans (first ansv*)]
2823   - (Choice. (subunify this argv (reify-tabled this ans))
2824   - (fn [] (reuse-loop (disj ansv* ans)))))))]
  2892 + (choice (subunify this argv (reify-tabled this ans))
  2893 + (-inc this (reuse-loop (disj ansv* ans)))))))]
2825 2894 (reuse-loop start))))
2826 2895
2827 2896 ;; unify an argument with an answer from a cache
@@ -2851,22 +2920,21 @@
2851 2920 (make-suspended-stream (:cache ss) (:ansv* ss)
2852 2921 (fn [] (bind ((:f ss)) g))))
2853 2922 this)))))
2854   -
2855   - IMPlus
2856   - (mplus [this f]
  2923 + IBindFair
  2924 + (bind-fair [this g]
2857 2925 (waiting-stream-check this
2858 2926 ;; success continuation
2859   - (fn [fp] (mplus fp f))
  2927 + (fn [f] (bind-fair f g))
2860 2928 ;; failure continuation
2861 2929 (fn []
2862   - (let [a-inf (f)]
2863   - (if (waiting-stream? a-inf)
2864   - (into a-inf this)
2865   - (mplus a-inf (fn [] this)))))))
2866   -
2867   - ITake
2868   - (take* [this]
2869   - (waiting-stream-check this (fn [f] (take* f)) (fn [] ()))))
  2930 + (into []
  2931 + (map (fn [ss]
  2932 + (make-suspended-stream (:cache ss) (:ansv* ss)
  2933 + (fn [] (bind-fair ((:f ss)) g))))
  2934 + this)))))
  2935 + IBranch
  2936 + (children [this]
  2937 + (waiting-stream-check this (fn [a] a) (fn [] nil))))
2870 2938
2871 2939 (defn master
2872 2940 "Take the argument to the goal and check that we don't
@@ -2903,7 +2971,7 @@
2903 2971 (reuse a argv cache nil nil))))))))
2904 2972
2905 2973 (defmacro tabled
2906   - "Macro for defining a tabled goal. Prefer ^:tabled with the
  2974 + "Macro for defining a tabled goal. Prefer ^:tabled with the
2907 2975 defne/a/u forms over using this directly."
2908 2976 [args & grest]
2909 2977 `(let [table# (atom {})]
@@ -3040,7 +3108,7 @@
3040 3108 (verify-all-bound* a (seq constrained))))
3041 3109
3042 3110 ;; FIXME: Nada Amin's quine code blows up here, seems like somehow
3043   -;; things might be getting out of sync?
  3111 +;; things might be getting out of sync?
3044 3112
3045 3113 (defn enforceable-constrained [a]
3046 3114 (let [cs (:cs a)
@@ -3072,8 +3140,8 @@
3072 3140 (filter reifiable?)
3073 3141 (map #(reifyc % v r a)))]
3074 3142 (if (empty? rcs)
3075   - (choice (list v) empty-f)
3076   - (choice (list `(~v :- ~@rcs)) empty-f))))
  3143 + (Return. v)
  3144 + (Return. `(~v :- ~@rcs)))))
3077 3145
3078 3146 (defn reifyg [x]
3079 3147 (all
@@ -3082,11 +3150,10 @@
3082 3150 (let [v (walk* a x)
3083 3151 r (-reify* empty-s v)]
3084 3152 (if (zero? (count r))
3085   - (choice (list v) empty-f)
  3153 + (Return. v)
3086 3154 (let [v (walk* r v)]
3087 3155 (reify-constraints v r a)))))))
3088 3156
3089   -
3090 3157 (defn cgoal [c]
3091 3158 (reify
3092 3159 clojure.lang.IFn
@@ -3371,7 +3438,7 @@
3371 3438 (cgoal (fdc (=fdc u v))))
3372 3439
3373 3440 (defn !=fdc [u v]
3374   - (reify
  3441 + (reify
3375 3442 clojure.lang.IFn
3376 3443 (invoke [this s]
3377 3444 (let-dom s [u du v dv]
@@ -3399,7 +3466,7 @@
3399 3466 ;; and at least du or dv has a singleton domain
3400 3467 (and (domain? du) (domain? dv)
3401 3468 (or (singleton-dom? du)
3402   - (singleton-dom? dv)))))))
  3469 + (singleton-dom? dv)))))))
3403 3470
3404 3471 (defn !=fd
3405 3472 "A finite domain constraint. u and v must not be equal. u and v
@@ -3408,7 +3475,7 @@
3408 3475 (cgoal (fdc (!=fdc u v))))
3409 3476
3410 3477 (defn <=fdc [u v]
3411   - (reify
  3478 + (reify
3412 3479 clojure.lang.IFn
3413 3480 (invoke [this s]
3414 3481 (let-dom s [u du v dv]
@@ -3467,7 +3534,7 @@
3467 3534 s))))
3468 3535
3469 3536 (defn +fdc [u v w]
3470   - (reify
  3537 + (reify
3471 3538 clojure.lang.IFn
3472 3539 (invoke [this s]
3473 3540 (let-dom s [u du v dv w dw]
@@ -3588,7 +3655,7 @@
3588 3655
3589 3656 (defn *fd
3590 3657 "A finite domain constraint for multiplication and
3591   - thus division. u, v & w must be eventually be given
  3658 + thus division. u, v & w must be eventually be given
3592 3659 domains if vars."
3593 3660 [u v w]
3594 3661 (cgoal (fdc (*fdc u v w))))
@@ -3599,10 +3666,10 @@
3599 3666 (defn -distinctfdc
3600 3667 "The real *individual* distinctfd constraint. x is a var that now is bound to
3601 3668 a single value. y* were the non-singleton bound vars that existed at the
3602   - construction of the constraint. n* is the set of singleton domain values
3603   - that existed at the construction of the constraint. We use categorize to
  3669 + construction of the constraint. n* is the set of singleton domain values
  3670 + that existed at the construction of the constraint. We use categorize to
3604 3671 determine the current non-singleton bound vars and singleton vlaues. if x
3605   - is in n* or the new singletons we have failed. If not we simply remove
  3672 + is in n* or the new singletons we have failed. If not we simply remove
3606 3673 the value of x from the remaining non-singleton domains bound to vars."
3607 3674 ([x y* n*] (-distinctfdc x y* n* nil))
3608 3675 ([x y* n* id]
@@ -3658,9 +3725,9 @@
3658 3725
3659 3726 (defn distinctfdc
3660 3727 "The real distinctfd constraint. v* can be seq of logic vars and
3661   - values or it can be a logic var itself. This constraint does not
  3728 + values or it can be a logic var itself. This constraint does not
3662 3729 run until v* has become ground. When it has become ground we group
3663   - v* into a set of logic vars and a sorted set of known singleton
  3730 + v* into a set of logic vars and a sorted set of known singleton
3664 3731 values. We then construct the individual constraint for each var."
3665 3732 ([v*] (distinctfdc v* nil))
3666 3733 ([v* id]
@@ -3698,8 +3765,8 @@
3698 3765 (watched-stores [this] #{::subst}))))
3699 3766
3700 3767 (defn distinctfd
3701   - "A finite domain constraint that will guarantee that
3702   - all vars that occur in v* will be unified with unique
  3768 + "A finite domain constraint that will guarantee that
  3769 + all vars that occur in v* will be unified with unique
3703 3770 values. v* need not be ground. Any vars in v* should
3704 3771 eventually be given a domain."
3705 3772 [v*]
@@ -3841,7 +3908,7 @@
3841 3908 (when-not (= vf ::not-found)
3842 3909 (if-let [cs (disunify s (get u kf) vf cs)]
3843 3910 (recur (next ks) cs)
3844   - nil)))
  3911 + nil)))
3845 3912 cs))
3846 3913 nil)))
3847 3914
@@ -4068,8 +4135,8 @@
4068 4135
4069 4136 (defn featurec
4070 4137 "Ensure that a map contains at least the key-value pairs
4071   - in the map fs. fs must be partially instantiated - that is,
4072   - it may contain values which are logic variables to support
  4138 + in the map fs. fs must be partially instantiated - that is,
  4139 + it may contain values which are logic variables to support
4073 4140 feature extraction."
4074 4141 [x fs]
4075 4142 (cgoal (-featurec x fs)))
@@ -4188,7 +4255,7 @@
4188 4255 (fc t s)
4189 4256 (when-let [s (fc (lfirst t) s)]
4190 4257 (recur (lnext t) s)))))
4191   -
  4258 +
4192 4259 clojure.lang.Sequential
4193 4260 (-constrain-tree [t fc s]
4194 4261 (loop [t (seq t) s s]
32 src/main/clojure/clojure/core/logic/bench.clj
@@ -91,7 +91,7 @@
91 91
92 92 (comment
93 93 (run 1 [q] (zebrao q))
94   -
  94 +
95 95 ;; SWI-Prolog 6-8.5s
96 96 ;; ~2.4s
97 97 (binding [*occurs-check* false]
@@ -142,7 +142,7 @@
142 142 (== q (llist a b d))
143 143 (bounded-listo q 6)
144 144 (all-connected-to-allo q)))
145   -
  145 +
146 146 ;; 350-400ms
147 147 (dotimes [_ 5]
148 148 (time
@@ -225,7 +225,7 @@
225 225 ;; direct translation does not work
226 226 ;; because of the subtraction constraints
227 227 ;; also, some domain inference would be nice
228   -
  228 +
229 229 (defne noattackfd [y ys d]
230 230 ([_ () _])
231 231 ([y1 [y2 . yr] d]
@@ -365,13 +365,13 @@
365 365 ;; ~1200ms, a little bit slower w/ distribute step
366 366 (dotimes [_ 5]
367 367 (time
368   - (dotimes [_ 100]
  368 + (dotimes [_ 100]
369 369 (cryptarithfd-1))))
370 370
371 371 ;; 3X slower still
372 372 (dotimes [_ 5]
373 373 (time
374   - (dotimes [_ 10]
  374 + (dotimes [_ 10]
375 375 (cryptarithfd-1))))
376 376
377 377 ;; WORKS: takes a long time ([5 2 6 4 8 1 9 7 3 0])
@@ -436,7 +436,7 @@
436 436 (everyg #(infd % (interval 1 5)) vs)
437 437 (!=fd baker 5) (!=fd cooper 1)
438 438 (!=fd fletcher 5) (!=fd fletcher 1)
439   - (<fd cooper miller)
  439 + (<fd cooper miller)
440 440 (not-adjacento smith fletcher)
441 441 (not-adjacento fletcher cooper)))))
442 442
@@ -494,9 +494,9 @@
494 494 ;; 620ms
495 495 (dotimes [_ 10]
496 496 (time
497   - (dotimes [_ 1e3]
  497 + (dotimes [_ 1e3]
498 498 (simple-eqfd))))
499   -
  499 +
500 500 (run* [q]
501 501 (fresh [a b]
502 502 (*fd a 3 34)
@@ -554,7 +554,7 @@
554 554 (defn matches [n]
555 555 (run 1 [q]
556 556 (fresh [a b c d]
557   - (infd a b c d (interval 1 n))
  557 + (infd a b c d (interval 1 n))
558 558 (distinctfd [a b c d])
559 559 (== a 1)
560 560 (<=fd a b) (<=fd b c) (<=fd c d)
@@ -614,7 +614,7 @@
614 614 ;; 2100ms
615 615 (dotimes [_ 10]
616 616 (time
617   - (dotimes [_ 1e3]
  617 + (dotimes [_ 1e3]
618 618 (small-sudokufd))))
619 619
620 620 (small-sudokufd)
@@ -650,7 +650,7 @@
650 650 (get-square rows x y)))
651 651
652 652 (defn sudokufd [hints]
653   - (let [vars (repeatedly 81 lvar)
  653 + (let [vars (repeatedly 81 lvar)
654 654 rows (->rows vars)
655 655 cols (->cols rows)
656 656 sqs (->squares rows)]
@@ -719,10 +719,10 @@
719 719 3 0 1 0 0 7 0 4 0
720 720 7 2 0 0 4 0 0 6 0
721 721 0 0 4 0 1 0 0 0 3])
722   -
  722 +
723 723 (sudokufd easy0)
724 724 (time (sudokufd easy0))
725   -
  725 +
726 726 (sudokufd easy1)
727 727 (time (sudokufd easy1))
728 728
@@ -777,7 +777,7 @@
777 777 0 0 0 0 9 0 2 0 0
778 778 0 0 8 0 7 0 4 0 0
779 779 0 0 3 0 6 0 0 0 0
780   -
  780 +
781 781 0 1 0 0 0 2 8 9 0
782 782 0 4 0 0 0 0 0 0 0
783 783 0 5 0 1 0 0 0 0 0])
@@ -854,6 +854,6 @@
854 854 ;; 2800ms
855 855 (dotimes [_ 5]
856 856 (time
857   - (dotimes [_ 100]
  857 + (dotimes [_ 100]
858 858 (safefd))))
859   - )
  859 + )
68 src/main/clojure/clojure/core/logic/par.clj
... ... @@ -0,0 +1,68 @@
  1 +(ns clojure.core.logic.par
  2 + (:refer-clojure :exclude [==])
  3 + (use clojure.core.logic))
  4 +
  5 +;; fork-join wrapper from clojure.reducer
  6 +
  7 +(defmacro ^:private compile-if
  8 + [exp then else]
  9 + (if (try (eval exp)
  10 + (catch Throwable _ false))
  11 + `(do ~then)
  12 + `(do ~else)))
  13 +
  14 +(compile-if
  15 + (Class/forName "java.util.concurrent.ForkJoinTask")
  16 + ;; We're running a JDK 7+
  17 + (do
  18 + (def pool (delay (java.util.concurrent.ForkJoinPool.)))
  19 +
  20 + (defn- fjtask [^Callable f]
  21 + (java.util.concurrent.ForkJoinTask/adapt f))
  22 +
  23 + (defn- fjinvoke [f]
  24 + (if (java.util.concurrent.ForkJoinTask/inForkJoinPool)
  25 + (f)
  26 + (.invoke ^java.util.concurrent.ForkJoinPool @pool ^java.util.concurrent.ForkJoinTask (fjtask f))))
  27 +
  28 + (defn- fjfork [task] (.fork ^java.util.concurrent.ForkJoinTask task))
  29 +
  30 + (defn- fjjoin [task] (.join ^java.util.concurrent.ForkJoinTask task)))
  31 + ;; We're running a JDK <7
  32 + (do
  33 + (def pool (delay (jsr166y.ForkJoinPool.)))
  34 +
  35 + (defn- fjtask [^Callable f]
  36 + (jsr166y.ForkJoinTask/adapt f))
  37 +
  38 + (defn- fjinvoke [f]
  39 + (if (jsr166y.ForkJoinTask/inForkJoinPool)
  40 + (f)
  41 + (.invoke ^jsr166y.ForkJoinPool @pool ^jsr166y.ForkJoinTask (fjtask f))))
  42 +
  43 + (defn- fjfork [task] (.fork ^jsr166y.ForkJoinTask task))
  44 +
  45 + (defn- fjjoin [task] (.join ^jsr166y.ForkJoinTask task))))
  46 +
  47 +;; parallel solvers
  48 +
  49 +(declare dfs-par)
  50 +
  51 +(defn dfs-par*
  52 + ([]
  53 + nil)
  54 + ([node]
  55 + (dfs-par node))
  56 + [[node-a node-b]
  57 + (let [task-b (fjfork (fjtask #(dfs-par node-b)))
  58 + results-a (dfs-par node-a)
  59 + results-b (fjjoin task-b)]
  60 + (concat results-a results-b))])
  61 +
  62 +(defn dfs-par [node]
  63 + (fjinvoke
  64 + #(if (leaf? node)
  65 + (list (value node))
  66 + (apply dfs-par* (children node)))))
  67 +
  68 +;; TODO bfs-par
52 src/test/clojure/clojure/core/logic/tests.clj
@@ -443,6 +443,24 @@
443 443 '(true))))
444 444
445 445 ;; =============================================================================
  446 +;; Fair conjuctions
  447 +
  448 +(def endlesso
  449 + (fresh [] endlesso))
  450 +
  451 +(deftest test-all-fair
  452 + (is (= (run* [q]
  453 + (all-fair
  454 + endlesso
  455 + u#))
  456 + ()))
  457 + (is (= (run* [q]
  458 + (all-fair
  459 + u#
  460 + endlesso))
  461 + ())))
  462 +
  463 +;; =============================================================================
446 464 ;; TRS
447 465
448 466 (defn pairo [p]
@@ -703,7 +721,7 @@
703 721 (fresh []
704 722 (conde
705 723 [f2 (conde
706   - [f2]
  724 + [f2]
707 725 [(== false false)])]
708 726 [(== false false)])))
709 727
@@ -768,16 +786,10 @@
768 786 ;; -----------------------------------------------------------------------------
769 787 ;; condu (committed-choice)
770 788
771   -(comment
772   - (defn onceo [g]
773   - (condu
774   - (g s#)))
775   -
776   - (deftest test-condu-1
777   - (is (= (run* [x]
778   - (onceo (teacupo x)))
779   - '(tea))))
780   - )
  789 +(deftest test-condu-1
  790 + (is (= (run* [x]
  791 + (onceo (teacupo x)))
  792 + '(tea))))
781 793
782 794 (deftest test-condu-2
783 795 (is (= (into #{}
@@ -1210,7 +1222,7 @@
1210 1222 ;; -----------------------------------------------------------------------------
1211 1223 ;; Pattern matching functions preserve metadata
1212 1224
1213   -(defne ^:tabled dummy
  1225 +(defne ^:tabled dummy
1214 1226 "Docstring"
1215 1227 [x l]
1216 1228 ([_ [x . tail]])
@@ -1570,7 +1582,7 @@
1570 1582 (is (= (intersection mi0 7) 7))
1571 1583 (is (= (intersection 7 mi0) 7))))
1572 1584
1573   -;; |-----|
  1585 +;; |-----|
1574 1586 ;; |-----|
1575 1587 (deftest test-intersection-mimi-3
1576 1588 (let [mi0 (multi-interval (interval 1 4) (interval 7 10))]
@@ -1628,7 +1640,7 @@
1628 1640 (multi-interval (interval 1 4) (interval 6 8))))))
1629 1641
1630 1642 ;; |---| |---|
1631   -;; N
  1643 +;; N