Generify constraints in linear real arithmetic (#7)

paultristanwagner · Mar 3, 2024 · 881ba90 · 881ba90
1 parent 34bdc86
commit 881ba90
Show file tree

Hide file tree

Showing 11 changed files with 575 additions and 292 deletions.
diff --git a/src/main/java/me/paultristanwagner/satchecking/parse/LinearConstraintLexer.java b/src/main/java/me/paultristanwagner/satchecking/parse/LinearConstraintLexer.java
@@ -7,7 +7,15 @@ public class LinearConstraintLexer extends Lexer {
   public LinearConstraintLexer(String input) {
     super(input);
 
-    registerTokenTypes(MIN, MAX, FRACTION, DECIMAL, IDENTIFIER, EQUALS, LOWER_EQUALS, GREATER_EQUALS, PLUS, MINUS, LPAREN, RPAREN);
+    registerTokenTypes(
+        MIN,
+        MAX,
+        EQUALS,
+        LOWER_EQUALS,
+        GREATER_EQUALS,
+        LPAREN,
+        RPAREN
+    );
 
     initialize(input);
   }

diff --git a/src/main/java/me/paultristanwagner/satchecking/parse/LinearConstraintParser.java b/src/main/java/me/paultristanwagner/satchecking/parse/LinearConstraintParser.java
@@ -1,161 +1,111 @@
 package me.paultristanwagner.satchecking.parse;
 
 import me.paultristanwagner.satchecking.theory.LinearConstraint;
+import me.paultristanwagner.satchecking.theory.LinearConstraint.Bound;
 import me.paultristanwagner.satchecking.theory.LinearConstraint.MaximizingConstraint;
 import me.paultristanwagner.satchecking.theory.LinearConstraint.MinimizingConstraint;
-import me.paultristanwagner.satchecking.theory.arithmetic.Number;
+import me.paultristanwagner.satchecking.theory.LinearTerm;
+
+import java.util.Scanner;
 
 import static me.paultristanwagner.satchecking.parse.TokenType.*;
+import static me.paultristanwagner.satchecking.parse.TokenType.GREATER_EQUALS;
 import static me.paultristanwagner.satchecking.theory.LinearConstraint.Bound.*;
-import static me.paultristanwagner.satchecking.theory.arithmetic.Number.ONE;
 
 public class LinearConstraintParser implements Parser<LinearConstraint> {
 
+  public static void main(String[] args) {
+    LinearConstraintParser parser = new LinearConstraintParser();
+
+    Scanner scanner = new Scanner(System.in);
+    String line;
+    while ((line = scanner.nextLine()) != null) {
+      try {
+        LinearConstraint constraint = parser.parse(line);
+        System.out.println(constraint);
+        System.out.println("lhs = " + constraint.getLeftHandSide());
+        System.out.println("rhs = " + constraint.getRightHandSide());
+        System.out.println("bound = " + constraint.getBound());
+        System.out.println("lhs - rhs = " + constraint.getDifference());
+      } catch (SyntaxError e) {
+        e.printWithContext();
+        e.printStackTrace();
+      }
+    }
+  }
+
   /*
    *  Grammar for Linear constraints:
-   *    <S> ::= <TERM> '=' <RATIONAL>
-   *          | <TERM> '<=' <RATIONAL>
-   *          | <TERM> '>=' <RATIONAL>
+   *    <S> ::= <TERM> '=' <TERM>
+   *          | <TERM> '<=' <TERM
+   *          | <TERM> '>=' <TERM>
    *          | MIN '(' <TERM> ')'
    *          | MAX '(' <TERM> ')'
    *
-   *    <TERM> ::= [ <SIGNS> ] [ <RATIONAL> ] IDENTIFIER
-   *             | [ <SIGNS> ] [ <RATIONAL> ] IDENTIFIER [ <SIGNS> <TERM> ]
-   *
-   *    <SIGNS> ::= '+' [ <SIGNS> ]
-   *              | '-' [ <SIGNS> ]
-   *
-   *    <RATIONAL> ::= FRACTION | DECIMAL
-   *
    */
   @Override
   public ParseResult<LinearConstraint> parseWithRemaining(String string) {
     Lexer lexer = new LinearConstraintLexer(string);
 
-    lexer.requireNextToken();
-
-    LinearConstraint lc = TERM(lexer);
-
-    return new ParseResult<>(lc, lexer.getCursor(), lexer.getCursor() == string.length());
-  }
-
-  private static LinearConstraint TERM(Lexer lexer) {
-    LinearConstraint lc;
     boolean optimization = false;
+    boolean minimization = false;
 
     if (lexer.canConsume(MIN)) {
-      optimization = true;
       lexer.consume(MIN);
-
       lexer.consume(LPAREN);
-      lc = new MinimizingConstraint();
-    } else if (lexer.canConsume(MAX)) {
+
       optimization = true;
+      minimization = true;
+    } else if (lexer.canConsume(MAX)) {
       lexer.consume(MAX);
-
       lexer.consume(LPAREN);
-      lc = new MaximizingConstraint();
-    } else {
-      lc = new LinearConstraint();
-    }
 
-    Number coefficient = OPTIONAL_SIGNS(lexer).multiply(OPTIONAL_RATIONAL(lexer));
-    Token variableToken = lexer.getLookahead();
-    lexer.consume(IDENTIFIER);
-    String variable = variableToken.getValue();
-    lc.setCoefficient(variable, coefficient);
-
-    while (lexer.canConsumeEither(PLUS, MINUS, FRACTION, DECIMAL)) {
-      coefficient = OPTIONAL_SIGNS(lexer).multiply(OPTIONAL_RATIONAL(lexer));
-      variableToken = lexer.getLookahead();
+      optimization = true;
+    }
 
-      lexer.consume(IDENTIFIER);
+    LinearTerm lhs = TERM(lexer);
 
-      variable = variableToken.getValue();
-      lc.setCoefficient(variable, coefficient);
-    }
+    LinearConstraint lc;
+    if(optimization) {
+      if(minimization) {
+        lc = new MinimizingConstraint(lhs);
+      } else {
+        lc = new MaximizingConstraint(lhs);
+      }
 
-    if (optimization) {
       lexer.consume(RPAREN);
-      return lc;
+      return new ParseResult<>(lc, lexer.getCursor(), lexer.getCursor() == string.length());
     }
 
-    lexer.requireEither(EQUALS, LOWER_EQUALS, GREATER_EQUALS);
-    if (lexer.canConsume(EQUALS)) {
-      lexer.consume(EQUALS);
-      lc.setBound(EQUAL);
-    } else if (lexer.canConsume(LOWER_EQUALS)) {
-      lexer.consume(LOWER_EQUALS);
-      lc.setBound(UPPER);
-    } else {
-      lexer.consume(GREATER_EQUALS);
-      lc.setBound(LOWER);
-    }
+    Bound bound = BOUND(lexer);
 
-    Number value = OPTIONAL_SIGNS(lexer).multiply(RATIONAL(lexer));
-    lc.setValue(value);
+    LinearTerm rhs = TERM(lexer);
 
-    return lc;
-  }
+    lc = new LinearConstraint(lhs, rhs, bound);
 
-  private static Number OPTIONAL_SIGNS(Lexer lexer) {
-    if (lexer.canConsumeEither(PLUS, MINUS)) {
-      return SIGNS(lexer);
-    } else {
-      return ONE();
-    }
+    return new ParseResult<>(lc, lexer.getCursor(), lexer.getCursor() == string.length());
   }
 
-  private static Number SIGNS(Lexer lexer) {
-    lexer.requireEither(PLUS, MINUS);
-
-    Number sign = ONE();
-    do {
-      if (lexer.canConsume(PLUS)) {
-        lexer.consume(PLUS);
-      } else {
-        lexer.consume(MINUS);
-        sign = sign.negate();
-      }
-    } while (lexer.canConsumeEither(PLUS, MINUS));
-
-    return sign;
-  }
+  private static LinearTerm TERM(Lexer lexer) {
+    LinearTermParser parser = new LinearTermParser();
+    ParseResult<LinearTerm> result = parser.parseWithRemaining(lexer.getRemaining());
 
-  private static Number OPTIONAL_RATIONAL(Lexer lexer) {
-    if (lexer.canConsumeEither(FRACTION, DECIMAL)) {
-      return RATIONAL(lexer);
-    }
+    lexer.skip(result.charsRead());
 
-    return ONE();
+    return result.result();
   }
 
-  private static Number RATIONAL(Lexer lexer) {
-    lexer.requireEither(FRACTION, DECIMAL);
-
-    if (lexer.canConsume(FRACTION)) {
-      return FRACTION(lexer);
+  private static Bound BOUND(Lexer lexer) {
+    lexer.requireEither(EQUALS, LOWER_EQUALS, GREATER_EQUALS);
+    if (lexer.canConsume(EQUALS)) {
+      lexer.consume(EQUALS);
+      return EQUAL;
+    } else if (lexer.canConsume(LOWER_EQUALS)) {
+      lexer.consume(LOWER_EQUALS);
+      return LESS_EQUALS;
     } else {
-      return DECIMAL(lexer);
+      lexer.consume(GREATER_EQUALS);
+      return Bound.GREATER_EQUALS;
     }
   }
-
-  private static Number DECIMAL(Lexer lexer) {
-    Token token = lexer.getLookahead();
-    lexer.consume(DECIMAL);
-
-    return Number.parse(token.getValue());
-  }
-
-  private static Number FRACTION(Lexer lexer) {
-    Token token = lexer.getLookahead();
-    lexer.consume(FRACTION);
-
-    String[] parts = token.getValue().split("/");
-
-    long numerator = Long.parseLong(parts[0]);
-    long denominator = Long.parseLong(parts[1]);
-
-    return Number.number(numerator, denominator);
-  }
 }
diff --git a/src/main/java/me/paultristanwagner/satchecking/parse/LinearTermLexer.java b/src/main/java/me/paultristanwagner/satchecking/parse/LinearTermLexer.java
@@ -0,0 +1,20 @@
+package me.paultristanwagner.satchecking.parse;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.*;
+
+public class LinearTermLexer extends Lexer {
+
+  public LinearTermLexer(String input) {
+    super(input);
+
+    registerTokenTypes(
+        PLUS,
+        MINUS,
+        FRACTION,
+        DECIMAL,
+        IDENTIFIER
+    );
+
+    initialize(input);
+  }
+}
diff --git a/src/main/java/me/paultristanwagner/satchecking/parse/LinearTermParser.java b/src/main/java/me/paultristanwagner/satchecking/parse/LinearTermParser.java
@@ -0,0 +1,126 @@
+package me.paultristanwagner.satchecking.parse;
+
+import me.paultristanwagner.satchecking.theory.LinearTerm;
+import me.paultristanwagner.satchecking.theory.arithmetic.Number;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.*;
+import static me.paultristanwagner.satchecking.theory.arithmetic.Number.ONE;
+
+public class LinearTermParser implements Parser<LinearTerm> {
+
+  /*
+   * Grammar for linear terms:
+   *   <TERM> ::= [ <SIGNS> ] [ <RATIONAL> ] IDENTIFIER [ <SIGNS> <TERM> ]
+   *            | [ <SIGNS> ] <RATIONAL> [ <SIGNS> <TERM> ]
+   *
+   */
+
+  @Override
+  public ParseResult<LinearTerm> parseWithRemaining(String string) {
+    LinearTermLexer lexer = new LinearTermLexer(string);
+
+    lexer.requireNextToken();
+
+    LinearTerm term = new LinearTerm();
+
+    Number value = OPTIONAL_SIGNS(lexer);
+    boolean explicitValue = false;
+
+    if(lexer.canConsumeEither(DECIMAL, FRACTION)) {
+      explicitValue = true;
+      value = value.multiply(OPTIONAL_RATIONAL(lexer));
+    }
+
+    if(!explicitValue || lexer.canConsume(IDENTIFIER)) {
+      lexer.require(IDENTIFIER);
+      String identifier = lexer.getLookahead().getValue();
+      lexer.consume(IDENTIFIER);
+      term.addCoefficient(identifier, value);
+    } else {
+      term.addConstant(value);
+    }
+
+    while(lexer.canConsumeEither(PLUS, MINUS)) {
+      Number sign = SIGNS(lexer);
+      value = OPTIONAL_SIGNS(lexer);
+      explicitValue = false;
+
+      if(lexer.canConsumeEither(DECIMAL, FRACTION)) {
+        explicitValue = true;
+        value = value.multiply(OPTIONAL_RATIONAL(lexer));
+      }
+
+      if(!explicitValue || lexer.canConsume(IDENTIFIER)) {
+        lexer.require(IDENTIFIER);
+        String identifier = lexer.getLookahead().getValue();
+        lexer.consume(IDENTIFIER);
+        term.addCoefficient(identifier, sign.multiply(value));
+      } else {
+        term.addConstant(sign.multiply(value));
+      }
+    }
+
+    return new ParseResult<>(term, lexer.getCursor(), lexer.getRemaining().isEmpty());
+  }
+
+  private static Number OPTIONAL_SIGNS(Lexer lexer) {
+    if (lexer.canConsumeEither(PLUS, MINUS)) {
+      return SIGNS(lexer);
+    } else {
+      return ONE();
+    }
+  }
+
+  private static Number SIGNS(Lexer lexer) {
+    lexer.requireEither(PLUS, MINUS);
+
+    Number sign = ONE();
+    do {
+      if (lexer.canConsume(PLUS)) {
+        lexer.consume(PLUS);
+      } else {
+        lexer.consume(MINUS);
+        sign = sign.negate();
+      }
+    } while (lexer.canConsumeEither(PLUS, MINUS));
+
+    return sign;
+  }
+
+  private static Number OPTIONAL_RATIONAL(Lexer lexer) {
+    if (lexer.canConsumeEither(FRACTION, DECIMAL)) {
+      return RATIONAL(lexer);
+    }
+
+    return ONE();
+  }
+
+  private static Number RATIONAL(Lexer lexer) {
+    lexer.requireEither(FRACTION, DECIMAL);
+
+    if (lexer.canConsume(FRACTION)) {
+      return FRACTION(lexer);
+    } else {
+      return DECIMAL(lexer);
+    }
+  }
+
+  private static Number DECIMAL(Lexer lexer) {
+    Token token = lexer.getLookahead();
+    lexer.consume(DECIMAL);
+
+    return Number.parse(token.getValue());
+  }
+
+  private static Number FRACTION(Lexer lexer) {
+    Token token = lexer.getLookahead();
+    lexer.consume(FRACTION);
+
+    String[] parts = token.getValue().split("/");
+
+    long numerator = Long.parseLong(parts[0]);
+    long denominator = Long.parseLong(parts[1]);
+
+    return Number.number(numerator, denominator);
+  }
+}