Skip to content

Commit

Permalink
Adding extra test for name preservation, and fixed bug for bottom cla…
Browse files Browse the repository at this point in the history
…uses.
  • Loading branch information
haz committed Dec 9, 2022
1 parent 1523e8a commit 21ff041
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 1 deletion.
2 changes: 1 addition & 1 deletion nnf/tseitin.py
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ def process_node(node: NNF) -> Var:

aux = Var.aux()

if any(~var in children for var in children):
if simplify_tautologies and any(~var in children for var in children):
if isinstance(node, And):
clauses.append(Or({~aux}))
else:
Expand Down
8 changes: 8 additions & 0 deletions test_nnf.py
Original file line number Diff line number Diff line change
Expand Up @@ -1107,6 +1107,14 @@ def test_models(sentence: nnf.NNF):
assert model_set(real_models) == model_set(models)


@given(NNF())
def test_tautology_simplification_names(sentence: nnf.NNF):
names1 = set(sentence.vars())
T = sentence.to_CNF(simplify_tautologies=False)
names2 = set({v for v in T.vars() if not isinstance(v, nnf.Aux)})
assert names1 == names2


def test_tautology_simplification():
x = Var("x")
T = x | ~x
Expand Down

0 comments on commit 21ff041

Please sign in to comment.