Non-linear optimization, bug fixes in CAD

src/main/java/me/paultristanwagner/satchecking/parse/LinearConstraintParser.java

@@ -14,26 +14,6 @@
 
 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> '=' <TERM>

src/main/java/me/paultristanwagner/satchecking/parse/MultivariatePolynomialConstraintLexer.java

@@ -0,0 +1,19 @@
+package me.paultristanwagner.satchecking.parse;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.*;
+
+public class MultivariatePolynomialConstraintLexer extends Lexer {
+
+  public MultivariatePolynomialConstraintLexer(String input) {
+    super(input);
+
+    registerTokenTypes(
+        MIN,
+        MAX,
+        LPAREN,
+        RPAREN
+    );
+
+    this.initialize(input);
+  }
+}

src/main/java/me/paultristanwagner/satchecking/parse/MultivariatePolynomialConstraintParser.java

@@ -1,6 +1,5 @@
 package me.paultristanwagner.satchecking.parse;
 
-import me.paultristanwagner.satchecking.sat.Result;
 import me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomial;
 import me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint;
 
@@ -10,10 +9,22 @@
 import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.Comparison.LESS_THAN;
 import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.Comparison.LESS_THAN_OR_EQUALS;
 import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.Comparison.NOT_EQUALS;
+import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.MultivariateMaximizationConstraint.maximize;
+import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.MultivariateMinimizationConstraint.minimize;
 import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.multivariatePolynomialConstraint;
 
 public class MultivariatePolynomialConstraintParser implements Parser<MultivariatePolynomialConstraint> {
 
+  /*
+   * Grammar:
+   *   <Constraint> ::= <Polynomial> <Comparison> <Polynomial>
+   *                  | 'min' '(' <Polynomial> ')'
+   *                  | 'max' '(' <Polynomial> ')'
+   *
+   *   <Comparison> ::= "=" | "!=" | "<" | ">" | "<=" | ">="
+   *
+   */
+
   @Override
   public MultivariatePolynomialConstraint parse(String string) {
     ParseResult<MultivariatePolynomialConstraint> result = parseWithRemaining(string);
@@ -26,12 +37,36 @@ public MultivariatePolynomialConstraint parse(String string) {
 
   @Override
   public ParseResult<MultivariatePolynomialConstraint> parseWithRemaining(String string) {
+    Lexer lexer = new MultivariatePolynomialConstraintLexer(string);
+    if(lexer.canConsumeEither(MIN, MAX)) {
+      boolean isMin = lexer.canConsume(MIN);
+      lexer.consumeEither(MIN, MAX);
+      lexer.consume(LPAREN);
+
+      Parser<MultivariatePolynomial> parser = new PolynomialParser();
+      ParseResult<MultivariatePolynomial> result = parser.parseWithRemaining(lexer.getRemaining());
+      MultivariatePolynomial p = result.result();
+
+      lexer.skip(result.charsRead());
+
+      lexer.consume(RPAREN);
+
+      MultivariatePolynomialConstraint constraint;
+      if(isMin) {
+        constraint = minimize(p);
+      } else {
+        constraint = maximize(p);
+      }
+
+      return new ParseResult<>(constraint, lexer.getCursor(), true);
+    }
+
     Parser<MultivariatePolynomial> parser = new PolynomialParser();
 
     ParseResult<MultivariatePolynomial> pResult = parser.parseWithRemaining(string);
     MultivariatePolynomial p = pResult.result();
 
-    Lexer lexer = new ComparisonLexer(string.substring(pResult.charsRead()));
+    lexer = new ComparisonLexer(string.substring(pResult.charsRead()));
     MultivariatePolynomialConstraint.Comparison comparison = parseComparison(lexer);
 
     ParseResult<MultivariatePolynomial> qResult = parser.parseWithRemaining(lexer.getRemaining());

src/main/java/me/paultristanwagner/satchecking/parse/PolynomialParser.java

@@ -3,26 +3,13 @@
 import me.paultristanwagner.satchecking.theory.arithmetic.Number;
 import me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomial;
 
-import java.util.Scanner;
-
 import static me.paultristanwagner.satchecking.parse.TokenType.*;
 import static me.paultristanwagner.satchecking.theory.arithmetic.Number.number;
 import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomial.constant;
 import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomial.variable;
 
 public class PolynomialParser implements Parser<MultivariatePolynomial> {
 
-  public static void main(String[] args){
-    Scanner scanner = new Scanner(System.in);
-    PolynomialParser parser = new PolynomialParser();
-
-    String line;
-    while ((line = scanner.nextLine()) != null) {
-      MultivariatePolynomial polynomial = parser.parse(line);
-      System.out.println(polynomial);
-    }
-  }
-
   /*
    * Grammar for polynomial constraints:
    *   <S> ::= <TERM> EQUALS 0

src/main/java/me/paultristanwagner/satchecking/smt/VariableAssignment.java

@@ -36,4 +36,18 @@ public String toString() {
 
     return builder.toString();
   }
+
+  @Override
+  public boolean equals(Object o) {
+    if (this == o) return true;
+    if (o == null || getClass() != o.getClass()) return false;
+    VariableAssignment<?> that = (VariableAssignment<?>) o;
+    return Objects.equals(this.keySet(), that.keySet()) &&
+        this.keySet().stream().allMatch(key -> Objects.equals(this.get(key), that.get(key)));
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(this.keySet().stream().map(key -> Objects.hash(key, this.get(key))).toArray());
+  }
 }

src/main/java/me/paultristanwagner/satchecking/theory/nonlinear/CAD.java

@@ -1,92 +1,59 @@
 package me.paultristanwagner.satchecking.theory.nonlinear;
 
-import me.paultristanwagner.satchecking.parse.Parser;
-import me.paultristanwagner.satchecking.parse.PolynomialParser;
-import me.paultristanwagner.satchecking.smt.VariableAssignment;
-import me.paultristanwagner.satchecking.theory.arithmetic.Rational;
-
 import java.util.*;
 
 import static me.paultristanwagner.satchecking.theory.nonlinear.Cell.emptyCell;
 import static me.paultristanwagner.satchecking.theory.nonlinear.Interval.IntervalBoundType.OPEN;
 import static me.paultristanwagner.satchecking.theory.nonlinear.Interval.*;
-import static me.paultristanwagner.satchecking.theory.nonlinear.RealAlgebraicNumber.realAlgebraicNumber;
 
 public class CAD {
 
-  public static void main(String[] args) {
-    Parser<MultivariatePolynomial> parser = new PolynomialParser();
-    MultivariatePolynomial p = parser.parse("x^2 + y^2 - 1");
-    MultivariatePolynomial q = parser.parse("x^2 + y^3 - 1/2");
-
-    RealAlgebraicNumber x = realAlgebraicNumber(parser.parse("x^6-2x^4+2x^2-3/4").toUnivariatePolynomial(), Rational.parse("105/128"), Rational.parse("27/32"));
-    RealAlgebraicNumber y = realAlgebraicNumber(parser.parse("x^6-1x^4+x^2-1/4").toUnivariatePolynomial(), Rational.parse("1/2"), Rational.parse("3/4"));
-
-    System.out.println(p);
-    System.out.println(q);
-    System.out.println(x);
-    System.out.println(y);
-
-
-
-  }
-
-  private List<String> variables;
-  private Set<MultivariatePolynomial> polynomials;
-
-  public CAD(Set<MultivariatePolynomial> polynomials) {
-    this.polynomials = polynomials;
-
-    Set<String> variablesSet = new HashSet<>();
-    for (MultivariatePolynomial polynomial : polynomials) {
-      variablesSet.addAll(polynomial.variables);
-    }
-    this.variables = new ArrayList<>(variablesSet);
-
-
-  }
-
-  public Set<VariableAssignment<RealAlgebraicNumber>> compute(
+  public Set<Cell> compute(
       Set<MultivariatePolynomialConstraint> constraints
   ) {
-    return compute(constraints, false);
+    return compute(constraints, null);
   }
 
-  public Set<VariableAssignment<RealAlgebraicNumber>> compute(
+  public Set<Cell> compute(
       Set<MultivariatePolynomialConstraint> constraints,
-      boolean onlyEqualities
+      List<String> variableOrdering
   ) {
-    this.polynomials = new HashSet<>();
+    Set<MultivariatePolynomial> polynomials = new HashSet<>();
     for (MultivariatePolynomialConstraint constraint : constraints) {
-      this.polynomials.add(constraint.getPolynomial());
+      polynomials.add(constraint.getPolynomial());
     }
 
-    Set<String> variablesSet = new HashSet<>();
-    for (MultivariatePolynomial polynomial : polynomials) {
-      variablesSet.addAll(polynomial.variables);
+    if(variableOrdering == null) {
+      Set<String> variablesSet = new HashSet<>();
+      for (MultivariatePolynomial polynomial : polynomials) {
+        variablesSet.addAll(polynomial.variables);
+      }
+      variableOrdering = new ArrayList<>(variablesSet);
     }
-    this.variables = new ArrayList<>(variablesSet);
 
     // phase 1: projection
     Map<Integer, Set<MultivariatePolynomial>> p = new HashMap<>();
-    p.put(variables.size(), polynomials);
+    p.put(variableOrdering.size(), polynomials);
+
+    for (int r = variableOrdering.size() - 1; r >= 1; r--) {
+      String variable = variableOrdering.get(r);
 
-    for (int r = variables.size() - 1; r >= 1; r--) {
-      String variable = variables.get(r);
       Set<MultivariatePolynomial> proj = mcCallumProjection(p.get(r + 1), variable);
       p.put(r, proj);
 
-      String previousVariable = variables.get(r);
-      p.get(r + 1).stream().filter(poly -> !poly.highestVariable().equals(previousVariable));
+      String previousVariable = variableOrdering.get(r);
+
+      // todo: highestVariable could cause errors
+      p.get(r + 1).removeIf(poly -> !poly.highestVariable().equals(previousVariable));
     }
 
     // phase 2: lifting
     List<List<Cell>> D = new ArrayList<>();
     D.add(List.of(emptyCell()));
 
-    for (int i = 1; i <= variables.size(); i++) {
+    for (int i = 1; i <= variableOrdering.size(); i++) {
       List<Cell> D_i = new ArrayList<>();
-      String variable = variables.get(i - 1);
+      String variable = variableOrdering.get(i - 1);
 
       for (Cell R : D.get(i - 1)) {
         Map<String, RealAlgebraicNumber> s = R.chooseSamplePoint();
@@ -114,40 +81,26 @@ public Set<VariableAssignment<RealAlgebraicNumber>> compute(
         }
 
         if (sortedRoots.isEmpty()) {
-          if (!onlyEqualities) {
-            D_i.add(R.extend(variable, unboundedInterval()));
-          }
+          D_i.add(R.extend(variable, unboundedInterval()));
         } else {
-          if (!onlyEqualities) {
-            D_i.add(R.extend(variable, intervalLowerUnbounded(sortedRoots.get(0), OPEN)));
-            D_i.add(R.extend(variable, intervalUpperUnbounded(sortedRoots.get(sortedRoots.size() - 1), OPEN)));
-
-          }
-          D_i.add(R.extend(variable, pointInterval(sortedRoots.get(sortedRoots.size() - 1))));
+          D_i.add(R.extend(variable, intervalLowerUnbounded(sortedRoots.get(0).copy(), OPEN)));
+          D_i.add(R.extend(variable, intervalUpperUnbounded(sortedRoots.get(sortedRoots.size() - 1).copy(), OPEN)));
+          D_i.add(R.extend(variable, pointInterval(sortedRoots.get(sortedRoots.size() - 1).copy())));
         }
 
         for (int j = 0; j < sortedRoots.size() - 1; j++) {
           RealAlgebraicNumber a = sortedRoots.get(j);
           RealAlgebraicNumber b = sortedRoots.get(j + 1);
 
-          D_i.add(R.extend(variable, pointInterval(a)));
-          if (!onlyEqualities) {
-            D_i.add(R.extend(variable, interval(a, b, OPEN, OPEN)));
-          }
+          D_i.add(R.extend(variable, pointInterval(a.copy())));
+          D_i.add(R.extend(variable, interval(a.copy(), b.copy(), OPEN, OPEN)));
         }
       }
 
       D.add(D_i);
     }
 
-    List<Cell> result = D.get(variables.size());
-    Set<VariableAssignment<RealAlgebraicNumber>> assignments = new HashSet<>();
-    for (Cell cell : result) {
-      VariableAssignment<RealAlgebraicNumber> assignment = new VariableAssignment<>(cell.chooseSamplePoint());
-      assignments.add(assignment);
-    }
-
-    return assignments;
+    return new HashSet<>(D.get(variableOrdering.size()));
   }
 
   public Set<MultivariatePolynomial> mcCallumProjection(