Merge pull request #17 from QuMuLab/memoization

Memoization and other optimizations and fixes

Author: blyxxyz

.travis.yml

@@ -8,7 +8,9 @@ python:
   - "3.6"
   - "3.7"
   - "3.8"
+  - "3.9-dev"
   - "pypy3.5"
+  - "pypy3"
 
 install:
   - pip install tox-travis

CONTRIBUTING.md

@@ -1,10 +1,82 @@
 # Contributing to python-nnf
 
-More information coming soon.
+## Running the tests and linters
 
-## Notes for now
+[`tox`](https://tox.readthedocs.io/en/latest/) is used to run the tests and linters. After installing it, run:
 
-- `tox -e py3`
-- Set notation for Internal nodes (rather than lists)
-- Use of `@memoize`
-- Use of Typing / mypy
+```
+tox
+```
+
+This will install and run all the tooling.
+
+`tox` aborts early if one of the steps fails. To run just the tests (for example if you can't get `mypy` to work), install and run [`pytest`](https://docs.pytest.org/en/latest/getting-started.html). To run just one particular test, run `pytest -k <name of test>`.
+
+## Mypy
+
+[Mypy](https://mypy.readthedocs.io/en/stable/) is used for static typing. This is also managed by `tox`.
+
+You can look at the existing code for cues. If you can't figure it out, just leave it be and we'll look at it during code review.
+
+## Hypothesis
+
+[Hypothesis](https://hypothesis.readthedocs.io/en/latest/) is used for property-based testing: it generates random sentences for tests to use. See the existing tests for examples.
+
+It's ideal for a feature to have both tests that do use Hypothesis and tests that don't.
+
+## Memoization
+
+[Memoization](https://en.wikipedia.org/wiki/Memoization) is used in various places to avoid computing the same thing multiple times. A memoized function remembers past calls so it can return the same return value again in the future.
+
+A downside of memoization is that it increases memory usage.
+
+It's used in two patterns throughout the codebase:
+
+### Temporary internal memoization with `@memoize`
+
+This is used for functions that run on individual nodes of sentences, within a method. For example:
+
+```python
+    def height(self) -> int:
+        """The number of edges between here and the furthest leaf."""
+        @memoize
+        def height(node: NNF) -> int:
+            if isinstance(node, Internal) and node.children:
+                return 1 + max(height(child) for child in node.children)
+            return 0
+
+        return height(self)
+```
+
+Because the function is defined inside the method, it's garbage collected along with its cache when the method returns. This makes sure we don't keep all the individual node heights in memory indefinitely.
+
+### Memoizing sentence properties with `@weakref_memoize`
+
+This is used for commonly used methods that run on whole sentences. For example:
+
+```python
+    @weakref_memoize
+    def vars(self) -> t.FrozenSet[Name]:
+        """The names of all variables that appear in the sentence."""
+        return frozenset(node.name
+                         for node in self.walk()
+                         if isinstance(node, Var))
+```
+
+This lets us call `.vars()` often without worrying about performance.
+
+Unlike the other decorator, this one uses `weakref`, so it doesn't interfere with garbage collection. It's slightly less efficient though, so the temporary functions from the previous section are better off with `@memoize`.
+
+## Documentation
+
+Methods are documented with reStructuredText inside docstrings. This looks a little like markdown, but it's different, so take care and look at other docstrings for examples.
+
+Documentation is automatically generated and ends up at [Read the Docs](https://python-nnf.readthedocs.io/en/latest/).
+
+To build the documentation locally, run `make html` inside the `docs/` directory. This generates a manual in `docs/_build/html/`.
+
+New modules have to be added to `docs/nnf.rst` to be documented.
+
+## Style/miscellaneous
+
+- Prefer sets over lists where it make sense. For example, `Or({~c for c in children} | {aux})` instead of `Or([~c for c in children] + [aux])`.

docs/caveats.rst

@@ -44,11 +44,11 @@ Decomposability and determinism
 
 A lot of methods are much faster to perform on sentences that are decomposable or deterministic, such as model enumeration.
 
-Decomposability is automatically detected. However, you can skip the check if you already know whether the sentence is decomposable or not, by passing ``decomposable=True`` or ``decomposable=False`` as a keyword argument.
+Decomposability is automatically detected.
 
-Determinism is too expensive to automatically detect, but it can give a huge speedup. If you know a sentence to be deterministic, pass ``deterministic=True`` as a keyword argument to take advantage.
+Determinism is too expensive to automatically detect, but it can give a huge speedup. If you know a sentence to be deterministic, run ``.mark_deterministic()`` to enable the relevant optimizations.
 
-A compiler like `DSHARP <https://github.com/QuMuLab/dsharp>`_ may be able to convert some sentences into equivalent deterministic decomposable sentences. The output of DSHARP can be loaded using the :mod:`nnf.dsharp` module.
+A compiler like `DSHARP <https://github.com/QuMuLab/dsharp>`_ may be able to convert some sentences into equivalent deterministic decomposable sentences. The output of DSHARP can be loaded using the :mod:`nnf.dsharp` module. Sentences returned by :func:`nnf.dsharp.compile` are automatically marked as deterministic.
 
 Other duplication inefficiencies
 --------------------------------

examples/socialchoice.py

@@ -4,11 +4,10 @@
 import functools
 import itertools
 
-import nnf
+from nnf import amc, And, Or, Var, true, false
 
-from nnf import amc, And, Or, Var
-
-memoize = functools.lru_cache(None)  # huge speedup
+# Cache generated nodes
+memoize = functools.lru_cache(None)
 
 
 def powerset(iterable):
@@ -21,8 +20,6 @@ def powerset(iterable):
 
 def lin(candidates):
     # candidates must be hashable, have total ordering
-    builder = nnf.Builder()
-
     candidates = frozenset(candidates)
     n = len(candidates)
     T = frozenset(powerset(candidates))
@@ -32,25 +29,24 @@ def lin(candidates):
     def defeats(i, j):
         assert i != j
         if i < j:
-            return builder.Var((i, j))
+            return Var((i, j))
         else:
-            return builder.Var((j, i), False)
+            return Var((j, i), False)
 
     @memoize
     def C(S):
         if S == candidates:
-            return builder.true
+            return true
 
-        return builder.Or(C_child(i, S)
-                          for i in candidates - S)
+        return Or(C_child(i, S) for i in candidates - S)
 
     @memoize
     def C_child(i, S):
         children = {C(S | {i})}
         children.update(defeats(i, j)
                         for j in candidates - S
                         if i != j)
-        return builder.And(children)
+        return And(children)
 
     return C(frozenset())
 
@@ -81,17 +77,17 @@ def order_to_model(order):
 def kemeny(votes):
     labels = collections.Counter()
     for vote in votes:
-        for name, true in order_to_model(vote).items():
-            labels[nnf.Var(name, true)] += 1
+        for name, truthiness in order_to_model(vote).items():
+            labels[Var(name, truthiness)] += 1
     return {model_to_order(model)
             for model in amc.maxplus_reduce(lin(votes[0]), labels).models()}
 
 
 def slater(votes):
     totals = collections.Counter()
     for vote in votes:
-        for name, true in order_to_model(vote).items():
-            totals[nnf.Var(name, true)] += 1
+        for name, truthiness in order_to_model(vote).items():
+            totals[Var(name, truthiness)] += 1
     labels = {}
     for var in totals:
         labels[var] = 1 if totals[var] > totals[~var] else 0
@@ -143,7 +139,7 @@ def test():
     s_3 = s.condition({(0, 1): True, (1, 2): True, (0, 2): False})
     assert len(list(s_3.models())) == 0
     assert not s_3.satisfiable()
-    assert s_3.simplify() == nnf.false
+    assert s_3.simplify() == false
 
     # strings as candidates
     named = lin({"Alice", "Bob", "Carol"})

mypy.ini

@@ -0,0 +1,3 @@
+# -*- conf -*-
+[mypy]
+strict = True