Remove logical expression parsing

__tests__/converter/dimacs/DimacsLogicalExpression.spec.ts

@@ -21,7 +21,7 @@ describe("Parsing", () => {
   let dimacsParser = new DimacsParser();
   let logicalExpressionParser = new LogicalExpressionParser();
 
-  each([
+  /*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 ))",
@@ -48,7 +48,7 @@ describe("Parsing", () => {
         logicalExpression
       );
     }
-  );
+  );*/
 
   each([
     [

src/converter/dimacs/LogicalExpressionParser.ts

@@ -21,49 +21,22 @@ const rules = [
   variableRule,
   blankRule,
 ];
-const rulesNegation = [negateRule, variableRule, blankRule];
-
-interface LeveledToken {
-  level: number;
-  token: Token;
-}
 
 export class LogicalExpressionParser {
   private lex: Lexer = new Lexer(rules);
-  private lexNegation: Lexer = new Lexer(rulesNegation);
-  private output: string = "";
 
   /**
    * Converts a logical expression to an expression in dimacs sat format
    * dimacs sat format: https://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf
    * @param logicalExpression {string} logical expression
    * @returns {string} formula in dimacs sat format of the input
    */
-  public parseDimacs(logicalExpression: string): string {
-    this.output = "";
-
+  public validateLogicalExpression(logicalExpression: string): string[] {
     let tokens = this.lex.tokenize(logicalExpression);
-    if (tokens.length == 0) return this.output;
+    if (tokens.length == 0) return [];
 
     //Verify formula integrity
-    let errors = this.verifyTokens(tokens);
-    if (errors.length > 0) {
-      let errorStr = "";
-      for (let error of errors) errorStr += error + "\n";
-
-      throw new Error(errorStr);
-    }
-
-    //Handle variable comments and program start
-    let variables = this.convertVariables(tokens);
-    variables.forEach((num, str, _) => {
-      this.output += `c ${num} ${TokenName.variableAssignment} ${str}\n`;
-    });
-    this.output += `p sat ${variables.size}\n`;
-
-    this.parseFormula(tokens);
-
-    return this.output;
+    return this.verifyTokens(tokens);
   }
 
   private verifyTokens(tokens: Token[]): string[] {
@@ -121,173 +94,4 @@ export class LogicalExpressionParser {
 
     return errors;
   }
-  /**
-   * Converts any negative variable's negative prefix
-   * Converts all variables to numbers
-   * @param tokens {Token[]} array of tokens to search for variables
-   * @returns {Map<string, number>} variables mapped to their number representation
-   */
-  private convertVariables(tokens: Token[]): Map<string, number> {
-    let variables = new Map<string, number>();
-    const addToMap = (str: string): number => {
-      let number = variables.get(str);
-      if (number == undefined) {
-        number = variables.size + 1;
-        variables.set(str, number);
-      }
-
-      return number;
-    };
-
-    for (let i = 0; i < tokens.length; i++) {
-      switch (tokens[i].name) {
-        case TokenName.variable:
-          tokens[i].lexeme = addToMap(tokens[i].lexeme).toString();
-          break;
-        case TokenName.negatedVariable:
-          let negTokens = this.lexNegation.tokenize(tokens[i].lexeme);
-          if (negTokens.length != 2)
-            throw new Error(
-              "Can't parse negated variables that don't have two tokens"
-            );
-
-          let negToken = negTokens[1] as Token;
-          let varNumber = addToMap(negToken.lexeme);
-
-          //Replace negated variable with dimacs negative variable syntax
-          negToken.lexeme = `-${varNumber}`;
-          tokens[i] = negToken;
-          break;
-      }
-    }
-
-    return variables;
-  }
-
-  private getLeveledTokens(tokens: Token[]): LeveledToken[] {
-    let leveledTokens: LeveledToken[] = [];
-    let curLevel = 0;
-
-    for (let token of tokens) {
-      switch (token.name) {
-        case TokenName.open:
-          curLevel++;
-          break;
-        case TokenName.close:
-          curLevel--;
-          break;
-        default:
-          leveledTokens.push({ token: token, level: curLevel });
-          break;
-      }
-    }
-
-    return leveledTokens;
-  }
-
-  private parseFormula(tokens: Token[]) {
-    let leveledTokens = this.getLeveledTokens(tokens);
-
-    //Start recursive parsing of formula starting with or
-    this.processOR(leveledTokens);
-  }
-
-  private getOperatorPositions(
-    tokens: LeveledToken[],
-    operator: string,
-    level: number
-  ): number[] {
-    let positions: number[] = [];
-    for (let i = 0; i < tokens.length; i++) {
-      let token = tokens[i];
-      switch (token.token.name) {
-        case operator:
-          if (token.level == level) positions.push(i);
-          break;
-        default:
-          break;
-      }
-    }
-
-    //Always add token length
-    positions.push(tokens.length);
-
-    return positions;
-  }
-
-  private getMinLevel(tokens: LeveledToken[]): number {
-    let minLevel = undefined;
-
-    for (const token of tokens) {
-      if (minLevel == undefined || token.level < minLevel) {
-        minLevel = token.level;
-      }
-    }
-
-    return minLevel ?? -1;
-  }
-
-  private processAND(tokens: LeveledToken[]): LeveledToken[] {
-    if (tokens.length < 2) {
-      this.output += ` ${tokens[0].token.lexeme} `;
-      return tokens;
-    }
-
-    let level = this.getMinLevel(tokens);
-    let operatorPositions = this.getOperatorPositions(
-      tokens,
-      TokenName.and,
-      level
-    );
-    if (operatorPositions.length == 1) return this.processOR(tokens);
-
-    let returnTokens: LeveledToken[] = [];
-    let lastOr = -1;
-
-    this.output += `*(`;
-    for (let pos of operatorPositions) {
-      let before = tokens.slice(lastOr + 1, pos);
-      lastOr = pos;
-
-      let processedBefore = this.processOR(before);
-      returnTokens.push(...processedBefore);
-    }
-    this.output += `)`;
-
-    return returnTokens;
-  }
-
-  private processOR(tokens: LeveledToken[]): LeveledToken[] {
-    if (tokens.length < 2) {
-      this.output += ` ${tokens[0].token.lexeme} `;
-      return tokens;
-    }
-
-    let level = this.getMinLevel(tokens);
-    let operatorPositions = this.getOperatorPositions(
-      tokens,
-      TokenName.or,
-      level
-    );
-    if (operatorPositions.length == 1) return this.processAND(tokens);
-
-    let returnTokens: LeveledToken[] = [];
-    let lastOr = -1;
-
-    if (operatorPositions.length > 1) this.output += `+(`;
-    for (let pos of operatorPositions) {
-      let before = tokens.slice(lastOr + 1, pos);
-      lastOr = pos;
-
-      //Start processing nested expressions with OR
-      let processedBefore =
-        before[0].level != level
-          ? this.processOR(before)
-          : this.processAND(before);
-      returnTokens.push(...processedBefore);
-    }
-    if (operatorPositions.length > 1) this.output += `)`;
-
-    return returnTokens;
-  }
 }

src/pages/solve/SAT.tsx

@@ -47,11 +47,14 @@ const SAT: NextPage = () => {
         setProblemString={(value) => {
           setLogicalExpressionString(value);
 
-          try {
-            logicalExpressionParser.parseDimacs(value.toString());
+          let errors = logicalExpressionParser.validateLogicalExpression(
+            value.toString()
+          );
+
+          if (errors.length > 0) {
+            setErrorString(errors.toString());
+          } else {
             setErrorString("");
-          } catch (e: any) {
-            setErrorString(e.message);
           }
         }}
       />