From 336f9a14cfb6ede886be805e799a9133a60b1b65 Mon Sep 17 00:00:00 2001
From: Jonas Zohren <jonas.zohren@adesso.de>
Date: Fri, 26 Feb 2021 00:08:57 +0100
Subject: [PATCH] Fix: pureLiteralElimination
---
src/dpll-algo.ts | 13 +-----------
src/grapher.ts | 46 ------------------------------------------
test/dpll-algo.spec.ts | 22 ++++++++++++++++++++
3 files changed, 23 insertions(+), 58 deletions(-)
delete mode 100644 src/grapher.ts
diff --git a/src/dpll-algo.ts b/src/dpll-algo.ts
index 4092626..f9cc5f1 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 3ee1c10..0000000
--- 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 a1ed4b8..73fda59 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));
+ });
+ });
});
--
GitLab