constructor for tuple_exprt with type

kroening · kroening · commit a7ba766e8563 · 2022-04-14T18:11:35.000-04:00
This adds a constructor for tuple_exprt that allows setting the type.
diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h
@@ -185,6 +185,11 @@ class tuple_exprt : public multi_ary_exprt
     : multi_ary_exprt(ID_tuple, std::move(operands), typet())
   {
   }
+
+  tuple_exprt(exprt::operandst operands, typet type)
+    : multi_ary_exprt(ID_tuple, std::move(operands), std::move(type))
+  {
+  }
 };
 
 /// \brief Application of (mathematical) function

Original file line number	Diff line number	Diff line change
`@@ -185,6 +185,11 @@ class tuple_exprt : public multi_ary_exprt`
`185`	`185`	`: multi_ary_exprt(ID_tuple, std::move(operands), typet())`
`186`	`186`	`{`
`187`	`187`	`}`
	`188`	`+`
	`189`	`+ tuple_exprt(exprt::operandst operands, typet type)`
	`190`	`+ : multi_ary_exprt(ID_tuple, std::move(operands), std::move(type))`
	`191`	`+ {`
	`192`	`+ }`
`188`	`193`	`};`
`189`	`194`
`190`	`195`	`/// \brief Application of (mathematical) function`