1 files changed, 52 insertions, 0 deletions
diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp
new file mode 100644
index 00000000..e8f30c9e
--- /dev/null
+++ b/lib/Solver/SolverImpl.cpp
@@ -0,0 +1,52 @@
+//===-- SolverImpl.cpp ----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+
+using namespace klee;
+
+SolverImpl::~SolverImpl() {}
+
+bool SolverImpl::computeValidity(const Query &query, Solver::Validity &result) {
+  bool isTrue, isFalse;
+  if (!computeTruth(query, isTrue))
+    return false;
+  if (isTrue) {
+    result = Solver::True;
+  } else {
+    if (!computeTruth(query.negateExpr(), isFalse))
+      return false;
+    result = isFalse ? Solver::False : Solver::Unknown;
+  }
+  return true;
+}
+
+const char *SolverImpl::getOperationStatusString(SolverRunStatus statusCode) {
+  switch (statusCode) {
+  case SOLVER_RUN_STATUS_SUCCESS_SOLVABLE:
+    return "OPERATION SUCCESSFUL, QUERY IS SOLVABLE";
+  case SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE:
+    return "OPERATION SUCCESSFUL, QUERY IS UNSOLVABLE";
+  case SOLVER_RUN_STATUS_FAILURE:
+    return "OPERATION FAILED";
+  case SOLVER_RUN_STATUS_TIMEOUT:
+    return "SOLVER TIMEOUT";
+  case SOLVER_RUN_STATUS_FORK_FAILED:
+    return "FORK FAILED";
+  case SOLVER_RUN_STATUS_INTERRUPTED:
+    return "SOLVER PROCESS INTERRUPTED";
+  case SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE:
+    return "UNEXPECTED SOLVER PROCESS EXIT CODE";
+  case SOLVER_RUN_STATUS_WAITPID_FAILED:
+    return "WAITPID FAILED FOR SOLVER PROCESS";
+  default:
+    return "UNRECOGNIZED OPERATION STATUS";
+  }
+}