| 237 | } |
| 238 | |
| 239 | SortPointer CHCSmtLib2Interface::ScopedParser::toSort(SMTLib2Expression const& _expr) |
| 240 | { |
| 241 | if (isAtom(_expr)) |
| 242 | { |
| 243 | auto const& name = asAtom(_expr); |
| 244 | if (name == "Int") |
| 245 | return SortProvider::sintSort; |
| 246 | if (name == "Bool") |
| 247 | return SortProvider::boolSort; |
| 248 | auto tupleSort = lookupKnownTupleSort(name); |
| 249 | if (tupleSort) |
| 250 | return tupleSort.value(); |
| 251 | } |
| 252 | else |
| 253 | { |
| 254 | auto const& args = asSubExpressions(_expr); |
| 255 | if (asAtom(args[0]) == "Array") |
| 256 | { |
| 257 | smtSolverInteractionRequire(args.size() == 3, "Wrong format of Array sort in solver's response"); |
| 258 | auto domainSort = toSort(args[1]); |
| 259 | auto codomainSort = toSort(args[2]); |
| 260 | return std::make_shared<ArraySort>(std::move(domainSort), std::move(codomainSort)); |
| 261 | } |
| 262 | if (args.size() == 3 && isAtom(args[0]) && asAtom(args[0]) == "_" && isAtom(args[1]) |
| 263 | && asAtom(args[1]) == "int2bv") |
| 264 | return std::make_shared<BitVectorSort>(std::stoul(asAtom(args[2]))); |
| 265 | } |
| 266 | smtSolverInteractionRequire(false, "Unknown sort encountered"); |
| 267 | } |
| 268 | |
| 269 | smtutil::Expression CHCSmtLib2Interface::ScopedParser::parseQuantifier( |
| 270 | std::string const& _quantifierName, |
no test coverage detected