| 149 | } // namespace |
| 150 | |
| 151 | std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::vector<Expression> const& _expressionsToEvaluate) |
| 152 | { |
| 153 | std::string response = querySolver(dumpQuery(_expressionsToEvaluate)); |
| 154 | |
| 155 | CheckResult result; |
| 156 | // TODO proper parsing |
| 157 | if (boost::starts_with(response, "sat")) |
| 158 | result = CheckResult::SATISFIABLE; |
| 159 | else if (boost::starts_with(response, "unsat")) |
| 160 | result = CheckResult::UNSATISFIABLE; |
| 161 | else if (boost::starts_with(response, "unknown")) |
| 162 | result = CheckResult::UNKNOWN; |
| 163 | else |
| 164 | result = CheckResult::ERROR; |
| 165 | |
| 166 | std::vector<std::string> values; |
| 167 | if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) |
| 168 | values = parseValuesFromResponse(response); |
| 169 | return std::make_pair(result, values); |
| 170 | } |
| 171 | |
| 172 | std::string SMTLib2Interface::toSmtLibSort(SortPointer _sort) |
| 173 | { |
nothing calls this directly
no test coverage detected