Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Forgetting/projection. #16

Merged
merged 4 commits into from
Aug 7, 2020
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 47 additions & 0 deletions nnf/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -998,6 +998,53 @@ def pair(node: NNF) -> NNF:

return pair(sentence)

def project(self: T_NNF, vars: 't.FrozenSet[Name]') -> 'NNF':
haz marked this conversation as resolved.
Show resolved Hide resolved
"""Dual of `forget`: will forget all of the variables not given"""
haz marked this conversation as resolved.
Show resolved Hide resolved
return self.forget(self.vars() - vars)

def forget_aux(self: T_NNF) -> 'NNF':
haz marked this conversation as resolved.
Show resolved Hide resolved
"""Returns a theory that forgets all of the auxillary variables"""
aux_vars = frozenset({v for v in self.vars() if isinstance(v, Aux)})
return self.forget(aux_vars)

def forget(self: T_NNF, vars: 't.FrozenSet[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 vars: A frozenset of the variable names to be forgotten
"""

if self.decomposable():
return self._forget_with_subs(vars)
else:
return self._forget_with_shannon(vars)

def _forget_with_subs(self: T_NNF, vars: 't.FrozenSet[Name]') -> 'NNF':

@memoize
def forget_recurse(node: NNF) -> NNF:
if isinstance(node, Var) and node.name in vars:
return true
elif isinstance(node, Var):
return node
elif isinstance(node, And) or isinstance(node, Or):
new_children = map(forget_recurse, node.children)
return node.__class__(new_children)
blyxxyz marked this conversation as resolved.
Show resolved Hide resolved
else:
raise TypeError(node)

return forget_recurse(self).simplify()

def _forget_with_shannon(self: T_NNF, vars: 't.FrozenSet[Name]') -> 'NNF':
T = self
for v in vars:
haz marked this conversation as resolved.
Show resolved Hide resolved
T = t.cast(T_NNF, T.condition({v: True}) | T.condition({v: False}))
haz marked this conversation as resolved.
Show resolved Hide resolved
return T.simplify()

def deduplicate(self: T_NNF) -> T_NNF:
"""Return a copy of the sentence without any duplicate objects.

Expand Down
35 changes: 30 additions & 5 deletions test_nnf.py
Original file line number Diff line number Diff line change
Expand Up @@ -733,6 +733,35 @@ def test_iff(a: nnf.NNF, b: nnf.NNF):
c.satisfied_by(model))


@given(NNF())
def test_forget(sentence: nnf.NNF):
haz marked this conversation as resolved.
Show resolved Hide resolved
# Test that forgetting a backbone variable doesn't change the theory
T = sentence & Var('added_var')
assert sentence.equivalent(T.forget({'added_var'}))

# Assumption to reduce the time in testing
assume(sentence.size() <= 15)
haz marked this conversation as resolved.
Show resolved Hide resolved

# Test the tseitin projection
assert sentence.equivalent(sentence.to_CNF().forget_aux())

# Test that models of a projected theory are consistent with the original
assume(len(sentence.vars()) > 2)
haz marked this conversation as resolved.
Show resolved Hide resolved
vars = list(sentence.vars())[:2]
T = sentence.forget(vars)
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 = frozenset(list(sentence.vars())[:2])
vars2 = frozenset(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))
Expand Down Expand Up @@ -789,11 +818,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()))

Expand Down