From d9be4ec67ceba4d0e2a55811bc7c42274c017c33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juli=C3=A1n=20M=C3=A9ndez?= Date: Sun, 2 Feb 2025 15:05:40 +0100 Subject: [PATCH] negative hamiltons --- frontend/public/js/ce/ce.js | 6 +- frontend/public/js/ontology/ontology.js | 2 +- frontend/public/js/proof/axioms.js | 2 +- .../public/js/proof/rules/cd/diff/diff.js | 18 ++- .../proof/rules/cd/diff/hamiltonian-cycle.js | 109 +++++++++++++----- frontend/public/js/proof/trees/magic.js | 34 +++--- frontend/public/js/utils/controls.js | 4 +- frontend/public/js/utils/pan-zoom.js | 2 +- 8 files changed, 120 insertions(+), 57 deletions(-) diff --git a/frontend/public/js/ce/ce.js b/frontend/public/js/ce/ce.js index a162c73..1c9ff2a 100644 --- a/frontend/public/js/ce/ce.js +++ b/frontend/public/js/ce/ce.js @@ -786,7 +786,7 @@ function calcBoxWidth(longestString) { } function calcBoxHeight(stringList) { - if (stringList == 'Group') { + if (stringList === 'Group') { return (stringList.length + 35) + "px"; } else { @@ -837,7 +837,7 @@ function processData(mapper, model) { } }) // const edgeFromParent = edgeData.find((edge) => edge.source === id); - const parentId = edgeFromParent == null ? "" : edgeFromParent.target; + const parentId = edgeFromParent === null ? "" : edgeFromParent.target; labels = labels.replace(/\[|\]|\s/g, "").split(","); const text = labels; let longest = 1; @@ -867,7 +867,7 @@ function processData(mapper, model) { } }); // Updating Label and setting the important label as Important Concept - if (importantLabel != null) { + if (importantLabel !== null) { let labelIndex = labels.indexOf(importantLabel); if (labelIndex === -1) { labels.unshift(importantLabel); diff --git a/frontend/public/js/ontology/ontology.js b/frontend/public/js/ontology/ontology.js index 3c8f232..d0b8969 100644 --- a/frontend/public/js/ontology/ontology.js +++ b/frontend/public/js/ontology/ontology.js @@ -260,7 +260,7 @@ function processData(data) { }); const edgeFromParent = edges.find((edge) => edge.source === id); - const parentId = edgeFromParent == null ? "" : edgeFromParent.target; + const parentId = edgeFromParent === null ? "" : edgeFromParent.target; const text = getNodeTextList({ signature, axioms }); let longest = 1; diff --git a/frontend/public/js/proof/axioms.js b/frontend/public/js/proof/axioms.js index 8117966..cd4f986 100644 --- a/frontend/public/js/proof/axioms.js +++ b/frontend/public/js/proof/axioms.js @@ -287,7 +287,7 @@ export class AxiomsHelper { const s = []; let curr = d; - while (curr != null || s.length > 0) { + while (curr !== null || s.length > 0) { curr.children && curr.children.forEach(c => { s.push(c); curr = c; diff --git a/frontend/public/js/proof/rules/cd/diff/diff.js b/frontend/public/js/proof/rules/cd/diff/diff.js index de2e5c4..74dbf11 100644 --- a/frontend/public/js/proof/rules/cd/diff/diff.js +++ b/frontend/public/js/proof/rules/cd/diff/diff.js @@ -2,7 +2,7 @@ import { utils } from "../../rules.js"; import { controls, createVisContainer } from "../cd-rules.js"; import { stylesheet } from "../../../../../style/cy-cd-style.js"; import { params as cola } from "../../../../layouts/cola.js"; -import { hamiltonianCycle } from "./hamiltonian-cycle.js"; +import { negativeWeightHamilton } from "./hamiltonian-cycle.js"; import { throttle } from "../../../../utils/throttle.js"; const EPSILON = " - Є"; @@ -319,6 +319,7 @@ export class DifferenceCD { const edge = { id: `e-${i++}`, eid: p.eid, label: `${c}${_epsilon}`, + epsilon:_epsilon, weight: c, negated } @@ -346,6 +347,7 @@ export class DifferenceCD { id: `e-${i++}`, eid: p.eid, negated, source: nodes[y], target: nodes[x], label: `${c}${_epsilon}`, + epsilon: _epsilon, weight: c, } // x−y <= c ... (y, x) c }); @@ -417,7 +419,7 @@ export class DifferenceCD { start = cy.nodes()[Math.floor(Math.random() * (l))]; // starts at random node } - const hC = hamiltonianCycle({ + const hC = negativeWeightHamilton({ root: `#${start.data().id}`, directed: true, weight: (edge) => edge.data().weight, @@ -466,10 +468,14 @@ export class DifferenceCD { ); } - d3.select("#cycle-val").text(`${ - !Fraction(cycleValue).equals(0) ? f(cycleValue) : "" - }${EPSILONS(ep)}`); - + if (ep !== 0) { + d3.select("#cycle-val").text(`${ + !Fraction(cycleValue).equals(0) ? f(cycleValue) : "" + }${EPSILONS(ep)}`); + } else { + d3.select("#cycle-val").text(`${f(cycleValue)}${EPSILONS(ep)}`); + } + i += 1; if (i < ncycle.length) { timeout = setTimeout(highlightNextEle, 1000); diff --git a/frontend/public/js/proof/rules/cd/diff/hamiltonian-cycle.js b/frontend/public/js/proof/rules/cd/diff/hamiltonian-cycle.js index 2b63be8..eadc2c5 100644 --- a/frontend/public/js/proof/rules/cd/diff/hamiltonian-cycle.js +++ b/frontend/public/js/proof/rules/cd/diff/hamiltonian-cycle.js @@ -1,38 +1,47 @@ -function hamiltonianCycle(options, _eles) { +function negativeWeightHamilton (options, _eles) { let { weight, directed, root } = options; - let weightFn = weight; let eles = _eles; let cy = _eles.cy(); let edges = _eles.filter(e => e.group() === "edges"); let nodes = _eles.filter(e => e.group() === "nodes"); - root = cy.collection(root)[0]; // in case selector passed - let numNodes = nodes.length; - + let weightSum = 0; + const path = new Array(numNodes).fill(0); + const invertedEdgeMap = {}; + + root = cy.collection(root)[0]; // in case selector passed + + // find a hamiltonian cycle through recursion: for (var i = 0; i < numNodes; i++) { path[i] = -1; } - let weightSum = 0; - const invertedEdgeMap = {}; edges.forEach(e => { const d = e.data(); if (!invertedEdgeMap[d.source]) { invertedEdgeMap[d.source] = {}; } - invertedEdgeMap[d.source][d.target] = e; + if (!invertedEdgeMap[d.source][d.target]) { + invertedEdgeMap[d.source][d.target] = []; + } + + invertedEdgeMap[d.source][d.target].push(e); }); - function getEdge(src, target) { + function getEdge(src, target, all = false) { if (invertedEdgeMap[src] && invertedEdgeMap[src][target]) { - return invertedEdgeMap[src][target]; + if (all) { + return invertedEdgeMap[src][target]; + } else { + return invertedEdgeMap[src][target][0]; + } } } - /* true if the vertex v can be added at 'pos' */ + // returns true if the vertex v can be added at 'pos' function canAdd(v, path, pos) { const e = getEdge(path[pos - 1], v); @@ -40,25 +49,25 @@ function hamiltonianCycle(options, _eles) { return { can: false }; } - /* false if vertex has already been included */ + // reutnr false if vertex already in path for (const p of path) { if (p === v) { return { can: false }; } } - return { can: true, w: weightFn(e) }; + return { can: true, w: weight(e) }; } - function hamCycleUtil(path, pos) { + function hamiltonRecursion(path, pos) { // all nodes have been added - if (pos == numNodes) { + if (pos === numNodes) { // and an edge exists from last pos to root const e = getEdge(path[pos - 1], path[0]); if (e) { - weightSum += weightFn(e); + weightSum += weight(e); return true; } else { return false; @@ -77,7 +86,7 @@ function hamiltonianCycle(options, _eles) { weightSum += check.w; // recur to construct rest of the path - if (hamCycleUtil(path, pos + 1)) { + if (hamiltonRecursion(path, pos + 1)) { return true; } @@ -91,20 +100,68 @@ function hamiltonianCycle(options, _eles) { path[0] = root.data().id; - if (hamCycleUtil(path, 1) == false) { + if (hamiltonRecursion(path, 1) === false) { console.error("could not detect hamiltonian cycle") - return { cycle: [], weight: undefined } } + // hamiltonian cycle found in `path`, check if negative weight const cycle = []; - path.forEach((_, i) => { - if (i > 0) { - cycle.push(getEdge(path[i-1], path[i])); + const multiple = Object.values(invertedEdgeMap).filter(e => Object.keys(e).length === 1).length === 0; + + if (path.length === 2) { // only 2 variables involved, search for negative cycle + let w = 0; + let found = false; + getEdge(path[0], path[1], true).forEach(fe => { + if (!found) { + getEdge(path[1], path[0], true).forEach(be => { + if (!found) { + w = weight(fe) + weight(be); + if (w < 0) { + cycle.push(fe); + cycle.push(be); + found = true; + } + } + }) + } + }); + + if (found) { + return { cycle, weight: w }; + } // could be that the cycle has weight 0 and epsilons + } + + if (weightSum === 0 && multiple) { + console.error("can't decide for cycle"); + } + + if (weightSum > 0) { // should only happen if there was not a single <= premise + let w = 0; + + for (let i = path.length - 2; i >= 0; i--) { + const e = getEdge(path[i + 1], path[i]); + w += weight(e); + cycle.push(e); } - }) - cycle.push(getEdge(path[numNodes-1], path[0])) - return { cycle, weight: weightSum }; + const fe = getEdge(path[0], path[path.length - 1]); + w += weight(fe); + cycle.push(fe); + + if (w >= 0) { + console.error("could not detect negative hamiltonian cycle"); + } + + return { cycle, weight: w }; + } else { // cycle is already negative, or weight = 0 + path.forEach((_, i) => { + if (i > 0) { + cycle.push(getEdge(path[i - 1], path[i])); + } + }); + cycle.push(getEdge(path[path.length - 1], path[0])) + return { cycle, weight: weightSum }; + } } -export { hamiltonianCycle } \ No newline at end of file +export { negativeWeightHamilton } \ No newline at end of file diff --git a/frontend/public/js/proof/trees/magic.js b/frontend/public/js/proof/trees/magic.js index bf804c2..7cdbda6 100644 --- a/frontend/public/js/proof/trees/magic.js +++ b/frontend/public/js/proof/trees/magic.js @@ -176,11 +176,11 @@ export class MagicNavigation { } checkIfNewMagicIsNeeded(treeRoot, mainRoot) { - if (treeRoot.children == null) { + if (treeRoot.children === null) { return false; } - if (treeRoot.children[0].children == null) { + if (treeRoot.children[0].children === null) { return false; } @@ -191,7 +191,7 @@ export class MagicNavigation { continue; } - if (premise[i].children != null && premise[i].children[0].children != null) { + if (premise[i].children !== null && premise[i].children[0].children !== null) { toCheck = premise[i].children[0].children; for (let j = 0; j < toCheck.length; j++) { found = mainRoot.descendants() @@ -222,7 +222,7 @@ export class MagicNavigation { } pullUp(treeRoot) { - const magicImpossible = treeRoot.parent == null || treeRoot.data.target.type !== "mrule"; + const magicImpossible = treeRoot.parent === null || treeRoot.data.target.type !== "mrule"; if (proof.isDrawing || magicImpossible) { return; } @@ -252,7 +252,7 @@ export class MagicNavigation { newData.push(x.data) //check if the new premise is already a premise of the magic rule, if so keep it and all its descendants alreadyThere = treeRoot.parent.children.filter(y => y !== treeRoot).find(y => y.data.source.id === x.data.source.id); - if (alreadyThere != null) { + if (alreadyThere !== null) { alreadyThere.descendants().filter(y => y !== alreadyThere).forEach(y => { newData.push(y.data); }); @@ -362,7 +362,7 @@ export class MagicNavigation { pushUp(treeRoot) { //when magic is not possible - const magicImpossible = treeRoot.children == null || treeRoot.children[0].children == null || treeRoot.parent == null; + const magicImpossible = treeRoot.children === null || treeRoot.children[0].children === null || treeRoot.parent === null; if (proof.isDrawing || magicImpossible) { return; } @@ -383,8 +383,8 @@ export class MagicNavigation { }); treeRoot.parent.children.filter(x => x !== treeRoot).forEach(x => { - if (x.children != null) { - if (x.children[0].children != null) { + if (x.children !== null) { + if (x.children[0].children !== null) { x.children[0].children.forEach(y => { //don't add tautologies if (y.children[0].data.source.element !== "Asserted Conclusion" && !y.children[0].children) { @@ -405,7 +405,7 @@ export class MagicNavigation { newData.push(this.getNewEdge(newMagicBox, treeRoot.parent.data.target)); - if (treeRoot.parent.parent != null) { + if (treeRoot.parent.parent !== null) { this.addAllBut(treeRoot.parent.parent, newData); } @@ -415,7 +415,7 @@ export class MagicNavigation { pullDown(treeRoot) { //when magic is not possible - const magicImpossible = treeRoot.children == null || treeRoot.children[0].data.source.type !== "mrule"; + const magicImpossible = treeRoot.children === null || treeRoot.children[0].data.source.type !== "mrule"; if (proof.isDrawing || magicImpossible) { return; } @@ -447,8 +447,8 @@ export class MagicNavigation { //first, count how many axioms would not need a magic rule relevantPremiseCount = relevantPremise.length; - if (grandChild.children != null) { - if (grandChild.children[0].children != null) { + if (grandChild.children !== null) { + if (grandChild.children[0].children !== null) { grandChild.children[0].children.forEach(c => { if (relevantPremise.some(r => r.data.source.id === c.data.source.id)) { relevantPremiseCount--; @@ -512,7 +512,7 @@ export class MagicNavigation { pushDown(treeRoot) { //when magic is not possible - const magicImpossible = treeRoot.children == null || treeRoot.children[0].children == null || treeRoot.parent == null; + const magicImpossible = treeRoot.children === null || treeRoot.children[0].children === null || treeRoot.parent === null; if (proof.isDrawing || magicImpossible) { return; @@ -542,8 +542,8 @@ export class MagicNavigation { }); // treeRoot.parent.children.filter(x=>x!=treeRoot).forEach(x=>{ - // if(x.children != null){ - // if(x.children[0].children != null){ + // if(x.children !== null){ + // if(x.children[0].children !== null){ // x.children[0].children.forEach(y=>{ // //don't add tautologies // if(y.children[0].data.source.element!="Asserted Conclusion"){ @@ -566,7 +566,7 @@ export class MagicNavigation { newData.push(this.getNewEdge(newMagicBox, treeRoot.parent.data.target)); - if (treeRoot.parent.parent != null) { + if (treeRoot.parent.parent !== null) { this.addAllBut(treeRoot.parent.parent, newData); } @@ -595,7 +595,7 @@ export class MagicNavigation { getRoot(object) { let root = object; - while (root.parent != null) { + while (root.parent !== null) { root = root.parent; } diff --git a/frontend/public/js/utils/controls.js b/frontend/public/js/utils/controls.js index ef9f94a..6c889db 100644 --- a/frontend/public/js/utils/controls.js +++ b/frontend/public/js/utils/controls.js @@ -223,9 +223,9 @@ function init_resizer() { document.onkeyup = function (e) { startRedrawCSS(); const which = e.which || e.buttons; - if ((e.ctrlKey || e.altKey) && which == 39) { + if ((e.ctrlKey || e.altKey) && which === 39) { prevSibling.style.width = '100%'; - } else if ((e.ctrlKey || e.altKey) && which == 37) { + } else if ((e.ctrlKey || e.altKey) && which === 37) { prevSibling.style.width = '0%'; } finishRedrawCSS(); diff --git a/frontend/public/js/utils/pan-zoom.js b/frontend/public/js/utils/pan-zoom.js index e9bccd1..d675888 100644 --- a/frontend/public/js/utils/pan-zoom.js +++ b/frontend/public/js/utils/pan-zoom.js @@ -171,7 +171,7 @@ const thumbnailViewer = function (options) { const scopeContainer = document.querySelector(options.containerSelector + " .scope-container"); const updateMainViewPan = function (evt) { - if (evt.which == 0 && evt.button == 0) { + if (evt.which === 0 && evt.button === 0) { return false; } _updateMainViewPan(evt.clientX, evt.clientY, scopeContainer, _main, _thumb);