Handle custom tuple sorts in a general way

This commit is contained in:
Martin Blicha 2023-07-27 16:19:53 +02:00
parent 742642ebae
commit 4ecaa476fd

View File

@ -294,15 +294,7 @@ namespace
public:
SMTLibTranslationContext(SMTLib2Interface const& _smtlib2Interface) : m_smtlib2Interface(_smtlib2Interface) {}
SortPointer toSort(SMTLib2Expression const& expr)
{
if (isAtom(expr))
{
auto const& name = asAtom(expr);
if (name == "Int")
return SortProvider::sintSort;
if (name == "Bool")
return SortProvider::boolSort;
std::optional<SortPointer> lookupKnownTupleSort(std::string const& name) {
std::string quotedName = "|" + name + "|";
auto it = ranges::find_if(m_smtlib2Interface.sortNames(), [&](auto const& entry) {
return entry.second == name || entry.second == quotedName;
@ -314,6 +306,21 @@ namespace
return tupleSort;
}
}
return {};
}
SortPointer toSort(SMTLib2Expression const& expr)
{
if (isAtom(expr))
{
auto const& name = asAtom(expr);
if (name == "Int")
return SortProvider::sintSort;
if (name == "Bool")
return SortProvider::boolSort;
auto tupleSort = lookupKnownTupleSort(name);
if (tupleSort)
return tupleSort.value();
} else {
auto const& args = asSubExpressions(expr);
if (asAtom(args[0]) == "Array")
@ -346,13 +353,9 @@ namespace
for (size_t i = 1; i < _subExpr.size(); i++)
arguments.emplace_back(toSMTUtilExpression(_subExpr[i]));
std::string const& op = asAtom(_subExpr.front());
if (boost::starts_with(op, "struct")) {
auto sort = toSort(_subExpr.front());
auto sortSort = std::make_shared<SortSort>(sort);
return Expression::tuple_constructor(Expression(sortSort), arguments);
} else if (op.find("array_tuple") != std::string::npos) {
auto sort = toSort(_subExpr.front());
auto sortSort = std::make_shared<SortSort>(sort);
if (auto tupleSort = lookupKnownTupleSort(op); tupleSort)
{
auto sortSort = std::make_shared<SortSort>(tupleSort.value());
return Expression::tuple_constructor(Expression(sortSort), arguments);
} else {
std::set<std::string> boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=",