QF_NRA prototype (#6)

README.md

@@ -46,9 +46,21 @@ Tseitin's transformation:
 ```
 
 # SMT solver
-An SMT solver is implemented for linear real arithmetic (QF_LRA), linear integer arithmetic (QF_LIA), equality logic (QF_EQ), equality logic with uninterpreted functions (QF_EQUF) and bit vector arithmetic (QF_BV).
+An SMT solver is implemented for non-linear real arithmetic (QF_NRA), linear real arithmetic (QF_LRA), linear integer arithmetic (QF_LIA), equality logic (QF_EQ), equality logic with uninterpreted functions (QF_EQUF) and bit vector arithmetic (QF_BV).
 
 ## Examples
+### QF_NRA (⚠️ highly experimental ⚠️)
+```c++
+> smt QF_NRA (x^2 + y^2 = 1) & (x^2 + y^3 = 1/2)
+SAT:
+x=(x^6-2x^4+2x^2-3/4, 3/4, 15/16) ≈ 0.8249554777467228; y=(x^9+1/2x^6+3/4x^3+1/8, -7/4, 7/4) ≈ -0.5651977173836394;
+Time: 456ms
+```
+```c++
+> smt QF_NRA (x*y > 0) & (y*z > 0) & (x*z > 0) & (x + y + z = 0)
+UNSAT
+Time: 7ms
+```
 ### QF_LRA
 ```c++
 > smt QF_LRA (x<=-3 | x>=3) & (y=5) & (x+y>=12)

src/main/java/me/paultristanwagner/satchecking/command/impl/SMTCommand.java

@@ -25,13 +25,16 @@ public SMTCommand() {
         "smt <theory> <cnf of theory constraints>",
         """
               Available theories:
+                QF_NRA (Non-linear real arithmetic) (! highly experimental !),
                 QF_LRA (Linear real arithmetic),
                 QF_LIA (Linear integer arithmetic),
                 QF_EQ (Equality logic),
                 QF_EQUF (Equality logic with uninterpreted functions),
                 QF_BV (Bitvector arithmetic)
               
               Examples:
+                smt QF_NRA (x^2 + y^2 = 1) & (x^2 + y^3 = 1/2)
+              
                 smt QF_LRA (x <= 5) & (max(x))
               
                 smt QF_LIA (x <= 3/2) & (max(x))

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

@@ -0,0 +1,21 @@
+package me.paultristanwagner.satchecking.parse;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.*;
+
+public class ComparisonLexer extends Lexer {
+
+  public ComparisonLexer(String input) {
+    super(input);
+
+    registerTokenTypes(
+        EQUALS,
+        NOT_EQUALS,
+        GREATER_EQUALS,
+        LOWER_EQUALS,
+        LESS_THAN,
+        GREATER_THAN
+    );
+
+    initialize(input);
+  }
+}

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

@@ -156,6 +156,6 @@ private static Number FRACTION(Lexer lexer) {
     long numerator = Long.parseLong(parts[0]);
     long denominator = Long.parseLong(parts[1]);
 
-    return Number.of(numerator, denominator);
+    return Number.number(numerator, denominator);
   }
 }

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

@@ -0,0 +1,70 @@
+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;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.*;
+import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.Comparison.GREATER_THAN;
+import static me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint.Comparison.GREATER_THAN_OR_EQUALS;
+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.multivariatePolynomialConstraint;
+
+public class MultivariatePolynomialConstraintParser implements Parser<MultivariatePolynomialConstraint> {
+
+  @Override
+  public MultivariatePolynomialConstraint parse(String string) {
+    ParseResult<MultivariatePolynomialConstraint> result = parseWithRemaining(string);
+    if(!result.complete()) {
+      throw new SyntaxError("Expected end of input", string, result.charsRead());
+    }
+
+    return result.result();
+  }
+
+  @Override
+  public ParseResult<MultivariatePolynomialConstraint> parseWithRemaining(String string) {
+    Parser<MultivariatePolynomial> parser = new PolynomialParser();
+
+    ParseResult<MultivariatePolynomial> pResult = parser.parseWithRemaining(string);
+    MultivariatePolynomial p = pResult.result();
+
+    Lexer lexer = new ComparisonLexer(string.substring(pResult.charsRead()));
+    MultivariatePolynomialConstraint.Comparison comparison = parseComparison(lexer);
+
+    ParseResult<MultivariatePolynomial> qResult = parser.parseWithRemaining(lexer.getRemaining());
+    MultivariatePolynomial q = qResult.result();
+
+    MultivariatePolynomial d = p.subtract(q);
+    MultivariatePolynomialConstraint constraint = multivariatePolynomialConstraint(d, comparison);
+
+    int charsRead = pResult.charsRead() + lexer.getCursor() + qResult.charsRead();
+    return new ParseResult<>(constraint, charsRead, qResult.complete());
+  }
+
+  private MultivariatePolynomialConstraint.Comparison parseComparison(Lexer lexer) {
+    if(lexer.canConsume(TokenType.EQUALS)) {
+      lexer.consume(TokenType.EQUALS);
+      return MultivariatePolynomialConstraint.Comparison.EQUALS;
+    } else if(lexer.canConsume(TokenType.NOT_EQUALS)) {
+      lexer.consume(TokenType.NOT_EQUALS);
+      return NOT_EQUALS;
+    } else if(lexer.canConsume(TokenType.LESS_THAN)) {
+      lexer.consume(TokenType.LESS_THAN);
+      return LESS_THAN;
+    } else if(lexer.canConsume(TokenType.GREATER_THAN)) {
+      lexer.consume(TokenType.GREATER_THAN);
+      return GREATER_THAN;
+    } else if(lexer.canConsume(LOWER_EQUALS)) {
+      lexer.consume(LOWER_EQUALS);
+      return LESS_THAN_OR_EQUALS;
+    } else if(lexer.canConsume(GREATER_EQUALS)) {
+      lexer.consume(GREATER_EQUALS);
+      return GREATER_THAN_OR_EQUALS;
+    } else {
+      throw new SyntaxError("Expected comparison operator", lexer.getInput(), lexer.getCursor());
+    }
+  }
+}

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

@@ -0,0 +1,21 @@
+package me.paultristanwagner.satchecking.parse;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.*;
+
+public class PolynomialLexer extends Lexer {
+
+  public PolynomialLexer(String input) {
+    super(input);
+
+    registerTokenTypes(
+        PLUS,
+        MINUS,
+        FRACTION,
+        DECIMAL,
+        IDENTIFIER,
+        TIMES,
+        POWER);
+
+    initialize(input);
+  }
+}

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

@@ -0,0 +1,145 @@
+package me.paultristanwagner.satchecking.parse;
+
+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
+   *
+   *   <TERM> ::= <MONOMIAL> PLUS <MONOMIAL>
+   *            | <MONOMIAL> MINUS <MONOMIAL>
+   *            | <MONOMIAL>
+   *
+   *  <MONOMIAL> ::= <FACTOR> TIMES <FACTOR>
+   *               | <FACTOR>
+   *
+   *  <FACTOR> ::= FRACTION
+   *             | DECIMAL
+   *             | IDENTIFIER
+   *             | IDENTIFIER POWER INTEGER
+   */
+
+  public MultivariatePolynomial parse(String string) {
+    ParseResult<MultivariatePolynomial> result = parseWithRemaining(string);
+
+    if (!result.complete()) {
+      throw new SyntaxError("Expected end of input", string, result.charsRead());
+    }
+
+    return result.result();
+  }
+
+  @Override
+  public ParseResult<MultivariatePolynomial> parseWithRemaining(String string) {
+    Lexer lexer = new PolynomialLexer(string);
+
+    lexer.requireNextToken();
+
+    MultivariatePolynomial polynomial = parseTerm(lexer);
+
+    return new ParseResult<>(polynomial, lexer.getCursor(), lexer.getCursor() == string.length());
+  }
+
+  private MultivariatePolynomial parseTerm(Lexer lexer) {
+    MultivariatePolynomial term1 = parseMonomial(lexer);
+
+    while(lexer.canConsume(PLUS) || lexer.canConsume(MINUS)){
+      if (lexer.canConsume(PLUS)) {
+        lexer.consume(PLUS);
+        MultivariatePolynomial term2 = parseMonomial(lexer);
+        term1 = term1.add(term2);
+      } else if (lexer.canConsume(MINUS)) {
+        lexer.consume(MINUS);
+        MultivariatePolynomial term2 = parseMonomial(lexer);
+        term1 = term1.subtract(term2);
+      }
+    }
+
+    return term1;
+  }
+
+  private MultivariatePolynomial parseMonomial(Lexer lexer) {
+    MultivariatePolynomial monomial1 = parseFactor(lexer);
+
+    while (lexer.canConsumeEither(TIMES, IDENTIFIER)) {
+      if(lexer.canConsume(TIMES)) {
+        lexer.consume(TIMES);
+      }
+      MultivariatePolynomial monomial2 = parseFactor(lexer);
+      monomial1 = monomial1.multiply(monomial2);
+    }
+
+    return monomial1;
+  }
+
+  private int parseSign(Lexer lexer) {
+    int sign = 1;
+    while(lexer.canConsumeEither(PLUS, MINUS)){
+      if (lexer.canConsume(PLUS)) {
+        lexer.consume(PLUS);
+      } else if (lexer.canConsume(MINUS)) {
+        lexer.consume(MINUS);
+        sign *= -1;
+      }
+    }
+
+    return sign;
+  }
+
+  private MultivariatePolynomial parseFactor(Lexer lexer) {
+    int sign = parseSign(lexer);
+
+    if (lexer.canConsumeEither(DECIMAL, FRACTION)) {
+      String value = lexer.getLookahead().getValue();
+      lexer.consumeEither(DECIMAL, FRACTION);
+      Number number = Number.parse(value);
+
+      if(sign == -1) {
+        number = number.negate();
+      }
+
+      return constant(number);
+    }
+
+    if (lexer.canConsume(IDENTIFIER)) {
+      String variable = lexer.getLookahead().getValue();
+      lexer.consume(IDENTIFIER);
+
+      if (lexer.canConsume(POWER)) {
+        lexer.consume(POWER);
+        lexer.require(DECIMAL);
+        String exponent = lexer.getLookahead().getValue();
+        lexer.consume(DECIMAL);
+
+        MultivariatePolynomial monomial = variable(variable).pow(Integer.parseInt(exponent));
+
+        return monomial.multiply(constant(number(sign)));
+      }
+
+      return variable(variable).multiply(constant(number(sign)));
+    }
+
+    throw new SyntaxError("Expected either a decimal or an identifier", lexer.getInput(), lexer.getCursor());
+  }
+}

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

@@ -7,6 +7,7 @@
 import me.paultristanwagner.satchecking.theory.EqualityFunctionConstraint;
 import me.paultristanwagner.satchecking.theory.LinearConstraint;
 import me.paultristanwagner.satchecking.theory.bitvector.constraint.BitVectorConstraint;
+import me.paultristanwagner.satchecking.theory.nonlinear.MultivariatePolynomialConstraint;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -78,7 +79,10 @@ private T LITERAL(Lexer lexer) {
 
     ParseResult<T> parseResult;
     try {
-      if (constraintClass == LinearConstraint.class) {
+      if(constraintClass == MultivariatePolynomialConstraint.class) {
+        MultivariatePolynomialConstraintParser multivariatePolynomialConstraintParser = new MultivariatePolynomialConstraintParser();
+        parseResult = (ParseResult<T>) multivariatePolynomialConstraintParser.parseWithRemaining(remaining);
+      } else if (constraintClass == LinearConstraint.class) {
         LinearConstraintParser linearConstraintParser = new LinearConstraintParser();
         parseResult = (ParseResult<T>) linearConstraintParser.parseWithRemaining(remaining);
       } else if (constraintClass == EqualityConstraint.class) {

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

@@ -23,6 +23,7 @@ public class TokenType {
   static final TokenType MINUS = TokenType.of("-", "^-");
   static final TokenType TIMES = TokenType.of("*", "^\\*");
   static final TokenType DIVIDE = TokenType.of("/", "^\\/");
+  static final TokenType POWER = TokenType.of("^", "^\\^");
   static final TokenType REMAINDER = TokenType.of("*", "^\\%");
   static final TokenType AND = TokenType.of("and", "^(&|&&|and|AND|∧)");
   static final TokenType OR = TokenType.of("or", "^(\\|\\||\\||or|OR|∨)");

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

@@ -2,30 +2,35 @@
 
 import java.util.*;
 
-public class VariableAssignment<O> {
+public class VariableAssignment<O> extends HashMap<String, O> {
 
-  private final Map<String, O> assignments = new HashMap<>();
+  public VariableAssignment() {
+  }
+
+  public VariableAssignment(Map<String, O> assignments) {
+    this.putAll(assignments);
+  }
 
   public void assign(String variable, O value) {
-    assignments.put(variable, value);
+    this.put(variable, value);
   }
 
   public O getAssignment(String variable) {
-    return assignments.get(variable);
+    return this.get(variable);
   }
 
   public Set<String> getVariables() {
-    return assignments.keySet();
+    return this.keySet();
   }
 
   @Override
   public String toString() {
     StringBuilder builder = new StringBuilder();
-    List<String> variables = new ArrayList<>(assignments.keySet());
+    List<String> variables = new ArrayList<>(this.keySet());
     variables.sort(String::compareTo);
 
     for (String variable : variables) {
-      O value = assignments.get(variable);
+      O value = this.get(variable);
       builder.append(variable).append("=").append(value).append("; ");
     }