fix: fixed equivalence evaluation by setting up bijection between the two formulas atoms

Author: ashwin6-dev

evaluation_function/domain/evaluators.py

@@ -1,4 +1,4 @@
-from itertools import product
+from itertools import product, permutations
 from typing import Mapping, Set
 from .formula import (
     Formula,
@@ -71,6 +71,8 @@ def _extract_atoms(formula: Formula) -> Set[Atom]:
 
 
 class EquivalenceEvaluator:
+    """Checks if two formulas are equivalent up to renaming of atoms (so e.g. 's' and 'p' are equivalent)."""
+
     def __init__(self, formula1: Formula, formula2: Formula):
         self._formula1 = formula1
         self._formula2 = formula2
@@ -80,27 +82,41 @@ def evaluate(self) -> bool:
         return ok
 
     def evaluate_with_counterexample(self) -> tuple[bool, dict | None]:
-        """Returns (are_equivalent, counterexample_or_none). Counterexample has assignment, response_value, expected_value."""
-        atoms1 = _extract_atoms(self._formula1)
-        atoms2 = _extract_atoms(self._formula2)
-        all_atoms = list(atoms1 | atoms2)
-
-        for assignment_values in product([False, True], repeat=len(all_atoms)):
-            assignment_dict = {atom: val for atom, val in zip(all_atoms, assignment_values)}
-            assignment = Assignment(assignment_dict)
-
-            evaluator1 = FormulaEvaluator(self._formula1, assignment)
-            evaluator2 = FormulaEvaluator(self._formula2, assignment)
-            v1, v2 = evaluator1.evaluate(), evaluator2.evaluate()
-
-            if v1 != v2:
-                assignment_str = {atom.name: val for atom, val in assignment_dict.items()}
-                return False, {
-                    "assignment": assignment_str,
-                    "response_value": v1,
-                    "expected_value": v2,
-                }
-        return True, None
+        """Returns (are_equivalent, counterexample_or_none). Equivalent = same truth behaviour under some renaming of atoms."""
+        atoms1 = sorted(_extract_atoms(self._formula1), key=lambda a: a.name)
+        atoms2 = sorted(_extract_atoms(self._formula2), key=lambda a: a.name)
+
+        if len(atoms1) != len(atoms2):
+            return False, {
+                "assignment": {},
+                "response_value": None,
+                "expected_value": None,
+                "reason": f"different number of atoms: {len(atoms1)} vs {len(atoms2)}",
+            }
+
+        n = len(atoms1)
+        first_counterexample = None
+        for perm in permutations(range(n)):
+            # perm[j] = index in atoms2 that atoms1[j] is renamed to; so atoms1[j] gets value of atoms2[perm[j]]
+            for assignment_values in product([False, True], repeat=n):
+                assignment2_dict = {atoms2[i]: assignment_values[i] for i in range(n)}
+                assignment1_dict = {atoms1[j]: assignment_values[perm[j]] for j in range(n)}
+                a1 = Assignment(assignment1_dict)
+                a2 = Assignment(assignment2_dict)
+                v1 = FormulaEvaluator(self._formula1, a1).evaluate()
+                v2 = FormulaEvaluator(self._formula2, a2).evaluate()
+                if v1 != v2:
+                    if first_counterexample is None:
+                        first_counterexample = {
+                            "assignment": {atoms2[i].name: assignment_values[i] for i in range(n)},
+                            "response_value": v1,
+                            "expected_value": v2,
+                        }
+                    break
+            else:
+                return True, None
+
+        return False, first_counterexample
 
 
 class SatisfiabilityEvaluator:

evaluation_function/evaluation.py

@@ -126,11 +126,14 @@ def evaluation_function(
                     f"Comparing your formula \"{response_formula}\" with expected \"{equivalent}\". They are not equivalent."
                 ))
                 if counterex:
