Fix ambiguous parsing issue

ftsrg · Oct 13, 2021 · 5c7090f · 5c7090f
1 parent 1eb4413
commit 5c7090f
Show file tree

Hide file tree

Showing 9 changed files with 112 additions and 12 deletions.
diff --git a/...er/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java b/...er/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibItpSolver.java
@@ -110,7 +110,7 @@ public SolverStatus check() {
             throw new SmtLibSolverException(res.getReason());
         }
         else if(res.isSpecific()) {
-            final CheckSatResponse checkSatResponse = res.asSpecific();
+            final CheckSatResponse checkSatResponse = res.asSpecific().asCheckSatResponse();
             if(checkSatResponse.isSat()) {
                 status = SolverStatus.SAT;
             }
@@ -185,7 +185,7 @@ private Valuation extractModel() {
             throw new SmtLibSolverException(res.getReason());
         }
         else if(res.isSpecific()) {
-            final GetModelResponse getModelResponse = res.asSpecific();
+            final GetModelResponse getModelResponse = res.asSpecific().asGetModelResponse();
             return new SmtLibValuation(symbolTable, transformationManager, termTransformer, getModelResponse.getModel());
         }
         else {

diff --git a/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java
@@ -120,7 +120,7 @@ public SolverStatus check() {
             throw new SmtLibSolverException(res.getReason());
         }
         else if(res.isSpecific()) {
-            final CheckSatResponse checkSatResponse = res.asSpecific();
+            final CheckSatResponse checkSatResponse = res.asSpecific().asCheckSatResponse();
             if(checkSatResponse.isSat()) {
                 status = SolverStatus.SAT;
             }
@@ -187,7 +187,7 @@ private Valuation extractModel() {
             throw new SmtLibSolverException(res.getReason());
         }
         else if(res.isSpecific()) {
-            final GetModelResponse getModelResponse = res.asSpecific();
+            final GetModelResponse getModelResponse = res.asSpecific().asGetModelResponse();
             return new SmtLibValuation(symbolTable, transformationManager, termTransformer, getModelResponse.getModel());
         }
         else {
@@ -219,7 +219,7 @@ private Collection<Expr<BoolType>> extractUnsatCore() {
             throw new SmtLibSolverException(res.getReason());
         }
         else if(res.isSpecific()) {
-            final GetUnsatCoreResponse getUnsatCoreResponse = res.asSpecific();
+            final GetUnsatCoreResponse getUnsatCoreResponse = res.asSpecific().asGetUnsatCoreResponse();
             unsatCoreLabels = getUnsatCoreResponse.getLabels();
         }
         else {

diff --git a/.../solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/model/SmtLibModel.java b/.../solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/model/SmtLibModel.java
@@ -17,4 +17,8 @@ public Collection<String> getDecls() {
     public String getTerm(final String symbol) {
         return values.get(symbol);
     }
+
+    public int size() {
+        return values.size();
+    }
 }
diff --git a/...r-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/CheckSatResponse.java b/...r-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/CheckSatResponse.java
@@ -7,7 +7,7 @@
 import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.PS_Unknown;
 import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.PS_Unsat;
 
-public class CheckSatResponse implements SpecificResponse {
+public class CheckSatResponse extends SpecificResponse {
     private enum Status {
         SAT, UNSAT, UNKNOWN
     }

diff --git a/...er-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/GeneralResponse.java b/...er-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/GeneralResponse.java
@@ -7,6 +7,8 @@
 import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.ResponseContext;
 import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Specific_success_responseContext;
 
+import static com.google.common.base.Preconditions.checkState;
+
 public class GeneralResponse {
     private final boolean successful;
     private final String reason;
@@ -51,15 +53,16 @@ public boolean isError() {
     }
 
     public String getReason() {
+        checkState(isError());
         return reason;
     }
 
     public boolean isSpecific() {
         return successful && specificResponse != null;
     }
 
-    @SuppressWarnings("unchecked")
-    public <T extends SpecificResponse> T asSpecific() {
-        return (T) specificResponse;
+    public SpecificResponse asSpecific() {
+        checkState(isSpecific());
+        return specificResponse;
     }
 }
diff --git a/...r-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/GetModelResponse.java b/...r-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/GetModelResponse.java
@@ -7,6 +7,7 @@
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.misc.Interval;
 
+import java.util.Collections;
 import java.util.Map;
 import java.util.stream.Collectors;
 
@@ -15,7 +16,7 @@
 import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Model_response_fun_recContext;
 import static hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Model_response_funs_recContext;
 
-public class GetModelResponse implements SpecificResponse {
+public class GetModelResponse extends SpecificResponse {
     private final SmtLibModel model;
 
     private GetModelResponse(final Map<String, String> values) {
@@ -51,6 +52,10 @@ public Tuple2<String, String> visitModel_response_funs_rec(Model_response_funs_r
         })).collect(Collectors.toUnmodifiableMap(Tuple2::get1, Tuple2::get2)));
     }
 
+    public static GetModelResponse empty() {
+        return new GetModelResponse(Collections.emptyMap());
+    }
+
     public SmtLibModel getModel() {
         return model;
     }

diff --git a/...tlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/GetUnsatCoreResponse.java b/...tlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/GetUnsatCoreResponse.java
@@ -4,9 +4,10 @@
 import org.antlr.v4.runtime.RuleContext;
 
 import java.util.Collection;
+import java.util.Collections;
 import java.util.stream.Collectors;
 
-public class GetUnsatCoreResponse implements SpecificResponse {
+public class GetUnsatCoreResponse extends SpecificResponse {
     private final Collection<String> labels;
 
     private GetUnsatCoreResponse(Collection<String> labels) {
@@ -19,6 +20,10 @@ public static GetUnsatCoreResponse fromContext(Get_unsat_core_responseContext ct
         );
     }
 
+    public static GetUnsatCoreResponse empty() {
+        return new GetUnsatCoreResponse(Collections.emptyList());
+    }
+
     public Collection<String> getLabels() {
         return labels;
     }

diff --git a/...r-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/SpecificResponse.java b/...r-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/parser/SpecificResponse.java
@@ -4,7 +4,9 @@
 import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser;
 import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser.Specific_success_responseContext;
 
-public interface SpecificResponse {
+import static com.google.common.base.Preconditions.checkState;
+
+public abstract class SpecificResponse {
     static SpecificResponse fromContext(final Specific_success_responseContext ctx) {
         return ctx.accept(new SMTLIBv2BaseVisitor<>() {
             @Override
@@ -23,4 +25,51 @@ public SpecificResponse visitGet_model_response(SMTLIBv2Parser.Get_model_respons
             }
         });
     }
+
+    public boolean isCheckSatResponse() {
+        return this instanceof CheckSatResponse;
+    }
+
+    public boolean isGetUnsatCoreResponse() {
+        return
+            this instanceof GetUnsatCoreResponse ||
+            this instanceof GetModelResponse && ((GetModelResponse) this).getModel().size() == 0;
+    }
+
+    public boolean isGetModelResponse() {
+        return
+            this instanceof GetModelResponse ||
+            this instanceof GetUnsatCoreResponse && ((GetUnsatCoreResponse) this).getLabels().size() == 0;
+    }
+
+    public CheckSatResponse asCheckSatResponse() {
+        checkState(isCheckSatResponse());
+        return (CheckSatResponse) this;
+    }
+
+    public GetUnsatCoreResponse asGetUnsatCoreResponse() {
+        checkState(isGetUnsatCoreResponse());
+        if(this instanceof GetUnsatCoreResponse) {
+            return (GetUnsatCoreResponse) this;
+        }
+        else if(this instanceof GetModelResponse) {
+            return GetUnsatCoreResponse.empty();
+        }
+        else {
+            throw new AssertionError();
+        }
+    }
+
+    public GetModelResponse asGetModelResponse() {
+        checkState(isGetModelResponse());
+        if(this instanceof GetModelResponse) {
+            return (GetModelResponse) this;
+        }
+        else if(this instanceof GetUnsatCoreResponse) {
+            return GetModelResponse.empty();
+        }
+        else {
+            throw new AssertionError();
+        }
+    }
 }
diff --git a/...s/solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibParserTest.java b/...s/solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibParserTest.java
@@ -0,0 +1,34 @@
+package hu.bme.mit.theta.solver.smtlib;
+
+import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Lexer;
+import hu.bme.mit.theta.solver.smtlib.dsl.gen.SMTLIBv2Parser;
+import hu.bme.mit.theta.solver.smtlib.solver.parser.GeneralResponse;
+import hu.bme.mit.theta.solver.smtlib.solver.parser.ThrowExceptionErrorListener;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.junit.Assert;
+import org.junit.Test;
+
+public class SmtLibParserTest {
+    @Test
+    public void ambiguousParsingTest() {
+
+        final var response = "(\n)";
+
+        final var lexer = new SMTLIBv2Lexer(CharStreams.fromString(response));
+        final var parser = new SMTLIBv2Parser(new CommonTokenStream(lexer));
+        lexer.removeErrorListeners();
+        lexer.addErrorListener(new ThrowExceptionErrorListener());
+        parser.removeErrorListeners();
+        parser.addErrorListener(new ThrowExceptionErrorListener());
+
+        var general = GeneralResponse.fromContext(parser.response());
+        Assert.assertTrue(general.isSpecific());
+
+        Assert.assertTrue(general.asSpecific().isGetUnsatCoreResponse());
+        Assert.assertEquals(0, general.asSpecific().asGetUnsatCoreResponse().getLabels().size());
+
+        Assert.assertTrue(general.asSpecific().isGetModelResponse());
+        Assert.assertEquals(0, general.asSpecific().asGetModelResponse().getModel().size());
+    }
+}