Problem History

__tests__/converter/dimacs/DimacsLogicalExpression.spec.ts

@@ -1,8 +1,7 @@
 import each from "jest-each";
-import { regexBlank } from "../../../src/converter/dimacs/Syntax/CommonSyntax";
 import { DimacsParser } from "../../../src/converter/dimacs/DimacsParser";
+import { regexBlank } from "../../../src/converter/dimacs/Syntax/CommonSyntax";
 import { regexComment } from "../../../src/converter/dimacs/Syntax/DimacsSyntax";
-import { LogicalExpressionParser } from "../../../src/converter/dimacs/LogicalExpressionParser";
 import { regexNOT } from "../../../src/converter/dimacs/Syntax/LogicalExpressionSyntax";
 
 function isEquivalentLogicalExpression(f1: string, f2: string) {
@@ -19,36 +18,6 @@ function isEquivalentDimacs(f1: string, f2: string) {
 
 describe("Parsing", () => {
   let dimacsParser = new DimacsParser();
-  let logicalExpressionParser = new LogicalExpressionParser();
-
-  each([
-    [
-      "((1 or 2 or not 3) and (!4 and (not 5 and 6)) and 3 and (7 or 2))",
-      "c First comment\nc Some Comment\nc 1 => 1\np sat 7\n*(+( 1  2  -3 )*( -4 *( -5  6 )) 3 +( 7  2 ))",
-    ],
-    [
-      "(1 or (2 and 3) or (((1 and 4) or 5) and 6))",
-      "p sat 6\n+(1 *(2  3)*(+(*(1  4) 5) 6))",
-    ],
-    [
-      "(((1 and not 2 and 3 and 4) or 3) and 5)",
-      "c Sample DIMACS .sat file\np sat 5\n*(+(*(1  -2  3  4) 3) 5)",
-    ],
-    ["((1 and not 2) or 3)", "p sat 3\n+(*(1 -2) 3)"],
-    ["((1 and 2) or not 3)", "p sat 3\n+(*(1 2) -3)"],
-  ]).test(
-    "parsing bi-directional",
-    (logicalExpression: string, dimacs: string) => {
-      isEquivalentDimacs(
-        logicalExpressionParser.parseDimacs(logicalExpression),
-        dimacs
-      );
-      isEquivalentLogicalExpression(
-        dimacsParser.parseLogicalExpression(dimacs),
-        logicalExpression
-      );
-    }
-  );
 
   each([
     [

src/api/ToolboxAPI.ts

@@ -10,6 +10,19 @@ import { SolveRequest } from "./data-model/SolveRequest";
  */
 export const baseUrl = () => process.env.NEXT_PUBLIC_API_BASE_URL;
 
+function invalidSolution(reason: string): Solution {
+  return {
+    id: -1,
+    status: SolutionStatus.INVALID,
+    solverName: "",
+    executionMilliseconds: 0,
+    solutionData: "",
+    debugData: "",
+    metaData: "",
+    error: `${reason}`,
+  };
+}
+
 export async function postProblem<T>(
   problemType: string,
   solveRequest: SolveRequest<T>
@@ -23,18 +36,19 @@ export async function postProblem<T>(
   })
     .then((response) => response.json())
     .then((json) => json as Solution)
-    .catch((reason) => {
-      return {
-        id: -1,
-        status: SolutionStatus.INVALID,
-        solverName: "",
-        executionMilliseconds: 0,
-        solutionData: "",
-        debugData: "",
-        metaData: "",
-        error: `${reason}`,
-      };
-    });
+    .catch(invalidSolution);
+}
+
+export async function fetchSolution(problemType: string, solutionId: number) {
+  return fetch(`${baseUrl()}/solution/${problemType}?id=${solutionId}`, {
+    method: "GET",
+    headers: {
+      "Content-Type": "application/json",
+    },
+  })
+    .then((response) => response.json())
+    .then((json) => json as Solution)
+    .catch(invalidSolution);
 }
 
 export async function fetchSolvers(

src/components/solvers/History.tsx

@@ -0,0 +1,52 @@
+import {
+  Button,
+  Divider,
+  Heading,
+  List,
+  ListItem,
+  Stack,
+  Tooltip,
+} from "@chakra-ui/react";
+import { ProblemState } from "./HistoryStorage";
+
+interface HistoryProps<T> {
+  problemStates: ProblemState<T>[];
+
+  onRequestRollback: (problemState: ProblemState<T>) => void;
+}
+
+export const History = <T extends {}>(props: HistoryProps<T>) => {
+  if (props.problemStates.length == 0) return null;
+
+  function reloadState(state: ProblemState<T>) {
+    props.onRequestRollback(state);
+  }
+
+  return (
+    <Stack>
+      <Heading as="h3" size="md" textAlign="center">
+        History
+      </Heading>
+      <List>
+        {props.problemStates.map((x) => {
+          let problemString = x.problemInput.toString();
+          return (
+            <ListItem key={problemString}>
+              <Tooltip label={problemString}>
+                <Button
+                  width="200px"
+                  overflow="hidden"
+                  variant="link"
+                  onClick={(_) => reloadState(x)}
+                >
+                  {problemString}
+                </Button>
+              </Tooltip>
+              <Divider />
+            </ListItem>
+          );
+        })}
+      </List>
+    </Stack>
+  );
+};

src/components/solvers/HistoryStorage.ts

@@ -0,0 +1,30 @@
+import { SolutionIds } from "./ProgressHandler";
+
+export interface ProblemState<T> {
+  /**
+   * Problem input
+   */
+  problemInput: T;
+  /**
+   * Ids of the solutions of the problem input per problem type
+   */
+  solutionIds: SolutionIds;
+}
+
+export function getHistory<T>(problemTypes: string[]): ProblemState<T>[] {
+  let historyItem = localStorage.getItem(getStoreId(problemTypes));
+  if (historyItem === null) return [];
+
+  return JSON.parse(historyItem);
+}
+
+export function storeHistory<T>(
+  problemTypes: string[],
+  history: ProblemState<T>[]
+) {
+  localStorage.setItem(getStoreId(problemTypes), JSON.stringify(history));
+}
+
+export function getStoreId(problemTypes: string[]) {
+  return `problemStates-${problemTypes}`;
+}

src/components/solvers/ProgressHandler.tsx

@@ -1,19 +1,26 @@
-import { Box, Center, HStack, VStack } from "@chakra-ui/react";
-import React, { useState } from "react";
-import { GoButton } from "./buttons/GoButton";
-import { postProblem } from "../../api/ToolboxAPI";
-import { SolutionView } from "./SolutionView";
-import { Container } from "../Container";
+import { Box, Center, HStack } from "@chakra-ui/react";
+import { useEffect, useState } from "react";
 import { Solution } from "../../api/data-model/Solution";
 import { SolveRequest } from "../../api/data-model/SolveRequest";
+import { fetchSolution, postProblem } from "../../api/ToolboxAPI";
+import { Container } from "../Container";
+import { GoButton } from "./buttons/GoButton";
+import { History } from "./History";
+import { getHistory, ProblemState, storeHistory } from "./HistoryStorage";
+import { SolutionView } from "./SolutionView";
 import { SolverPicker } from "./SolverPicker";
 
+export type SolutionIds = {
+  [problemTypeId: string]: number;
+};
+
 export interface ProgressHandlerProps<T> {
   /**
    * List of problem types that should be solved with the given input.
    */
   problemTypes: string[];
   problemInput: T;
+  setProblemInput: (t: T) => void;
 }
 
 export const ProgressHandler = <T extends {}>(
@@ -22,11 +29,26 @@ export const ProgressHandler = <T extends {}>(
   const [wasClicked, setClicked] = useState<boolean>(false);
   const [finished, setFinished] = useState<boolean>(false);
   const [solutions, setSolutions] = useState<Solution[]>();
+  const [problemStates, setProblemStates] = useState<ProblemState<T>[]>([]);
   const [solveRequest, setSolveRequest] = useState<SolveRequest<T>>({
     requestContent: props.problemInput,
     requestedSubSolveRequests: {},
   });
 
+  useEffect(() => {
+    // Handle problem states from local storage
+    if (problemStates.length == 0) {
+      let history = getHistory<T>(props.problemTypes);
+      if (history.length > 0) {
+        setProblemStates(history);
+      }
+    }
+  }, [problemStates, props.problemTypes]);
+
+  useEffect(() => {
+    storeHistory(props.problemTypes, problemStates);
+  }, [problemStates, props.problemTypes]);
+
   async function startSolving() {
     setClicked(true);
     setFinished(false);
@@ -39,7 +61,35 @@ export const ProgressHandler = <T extends {}>(
     setSolveRequest(newSolveRequest);
     Promise.all(
       props.problemTypes.map((problemType) =>
-        postProblem(problemType, newSolveRequest)
+        postProblem(problemType, newSolveRequest).then((s) => ({
+          problemType: problemType,
+          solution: s,
+        }))
+      )
+    ).then((result) => {
+      let solutionIdMap = result.reduce((acc, item) => {
+        acc[item.problemType] = item.solution.id;
+        return acc;
+      }, {} as SolutionIds);
+
+      let newProblemState: ProblemState<T> = {
+        problemInput: props.problemInput,
+        solutionIds: solutionIdMap,
+      };
+
+      setSolutions(result.map((x) => x.solution));
+      setProblemStates([...problemStates, newProblemState]);
+      setFinished(true);
+    });
+  }
+
+  async function loadSolution(ids: SolutionIds) {
+    setClicked(true);
+    setFinished(false);
+
+    Promise.all(
+      props.problemTypes.map((problemType) =>
+        fetchSolution(problemType, ids[problemType])
       )
     ).then((solutions) => {
       setSolutions(solutions);
@@ -86,6 +136,14 @@ export const ProgressHandler = <T extends {}>(
             </Box>
           ))
         : null}
+
+      <History
+        problemStates={problemStates}
+        onRequestRollback={(problemState) => {
+          props.setProblemInput(problemState.problemInput);
+          loadSolution(problemState.solutionIds);
+        }}
+      />
     </Container>
   );
 };

src/components/solvers/SAT/TextArea.tsx

@@ -1,13 +1,12 @@
+import { Box } from "@chakra-ui/react";
+import { highlight } from "prismjs";
 import "prismjs/themes/prism-solarizedlight.css"; //TODO: use custom styling
-import React from "react";
 import Editor from "react-simple-code-editor";
-import { highlight } from "prismjs";
-import { Box, Container } from "@chakra-ui/react";
 import { SAT_language } from "./prism-SAT";
 
 interface TextAreaProps {
   problemString: string;
-  setProblemString: React.Dispatch<React.SetStateAction<string>>;
+  setProblemString: (problemString: string) => void;
 }
 
 export const TextArea = (props: TextAreaProps) => {

src/components/solvers/SAT/prism-SAT.ts

@@ -1,7 +1,7 @@
 import { regexVariable } from "../../../converter/dimacs/Syntax/CommonSyntax";
 import {
   regexAND,
-  regexNOTVariable,
+  regexNOT,
   regexOR,
 } from "../../../converter/dimacs/Syntax/LogicalExpressionSyntax";
 
@@ -16,7 +16,7 @@ export const SAT_language = {
   },
   "SAT-punctuation": /[()]/,
   negation: {
-    pattern: regexNOTVariable,
+    pattern: regexNOT,
     alias: "string",
   },
   "SAT-variable": {

src/components/solvers/TextInputMask.tsx

@@ -1,24 +1,21 @@
-import { Divider, Text, Textarea } from "@chakra-ui/react";
+import { Divider, Textarea } from "@chakra-ui/react";
 import Head from "next/head";
-import React, { ReactElement, useState } from "react";
+import { ReactElement, useState } from "react";
 import { Container } from "../Container";
-import { Main } from "../Main";
-import { Help } from "./SAT/Help";
 import { EditorControls } from "./EditorControls";
 
 export interface TextInputMaskProperties {
   textPlaceholder: string;
-  onTextChanged: (text: string) => void;
+  text: string;
+  onTextChanged: (value: string) => void;
   body?: ReactElement;
 }
 
 export const TextInputMask = (props: TextInputMaskProperties) => {
-  const [text, setText] = useState<string>("");
   const [errorString, setErrorString] = useState("");
 
   function onTextChanged(text: string): void {
     try {
-      setText(text);
       props.onTextChanged(text);
 
       setErrorString("");
@@ -40,11 +37,11 @@ export const TextInputMask = (props: TextInputMaskProperties) => {
         errorText={errorString}
         idleText={props.textPlaceholder + " 👇"}
         onUpload={onTextChanged}
-        editorContent={text}
+        editorContent={props.text}
       />
       <Textarea
         placeholder={props.textPlaceholder}
-        value={text}
+        value={props.text}
         minHeight="10rem"
         isInvalid={errorString != ""}
         onChange={(x) => onTextChanged(x.target.value)}