-                    asn = ", ".join(f"{k}={counterex['assignment'][k]}" for k in sorted(counterex["assignment"]))
-                    feedback.append((
-                        "counterexample",
-                        f"Under assignment ({asn}): your formula = {counterex['response_value']}, expected formula = {counterex['expected_value']}."
-                    ))
+                    if counterex.get("reason"):
+                        feedback.append(("counterexample", counterex["reason"]))
+                    elif counterex.get("assignment") is not None:
+                        asn = ", ".join(f"{k}={counterex['assignment'][k]}" for k in sorted(counterex["assignment"]))
+                        feedback.append((
+                            "counterexample",
+                            f"Under assignment ({asn}): your formula = {counterex['response_value']}, expected formula = {counterex['expected_value']}."
+                        ))
         elif tautology:
             ev = TautologyEvaluator(formula)
             is_correct, counterex = ev.evaluate_with_counterexample()

evaluation_function/evaluation_test.py

@@ -32,7 +32,7 @@ def test_evaluation_default(self):
 
     def test_check_tautology(self):
         response = {"formula": "p ∨ ¬p"}
-        answer = {"satisability": False, "tautology": True, "equivalent": None, "truthTable": None}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
         params = Params()
 
         result = evaluation_function(response, answer, params).to_dict()
@@ -41,7 +41,7 @@ def test_check_tautology(self):
 
     def test_check_tautology_fail(self):
         response = {"formula": "p ∧ ¬p"}
-        answer = {"satisability": False, "tautology": True, "equivalent": None, "truthTable": None}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
         params = Params()
 
         result = evaluation_function(response, answer, params).to_dict()
@@ -84,6 +84,16 @@ def test_check_equivalence_fail(self):
 
         self.assertFalse(result.get("is_correct"))
 
