import { PropositionalFormula, PropositionalArgument } from '../../../types.js';
/**
* Core truth table generation logic
* Handles variable extraction, assignment generation, and table structure
*/
export class TruthTableGenerator {
// Safety limit: Maximum 12 variables (4096 rows)
// More than 12 variables (8192+ rows) can cause memory issues and slow performance
private static readonly MAX_VARIABLES = 12;
/**
* Extract all unique variables from a set of formulas
* @param formulas Propositional formulas
* @returns Array of unique variable names sorted alphabetically
*/
extractVariables(formulas: PropositionalFormula[]): string[] {
const variables = new Set<string>();
const extractVarsFromFormula = (formula: PropositionalFormula): void => {
if (formula.type === 'variable') {
variables.add(formula.name);
} else if (formula.type === 'unary') {
extractVarsFromFormula(formula.operand);
} else if (formula.type === 'binary') {
extractVarsFromFormula(formula.left);
extractVarsFromFormula(formula.right);
}
};
formulas.forEach(formula => extractVarsFromFormula(formula));
// Sort alphabetically
return Array.from(variables).sort();
}
/**
* Generate all possible truth assignments for a set of variables
* @param variables Variable names
* @returns Array of assignments (each assignment is a map from variable name to boolean value)
* @throws Error if number of variables exceeds MAX_VARIABLES
*/
generateAssignments(variables: string[]): Map<string, boolean>[] {
// Safety check: prevent exponential blowup
if (variables.length > TruthTableGenerator.MAX_VARIABLES) {
throw new Error(
`Too many variables (${variables.length}). Maximum allowed is ${TruthTableGenerator.MAX_VARIABLES} ` +
`(${Math.pow(2, TruthTableGenerator.MAX_VARIABLES)} rows). ` +
`This formula would generate ${Math.pow(2, variables.length)} rows, which could cause memory issues.`
);
}
const assignments: Map<string, boolean>[] = [];
const numAssignments = Math.pow(2, variables.length);
for (let i = 0; i < numAssignments; i++) {
const assignment = new Map<string, boolean>();
for (let j = 0; j < variables.length; j++) {
// Convert i to binary and check if the jth bit is set
const bitValue = (i & (1 << (variables.length - j - 1))) !== 0;
assignment.set(variables[j], bitValue);
}
assignments.push(assignment);
}
return assignments;
}
/**
* Extract formulas from input (handles both single formulas and arguments)
* @param input Formula or argument to process
* @returns Array of formulas and whether it's an argument
*/
extractFormulas(input: PropositionalFormula | PropositionalArgument): {
formulas: PropositionalFormula[];
isArgument: boolean;
} {
const isArgument = 'premises' in input && 'conclusion' in input;
const formulas = isArgument
? [...(input as PropositionalArgument).premises, (input as PropositionalArgument).conclusion]
: [input as PropositionalFormula];
return { formulas, isArgument };
}
/**
* Generate the structure for a truth table
* @param input Formula or argument to visualize
* @returns Truth table structure
*/
generateTableStructure(input: PropositionalFormula | PropositionalArgument) {
const { formulas, isArgument } = this.extractFormulas(input);
const variables = this.extractVariables(formulas);
const assignments = this.generateAssignments(variables);
return {
formulas,
variables,
assignments,
isArgument
};
}
}
