Merge pull request #8467 from diffblue/smt2-cond

SMT2: implement cond

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,

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;
+}

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 <>