| 116 | namespace |
| 117 | { |
| 118 | std::vector<std::string> parseValuesFromResponse(std::string const& _response) |
| 119 | { |
| 120 | std::stringstream ss(_response); |
| 121 | std::string answer; |
| 122 | ss >> answer; |
| 123 | smtSolverInteractionRequire(answer == "sat", "SMT: Parsing model values only possible after sat answer"); |
| 124 | |
| 125 | std::vector<SMTLib2Expression> parsedOutput; |
| 126 | SMTLib2Parser parser(ss); |
| 127 | try |
| 128 | { |
| 129 | while (!parser.isEOF()) |
| 130 | parsedOutput.push_back(parser.parseExpression()); |
| 131 | } |
| 132 | catch(SMTLib2Parser::ParsingException&) |
| 133 | { |
| 134 | smtSolverInteractionRequire(false, "Error during parsing SMT answer"); |
| 135 | } |
| 136 | smtSolverInteractionRequire(parsedOutput.size() == 1, "SMT: Expected model values as a single s-expression"); |
| 137 | auto const& values = parsedOutput[0]; |
| 138 | smtSolverInteractionRequire(!isAtom(values), "Invalid format of values in SMT answer"); |
| 139 | std::vector<std::string> parsedValues; |
| 140 | for (auto const& nameValuePair: asSubExpressions(values)) |
| 141 | { |
| 142 | smtSolverInteractionRequire(!isAtom(nameValuePair), "Invalid format of values in SMT answer"); |
| 143 | smtSolverInteractionRequire(asSubExpressions(nameValuePair).size() == 2, "Invalid format of values in SMT answer"); |
| 144 | auto const& value = asSubExpressions(nameValuePair)[1]; |
| 145 | parsedValues.push_back(value.toString()); |
| 146 | } |
| 147 | return parsedValues; |
| 148 | } |
| 149 | } // namespace |
| 150 | |
| 151 | std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::vector<Expression> const& _expressionsToEvaluate) |