leborchuk commented on PR #1762: URL: https://github.com/apache/cloudberry/pull/1762#issuecomment-4778866970
Checked the 1st commit 7f13fc4fa537b7a96cbb156c74c719eb45092d5a for correctness - all Ok, the code is correct. What I checked. The focus was on function `convert_expr_to_cnf_complete`. We transform logical expression to simplified form, lets check the original equation and transformed one. The only known for me method is https://en.wikipedia.org/wiki/Karnaugh_map So we have the original expression, lets create Karnaugh map for it, then transform expression, again create Karnaugh map, compare maps, and also check if the transformed equation the same we could generate using rules for Karnaugh map. To do so I generate python code based on `prepqual.c`, manually checked generated code for correctness, and then launch code and see the results. Here the results (T1 and T2 are the same, I excluded T2 from comparison): ``` ###################################################################### TEST CASE 1: T1: (A AND B) OR (A AND C) ###################################################################### ============================================================ ORIGINAL: T1: (A AND B) OR (A AND C) Expression: ((A AND B) OR (A AND C)) Variables: ['A', 'B', 'C'] BC=00 BC=01 BC=11 BC=10 A=0: 0 0 0 0 A=1: 0 1 1 1 ============================================================ CNF RESULT Expression: (A AND (A OR C) AND (B OR A) AND (B OR C)) Variables: ['A', 'B', 'C'] BC=00 BC=01 BC=11 BC=10 A=0: 0 0 0 0 A=1: 0 1 1 1 Original truth table (bitvec): 11100000 CNF result truth table (bitvec): 11100000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 3: T3: (A∧B) ∨ (A∧C) ∨ (D∧B) ∨ (D∧C) ###################################################################### ============================================================ ORIGINAL: T3: (A∧B) ∨ (A∧C) ∨ (D∧B) ∨ (D∧C) Expression: ((A AND B) OR (A AND C) OR (D AND B) OR (D AND C)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 1 0 AB=01: 0 1 1 0 AB=11: 1 1 1 1 AB=10: 0 0 1 1 ============================================================ CNF RESULT Expression: ((A OR D) AND (B OR C)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 1 0 AB=01: 0 1 1 0 AB=11: 1 1 1 1 AB=10: 0 0 1 1 Original truth table (bitvec): 1111110010101000 CNF result truth table (bitvec): 1111110010101000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 4: T4: (A∨B) ∧ (C∨D) [already CNF] ###################################################################### ============================================================ ORIGINAL: T4: (A∨B) ∧ (C∨D) [already CNF] Expression: ((A OR B) AND (C OR D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 1 1 1 AB=11: 0 1 1 1 AB=10: 0 1 1 1 ============================================================ CNF RESULT Expression: ((A OR B) AND (C OR D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 1 1 1 AB=11: 0 1 1 1 AB=10: 0 1 1 1 Original truth table (bitvec): 1110111011100000 CNF result truth table (bitvec): 1110111011100000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 5: T5: A ∧ B ∧ C [trivial AND] ###################################################################### ============================================================ ORIGINAL: T5: A ∧ B ∧ C [trivial AND] Expression: (A AND B AND C) Variables: ['A', 'B', 'C'] BC=00 BC=01 BC=11 BC=10 A=0: 0 0 0 0 A=1: 0 0 1 0 ============================================================ CNF RESULT Expression: (A AND B AND C) Variables: ['A', 'B', 'C'] BC=00 BC=01 BC=11 BC=10 A=0: 0 0 0 0 A=1: 0 0 1 0 Original truth table (bitvec): 10000000 CNF result truth table (bitvec): 10000000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 6: T6: A ∨ B ∨ C [trivial OR] ###################################################################### ============================================================ ORIGINAL: T6: A ∨ B ∨ C [trivial OR] Expression: (A OR B OR C) Variables: ['A', 'B', 'C'] BC=00 BC=01 BC=11 BC=10 A=0: 0 1 1 1 A=1: 1 1 1 1 ============================================================ CNF RESULT Expression: (A OR B OR C) Variables: ['A', 'B', 'C'] BC=00 BC=01 BC=11 BC=10 A=0: 0 1 1 1 A=1: 1 1 1 1 Original truth table (bitvec): 11111110 CNF result truth table (bitvec): 11111110 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 7: T7: ((A∧B) ∨ C) ∧ D ###################################################################### ============================================================ ORIGINAL: T7: ((A∧B) ∨ C) ∧ D Expression: (((A AND B) OR C) AND D) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 1 0 AB=01: 0 0 1 0 AB=11: 0 1 1 0 AB=10: 0 0 1 0 ============================================================ CNF RESULT Expression: ((C OR A) AND (C OR B) AND D) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 1 0 AB=01: 0 0 1 0 AB=11: 0 1 1 0 AB=10: 0 0 1 0 Original truth table (bitvec): 1010100010001000 CNF result truth table (bitvec): 1010100010001000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 8: T8: (A∧B∧C) ∨ (A∧B∧D) ###################################################################### ============================================================ ORIGINAL: T8: (A∧B∧C) ∨ (A∧B∧D) Expression: ((A AND B AND C) OR (A AND B AND D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 0 0 0 AB=11: 0 1 1 1 AB=10: 0 0 0 0 ============================================================ CNF RESULT Expression: (A AND (A OR B) AND (A OR D) AND B AND (B OR D) AND (C OR A) AND (C OR B) AND (C OR D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 0 0 0 AB=11: 0 1 1 1 AB=10: 0 0 0 0 Original truth table (bitvec): 1110000000000000 CNF result truth table (bitvec): 1110000000000000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 9: T9: (A∧B) ∨ (A∧C) ∨ (A∧D) ###################################################################### ============================================================ ORIGINAL: T9: (A∧B) ∨ (A∧C) ∨ (A∧D) Expression: ((A AND B) OR (A AND C) OR (A AND D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 0 0 0 AB=11: 1 1 1 1 AB=10: 0 1 1 1 ============================================================ CNF RESULT Expression: (A AND (A OR D) AND (A OR C) AND (B OR A) AND (B OR C OR D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 0 0 0 AB=11: 1 1 1 1 AB=10: 0 1 1 1 Original truth table (bitvec): 1111111000000000 CNF result truth table (bitvec): 1111111000000000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ###################################################################### TEST CASE 10: T10: (A∧B∧C) ∨ (A∧B∧D) ∨ (¬A∧B∧C) ∨ (¬A∧B∧D) ###################################################################### ============================================================ ORIGINAL: T10: (A∧B∧C) ∨ (A∧B∧D) ∨ (¬A∧B∧C) ∨ (¬A∧B∧D) Expression: ((A AND B AND C) OR (A AND B AND D) OR (NOT(A) AND B AND C) OR (NOT(A) AND B AND D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 1 1 1 AB=11: 0 1 1 1 AB=10: 0 0 0 0 ============================================================ CNF RESULT Expression: ((A OR NOT(A)) AND (A OR B) AND (B OR NOT(A)) AND B AND (B OR D) AND (B OR C) AND (C OR D)) Variables: ['A', 'B', 'C', 'D'] CD=00 CD=01 CD=11 CD=10 AB=00: 0 0 0 0 AB=01: 0 1 1 1 AB=11: 0 1 1 1 AB=10: 0 0 0 0 Original truth table (bitvec): 1110000011100000 CNF result truth table (bitvec): 1110000011100000 Logically equivalent: YES ✓ In CNF form: yes Result: PASS ====================================================================== SUMMARY ====================================================================== # Status CNF? Description --- ------ -------------------- ------------------------------ 1 PASS yes T1: (A AND B) OR (A AND C) 3 PASS yes T3: (A∧B) ∨ (A∧C) ∨ (D∧B) ∨ (D∧C) 4 PASS yes T4: (A∨B) ∧ (C∨D) [already CNF] 5 PASS yes T5: A ∧ B ∧ C [trivial AND] 6 PASS yes T6: A ∨ B ∨ C [trivial OR] 7 PASS yes T7: ((A∧B) ∨ C) ∧ D 8 PASS yes T8: (A∧B∧C) ∨ (A∧B∧D) 9 PASS yes T9: (A∧B) ∨ (A∧C) ∨ (A∧D) 10 PASS yes T10: (A∧B∧C) ∨ (A∧B∧D) ∨ (¬A∧B∧C) ∨ (¬A∧B∧D) ================================================== CNF Conversion Results: ================================================== T1: (A AND (A OR C) AND (B OR A) AND (B OR C)) T3: ((A OR D) AND (B OR C)) T4: ((A OR B) AND (C OR D)) T5: (A AND B AND C) T6: (A OR B OR C) T7: ((C OR A) AND (C OR B) AND D) T8: (A AND (A OR B) AND (A OR D) AND B AND (B OR D) AND (C OR A) AND (C OR B) AND (C OR D)) T9: (A AND (A OR D) AND (A OR C) AND (B OR A) AND (B OR C OR D)) T10: ((A OR NOT(A)) AND (A OR B) AND (B OR NOT(A)) AND B AND (B OR D) AND (B OR C) AND (C OR D)) ``` Here the generated python code for check conversion: ``` #!/usr/bin/env python3 """ Verification of convert_expr_to_cnf_complete() from prepqual.c using truth tables (Karnaugh maps) to confirm logical equivalence. We replicate the C algorithm in Python, apply it to 10 test predicates, and compare input/output truth tables to verify correctness. """ import itertools from dataclasses import dataclass from typing import List, Optional, Set, Tuple, FrozenSet from copy import deepcopy # ───────────────────────────────────────────────────────────────────── # Expression AST (mirrors BoolExpr / OpExpr from PostgreSQL) # ───────────────────────────────────────────────────────────────────── @dataclass(frozen=True) class Var: """A boolean variable, e.g. Var('A')""" name: str def __repr__(self): return self.name @dataclass(frozen=True) class NotExpr: arg: object def __repr__(self): return f"NOT({self.arg})" @dataclass(frozen=True) class AndExpr: args: tuple # frozen tuple for hashability def __repr__(self): return "(" + " AND ".join(str(a) for a in self.args) + ")" @dataclass(frozen=True) class OrExpr: args: tuple def __repr__(self): return "(" + " OR ".join(str(a) for a in self.args) + ")" @dataclass(frozen=True) class Const: value: bool def __repr__(self): return "TRUE" if self.value else "FALSE" # ───────────────────────────────────────────────────────────────────── # Helper constructors # ───────────────────────────────────────────────────────────────────── def AND(*args): flat = [] for a in args: if isinstance(a, AndExpr): flat.extend(a.args) else: flat.append(a) return AndExpr(tuple(flat)) def OR(*args): flat = [] for a in args: if isinstance(a, OrExpr): flat.extend(a.args) else: flat.append(a) return OrExpr(tuple(flat)) def NOT(a): return NotExpr(a) # ───────────────────────────────────────────────────────────────────── # Evaluation # ───────────────────────────────────────────────────────────────────── def evaluate(expr, env: dict) -> bool: if isinstance(expr, Var): return env[expr.name] if isinstance(expr, Const): return expr.value if isinstance(expr, NotExpr): return not evaluate(expr.arg, env) if isinstance(expr, AndExpr): return all(evaluate(a, env) for a in expr.args) if isinstance(expr, OrExpr): return any(evaluate(a, env) for a in expr.args) raise TypeError(f"Unknown expr type: {type(expr)}") def collect_vars(expr) -> set: if isinstance(expr, Var): return {expr.name} if isinstance(expr, Const): return set() if isinstance(expr, NotExpr): return collect_vars(expr.arg) if isinstance(expr, (AndExpr, OrExpr)): s = set() for a in expr.args: s |= collect_vars(a) return s raise TypeError(f"Unknown expr type: {type(expr)}") # ───────────────────────────────────────────────────────────────────── # Truth table generation # ───────────────────────────────────────────────────────────────────── def truth_table(expr, var_names: list) -> list: """Return list of (assignment_dict, result_bool) for all combinations.""" rows = [] for vals in itertools.product([False, True], repeat=len(var_names)): env = dict(zip(var_names, vals)) rows.append((env, evaluate(expr, env))) return rows def truth_table_bitvec(expr, var_names: list) -> int: """Compact truth table as a bitmask (bit i = row i result).""" bv = 0 for i, vals in enumerate(itertools.product([False, True], repeat=len(var_names))): env = dict(zip(var_names, vals)) if evaluate(expr, env): bv |= (1 << i) return bv # ───────────────────────────────────────────────────────────────────── # Karnaugh map display (2-4 variables) # ───────────────────────────────────────────────────────────────────── def print_karnaugh_map(expr, var_names: list, label: str = ""): n = len(var_names) tt = truth_table(expr, var_names) print(f"\n{'=' * 60}") if label: print(f" {label}") print(f" Expression: {expr}") print(f" Variables: {var_names}") if n == 2: _print_kmap_2(tt, var_names) elif n == 3: _print_kmap_3(tt, var_names) elif n == 4: _print_kmap_4(tt, var_names) else: # Fallback: just print truth table _print_truth_table(tt, var_names) print() def _val(tt, env_match): for env, res in tt: if all(env[k] == v for k, v in env_match.items()): return '1' if res else '0' return '?' def _print_truth_table(tt, var_names): header = " | ".join(f"{v:>5}" for v in var_names) + " | OUT" print(f" {header}") print(f" {'-' * len(header)}") for env, res in tt: row = " | ".join(f"{int(env[v]):>5}" for v in var_names) print(f" {row} | {'1' if res else '0'}") def _print_kmap_2(tt, vn): """2-var Karnaugh map: rows=vn[0], cols=vn[1]""" print(f" {vn[1]}=0 {vn[1]}=1") for r in [0, 1]: vals = [] for c in [0, 1]: vals.append(_val(tt, {vn[0]: bool(r), vn[1]: bool(c)})) print(f" {vn[0]}={r}: {vals[0]} {vals[1]}") def _print_kmap_3(tt, vn): """3-var Karnaugh map: rows=vn[0], cols=vn[1]vn[2] in Gray code""" gray2 = [(0, 0), (0, 1), (1, 1), (1, 0)] header = " " + " ".join(f"{vn[1]}{vn[2]}={b1}{b2}" for b1, b2 in gray2) print(header) for r in [0, 1]: vals = [] for b1, b2 in gray2: vals.append(_val(tt, {vn[0]: bool(r), vn[1]: bool(b1), vn[2]: bool(b2)})) print(f" {vn[0]}={r}: " + " ".join(vals)) def _print_kmap_4(tt, vn): """4-var Karnaugh map: rows=vn[0]vn[1], cols=vn[2]vn[3] in Gray code""" gray2 = [(0, 0), (0, 1), (1, 1), (1, 0)] header = " " + " ".join(f"{vn[2]}{vn[3]}={b1}{b2}" for b1, b2 in gray2) print(header) for r1, r2 in gray2: vals = [] for c1, c2 in gray2: vals.append(_val(tt, {vn[0]: bool(r1), vn[1]: bool(r2), vn[2]: bool(c1), vn[3]: bool(c2)})) print(f" {vn[0]}{vn[1]}={r1}{r2}: " + " ".join(vals)) # ───────────────────────────────────────────────────────────────────── # CNF conversion — faithful port of prepqual.c algorithm # ───────────────────────────────────────────────────────────────────── def is_or(e): return isinstance(e, OrExpr) def is_and(e): return isinstance(e, AndExpr) def remove_duplicates_in_list(clauses: list) -> list: """remove_duplicates_in_list() from prepqual.c""" result = [] for c in clauses: if c not in result: result.append(c) return result def or_clause_subsumes(or1, or2) -> bool: """ or_clause_subsumes() from prepqual.c (A OR B) subsumes (A OR B OR C) — we can keep the shorter one. """ if not is_or(or1) or not is_or(or2): return False for a1 in or1.args: if a1 not in or2.args: return False return True def remove_duplicate_and_subsumed_clauses(clauses: list) -> list: """remove_duplicate_and_subsumed_clauses() from prepqual.c""" result = [] for clause in clauses: keep = True new_result = [] for existing in result: if clause == existing: keep = False new_result.append(existing) continue if is_or(clause) and is_or(existing): if or_clause_subsumes(existing, clause): keep = False new_result.append(existing) continue elif or_clause_subsumes(clause, existing): # Current subsumes existing — drop existing, keep current # NOTE: C code does break here, so it only removes one. # We replicate that behavior. continue # skip existing else: new_result.append(existing) else: new_result.append(existing) result = new_result if keep: result.append(clause) return result def flatten_or_args_complete(args: list) -> list: result = [] for a in args: if is_or(a): result.extend(flatten_or_args_complete(list(a.args))) else: result.append(a) return remove_duplicates_in_list(result) def flatten_and_args_complete(args: list) -> list: result = [] for a in args: if is_and(a): result.extend(flatten_and_args_complete(list(a.args))) else: result.append(a) return remove_duplicates_in_list(result) def deduplicate_cnf_result(expr): if not is_and(expr): return expr unique = remove_duplicate_and_subsumed_clauses(list(expr.args)) if len(unique) == 0: return Const(True) elif len(unique) == 1: return unique[0] else: return AndExpr(tuple(unique)) def combine_cnf_clauses_complete(clauses: list): if len(clauses) == 0: return Const(True) if len(clauses) == 1: return clauses[0] all_clauses = [] for c in clauses: if is_and(c): all_clauses.extend(list(c.args)) else: all_clauses.append(c) all_clauses = remove_duplicate_and_subsumed_clauses(all_clauses) if len(all_clauses) == 0: return Const(True) elif len(all_clauses) == 1: return all_clauses[0] else: return AndExpr(tuple(all_clauses)) def distribute_or_over_ands_complete(non_ands: list, and_clauses: list): first_and = and_clauses[0] first_and_args = remove_duplicates_in_list(list(first_and.args)) remaining_ands = and_clauses[1:] base_args = remove_duplicates_in_list(non_ands) + remaining_ands distributed = [] for subclause in first_and_args: new_or_args = list(base_args) + [subclause] new_or_args = remove_duplicates_in_list(new_or_args) new_or = OrExpr(tuple(new_or_args)) cnf_or = convert_expr_to_cnf_complete(new_or) distributed.append(cnf_or) return combine_cnf_clauses_complete(distributed) def convert_or_to_cnf_complete(expr): or_args = [] for a in expr.args: or_args.append(convert_expr_to_cnf_complete(a)) or_args = flatten_or_args_complete(or_args) or_args = remove_duplicates_in_list(or_args) and_clauses = [] non_and_clauses = [] has_and = False for a in or_args: if is_and(a): and_clauses.append(a) has_and = True else: non_and_clauses.append(a) if not has_and: if len(or_args) == 0: return Const(True) elif len(or_args) == 1: return or_args[0] else: return OrExpr(tuple(or_args)) result = distribute_or_over_ands_complete(non_and_clauses, and_clauses) return deduplicate_cnf_result(result) def convert_and_to_cnf_complete(expr): and_args = [] for a in expr.args: and_args.append(convert_expr_to_cnf_complete(a)) and_args = flatten_and_args_complete(and_args) and_args = remove_duplicates_in_list(and_args) if len(and_args) == 0: return Const(True) elif len(and_args) == 1: return and_args[0] else: return AndExpr(tuple(and_args)) def convert_expr_to_cnf_complete(expr): """Main entry — mirrors convert_expr_to_cnf_complete() from prepqual.c""" if expr is None: return None if not is_or(expr) and not is_and(expr): return expr if is_or(expr): return convert_or_to_cnf_complete(expr) if is_and(expr): return convert_and_to_cnf_complete(expr) return expr # ───────────────────────────────────────────────────────────────────── # CNF validation helper # ───────────────────────────────────────────────────────────────────── def is_cnf(expr) -> bool: """Check if expression is in CNF: AND of (OR of literals).""" if isinstance(expr, (Var, NotExpr, Const)): return True # single literal is trivially CNF if is_or(expr): # All args must be literals (Var, NotExpr, Const) return all(isinstance(a, (Var, NotExpr, Const)) for a in expr.args) if is_and(expr): for a in expr.args: if is_and(a): return False # nested AND — not flat if is_or(a): if not all(isinstance(x, (Var, NotExpr, Const)) for x in a.args): return False elif not isinstance(a, (Var, NotExpr, Const)): return False return True return False # ───────────────────────────────────────────────────────────────────── # Define 10 test predicates # ───────────────────────────────────────────────────────────────────── A, B, C, D = Var('A'), Var('B'), Var('C'), Var('D') test_cases = [ # 1. Simple: (A AND B) OR (A AND C) # Expected CNF: A AND (B OR C) ( "T1: (A AND B) OR (A AND C)", OR(AND(A, B), AND(A, C)), ['A', 'B', 'C'], ), # 2. From commit message: (s='s' AND year=2001) OR (s='s' AND year=2002) # Using A=s='s', B=year=2001, C=year=2002 # Expected CNF: A AND (B OR C) ( "T2: (A AND B) OR (A AND C) [commit example simplified]", OR(AND(A, B), AND(A, C)), ['A', 'B', 'C'], ), # 3. Four-term: (A AND B) OR (A AND C) OR (D AND B) OR (D AND C) # Expected CNF: (A OR D) AND (B OR C) ( "T3: (A∧B) ∨ (A∧C) ∨ (D∧B) ∨ (D∧C)", OR(AND(A, B), AND(A, C), AND(D, B), AND(D, C)), ['A', 'B', 'C', 'D'], ), # 4. Already in CNF: (A OR B) AND (C OR D) # Should stay the same ( "T4: (A∨B) ∧ (C∨D) [already CNF]", AND(OR(A, B), OR(C, D)), ['A', 'B', 'C', 'D'], ), # 5. Single AND: A AND B AND C # Already CNF ( "T5: A ∧ B ∧ C [trivial AND]", AND(A, B, C), ['A', 'B', 'C'], ), # 6. Single OR: A OR B OR C # Already CNF (single clause) ( "T6: A ∨ B ∨ C [trivial OR]", OR(A, B, C), ['A', 'B', 'C'], ), # 7. Nested: ((A AND B) OR C) AND D # Expected CNF: (A OR C) AND (B OR C) AND D ( "T7: ((A∧B) ∨ C) ∧ D", AND(OR(AND(A, B), C), D), ['A', 'B', 'C', 'D'], ), # 8. Complex from commit: (A AND B AND C) OR (A AND B AND D) # Expected CNF: A AND B AND (C OR D) ( "T8: (A∧B∧C) ∨ (A∧B∧D)", OR(AND(A, B, C), AND(A, B, D)), ['A', 'B', 'C', 'D'], ), # 9. Three-way OR with overlap: # (A AND B) OR (A AND C) OR (A AND D) # Expected CNF: A AND (B OR C OR D) ( "T9: (A∧B) ∨ (A∧C) ∨ (A∧D)", OR(AND(A, B), AND(A, C), AND(A, D)), ['A', 'B', 'C', 'D'], ), # 10. Full commit example: # (A AND B AND C) OR (A AND B AND D) OR (NOT(A) AND B AND C) OR (NOT(A) AND B AND D) # = B AND (C OR D) (A cancels out) ( "T10: (A∧B∧C) ∨ (A∧B∧D) ∨ (¬A∧B∧C) ∨ (¬A∧B∧D)", OR(AND(A, B, C), AND(A, B, D), AND(NOT(A), B, C), AND(NOT(A), B, D)), ['A', 'B', 'C', 'D'], ), ] # ───────────────────────────────────────────────────────────────────── # Run verification # ───────────────────────────────────────────────────────────────────── def main(): print("=" * 70) print(" VERIFICATION OF convert_expr_to_cnf_complete()") print(" Using Karnaugh Maps / Truth Tables") print("=" * 70) all_pass = True results_summary = [] for i, (label, expr, var_names) in enumerate(test_cases, 1): print(f"\n{'#' * 70}") print(f" TEST CASE {i}: {label}") print(f"{'#' * 70}") # Show original expression and its Karnaugh map print_karnaugh_map(expr, var_names, f"ORIGINAL: {label}") # Apply CNF conversion cnf_expr = convert_expr_to_cnf_complete(expr) # Show converted expression and its Karnaugh map print_karnaugh_map(cnf_expr, var_names, f"CNF RESULT") # Compare truth tables orig_bv = truth_table_bitvec(expr, var_names) cnf_bv = truth_table_bitvec(cnf_expr, var_names) equivalent = (orig_bv == cnf_bv) cnf_form = is_cnf(cnf_expr) status = "PASS" if equivalent else "FAIL" cnf_status = "yes" if cnf_form else "NO (not strict CNF)" print(f" Original truth table (bitvec): {orig_bv:0{2**len(var_names)}b}") print(f" CNF result truth table (bitvec): {cnf_bv:0{2**len(var_names)}b}") print(f" Logically equivalent: {'YES ✓' if equivalent else 'NO ✗ MISMATCH!'}") print(f" In CNF form: {cnf_status}") print(f" Result: {status}") if not equivalent: all_pass = False # Show differing rows print("\n DIFFERING ROWS:") tt_orig = truth_table(expr, var_names) tt_cnf = truth_table(cnf_expr, var_names) for (env_o, res_o), (env_c, res_c) in zip(tt_orig, tt_cnf): if res_o != res_c: assign = ", ".join(f"{v}={'1' if env_o[v] else '0'}" for v in var_names) print(f" {assign}: original={int(res_o)}, cnf={int(res_c)}") results_summary.append((i, label, status, cnf_status, str(cnf_expr))) # ───────────────────────────────────────────────────────────────── # Summary # ───────────────────────────────────────────────────────────────── print(f"\n\n{'=' * 70}") print(" SUMMARY") print(f"{'=' * 70}") print(f" {'#':>3} {'Status':>6} {'CNF?':>20} Description") print(f" {'-'*3} {'-'*6} {'-'*20} {'-'*30}") for idx, label, status, cnf_status, cnf_str in results_summary: print(f" {idx:>3} {status:>6} {cnf_status:>20} {label}") print() print(f" {'=' * 50}") print(f" CNF Conversion Results:") print(f" {'=' * 50}") for idx, label, status, cnf_status, cnf_str in results_summary: print(f" T{idx}: {cnf_str}") print() if all_pass: print(" ✓ ALL 10 TEST CASES PASSED — CNF conversion is logically correct.") else: print(" ✗ SOME TEST CASES FAILED — CNF conversion has bugs!") return all_pass if __name__ == "__main__": success = main() exit(0 if success else 1) ``` -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected] --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
