import type { ConjunctiveClause, DisjunctiveClause, DpllAlgoStepNode, Variable, VariableOccurence, } from "./models"; let counter = 0; function getCounter() { return counter++; } export function getGraphCodeForNodeTree( startNodes: DpllAlgoStepNode[], startTerm: ConjunctiveClause ): string { const startTermString = conClauseToString(startTerm); const startCounter = getCounter(); return ( "graph TD\n" + startNodes .map((startNode) => dpllAlgoStepNodesToTree(startNode, startTermString, startCounter).join( "\n" ) ) .join("\n") ); } export function dpllAlgoStepNodesToTree( startNode: DpllAlgoStepNode, parentTermString: string, parentCounter: number ): string[] { const termString = conClauseToString(startNode.resultingTerm); const myCounter = getCounter(); const arrowFromParent = "N" + parentCounter + '["' + parentTermString + '"] -->|"' + startNode.stepTaken + " " + assignmentsToString(startNode.immediateAssignment) + ' "| N' + myCounter + '["' + (startNode.stepTaken === "Unsatisfiable" ? "❌" : startNode.stepTaken === "Satisfiable" ? "✅" : termString) + '"]'; const childrenArrows = startNode.children .map((c) => dpllAlgoStepNodesToTree(c, termString, myCounter)) .reduce((acc, curr) => [...acc, ...curr], []); return [arrowFromParent, ...childrenArrows]; } export function conClauseToString(term: ConjunctiveClause): string { return ( "{" + term.map((disClause) => disClauseToString(disClause)).join("∧") + "}" ); } function disClauseToString(term: DisjunctiveClause): string { return "{" + term.map((varOcc) => varOccToString(varOcc)).join("∨") + "}"; } function varOccToString(varOcc: VariableOccurence): string { return varOcc.polarity ? varOcc.name : "¬" + varOcc.name; } function assignmentsToString(assignments: Map<Variable, boolean>): string { return [...assignments.entries()] .map(([key, value]) => key + " ↦ " + value) .join(", "); }