negative hamiltons

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);

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;

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;

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);

frontend/public/js/proof/rules/cd/diff/hamiltonian-cycle.js

@@ -1,64 +1,73 @@
-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);
 
         if (!e) { 
             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 }
+export { negativeWeightHamilton }