+    def test_check_equivalence_different_atoms(self):
+        """Formulas with same structure but different atom names (e.g. 's' vs 'p') are equivalent up to renaming."""
+        response = {"formula": "s"}
+        answer = {"satisfiability": False, "tautology": False, "equivalent": "p", "validTruthTable": False}
+        params = Params()
+
+        result = evaluation_function(response, answer, params).to_dict()
+
+        self.assertTrue(result.get("is_correct"))
+
     def test_truth_table_valid(self):
         response = {
             "formula": "p ∧ q",
@@ -126,7 +136,7 @@ def test_truth_table_invalid(self):
 
     def test_invalid_response_type(self):
         response = "just a string"  # Invalid type
-        answer = {"satisability": False, "tautology": True, "equivalent": None, "truthTable": None}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
         params = Params()
 
         result = evaluation_function(response, answer, params).to_dict()
@@ -136,7 +146,7 @@ def test_invalid_response_type(self):
 
     def test_missing_formula_field(self):
         response = {"wrongField": "p"}
-        answer = {"satisability": False, "tautology": True, "equivalent": None, "truthTable": None}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
         params = Params()
 
         result = evaluation_function(response, answer, params).to_dict()
@@ -161,3 +171,181 @@ def test_multiple_params_selected(self):
 
         self.assertFalse(result.get("is_correct"))
 
+    # --- Equivalence (extra) ---
+
+    def test_equivalence_same_structure_three_atoms(self):
+        """Same structure with different atom names: (a ∧ b) ∧ c vs (p ∧ q) ∧ r."""
+        response = {"formula": "(a ∧ b) ∧ c"}
+        answer = {"satisfiability": False, "tautology": False, "equivalent": "(p ∧ q) ∧ r", "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+
+    def test_equivalence_different_number_of_atoms(self):
+        """Single atom vs binary: not equivalent (different structure)."""
+        response = {"formula": "p"}
+        answer = {"satisfiability": False, "tautology": False, "equivalent": "p ∧ q", "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+        self.assertIn("feedback", result)
+
+    def test_equivalence_negation_same_structure(self):
+        """¬s vs ¬p: equivalent up to renaming."""
+        response = {"formula": "¬s"}
+        answer = {"satisfiability": False, "tautology": False, "equivalent": "¬p", "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+
+    def test_equivalence_implication_same_structure(self):
+        """a → b vs p → q: equivalent up to renaming."""
+        response = {"formula": "a → b"}
+        answer = {"satisfiability": False, "tautology": False, "equivalent": "p → q", "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+
+    def test_equivalence_failure_includes_feedback(self):
+        """When equivalence fails, feedback should mention formulas and counterexample."""
+        response = {"formula": "p ∨ q"}
+        answer = {"satisfiability": False, "tautology": False, "equivalent": "p ∧ q", "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+        feedback = result.get("feedback_items", result.get("feedback", []))
+        feedback_str = str(feedback).lower()
+        self.assertTrue("equivalent" in feedback_str or "formula" in feedback_str or "counterexample" in feedback_str)
+
+    # --- Tautology (extra) ---
+
+    def test_tautology_implication_self(self):
+        """p → p is a tautology."""
+        response = {"formula": "p → p"}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+
+    def test_tautology_fail_single_atom(self):
+        """Single atom p is not a tautology."""
+        response = {"formula": "p"}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+
+    def test_tautology_failure_includes_feedback(self):
+        """Tautology failure should include feedback."""
+        response = {"formula": "p"}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+        self.assertIn("feedback", result)
+
+    # --- Satisfiability (extra) ---
+
+    def test_satisfiability_disjunction(self):
+        """p ∨ q is satisfiable."""
+        response = {"formula": "p ∨ q"}
+        answer = {"satisfiability": True, "tautology": False, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+
+    def test_satisfiability_failure_includes_feedback(self):
+        """Unsatisfiable formula should return False and include feedback."""
+        response = {"formula": "p ∧ ¬p"}
+        answer = {"satisfiability": True, "tautology": False, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+        self.assertIn("feedback", result)
+
+    # --- Truth table (extra) ---
+
+    def test_truth_table_required_but_missing(self):
+        """When answer expects truth table but response has no truthTable, should fail."""
+        response = {"formula": "p ∧ q"}
+        answer = {"satisfiability": False, "tautology": False, "equivalent": None, "validTruthTable": True}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+
+    def test_truth_table_single_atom(self):
+        """Truth table for single atom p: 2 rows."""
+        response = {
+            "formula": "p",
+            "truthTable": {
+                "variables": ["p"],
+                "cells": [["tt"], ["ff"]]
+            }
+        }
+        answer = {"satisfiability": False, "tautology": False, "equivalent": None, "validTruthTable": True}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+
+    def test_truth_table_invalid_cell_token(self):
+        """Cell value that is not tt/ff should fail."""
+        response = {
+            "formula": "p",
+            "truthTable": {
+                "variables": ["p"],
+                "cells": [["tt"], ["invalid"]]
+            }
+        }
+        answer = {"satisfiability": False, "tautology": False, "equivalent": None, "validTruthTable": True}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+
+    def test_truth_table_missing_combinations(self):
+        """Only one row for two atoms should fail (missing combinations)."""
+        response = {
+            "formula": "p ∧ q",
+            "truthTable": {
+                "variables": ["p", "q", "p ∧ q"],
+                "cells": [["tt", "tt", "tt"]]
+            }
+        }
+        answer = {"satisfiability": False, "tautology": False, "equivalent": None, "validTruthTable": True}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+
+    # --- Input / validation (extra) ---
+
+    def test_answer_not_dict(self):
+        """Answer must be a dict; string answer gives incorrect."""
+        response = {"formula": "p"}
+        answer = 42
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+
+    def test_response_as_json_string(self):
+        """Response can be a JSON string (parsed before use)."""
+        response = '{"formula": "p ∨ ¬p"}'
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+
+    def test_formula_not_string(self):
+        """Response formula must be a string."""
+        response = {"formula": 123}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertFalse(result.get("is_correct"))
+
+    def test_truth_table_mode_with_truth_table_false(self):
+        """validTruthTable False means we are not in truth table mode."""
+        response = {"formula": "p ∨ ¬p"}
+        answer = {"satisfiability": False, "tautology": True, "equivalent": None, "validTruthTable": False}
+        params = Params()
+        result = evaluation_function(response, answer, params).to_dict()
+        self.assertTrue(result.get("is_correct"))
+