Skip to content
Snippets Groups Projects
Commit 336f9a14 authored by Jonas Zohren's avatar Jonas Zohren
Browse files

Fix: pureLiteralElimination

parent d2332d15
Branches
No related tags found
No related merge requests found
Pipeline #15823 passed
......@@ -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 {
......
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 +
';"]'
);
}
......@@ -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));
});
});
});
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment