diff --git a/src/dpll-algo.ts b/src/dpll-algo.ts index 4092626948b45a1b2dc6e5f399bab5fff04d118f..f9cc5f1603983fc31287ca77b0927a7a074d1c64 100644 --- a/src/dpll-algo.ts +++ b/src/dpll-algo.ts @@ -74,18 +74,7 @@ export function eliminatePureLiteral( term: ConjunctiveClause, literalToEliminate: VariableOccurence ): ConjunctiveClause { - const fulfilledClausesRemoved = term.filter( - (disClause) => - !disClause.some( - (varOcc) => - varOcc.name === literalToEliminate.name && - varOcc.polarity === literalToEliminate.polarity - ) - ); - const unfilfilledVariablesRemoved = fulfilledClausesRemoved.map((disClause) => - disClause.filter((varOcc) => varOcc.name === literalToEliminate.name) - ); - return unfilfilledVariablesRemoved; + return propagateVariableAssignment(term, literalToEliminate); } export function hasEmptyDisjunctiveClauses(term: ConjunctiveClause): boolean { diff --git a/src/grapher.ts b/src/grapher.ts deleted file mode 100644 index 3ee1c10b9ba184bdd5f025f995d8f5751b79a80b..0000000000000000000000000000000000000000 --- a/src/grapher.ts +++ /dev/null @@ -1,46 +0,0 @@ -import type { AssignmentNode, AstNode, IfNode, WhileNode } from "./parser"; - -export function createMermaidString(ast: AstNode[]): string { - if (ast.length > 0) return "graph LR\n" + mermaidifyNodeList(ast); - else return "graph TD\na[Nothing there yet]"; -} - -function mermaidifyNodeList(astNodes: AstNode[]): string { - let lines: string[] = []; - const nodesWithRawExpressionToConnect: any[] = astNodes.filter( - (node) => node.type !== "Skip" - ); - lines = [ - ...lines, - nodesWithRawExpressionToConnect - .map((node) => generateMermaidBlock(node)) - .join(" --> "), - ]; - - // TODO: Connect with children - - return lines.join("\n"); -} - -function generateConnectionArrow( - firstNode: (WhileNode | IfNode | AssignmentNode) & AstNode, - secondNode: (WhileNode | IfNode | AssignmentNode) & AstNode -): string { - return ( - generateMermaidBlock(firstNode) + " --> " + generateMermaidBlock(secondNode) - ); -} - -function generateMermaidBlock( - node: (WhileNode | IfNode | AssignmentNode) & AstNode -): string { - return ( - "N" + - node.identifier + - '["[' + - node.rawExpression + - "]" + - node.identifier + - ';"]' - ); -} diff --git a/test/dpll-algo.spec.ts b/test/dpll-algo.spec.ts index a1ed4b8d98a08ff320a4a006dff40af2e4256efa..73fda59692a4a895e6340ac6bc6021ef5577725b 100644 --- a/test/dpll-algo.spec.ts +++ b/test/dpll-algo.spec.ts @@ -16,6 +16,7 @@ import { dpllAlgoStepNodesToTree, getGraphCodeForNodeTree, } from "../src/dpll-grapher"; +import { parse } from "../src/knf-parser"; describe("DPLL-Algo", function () { describe("#findFirstUnitClauseIndex()", function () { @@ -133,4 +134,25 @@ describe("DPLL-Algo", function () { ); }); }); + describe("#algoStep()", function () { + it("should be tested propperly", function () { + const inputClause: ConjunctiveClause = parse( + "{{X1∨X2∨X3}∧{¬X1∨X2∨¬X4}∧{X2}∧{¬X1∨X3}∧{¬X1∨¬X3∨X4}∧{X1∨¬X3}}" + ); + + /* + const res = algoStep(unsatExample); + console.dir(res[0]); + + const res2 = algoStep(res[0].resultingTerm); + console.dir(res2[0]); + + const res3 = algoStep(res2[0].resultingTerm); + console.dir(res3[0]); + */ + const res4 = runAlgo(inputClause); + console.log(JSON.stringify(res4, null, 2)); + console.log(getGraphCodeForNodeTree(res4, inputClause)); + }); + }); });