diff options
Diffstat (limited to 'lib/Solver/Solver.cpp')
-rw-r--r-- | lib/Solver/Solver.cpp | 46 |
1 files changed, 0 insertions, 46 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 6f4bbc5b..30424526 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -69,52 +69,6 @@ using namespace metaSMT::solver; #endif /* SUPPORT_METASMT */ - - -/***/ - -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"; - } -} - const char *Solver::validity_to_str(Validity v) { switch (v) { default: return "Unknown"; |