Add missing SMT solver option: MathSAT

kind2-mc · Apr 19, 2023 · 91002eb · 91002eb
1 parent 91503a2
commit 91002eb
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/build.gradle b/build.gradle
@@ -8,7 +8,7 @@ repositories {
 }
 
 dependencies {
-  implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.2'
+  implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.3'
   implementation 'org.eclipse.lsp4j:org.eclipse.lsp4j:0.13.0'
   testImplementation 'org.junit.jupiter:junit-jupiter-api:5.7.2'
   testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.7.2'

diff --git a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java
@@ -370,6 +370,8 @@ private SolverOption stringToSolver(String solver) {
       return SolverOption.BITWUZLA;
     case "CVC5":
       return SolverOption.CVC5;
+    case "MATHSAT":
+      return SolverOption.MATHSAT;
     case "YICES":
       return SolverOption.YICES;
     case "YICES2":
@@ -464,6 +466,11 @@ private void setSmtSolverPath(Kind2Api api, SolverOption solver,
           api.setcvc5Bin(smtConfigs.get("cvc5_bin").getAsString());
         }
         break;
+      case MATHSAT:
+        if (!smtConfigs.get("mathsat_bin").getAsString().equals("mathsat")) {
+          api.setMathSATBin(smtConfigs.get("mathsat_bin").getAsString());
+        }
+        break;
       case YICES:
         if (!smtConfigs.get("yices_bin").getAsString().equals("yices")) {
           api.setYicesBin(smtConfigs.get("yices_bin").getAsString());