From 19958fe5b9b44442ba270fd5db0e0ffba97c5f0e Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 23 Sep 2024 14:55:30 -0400
Subject: [PATCH] SMT2: implement cond

This adds support for cond_exprt, via a lowering to nested ?:, to the SMT
backend.
---
 src/solvers/smt2/smt2_conv.cpp |  5 +++++
 src/util/std_expr.cpp          | 29 +++++++++++++++++++++++++++++
 src/util/std_expr.h            |  3 +++
 3 files changed, 37 insertions(+)

diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index c1e26e2d0ec..c57790aeea0 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -2490,6 +2490,11 @@ void smt2_convt::convert_expr(const exprt &expr)
       out << ')';
     }
   }
+  else if(expr.id() == ID_cond)
+  {
+    // use the lowering
+    convert_expr(to_cond_expr(expr).lower());
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 506298c26ce..885f1b65ab5 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -260,3 +260,32 @@ exprt binding_exprt::instantiate(const variablest &new_variables) const
     values.push_back(new_variable);
   return instantiate(values);
 }
+
+exprt cond_exprt::lower() const
+{
+  INVARIANT(
+    operands().size() % 2 == 0, "cond must have even number of operands");
+
+  exprt result = nil_exprt();
+
+  auto &operands = this->operands();
+
+  // functional version -- go backwards
+  for(std::size_t i = operands.size(); i != 0; i -= 2)
+  {
+    INVARIANT(
+      i >= 2,
+      "since the number of operands is even if i is nonzero it must be "
+      "greater than two");
+
+    const exprt &cond = operands[i - 2];
+    const exprt &value = operands[i - 1];
+
+    if(result.is_nil())
+      result = value;
+    else
+      result = if_exprt{cond, value, std::move(result)};
+  }
+
+  return result;
+}
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 9c10b8e8389..39b68e83655 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -3491,6 +3491,9 @@ class cond_exprt : public multi_ary_exprt
     operands().push_back(condition);
     operands().push_back(value);
   }
+
+  // a lowering to nested if_exprt
+  exprt lower() const;
 };
 
 template <>