Forgetting/projection.

nnf/__init__.py

@@ -998,6 +998,53 @@ def pair(node: NNF) -> NNF:
 
         return pair(sentence)
 
+    def project(self, names: 't.Iterable[Name]') -> 'NNF':
+        """Dual of :meth:`forget`: will forget all variables not given"""
+        return self.forget(self.vars() - frozenset(names))
+
+    def forget_aux(self) -> 'NNF':
+        """Returns a theory that forgets all of the auxillary variables"""
+        return self.forget(v for v in self.vars() if isinstance(v, Aux))
+
+    def forget(self, names: 't.Iterable[Name]') -> 'NNF':
+        """Forget a set of variables from the theory.
+
+        Has the effect of returning a theory without the variables provided,
+        such that every model of the new theory has an extension (i.e., an
+        assignment) to the forgotten variables that is a model of the original
+        theory.
+
+        :param names: An iterable of the variable names to be forgotten
+        """
+
+        if self.decomposable():
+            return self._forget_with_subs(names)
+        else:
+            return self._forget_with_shannon(names)
+
+    def _forget_with_subs(self, names: 't.Iterable[Name]') -> 'NNF':
+
+        names = frozenset(names)
+
+        @memoize
+        def forget_recurse(node: NNF) -> NNF:
+            if isinstance(node, Var) and node.name in names:
+                return true
+            elif isinstance(node, Var):
+                return node
+            elif isinstance(node, Internal):
+                return node.map(forget_recurse)
+            else:
+                raise TypeError(node)
+
+        return forget_recurse(self).simplify()
+
+    def _forget_with_shannon(self, names: 't.Iterable[Name]') -> 'NNF':
+        T = self
+        for v in frozenset(names) & self.vars():
+            T = T.condition({v: True}) | T.condition({v: False})
+        return T.simplify()
+
     def deduplicate(self: T_NNF) -> T_NNF:
         """Return a copy of the sentence without any duplicate objects.
 

test_nnf.py

@@ -733,6 +733,36 @@ def test_iff(a: nnf.NNF, b: nnf.NNF):
                 c.satisfied_by(model))
 
 
+@given(NNF())
+def test_forget(sentence: nnf.NNF):
+    # Assumption to reduce the time in testing
+    assume(sentence.size() <= 15)
+
+    # Test that forgetting a backbone variable doesn't change the theory
+    T = sentence & Var('added_var')
+    assert sentence.equivalent(T.forget({'added_var'}))
+
+    # Test the tseitin projection
+    assert sentence.equivalent(sentence.to_CNF().forget_aux())
+
+    # Test that models of a projected theory are consistent with the original
+    names = list(sentence.vars())[:2]
+    T = sentence.forget(names)
+    assert not any([v in T.vars() for v in names])
+
+    for m in T.models():
+        assert sentence.condition(m).satisfiable()
+
+
+@given(NNF())
+def test_project(sentence: nnf.NNF):
+    # Test that we get the same as projecting and forgetting
+    assume(len(sentence.vars()) > 3)
+    vars1 = list(sentence.vars())[:2]
+    vars2 = list(sentence.vars())[2:]
+    assert sentence.forget(vars1).equivalent(sentence.project(vars2))
+
+
 @given(NNF())
 def test_pickling(sentence: nnf.NNF):
     new = pickle.loads(pickle.dumps(sentence))
@@ -789,11 +819,7 @@ def test_tseitin(sentence: nnf.NNF):
 
     T = tseitin.to_CNF(sentence)
     assert T.is_CNF()
-
-    # TODO: Once forgetting/projection is implemented,
-    #       do this more complete check
-    # aux = filter(lambda x: 'aux' in str(x.name), T.vars())
-    # assert T.forget(aux).equivalent(sentence)
+    assert T.forget_aux().equivalent(sentence)
 
     models = list(complete_models(T.models(), sentence.vars() | T.vars()))