dpll-grapher.ts

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("∨") + "}";