Fix semantic equivalence check in code

Author: v--

src/notebook/math/logic/propositional/sat.py

@@ -8,8 +8,8 @@
 from .variables import get_propositional_variables
 
 
-def iter_interpretations(formula: Formula) -> Iterable[PropositionalInterpretation]:
-    variables = sorted(get_propositional_variables(formula))
+def iter_interpretations(*formulas: Formula) -> Iterable[PropositionalInterpretation]:
+    variables = sorted(var for formula in formulas for var in get_propositional_variables(formula))
 
     for spec in product([True, False], repeat=len(variables)):
         yield PropositionalInterpretation(dict(zip(variables, spec, strict=True)))
@@ -39,15 +39,8 @@ def is_contradiction(formula: Formula) -> bool:
 
 
 def are_semantically_equivalent(first: Formula, second: Formula) -> bool:
-    for interp in iter_interpretations(first):
-        try:
-            eval_second = evaluate_propositional_formula(second, interp)
-        except MissingInterpretationError:
-            return False
-
-        eval_first = evaluate_propositional_formula(first, interp)
-
-        if eval_first != eval_second:
+    for interp in iter_interpretations(first, second):
+        if evaluate_propositional_formula(first, interp) != evaluate_propositional_formula(second, interp):
             return False
 
     return True

src/notebook/math/logic/transformation/test_constants.py

@@ -1,5 +1,5 @@
 from ....support.pytest import pytest_parametrize_kwargs
-from ..propositional import are_equisatisfiable, parse_propositional_formula
+from ..propositional import are_equisatisfiable, are_semantically_equivalent, parse_propositional_formula
 from .constants import collapse_constants, expand_constants
 
 
@@ -12,7 +12,7 @@
 def test_expand_constants(formula: str, expected: str) -> None:
     formula_ = parse_propositional_formula(formula)
     expected_ = parse_propositional_formula(expected)
-    assert are_equisatisfiable(formula_, expected_)
+    assert are_semantically_equivalent(formula_, expected_)
 
     expanded = expand_constants(formula_)
     assert expanded == expected_