Merge pull request #4 from mikhirurg/development

Fixed data platform-dependent problems for SMT solver classes
hezzel · Oct 11, 2024 · 80aeb2b · 80aeb2b
2 parents d89d571 + 246eeee
commit 80aeb2b
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 11 deletions.
diff --git a/app/smtsolver_win.bat b/app/smtsolver_win.bat
@@ -0,0 +1,3 @@
+@echo off
+
+z3 %1 > %2
diff --git a/app/src/main/java/charlie/solvesmt/ExternalSmtSolver.java b/app/src/main/java/charlie/solvesmt/ExternalSmtSolver.java
@@ -21,6 +21,7 @@
 import charlie.exceptions.ParseException;
 import charlie.util.ExceptionLogger;
 import charlie.smt.*;
+import charlie.util.SystemUtils;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -56,8 +57,15 @@ private void runSmtSolver() throws IOException, InterruptedException {
     // clean up old result, if any
     try { Process p = rt.exec(new String[] {"rm", "result"}); p.waitFor(); } catch (Exception e) {}
     // start new smtsolver process
-    Process p = rt.exec(new String[] {"./smtsolver", "problem.smt2", "result" });
-    p.waitFor();
+    Process p = null;
+    if (SystemUtils.IS_OS_WINDOWS) {
+      p = rt.exec(new String[] {"smtsolver_win.bat", "problem.smt2", "result"});
+    } else if (SystemUtils.IS_UNIX_LIKE){
+      p = rt.exec(new String[] {"./smtsolver", "problem.smt2", "result" });
+    }
+    if (p != null) {
+      p.waitFor();
+    }
   }
 
   /**

diff --git a/app/src/main/java/charlie/solvesmt/ProcessSmtSolver.java b/app/src/main/java/charlie/solvesmt/ProcessSmtSolver.java
@@ -17,7 +17,11 @@
 
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
+
+import java.io.File;
 import java.io.InputStream;
+import java.nio.file.Files;
+import java.nio.file.Path;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Optional;
@@ -53,7 +57,7 @@ public String toString() {
     @Contract(pure = true)
     public @NotNull String getCommandName() {
       return switch (this) {
-        case Z3: yield  "z3 -in";
+        case Z3: yield  "z3";
         case CVC5: yield  "cvc";
         case YICES2: yield  "yices-smt2";
       };
@@ -85,13 +89,12 @@ public ProcessSmtSolver(@NotNull PhysicalSolver physicalSolver) {
     _physicalSolver = physicalSolver;
   }
 
-  /** Create a process caller for the given input string, with the given timeout (in seconds). */
-  private ProcessCaller createSmtSolverProcess(String smtLibString, int timeout) {
+  /** Create a process caller for the given input file with SMT problem, with the given timeout (in
+   * seconds). */
+  private ProcessCaller createSmtSolverProcess(Path smtProblemFile, int timeout) {
     List<String> commands = new ArrayList<>();
 
-    String commandEchoString = ProcessCaller.callSystemEcho(smtLibString);
-
-    commands.add(commandEchoString + " | " + _physicalSolver.getCommandName());
+    commands.add(_physicalSolver.getCommandName() + " " + smtProblemFile.toString());
 
     return new ProcessCaller(commands, timeout);
   }
@@ -112,10 +115,16 @@ private ProcessCaller createSmtSolverProcess(String smtLibString, int timeout) {
   public Answer checkSatisfiability(SmtProblem problem) {
     SMTLibString file = new SMTLibString(V26, QFNIA);
     String stringOfSmtProblem = file.buildSmtlibString(problem);
-    ProcessCaller pc = createSmtSolverProcess(stringOfSmtProblem, TIMEOUT);
-    String smtResultString = null;
+    String smtResultString;
     try {
+      Path smtProblemFile = Files.createTempFile("coraSMTTask_sat_", null);
+      Files.writeString(smtProblemFile, stringOfSmtProblem);
+
+      ProcessCaller pc = createSmtSolverProcess(smtProblemFile, TIMEOUT);
       Optional<String> optionalSmtResultString = pc.getResultAsString();
+
+      Files.delete(smtProblemFile);
+
       if (!optionalSmtResultString.isPresent()) {
         return new Answer.MAYBE("SMT solver process did not return an answer within the " +
                                 "time limit.");
@@ -163,9 +172,16 @@ public boolean checkValidity(SmtProblem problem) {
         negated
       );
 
-    ProcessCaller pc = createSmtSolverProcess(stringOfSmtProblem, TIMEOUT);
     try {
+
+      Path smtProblemFile = Files.createTempFile("coraSMTTask_validity_", null);
+      Files.writeString(smtProblemFile, stringOfSmtProblem);
+
+      ProcessCaller pc = createSmtSolverProcess(smtProblemFile, TIMEOUT);
       Optional<InputStream> is = pc.getResultAsInputStream();
+
+      Files.delete(smtProblemFile);
+
       if (is.isPresent()) {
         Scanner scanner = new Scanner(is.get());
         return SMTLibResponseHandler.readAnswer(scanner).equals("unsat");