Adding a complete_models method.

Author: haz

nnf/__init__.py

@@ -590,7 +590,7 @@ def neg(node: NNF) -> NNF:
 
         return neg(self)
 
-    def to_CNF(self: T_NNF) -> 'And[Or[Var]]':
+    def to_CNF(self) -> 'And[Or[Var]]':
         """Compile theory to a semantically equivalent CNF formula."""
         from nnf import tseitin
         return tseitin.to_CNF(self)
@@ -1567,6 +1567,20 @@ def map(self, func: t.Callable[[T_NNF_co], U_NNF]) -> 'Or[U_NNF]':
             ...
 
 
+def complete_models(
+        models: t.Iterable[Model],
+        names: t.FrozenSet[Name]
+) -> t.Iterator[Model]:
+    diff = None
+    for model in models:
+        if diff is None:
+            diff = names - model.keys()
+        for supplement in all_models(diff):
+            new = model.copy()
+            new.update(supplement)
+            yield new
+
+
 def decision(
         var: Var,
         if_true: T_NNF,

test_nnf.py

@@ -12,7 +12,8 @@
 
 import nnf
 
-from nnf import Var, And, Or, amc, dimacs, dsharp, operators, tseitin
+from nnf import Var, And, Or, amc, dimacs, dsharp, operators, \
+                tseitin, complete_models
 
 settings.register_profile('patient', deadline=2000,
                           suppress_health_check=(HealthCheck.too_slow,))
@@ -766,14 +767,24 @@ def test_tseitin(sentence: nnf.NNF):
     assert T.is_CNF()
 
     # Only do the following checks when we haven't simplified away some vars
-    assume(sentence.vars() <= T.vars())
+    # assume(sentence.vars() <= T.vars())
 
     # 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)
 
+    models = list(complete_models(T.models(), sentence.vars() | T.vars()))
+
     for mt in T.models():
         assert sentence.satisfied_by(mt)
 
     assert T.model_count() == sentence.model_count()
+
+@given(models())
+def test_complete_models(model: nnf.And[nnf.Var]):
+    t0, t1, t2 = [], ['test1'], ['test1', 'test2']
+    m = {v.name: v.true for v in model}
+    assert 1 == len(list(complete_models([m], list(m.keys())+t0)))
+    assert 2 == len(list(complete_models([m], list(m.keys())+t1)))
+    assert 4 == len(list(complete_models([m], list(m.keys())+t2)))