From 7ecea100928755fb5f5cb37b638799177b3114c1 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Fri, 14 Aug 2026 17:02:56 +1000
Subject: [PATCH 1/7] API BREAK: add preliminary support for union types
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This support is extremely limited. The intent is to allow parsing
`union` with librumur so users can build union-supporting tools on top,
but not to support `union` within `rumur`. Despite this, some partial
handling of `union` is added within `rumur`. The intent of this is to
avoid anything slipping through the cracks if/when `union` support is
added to `rumur` in future. I.e. any attempt to do this should result in
visible errors surfacing from these locations that need to be updated.

This change does not include changes to the parser itself, which will
arrive in an upcoming commit.

There are a number of notable divergences from CMurphi semantics:
  1. As discussed in an added comment, unions with 0 or 1 members are
     supported in contrast to CMurphi.
  2. Differing unions within other types make the containing types
     non-equal. E.g. CMurphi appears to consider variables of types
     `record a: union {foo, bar}; endrecord` and
     `record a: union {foo, baz}; endrecord` to be
     comparable/assignable/etc because they have at least one equivalent
     type interpretation. In Rumur, we do not consider these variables
     compatible in this way.

Gitlab: #331 “MultiSet support within scope?”
---
 librumur/include/rumur/TypeExpr.h             |  18 +++
 librumur/include/rumur/indexer.h              |   1 +
 librumur/include/rumur/traverse.h             |   6 +
 librumur/src/Expr.cc                          |   6 +-
 librumur/src/TypeExpr.cc                      | 124 ++++++++++++++++++
 librumur/src/indexer.cc                       |   6 +
 librumur/src/traverse.cc                      |  20 +++
 librumur/src/validate.cc                      |   6 +
 misc/murphi2xml.rng                           |  12 ++
 murphi2c/src/CLikeGenerator.cc                |   7 +
 murphi2c/src/CLikeGenerator.h                 |   1 +
 murphi2c/src/check.cc                         |   7 +
 .../src/DecomposeComplexComparisons.cc        |  24 +++-
 murphi2murphi/src/Printer.cc                  |   9 ++
 murphi2murphi/src/Printer.h                   |   1 +
 murphi2murphi/src/Stage.cc                    |   1 +
 murphi2murphi/src/Stage.h                     |   1 +
 murphi2smv/doc/murphi2smv.1                   |   2 +
 murphi2smv/src/codegen.cc                     |  14 ++
 murphi2uclid/doc/murphi2uclid.1               |   2 +
 murphi2uclid/src/check.cc                     |   4 +
 murphi2uclid/src/codegen.cc                   |   5 +
 murphi2xml/src/XMLPrinter.cc                  |  13 ++
 murphi2xml/src/XMLPrinter.h                   |   1 +
 rumur/CMakeLists.txt                          |   1 +
 rumur/src/check.cc                            |  20 +++
 rumur/src/check.h                             |   6 +
 rumur/src/generate-print.cc                   |   7 +
 rumur/src/generate-stmt.cc                    |   7 +
 rumur/src/main.cc                             |  13 ++
 rumur/src/smt/define-enum-members.cc          |   6 +
 rumur/src/smt/define-records.cc               |   6 +
 rumur/src/smt/simplify.cc                     |  11 ++
 rumur/src/smt/typeexpr-to-smt.cc              |   4 +
 rumur/src/symmetry-reduction.cc               |  10 ++
 35 files changed, 374 insertions(+), 8 deletions(-)
 create mode 100644 rumur/src/check.cc
 create mode 100644 rumur/src/check.h

diff --git a/librumur/include/rumur/TypeExpr.h b/librumur/include/rumur/TypeExpr.h
index a8592490..0adb8ae1 100644
--- a/librumur/include/rumur/TypeExpr.h
+++ b/librumur/include/rumur/TypeExpr.h
@@ -190,4 +190,22 @@ struct RUMUR_API_WITH_RTTI TypeExprID : public TypeExpr {
   bool constant() const override;
 };
 
+struct RUMUR_API_WITH_RTTI Union : public TypeExpr {
+  std::vector<Ptr<TypeExpr>> members;
+
+  Union(const std::vector<Ptr<TypeExpr>> &members_, const location &loc_);
+  Union *clone() const override;
+
+  void visit(BaseTraversal &visitor) override;
+  void visit(ConstBaseTraversal &visitor) const override;
+
+  mpz_class count() const override;
+  bool is_simple() const override;
+  void validate() const override;
+  mpz_class lower_bound() const override;
+  mpz_class upper_bound() const override;
+  void to_stream(std::ostream &out) const override;
+  bool constant() const override;
+};
+
 } // namespace rumur
diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h
index 16cccb4a..258865d1 100644
--- a/librumur/include/rumur/indexer.h
+++ b/librumur/include/rumur/indexer.h
@@ -85,6 +85,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal {
   void visit_typedecl(TypeDecl &n) override;
   void visit_typeexprid(TypeExprID &n) override;
   void visit_undefine(Undefine &n) override;
+  void visit_union(Union &n) override;
   void visit_vardecl(VarDecl &n) override;
   void visit_while(While &n) override;
   void visit_xor(Xor &n) override;
diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h
index 60d4bf56..d9f275a9 100644
--- a/librumur/include/rumur/traverse.h
+++ b/librumur/include/rumur/traverse.h
@@ -131,6 +131,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal {
   virtual void visit_typedecl(TypeDecl &n) = 0;
   virtual void visit_typeexprid(TypeExprID &n) = 0;
   virtual void visit_undefine(Undefine &n) = 0;
+  virtual void visit_union(Union &n) = 0;
   virtual void visit_vardecl(VarDecl &n) = 0;
   virtual void visit_while(While &n) = 0;
   virtual void visit_xor(Xor &n) = 0;
@@ -217,6 +218,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal {
   void visit_typedecl(TypeDecl &n) override;
   void visit_typeexprid(TypeExprID &n) override;
   void visit_undefine(Undefine &n) override;
+  void visit_union(Union &n) override;
   void visit_vardecl(VarDecl &n) override;
   void visit_while(While &n) override;
   void visit_xor(Xor &n) override;
@@ -295,6 +297,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal {
   virtual void visit_typedecl(const TypeDecl &n) = 0;
   virtual void visit_typeexprid(const TypeExprID &n) = 0;
   virtual void visit_undefine(const Undefine &n) = 0;
+  virtual void visit_union(const Union &n) = 0;
   virtual void visit_vardecl(const VarDecl &n) = 0;
   virtual void visit_while(const While &n) = 0;
   virtual void visit_xor(const Xor &n) = 0;
@@ -373,6 +376,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal {
   void visit_typedecl(const TypeDecl &n) override;
   void visit_typeexprid(const TypeExprID &n) override;
   void visit_undefine(const Undefine &n) override;
+  void visit_union(const Union &n) override;
   void visit_vardecl(const VarDecl &n) override;
   void visit_while(const While &n) override;
   void visit_xor(const Xor &n) override;
@@ -424,6 +428,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal {
   void visit_typedecl(const TypeDecl &n) final;
   void visit_typeexprid(const TypeExprID &n) final;
   void visit_undefine(const Undefine &n) final;
+  void visit_union(const Union &n) final;
   void visit_vardecl(const VarDecl &n) final;
   void visit_while(const While &n) final;
 };
@@ -485,6 +490,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal {
   void visit_ternary(const Ternary &n) final;
   void visit_typedecl(const TypeDecl &n) final;
   void visit_typeexprid(const TypeExprID &n) final;
+  void visit_union(const Union &n) final;
   void visit_vardecl(const VarDecl &n) final;
   void visit_xor(const Xor &n) final;
 
diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc
index 32f65580..293f6ac6 100644
--- a/librumur/src/Expr.cc
+++ b/librumur/src/Expr.cc
@@ -1398,8 +1398,10 @@ void FunctionCall::validate() const {
     // callee’s handles are compatible
     if (!v->is_readonly() && isa<Range>(param_type)) {
       const Ptr<TypeExpr> arg_type = a_type->resolve();
-      assert(isa<Range>(arg_type) &&
-             "non-range considered type-compatible with range");
+      if (!isa<Range>(arg_type))
+        throw Error("non-range typed function call argument passed as "
+                    "range-typed var parameter",
+                    (*it)->loc);
 
       auto p = dynamic_cast<const Range &>(*param_type);
       auto a = dynamic_cast<const Range &>(*arg_type);
diff --git a/librumur/src/TypeExpr.cc b/librumur/src/TypeExpr.cc
index 680531f2..1e0c75b5 100644
--- a/librumur/src/TypeExpr.cc
+++ b/librumur/src/TypeExpr.cc
@@ -147,6 +147,19 @@ static bool equal(const TypeExpr &t1, const TypeExpr &t2) {
     }
 
     void visit_typeexprid(const TypeExprID &n) final { dispatch(*n.referent); }
+
+    void visit_union(const Union &n) final {
+      if (auto u = dynamic_cast<const Union *>(t.get())) {
+        if (u->members.size() != n.members.size()) {
+          result = false;
+        } else {
+          for (size_t i = 0; i < n.members.size(); ++i)
+            result &= equal(*u->members[i], *n.members[i]);
+        }
+      } else {
+        result = false;
+      }
+    }
   };
 
   Equater eq(t1);
@@ -162,6 +175,22 @@ bool TypeExpr::coerces_to(const TypeExpr &other) const {
   if (isa<Range>(t1) && isa<Range>(t2))
     return true;
 
+  if (auto u = dynamic_cast<const Union *>(t2.get())) {
+    for (const Ptr<TypeExpr> &m : u->members) {
+      if (t1->coerces_to(*m))
+        return true;
+    }
+    return false;
+  }
+
+  if (auto u = dynamic_cast<const Union *>(t1.get())) {
+    for (const Ptr<TypeExpr> &m : u->members) {
+      if (m->coerces_to(*t2))
+        return true;
+    }
+    return false;
+  }
+
   return equal(*t1, *t2);
 }
 
@@ -477,4 +506,99 @@ bool TypeExprID::constant() const {
   return referent->value->constant();
 }
 
+Union::Union(const std::vector<Ptr<TypeExpr>> &members_, const location &loc_)
+    : TypeExpr(loc_), members(members_) {}
+
+Union *Union::clone() const { return new Union(*this); }
+
+void Union::visit(BaseTraversal &visitor) { visitor.visit_union(*this); }
+
+void Union::visit(ConstBaseTraversal &visitor) const {
+  visitor.visit_union(*this);
+}
+
+mpz_class Union::count() const {
+  mpz_class c = 1;
+  for (const Ptr<TypeExpr> &m : members)
+    c += m->count();
+  return c;
+}
+
+bool Union::is_simple() const {
+  for (const Ptr<TypeExpr> &m : members) {
+    if (!m->is_simple())
+      return false;
+  }
+  return true;
+}
+
+void Union::validate() const {
+  // In contrast to CMurphi, we treat unions containing 0 or 1 members as legal.
+  // We also allow a single type to appear multiple times within the union.
+  // There is no known practical use for most of these edge cases, but it
+  // simplifies work for generators of Murphi models.
+}
+
+mpz_class Union::lower_bound() const {
+  if (!is_simple())
+    throw Error("union is not a simple type and thus its lower bound cannot be "
+                "determined",
+                loc);
+
+  mpz_class bound;
+  bool set = false;
+  for (const Ptr<TypeExpr> &m : members) {
+    const mpz_class b = m->lower_bound();
+    if (!set || b < bound)
+      bound = b;
+    set = true;
+  }
+
+  if (!set)
+    bound = 0;
+
+  return bound;
+}
+
+mpz_class Union::upper_bound() const {
+  if (!is_simple())
+    throw Error("union is not a simple type and thus its upper bound cannot be "
+                "determined",
+                loc);
+
+  mpz_class bound;
+  bool set = false;
+  for (const Ptr<TypeExpr> &m : members) {
+    const mpz_class b = m->upper_bound();
+    if (!set || b > bound)
+      bound = b;
+    set = true;
+  }
+
+  if (!set)
+    bound = 0;
+
+  return bound;
+}
+
+void Union::to_stream(std::ostream &out) const {
+  out << "union {";
+  const char *separator = "";
+  for (const Ptr<TypeExpr> &m : members) {
+    out << separator << *m;
+    separator = ", ";
+  }
+  out << "}";
+}
+
+bool Union::constant() const {
+  for (const Ptr<TypeExpr> &m : members) {
+    if (!m->is_simple())
+      return false;
+    if (!m->constant())
+      return false;
+  }
+  return true;
+}
+
 } // namespace rumur
diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc
index fdbcbdca..76da1dbb 100644
--- a/librumur/src/indexer.cc
+++ b/librumur/src/indexer.cc
@@ -326,6 +326,12 @@ void Indexer::visit_undefine(Undefine &n) {
   dispatch(*n.rhs);
 }
 
+void Indexer::visit_union(Union &n) {
+  n.unique_id = next++;
+  for (Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void Indexer::visit_vardecl(VarDecl &n) {
   n.unique_id = next++;
   dispatch(*n.type);
diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc
index ea071d70..fe467ab5 100644
--- a/librumur/src/traverse.cc
+++ b/librumur/src/traverse.cc
@@ -267,6 +267,11 @@ void Traversal::visit_uexpr(UnaryExpr &n) { dispatch(*n.rhs); }
 
 void Traversal::visit_undefine(Undefine &n) { dispatch(*n.rhs); }
 
+void Traversal::visit_union(Union &n) {
+  for (Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void Traversal::visit_vardecl(VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
@@ -540,6 +545,11 @@ void ConstTraversal::visit_uexpr(const UnaryExpr &n) { dispatch(*n.rhs); }
 
 void ConstTraversal::visit_undefine(const Undefine &n) { dispatch(*n.rhs); }
 
+void ConstTraversal::visit_union(const Union &n) {
+  for (const Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void ConstTraversal::visit_vardecl(const VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
@@ -728,6 +738,11 @@ void ConstExprTraversal::visit_typeexprid(const TypeExprID &) {}
 
 void ConstExprTraversal::visit_undefine(const Undefine &n) { dispatch(*n.rhs); }
 
+void ConstExprTraversal::visit_union(const Union &n) {
+  for (const Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void ConstExprTraversal::visit_vardecl(const VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
@@ -946,6 +961,11 @@ void ConstStmtTraversal::visit_typeexprid(const TypeExprID &) {}
 
 void ConstStmtTraversal::visit_uexpr(const UnaryExpr &n) { dispatch(*n.rhs); }
 
+void ConstStmtTraversal::visit_union(const Union &n) {
+  for (const Ptr<TypeExpr> &m : n.members)
+    dispatch(*m);
+}
+
 void ConstStmtTraversal::visit_vardecl(const VarDecl &n) {
   if (n.type != nullptr)
     dispatch(*n.type);
diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc
index 1b577814..ca241ceb 100644
--- a/librumur/src/validate.cc
+++ b/librumur/src/validate.cc
@@ -415,6 +415,12 @@ class Validator : public ConstBaseTraversal {
     n.validate();
   }
 
+  void visit_union(const Union &n) final {
+    for (const Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+    n.validate();
+  }
+
   void visit_vardecl(const VarDecl &n) final {
     if (n.type != nullptr)
       dispatch(*n.type);
diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng
index 5cda0fa3..e88ad28d 100644
--- a/misc/murphi2xml.rng
+++ b/misc/murphi2xml.rng
@@ -1084,6 +1084,7 @@
       <ref name="record"/>
       <ref name="scalarset"/>
       <ref name="typeexprid"/>
+      <ref name="union"/>
     </choice>
   </define>
 
@@ -1116,6 +1117,17 @@
     </element>
   </define>
 
+  <define name="union">
+    <element name="union">
+      <ref name="location"/>
+      <ref name="content"/>
+      <zeroOrMore>
+        <ref name="typeexpr"/>
+        <ref name="content"/>
+      </zeroOrMore>
+    </element>
+  </define>
+
   <define name="unit">
     <element name="unit">
       <attribute name="filename">
diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc
index e13d244e..2177a808 100644
--- a/murphi2c/src/CLikeGenerator.cc
+++ b/murphi2c/src/CLikeGenerator.cc
@@ -521,6 +521,8 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t,
 
   const Ptr<TypeExpr> type = t.resolve();
 
+  assert(!isa<Union>(type) && "union type was not rejected during check()");
+
   // if this is boolean, handle it separately to other Enums to avoid
   // -Wswitch-bool warnings and cope with badly behaved users setting non-0/1
   // values
@@ -833,6 +835,11 @@ void CLikeGenerator::visit_undefine(const Undefine &n) {
   *this << "\n";
 }
 
+void CLikeGenerator::visit_union(const Union &) {
+  assert(!"union type was not rejected during check()");
+  __builtin_unreachable();
+}
+
 void CLikeGenerator::visit_while(const While &n) {
   *this << indentation() << "while " << *n.condition << " {\n";
   indent();
diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h
index c9240011..27c2889e 100644
--- a/murphi2c/src/CLikeGenerator.h
+++ b/murphi2c/src/CLikeGenerator.h
@@ -94,6 +94,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator
   void visit_typedecl(const rumur::TypeDecl &n) final;
   void visit_typeexprid(const rumur::TypeExprID &n) final;
   void visit_undefine(const rumur::Undefine &n) final;
+  void visit_union(const rumur::Union &n) final;
   void visit_while(const rumur::While &n) final;
   void visit_xor(const rumur::Xor &n) final;
 
diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc
index dda46b22..db113486 100644
--- a/murphi2c/src/check.cc
+++ b/murphi2c/src/check.cc
@@ -19,6 +19,13 @@ class Check : public ConstTraversal {
       ok = false;
     }
   }
+
+  void visit_union(const Union &) final {
+    if (ok) {
+      std::cerr << "union types are not supported\n";
+      ok = false;
+    }
+  }
 };
 
 } // namespace
diff --git a/murphi2murphi/src/DecomposeComplexComparisons.cc b/murphi2murphi/src/DecomposeComplexComparisons.cc
index ab9c5b71..df80cf53 100644
--- a/murphi2murphi/src/DecomposeComplexComparisons.cc
+++ b/murphi2murphi/src/DecomposeComplexComparisons.cc
@@ -1,4 +1,5 @@
 #include "DecomposeComplexComparisons.h"
+#include "../../common/isa.h"
 #include "Stage.h"
 #include <cassert>
 #include <climits>
@@ -66,6 +67,13 @@ static std::string explode(std::unordered_set<std::string> &ids,
 
   const Ptr<TypeExpr> t = type.resolve();
 
+  // if this is a union, assume there is no reasonable way to decompose its
+  // comparison
+  if (isa<Union>(t)) {
+    buf << prefix_a << stem << (is_eq ? " = " : " != ") << prefix_b << stem;
+    return buf.str();
+  }
+
   // if this is a record, join together a comparison of each of its fields
   if (auto r = dynamic_cast<const Record *>(t.get())) {
     std::string sep;
@@ -99,12 +107,15 @@ void DecomposeComplexComparisons::rewrite(const EquatableBinaryExpr &n,
                                           bool is_eq) {
 
   // if this is a comparison of simple types, we can let it pass through
-  const Ptr<TypeExpr> t = n.lhs->type();
-  if (t->is_simple()) {
-
-    assert(n.rhs->type()->is_simple() &&
-           "comparison of simple type to complex type");
+  const Ptr<TypeExpr> lhs_type = n.lhs->type();
+  const Ptr<TypeExpr> rhs_type = n.rhs->type();
+  if (lhs_type->is_simple() && rhs_type->is_simple()) {
+    next.dispatch(n);
+    return;
+  }
 
+  // is either side is of union type, we cannot decompose this
+  if (isa<Union>(lhs_type) || isa<Union>(rhs_type)) {
     next.dispatch(n);
     return;
   }
@@ -133,5 +144,6 @@ void DecomposeComplexComparisons::rewrite(const EquatableBinaryExpr &n,
   ids.insert(rhs_ids.begin(), rhs_ids.end());
 
   // write a decomposed version of the comparison
-  *top << explode(ids, n.lhs->to_string(), n.rhs->to_string(), "", *t, is_eq);
+  *top << explode(ids, n.lhs->to_string(), n.rhs->to_string(), "", *lhs_type,
+                  is_eq);
 }
diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc
index 20f9318c..646404d1 100644
--- a/murphi2murphi/src/Printer.cc
+++ b/murphi2murphi/src/Printer.cc
@@ -513,6 +513,15 @@ void Printer::visit_undefine(const Undefine &n) {
   top->sync_to(n.loc.end);
 }
 
+void Printer::visit_union(const Union &n) {
+  top->sync_to(n);
+  for (const Ptr<TypeExpr> &m : n.members) {
+    top->sync_to(*m);
+    top->dispatch(*m);
+  }
+  top->sync_to(n.loc.end);
+}
+
 void Printer::visit_vardecl(const VarDecl &n) {
   top->sync_to(n);
   top->sync_to(*n.type);
diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h
index 4de85f70..91931852 100644
--- a/murphi2murphi/src/Printer.h
+++ b/murphi2murphi/src/Printer.h
@@ -80,6 +80,7 @@ class Printer : public Stage {
   void visit_typedecl(const rumur::TypeDecl &n) final;
   void visit_typeexprid(const rumur::TypeExprID &n) final;
   void visit_undefine(const rumur::Undefine &n) final;
+  void visit_union(const rumur::Union &n) final;
   void visit_vardecl(const rumur::VarDecl &n) final;
   void visit_while(const rumur::While &n) final;
   void visit_xor(const rumur::Xor &n) final;
diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc
index 83df4e79..8215bc60 100644
--- a/murphi2murphi/src/Stage.cc
+++ b/murphi2murphi/src/Stage.cc
@@ -185,6 +185,7 @@ void IntermediateStage::visit_typeexprid(const TypeExprID &n) {
 void IntermediateStage::visit_undefine(const Undefine &n) {
   next.visit_undefine(n);
 }
+void IntermediateStage::visit_union(const Union &n) { next.visit_union(n); }
 void IntermediateStage::visit_vardecl(const VarDecl &n) {
   next.visit_vardecl(n);
 }
diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h
index f623fe23..d5ab7ea3 100644
--- a/murphi2murphi/src/Stage.h
+++ b/murphi2murphi/src/Stage.h
@@ -122,6 +122,7 @@ class IntermediateStage : public Stage {
   void visit_typedecl(const rumur::TypeDecl &n) override;
   void visit_typeexprid(const rumur::TypeExprID &n) override;
   void visit_undefine(const rumur::Undefine &n) override;
+  void visit_union(const rumur::Union &n) override;
   void visit_vardecl(const rumur::VarDecl &n) override;
   void visit_while(const rumur::While &n) override;
   void visit_xor(const rumur::Xor &n) override;
diff --git a/murphi2smv/doc/murphi2smv.1 b/murphi2smv/doc/murphi2smv.1
index 21b39229..0238859a 100644
--- a/murphi2smv/doc/murphi2smv.1
+++ b/murphi2smv/doc/murphi2smv.1
@@ -97,6 +97,8 @@ simple \fBrule\fRs
 .IP \[bu]
 \fBundefine\fR statements
 .IP \[bu]
+\fBunion\fR types
+.IP \[bu]
 \fBwhile\fR statements
 .RE
 .PP
diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc
index 913c1417..17860649 100644
--- a/murphi2smv/src/codegen.cc
+++ b/murphi2smv/src/codegen.cc
@@ -542,6 +542,20 @@ class Printer : public ConstBaseTraversal {
         << *n.rhs << "` --/\n";
   }
 
+  void visit_union(const Union &n) final {
+    *this << tab()
+          << "/-- FIXME: Murphi union types have no equivalent in SMV --/\n";
+
+    indent();
+    for (const Ptr<TypeExpr> &m : n.members) {
+      emit_leading_comments(*m);
+      *this << *m;
+    }
+    dedent();
+
+    *this << tab() << "/-- FIXME: end of union type --/\n";
+  }
+
   void visit_vardecl(const VarDecl &n) final {
     *this << tab() << "VAR " << n.name << " : " << *n.get_type() << ";\n";
   }
diff --git a/murphi2uclid/doc/murphi2uclid.1 b/murphi2uclid/doc/murphi2uclid.1
index 9dd1a678..1a353fc3 100644
--- a/murphi2uclid/doc/murphi2uclid.1
+++ b/murphi2uclid/doc/murphi2uclid.1
@@ -67,6 +67,8 @@ Aliases, in the form of declarations statements or rules
 .IP \[bu]
 The \fBisundefined\fR operator
 .IP \[bu]
+\fBunion\fR types
+.IP \[bu]
 The modulo operator, \fB%\fR
 .IP \[bu]
 The left and shift shift operators, \fB<<\fR and \fB>>\fR
diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc
index 1c30a7c0..2b370de6 100644
--- a/murphi2uclid/src/check.cc
+++ b/murphi2uclid/src/check.cc
@@ -268,6 +268,10 @@ class Checker : public ConstTraversal {
       n.body.back()->visit(*this);
   }
 
+  void visit_union(const Union &n) final {
+    throw Error("Uclid5 has no equivalent of union types", n.loc);
+  }
+
   void visit_while(const While &n) final {
     n.condition->visit(*this);
 
diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc
index 9c3e6081..206e43dd 100644
--- a/murphi2uclid/src/codegen.cc
+++ b/murphi2uclid/src/codegen.cc
@@ -953,6 +953,11 @@ class Printer : public ConstBaseTraversal {
     *this << tab() << "havoc " << *n.rhs << ";\n";
   }
 
+  void visit_union(const Union &) final {
+    assert(!"union type not rejected during check()");
+    __builtin_unreachable();
+  }
+
   void visit_vardecl(const VarDecl &n) final {
     *this << tab() << "var " << n.name << " : " << *n.get_type() << ";\n";
 
diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc
index d1137b93..50373a39 100644
--- a/murphi2xml/src/XMLPrinter.cc
+++ b/murphi2xml/src/XMLPrinter.cc
@@ -849,6 +849,19 @@ void XMLPrinter::visit_undefine(const Undefine &n) {
   o << "</undefine>";
 }
 
+void XMLPrinter::visit_union(const Union &n) {
+  sync_to(n);
+  o << "<union ";
+  add_location(n);
+  o << ">";
+  for (const Ptr<TypeExpr> &m : n.members) {
+    sync_to(*m);
+    dispatch(*m);
+  }
+  sync_to(n.loc.end);
+  o << "</union>";
+}
+
 void XMLPrinter::visit_vardecl(const VarDecl &n) {
   sync_to(n);
   o << "<vardecl name=\"" << n.name << "\" readonly=\"" << n.readonly << "\" ";
diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h
index 06887830..0a36e2cb 100644
--- a/murphi2xml/src/XMLPrinter.h
+++ b/murphi2xml/src/XMLPrinter.h
@@ -79,6 +79,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal {
   void visit_typedecl(const rumur::TypeDecl &n) final;
   void visit_typeexprid(const rumur::TypeExprID &n) final;
   void visit_undefine(const rumur::Undefine &n) final;
+  void visit_union(const rumur::Union &n) final;
   void visit_vardecl(const rumur::VarDecl &n) final;
   void visit_while(const rumur::While &n) final;
   void visit_xor(const rumur::Xor &n) final;
diff --git a/rumur/CMakeLists.txt b/rumur/CMakeLists.txt
index 04dda2f3..4b859c5b 100644
--- a/rumur/CMakeLists.txt
+++ b/rumur/CMakeLists.txt
@@ -25,6 +25,7 @@ add_executable(rumur
   ../common/escape.cc
   ../common/help.c
   src/assume-statements-count.cc
+  src/check.cc
   src/generate-allocations.cc
   src/generate-cover-array.cc
   src/generate-decl.cc
diff --git a/rumur/src/check.cc b/rumur/src/check.cc
new file mode 100644
index 00000000..49f78028
--- /dev/null
+++ b/rumur/src/check.cc
@@ -0,0 +1,20 @@
+#include "check.h"
+#include <rumur/rumur.h>
+
+using namespace rumur;
+
+namespace {
+
+class Check : public ConstTraversal {
+
+public:
+  void visit_union(const Union &n) final {
+    throw Error("union types are not supported", n.loc);
+  }
+};
+} // namespace
+
+void check(const rumur::Node &n) {
+  Check c;
+  c.dispatch(n);
+}
diff --git a/rumur/src/check.h b/rumur/src/check.h
new file mode 100644
index 00000000..486337a1
--- /dev/null
+++ b/rumur/src/check.h
@@ -0,0 +1,6 @@
+#pragma once
+
+#include <rumur/rumur.h>
+
+/// throw a `rumur::Error` if the given node contains anything unsupported
+void check(const rumur::Node &n);
diff --git a/rumur/src/generate-print.cc b/rumur/src/generate-print.cc
index af3d31f9..0c25e4e2 100644
--- a/rumur/src/generate-print.cc
+++ b/rumur/src/generate-print.cc
@@ -1,4 +1,5 @@
 #include "../../common/escape.h"
+#include "../../common/isa.h"
 #include "generate.h"
 #include "options.h"
 #include <cassert>
@@ -316,6 +317,8 @@ class Generator : public ConstTypeTraversal {
       return;
     }
 
+    assert(!isa<Union>(t) && "union type not rejected before code generation");
+
     assert(!"non-range, non-enum used as array index");
   }
 
@@ -516,6 +519,10 @@ class Generator : public ConstTypeTraversal {
 
     dispatch(*n.referent->value);
   }
+
+  void visit_union(const Union &n) final {
+    throw Error("union types are not supported", n.loc);
+  }
 };
 
 } // namespace
diff --git a/rumur/src/generate-stmt.cc b/rumur/src/generate-stmt.cc
index 12bb48ef..ed3bdd28 100644
--- a/rumur/src/generate-stmt.cc
+++ b/rumur/src/generate-stmt.cc
@@ -72,6 +72,13 @@ static void clear(std::ostream &out, const TypeExpr &t,
     return;
   }
 
+  if (auto u = dynamic_cast<const Union *>(type.get())) {
+    // Generate a clear for each interpretation of this type. This is not
+    // efficient, but at least simple.
+    for (const Ptr<TypeExpr> &m : u->members)
+      clear(out, *m, offset, depth);
+  }
+
   assert(!"unreachable");
 }
 
diff --git a/rumur/src/main.cc b/rumur/src/main.cc
index ba1be689..7725c37d 100644
--- a/rumur/src/main.cc
+++ b/rumur/src/main.cc
@@ -1,6 +1,7 @@
 #include "../../common/environ.h"
 #include "../../common/help.h"
 #include "ValueType.h"
+#include "check.h"
 #include "generate.h"
 #include "has-start-state.h"
 #include "log.h"
@@ -671,6 +672,18 @@ int main(int argc, char **argv) {
   if (!has_start_state(*m))
     *warn << "warning: model has no start state\n";
 
+  // check whether the model uses unsupported things
+  try {
+    *debug << "checking for use of unsupported features...\n";
+    check(*m);
+  } catch (Error &e) {
+    std::cerr << white() << bold() << input_filename << ':' << e.loc << ':'
+              << reset() << ' ' << red() << bold() << "error:" << reset() << ' '
+              << white() << bold() << e.what() << reset() << '\n';
+    print_location(input_filename, e.loc);
+    return EXIT_FAILURE;
+  }
+
   // run SMT simplification if the user enabled it
   if (options.smt.simplification == SmtSimplification::ON) {
     *debug << "SMT simplification...\n";
diff --git a/rumur/src/smt/define-enum-members.cc b/rumur/src/smt/define-enum-members.cc
index 7ab8d4f3..4f1948d3 100644
--- a/rumur/src/smt/define-enum-members.cc
+++ b/rumur/src/smt/define-enum-members.cc
@@ -68,6 +68,12 @@ class Definer : public ConstTypeTraversal {
   void visit_scalarset(const Scalarset &) final {
     // as a primitive, scalarsets can't contain any enum members
   }
+
+  void visit_union(const Union &n) final {
+    // define any enum members that occur within union members
+    for (const Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+  }
 };
 } // namespace
 
diff --git a/rumur/src/smt/define-records.cc b/rumur/src/smt/define-records.cc
index 3dc68c37..49db5700 100644
--- a/rumur/src/smt/define-records.cc
+++ b/rumur/src/smt/define-records.cc
@@ -63,6 +63,12 @@ class Definer : public ConstTypeTraversal {
   void visit_scalarset(const Scalarset &) final {
     // nothing to do
   }
+
+  void visit_union(const Union &n) final {
+    // define any records that are defined within this union
+    for (const Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+  }
 };
 } // namespace
 
diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc
index 7a9c89e8..87b88273 100644
--- a/rumur/src/smt/simplify.cc
+++ b/rumur/src/smt/simplify.cc
@@ -387,6 +387,11 @@ class Simplifier : public BaseTraversal {
 
   void visit_undefine(Undefine &n) final { dispatch(*n.rhs); }
 
+  void visit_union(Union &n) final {
+    for (Ptr<TypeExpr> &m : n.members)
+      dispatch(*m);
+  }
+
   void visit_vardecl(VarDecl &n) final { dispatch(*n.type); }
 
   void visit_while(While &n) final {
@@ -585,6 +590,12 @@ class Simplifier : public BaseTraversal {
         }
       }
 
+      void visit_union(const Union &) final {
+        // TODO: the constraints on a union should probably be the intersection
+        // of constraints on the union’s members
+        throw Unsupported();
+      }
+
       void visit_typeexprid(const TypeExprID &) final {
         assert(!"unreachable");
       }
diff --git a/rumur/src/smt/typeexpr-to-smt.cc b/rumur/src/smt/typeexpr-to-smt.cc
index 3d4d4af9..13105337 100644
--- a/rumur/src/smt/typeexpr-to-smt.cc
+++ b/rumur/src/smt/typeexpr-to-smt.cc
@@ -74,6 +74,10 @@ class Translator : public ConstTypeTraversal {
     assert(n.referent != nullptr && "unresolved TypeExprID in AST");
     *this << *n.referent->value;
   }
+
+  void visit_union(const Union &) final {
+    throw Unsupported("union types are not supported in SMT translation");
+  }
 };
 } // namespace
 
diff --git a/rumur/src/symmetry-reduction.cc b/rumur/src/symmetry-reduction.cc
index 341995fd..b48a0613 100644
--- a/rumur/src/symmetry-reduction.cc
+++ b/rumur/src/symmetry-reduction.cc
@@ -113,6 +113,8 @@ static void generate_apply_swap(std::ostream &out, const std::string &offset_a,
     return;
   }
 
+  assert(!isa<Union>(t) && "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_apply_swap");
 }
 
@@ -198,6 +200,9 @@ static void generate_swap_chunk(std::ostream &out, const TypeExpr &t,
     return;
   }
 
+  assert(!isa<Union>(type) &&
+         "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_swap_chunk");
 }
 
@@ -467,6 +472,8 @@ static void generate_apply_compare(std::ostream &out, const TypeExpr &type,
     return;
   }
 
+  assert(!isa<Union>(t) && "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_apply_compare");
 }
 
@@ -576,6 +583,9 @@ static void generate_compare_chunk(std::ostream &out, const TypeExpr &t,
     return;
   }
 
+  assert(!isa<Union>(type) &&
+         "union type not rejected before symmetry reduction");
+
   assert(!"missed case in generate_compare_chunk");
 }
 

From 3b58aa9dbfae7082c01b36368785fea530717e31 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Fri, 14 Aug 2026 17:02:56 +1000
Subject: [PATCH 2/7] support 'union' during lexing
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This still has no effect because `union` is not yet supported during
parsing.

Github: #331 “MultiSet support within scope?”
---
 librumur/src/lexer.l   | 2 +-
 librumur/src/parser.yy | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l
index 8b026bd1..647018de 100644
--- a/librumur/src/lexer.l
+++ b/librumur/src/lexer.l
@@ -113,7 +113,7 @@ then          { return rumur::parser::token::THEN;          }
 to            { return rumur::parser::token::TO;            }
 type          { return rumur::parser::token::TYPE;          }
 undefine      { return rumur::parser::token::UNDEFINE;      }
-union         { throw rumur::Error("union types are not supported", *loc); }
+union         { return rumur::parser::token::UNION;         }
 var           { return rumur::parser::token::VAR;           }
 while         { return rumur::parser::token::WHILE;         }
 
diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy
index b7f33cc6..11e4a384 100644
--- a/librumur/src/parser.yy
+++ b/librumur/src/parser.yy
@@ -185,6 +185,7 @@
 %token TO
 %token TYPE
 %token UNDEFINE
+%token UNION
 %token VAR
 %token WHILE
 

From d6b7949fea8c9da3bdbd08d0311b60fca04683cc Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Fri, 14 Aug 2026 17:02:56 +1000
Subject: [PATCH 3/7] support 'union' during parsing
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

At this point, it is possible to parse and process a model using `union`
types. Doing this on real world models is still challenging because
there is no support for `ismember` that most real world `union`-using
models also use.

Github: #331 “MultiSet support within scope?”
---
 doc/vs-cmurphi.rst     | 15 ++++++++++++++-
 librumur/src/parser.yy | 18 ++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst
index 99c037b4..48678b3b 100644
--- a/doc/vs-cmurphi.rst
+++ b/doc/vs-cmurphi.rst
@@ -37,7 +37,20 @@ Type System
 -----------
 CMurphi supports real arithmetic using the ``real`` data type. Rumur does not
 support this type and there are no plans to implement this or any floating point
-support. Similarly, Rumur does not support the ``union`` or ``multiset`` types.
+support. Similarly, Rumur does not support the ``multiset`` type.
+
+Unions
+^^^^^^
+Models that use the ``union`` type can be parsed with librumur, but generation
+of a checker using ``rumur`` is not supported. Some of the Rumur tools fully
+support union types, e.g. ``murphi2xml``, but others reject models with union
+types, e.g. ``murphi2uclid``.
+
+CMurphi only supports unions of scalarset and enum types. librumur supports
+unions of any types, simple or complex, including recursive (unions of unions).
+In contrast to CMurphi, librumur allows union types with 0 or 1 members. A union
+type with 0 members is vacuous, in the sense that values of this type can only
+ever be ``undefined``.
 
 Assumptions
 -----------
diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy
index 11e4a384..af03edaa 100644
--- a/librumur/src/parser.yy
+++ b/librumur/src/parser.yy
@@ -242,6 +242,8 @@
 %type <std::vector<rumur::Ptr<rumur::Decl>>>                 typedecl
 %type <std::vector<rumur::Ptr<rumur::Decl>>>                 typedecls
 %type <rumur::Ptr<rumur::TypeExpr>>                          typeexpr
+%type <std::vector<rumur::Ptr<rumur::TypeExpr>>>             typeexprs
+%type <std::vector<rumur::Ptr<rumur::TypeExpr>>>             typeexprs_cont
 %type <std::vector<rumur::Ptr<rumur::VarDecl>>>              vardecl
 %type <std::vector<rumur::Ptr<rumur::VarDecl>>>              vardecls
 %type <std::shared_ptr<bool>>                                var_opt
@@ -677,6 +679,22 @@ typeexpr: BOOLEAN {
   $$ = rumur::Ptr<rumur::Array>::make($3, $6, @$);
 } | SCALARSET '(' expr ')' {
   $$ = rumur::Ptr<rumur::Scalarset>::make($3, @$);
+} | UNION '{' typeexprs '}' {
+  $$ = rumur::Ptr<rumur::Union>::make($3, @$);
+};
+
+typeexprs: typeexprs_cont typeexpr comma_opt {
+  $$ = $1;
+  $$.push_back($2);
+} | %empty {
+  /* nothing required */
+};
+
+typeexprs_cont: typeexprs_cont typeexpr ',' {
+  $$ = $1;
+  $$.push_back($2);
+} | %empty {
+  /* nothing required */
 };
 
 vardecl: id_list_opt ':' typeexpr {

From 62a8c4931edc787401726f2e17d40d4832836d0d Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Sat, 15 Aug 2026 18:33:05 +1000
Subject: [PATCH 4/7] API BREAK: add preliminary support for 'ismember'
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This is still rejected by most Rumur tools. The intent is to just allow
librumur users to successfully parse models using `ismember`.

Gitlab: #331 “MultiSet support within scope?”
---
 doc/vs-cmurphi.rst                |  5 +++++
 librumur/include/rumur/Expr.h     | 19 +++++++++++++++++++
 librumur/include/rumur/indexer.h  |  1 +
 librumur/include/rumur/traverse.h |  6 ++++++
 librumur/src/Expr.cc              | 28 ++++++++++++++++++++++++++++
 librumur/src/indexer.cc           |  6 ++++++
 librumur/src/resolve-symbols.cc   |  6 ++++++
 librumur/src/traverse.cc          | 20 ++++++++++++++++++++
 librumur/src/validate.cc          |  6 ++++++
 misc/murphi2xml.rng               | 16 ++++++++++++++++
 murphi-format/src/format.c        |  3 +++
 murphi2c/src/CLikeGenerator.cc    |  5 +++++
 murphi2c/src/CLikeGenerator.h     |  1 +
 murphi2c/src/check.cc             |  7 +++++++
 murphi2murphi/src/Printer.cc      |  9 +++++++++
 murphi2murphi/src/Printer.h       |  1 +
 murphi2murphi/src/Stage.cc        |  3 +++
 murphi2murphi/src/Stage.h         |  1 +
 murphi2smv/src/codegen.cc         |  6 ++++++
 murphi2uclid/src/check.cc         |  4 ++++
 murphi2uclid/src/codegen.cc       |  5 +++++
 murphi2xml/src/XMLPrinter.cc      | 17 +++++++++++++++++
 murphi2xml/src/XMLPrinter.h       |  1 +
 rumur/src/check.cc                |  4 ++++
 rumur/src/generate-expr.cc        |  5 +++++
 rumur/src/smt/simplify.cc         |  7 +++++++
 rumur/src/smt/translate.cc        |  1 +
 27 files changed, 193 insertions(+)

diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst
index 48678b3b..39896992 100644
--- a/doc/vs-cmurphi.rst
+++ b/doc/vs-cmurphi.rst
@@ -52,6 +52,11 @@ In contrast to CMurphi, librumur allows union types with 0 or 1 members. A union
 type with 0 members is vacuous, in the sense that values of this type can only
 ever be ``undefined``.
 
+CMurphi requires the first argument to the ``ismember`` predicate to be a
+designator. librumur allows any expression. CMurphi requires the second argument
+to ``ismember`` to be a scalarset or enum type. librumur, in line with
+supporting unions of any types, allows the second argument to be any type.
+
 Assumptions
 -----------
 In addition to assertions and invariants that are supported by CMurphi, Rumur
diff --git a/librumur/include/rumur/Expr.h b/librumur/include/rumur/Expr.h
index 7e32e639..88e86350 100644
--- a/librumur/include/rumur/Expr.h
+++ b/librumur/include/rumur/Expr.h
@@ -676,6 +676,25 @@ struct RUMUR_API_WITH_RTTI Forall : public Expr {
   bool is_pure() const override;
 };
 
+struct RUMUR_API_WITH_RTTI IsMember : public Expr {
+
+  Ptr<Expr> peg;
+  Ptr<TypeExpr> hole;
+
+  IsMember(const Ptr<Expr> &peg_, const Ptr<TypeExpr> &hole_,
+           const location &loc_);
+  IsMember *clone() const override;
+
+  void visit(BaseTraversal &visitor) override;
+  void visit(ConstBaseTraversal &visitor) const override;
+
+  bool constant() const override;
+  Ptr<TypeExpr> type() const override;
+  mpz_class constant_fold() const override;
+  void to_stream(std::ostream &out) const override;
+  bool is_pure() const override;
+};
+
 struct RUMUR_API_WITH_RTTI IsUndefined : public UnaryExpr {
 
   IsUndefined(const Ptr<Expr> &expr_, const location &loc_);
diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h
index 258865d1..5aac00bc 100644
--- a/librumur/include/rumur/indexer.h
+++ b/librumur/include/rumur/indexer.h
@@ -52,6 +52,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal {
   void visit_if(If &n) override;
   void visit_ifclause(IfClause &n) override;
   void visit_implication(Implication &n) override;
+  void visit_ismember(IsMember &n) override;
   void visit_isundefined(IsUndefined &n) override;
   void visit_leq(Leq &n) override;
   void visit_lsh(Lsh &n) override;
diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h
index d9f275a9..c92bd0e8 100644
--- a/librumur/include/rumur/traverse.h
+++ b/librumur/include/rumur/traverse.h
@@ -98,6 +98,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal {
   virtual void visit_if(If &n) = 0;
   virtual void visit_ifclause(IfClause &n) = 0;
   virtual void visit_implication(Implication &n) = 0;
+  virtual void visit_ismember(IsMember &n) = 0;
   virtual void visit_isundefined(IsUndefined &n) = 0;
   virtual void visit_leq(Leq &n) = 0;
   virtual void visit_lsh(Lsh &n) = 0;
@@ -185,6 +186,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal {
   void visit_if(If &n) override;
   void visit_ifclause(IfClause &n) override;
   void visit_implication(Implication &n) override;
+  void visit_ismember(IsMember &n) override;
   void visit_isundefined(IsUndefined &n) override;
   void visit_leq(Leq &n) override;
   void visit_lsh(Lsh &n) override;
@@ -264,6 +266,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal {
   virtual void visit_if(const If &n) = 0;
   virtual void visit_ifclause(const IfClause &n) = 0;
   virtual void visit_implication(const Implication &n) = 0;
+  virtual void visit_ismember(const IsMember &n) = 0;
   virtual void visit_isundefined(const IsUndefined &n) = 0;
   virtual void visit_leq(const Leq &n) = 0;
   virtual void visit_lsh(const Lsh &n) = 0;
@@ -343,6 +346,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal {
   void visit_if(const If &n) override;
   void visit_ifclause(const IfClause &n) override;
   void visit_implication(const Implication &n) override;
+  void visit_ismember(const IsMember &n) override;
   void visit_isundefined(const IsUndefined &n) override;
   void visit_leq(const Leq &n) override;
   void visit_lsh(const Lsh &n) override;
@@ -463,6 +467,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal {
   void visit_gt(const Gt &n) final;
   void visit_ifclause(const IfClause &n) final;
   void visit_implication(const Implication &n) final;
+  void visit_ismember(const IsMember &n) final;
   void visit_isundefined(const IsUndefined &n) final;
   void visit_leq(const Leq &n) final;
   void visit_lsh(const Lsh &n) final;
@@ -530,6 +535,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal {
   void visit_if(const If &n) final;
   void visit_ifclause(const IfClause &n) final;
   void visit_implication(const Implication &n) final;
+  void visit_ismember(const IsMember &n) final;
   void visit_isundefined(const IsUndefined &n) final;
   void visit_leq(const Leq &n) final;
   void visit_lsh(const Lsh &n) final;
diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc
index 293f6ac6..82a2e02a 100644
--- a/librumur/src/Expr.cc
+++ b/librumur/src/Expr.cc
@@ -1674,6 +1674,34 @@ void Forall::to_stream(std::ostream &out) const {
 
 bool Forall::is_pure() const { return quantifier.is_pure() && expr->is_pure(); }
 
+IsMember::IsMember(const Ptr<Expr> &peg_, const Ptr<TypeExpr> &hole_,
+                   const location &loc_)
+    : Expr(loc_), peg(peg_), hole(hole_) {}
+
+IsMember *IsMember::clone() const { return new IsMember(*this); }
+
+void IsMember::visit(BaseTraversal &visitor) {
+  return visitor.visit_ismember(*this);
+}
+
+void IsMember::visit(ConstBaseTraversal &visitor) const {
+  return visitor.visit_ismember(*this);
+}
+
+bool IsMember::constant() const { return false; }
+
+Ptr<TypeExpr> IsMember::type() const { return Boolean; }
+
+mpz_class IsMember::constant_fold() const {
+  throw Error("ismember used in constant", loc);
+}
+
+void IsMember::to_stream(std::ostream &out) const {
+  out << "ismember(" << *peg << ", " << *hole << ')';
+}
+
+bool IsMember::is_pure() const { return peg->is_pure(); }
+
 IsUndefined::IsUndefined(const Ptr<Expr> &expr_, const location &loc_)
     : UnaryExpr(expr_, loc_) {}
 
diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc
index 76da1dbb..e2cf265e 100644
--- a/librumur/src/indexer.cc
+++ b/librumur/src/indexer.cc
@@ -161,6 +161,12 @@ void Indexer::visit_ifclause(IfClause &n) {
 
 void Indexer::visit_implication(Implication &n) { visit_bexpr(n); }
 
+void Indexer::visit_ismember(IsMember &n) {
+  n.unique_id = next++;
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void Indexer::visit_isundefined(IsUndefined &n) { visit_uexpr(n); }
 
 void Indexer::visit_leq(Leq &n) { visit_bexpr(n); }
diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc
index f6657084..7210bc36 100644
--- a/librumur/src/resolve-symbols.cc
+++ b/librumur/src/resolve-symbols.cc
@@ -234,6 +234,12 @@ class Resolver : public Traversal {
 
   void visit_implication(Implication &n) final { visit_bexpr(n); }
 
+  void visit_ismember(IsMember &n) final {
+    dispatch(*n.peg);
+    dispatch(*n.hole);
+    disambiguate(n.peg);
+  }
+
   void visit_isundefined(IsUndefined &n) final { visit_uexpr(n); }
 
   void visit_leq(Leq &n) final { visit_bexpr(n); }
diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc
index fe467ab5..e3dca41b 100644
--- a/librumur/src/traverse.cc
+++ b/librumur/src/traverse.cc
@@ -137,6 +137,11 @@ void Traversal::visit_ifclause(IfClause &n) {
 
 void Traversal::visit_implication(Implication &n) { visit_bexpr(n); }
 
+void Traversal::visit_ismember(IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void Traversal::visit_isundefined(IsUndefined &n) { visit_uexpr(n); }
 
 void Traversal::visit_leq(Leq &n) { visit_bexpr(n); }
@@ -411,6 +416,11 @@ void ConstTraversal::visit_ifclause(const IfClause &n) {
 
 void ConstTraversal::visit_implication(const Implication &n) { visit_bexpr(n); }
 
+void ConstTraversal::visit_ismember(const IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void ConstTraversal::visit_isundefined(const IsUndefined &n) { visit_uexpr(n); }
 
 void ConstTraversal::visit_leq(const Leq &n) { visit_bexpr(n); }
@@ -845,6 +855,11 @@ void ConstStmtTraversal::visit_implication(const Implication &n) {
   visit_bexpr(n);
 }
 
+void ConstStmtTraversal::visit_ismember(const IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void ConstStmtTraversal::visit_isundefined(const IsUndefined &n) {
   visit_uexpr(n);
 }
@@ -1084,6 +1099,11 @@ void ConstTypeTraversal::visit_implication(const Implication &n) {
   visit_bexpr(n);
 }
 
+void ConstTypeTraversal::visit_ismember(const IsMember &n) {
+  dispatch(*n.peg);
+  dispatch(*n.hole);
+}
+
 void ConstTypeTraversal::visit_isundefined(const IsUndefined &n) {
   visit_uexpr(n);
 }
diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc
index ca241ceb..31c7f785 100644
--- a/librumur/src/validate.cc
+++ b/librumur/src/validate.cc
@@ -207,6 +207,12 @@ class Validator : public ConstBaseTraversal {
     n.validate();
   }
 
+  void visit_ismember(const IsMember &n) final {
+    dispatch(*n.peg);
+    dispatch(*n.hole);
+    n.validate();
+  }
+
   void visit_isundefined(const IsUndefined &n) final {
     dispatch(*n.rhs);
     n.validate();
diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng
index e88ad28d..ad6fe4f2 100644
--- a/misc/murphi2xml.rng
+++ b/misc/murphi2xml.rng
@@ -290,6 +290,7 @@
       <ref name="geq"/>
       <ref name="gt"/>
       <ref name="implication"/>
+      <ref name="ismember"/>
       <ref name="isundefined"/>
       <ref name="leq"/>
       <ref name="lsh"/>
@@ -497,6 +498,21 @@
     </element>
   </define>
 
+  <define name="ismember">
+    <element name="ismember">
+      <ref name="location"/>
+      <ref name="content"/>
+      <element name="arg0">
+        <ref name="expr"/>
+      </element>
+      <ref name="content"/>
+      <element name="arg1">
+        <ref name="typeexpr"/>
+      </element>
+      <ref name="content"/>
+    </element>
+  </define>
+
   <define name="isundefined">
     <element name="isundefined">
       <ref name="location"/>
diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c
index ba7b5f16..75939879 100644
--- a/murphi-format/src/format.c
+++ b/murphi-format/src/format.c
@@ -289,6 +289,9 @@ static bool is_keyword(const char *text) {
   if (streq(text, "invariant"))
     return true;
 #if 0
+  // `ismember` is a keyword, but is used as if it were a function
+  if (streq(text, "ismember"))
+    return true;
   // `isundefined` is a keyword, but is used as if it were a function
   if (streq(text, "isundefined"))
     return true;
diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc
index 2177a808..013d8639 100644
--- a/murphi2c/src/CLikeGenerator.cc
+++ b/murphi2c/src/CLikeGenerator.cc
@@ -377,6 +377,11 @@ void CLikeGenerator::visit_implication(const Implication &n) {
   *this << "(!" << *n.lhs << " || " << *n.rhs << ")";
 }
 
+void CLikeGenerator::visit_ismember(const IsMember &) {
+  assert(!"ismember was not rejected during check()");
+  __builtin_unreachable();
+}
+
 void CLikeGenerator::visit_isundefined(const IsUndefined &) {
   // check() prevents a model with isundefined expressions from making it
   // through to here
diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h
index 27c2889e..fe0d6d09 100644
--- a/murphi2c/src/CLikeGenerator.h
+++ b/murphi2c/src/CLikeGenerator.h
@@ -64,6 +64,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator
   void visit_if(const rumur::If &n) final;
   void visit_ifclause(const rumur::IfClause &n) final;
   void visit_implication(const rumur::Implication &n) final;
+  void visit_ismember(const rumur::IsMember &) final;
   void visit_isundefined(const rumur::IsUndefined &) final;
   void visit_leq(const rumur::Leq &n) final;
   void visit_lsh(const rumur::Lsh &n) final;
diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc
index db113486..b57f824d 100644
--- a/murphi2c/src/check.cc
+++ b/murphi2c/src/check.cc
@@ -13,6 +13,13 @@ class Check : public ConstTraversal {
 public:
   bool ok = true;
 
+  void visit_ismember(const IsMember &) final {
+    if (ok) {
+      std::cerr << "ismember expressions are not supported\n";
+      ok = false;
+    }
+  }
+
   void visit_isundefined(const IsUndefined &) final {
     if (ok) {
       std::cerr << "isundefined expressions are not supported\n";
diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc
index 646404d1..1167df63 100644
--- a/murphi2murphi/src/Printer.cc
+++ b/murphi2murphi/src/Printer.cc
@@ -236,6 +236,15 @@ void Printer::visit_ifclause(const IfClause &n) {
 
 void Printer::visit_implication(const Implication &n) { visit_bexpr(n); }
 
+void Printer::visit_ismember(const IsMember &n) {
+  top->sync_to(n);
+  top->sync_to(*n.peg);
+  top->dispatch(*n.peg);
+  top->sync_to(*n.hole);
+  top->dispatch(*n.hole);
+  top->sync_to(n.loc.end);
+}
+
 void Printer::visit_isundefined(const IsUndefined &n) { visit_uexpr(n); }
 
 void Printer::visit_leq(const Leq &n) { visit_bexpr(n); }
diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h
index 91931852..c1bc53d6 100644
--- a/murphi2murphi/src/Printer.h
+++ b/murphi2murphi/src/Printer.h
@@ -47,6 +47,7 @@ class Printer : public Stage {
   void visit_if(const rumur::If &n) final;
   void visit_ifclause(const rumur::IfClause &n) final;
   void visit_implication(const rumur::Implication &n) final;
+  void visit_ismember(const rumur::IsMember &n) final;
   void visit_isundefined(const rumur::IsUndefined &n) final;
   void visit_leq(const rumur::Leq &n) final;
   void visit_lsh(const rumur::Lsh &n) final;
diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc
index 8215bc60..51839870 100644
--- a/murphi2murphi/src/Stage.cc
+++ b/murphi2murphi/src/Stage.cc
@@ -120,6 +120,9 @@ void IntermediateStage::visit_ifclause(const IfClause &n) {
 void IntermediateStage::visit_implication(const Implication &n) {
   next.visit_implication(n);
 }
+void IntermediateStage::visit_ismember(const IsMember &n) {
+  next.visit_ismember(n);
+}
 void IntermediateStage::visit_isundefined(const IsUndefined &n) {
   next.visit_isundefined(n);
 }
diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h
index d5ab7ea3..635d736f 100644
--- a/murphi2murphi/src/Stage.h
+++ b/murphi2murphi/src/Stage.h
@@ -89,6 +89,7 @@ class IntermediateStage : public Stage {
   void visit_if(const rumur::If &n) override;
   void visit_ifclause(const rumur::IfClause &n) override;
   void visit_implication(const rumur::Implication &n) override;
+  void visit_ismember(const rumur::IsMember &n) override;
   void visit_isundefined(const rumur::IsUndefined &n) override;
   void visit_leq(const rumur::Leq &n) override;
   void visit_lsh(const rumur::Lsh &n) override;
diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc
index 17860649..0abd922a 100644
--- a/murphi2smv/src/codegen.cc
+++ b/murphi2smv/src/codegen.cc
@@ -244,6 +244,12 @@ class Printer : public ConstBaseTraversal {
     *this << '(' << *n.lhs << " -> " << *n.rhs << ')';
   }
 
+  void visit_ismember(const IsMember &n) final {
+    *this << "/-- FIXME: Murphi ismember expressions have no equivalent in SMV "
+             "--/ ismember("
+          << *n.peg << ", " << *n.hole << ")";
+  }
+
   void visit_isundefined(const IsUndefined &n) final {
     *this << tab()
           << "/-- FIXME: Murphi isundefined statements have no equivalent in "
diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc
index 2b370de6..4a65a048 100644
--- a/murphi2uclid/src/check.cc
+++ b/murphi2uclid/src/check.cc
@@ -115,6 +115,10 @@ class Checker : public ConstTraversal {
       n.body.back()->visit(*this);
   }
 
+  void visit_ismember(const IsMember &n) final {
+    throw Error("Uclid5 has no equivalent of the ismember function", n.loc);
+  }
+
   void visit_lsh(const Lsh &n) final {
     // TODO: technically we could implement this as a Uclid5 function. However,
     // it is a little awkward because Uclid5 does not support generic functions
diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc
index 206e43dd..74a8918a 100644
--- a/murphi2uclid/src/codegen.cc
+++ b/murphi2uclid/src/codegen.cc
@@ -433,6 +433,11 @@ class Printer : public ConstBaseTraversal {
     *this << "(" << *n.lhs << " ==> " << *n.rhs << ")";
   }
 
+  void visit_ismember(const IsMember &) final {
+    assert(!"ismember not rejected during check()");
+    __builtin_unreachable();
+  }
+
   void visit_isundefined(const IsUndefined &) final {
     assert(!"isundefined not rejected during check()");
     __builtin_unreachable();
diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc
index 50373a39..0dad71c5 100644
--- a/murphi2xml/src/XMLPrinter.cc
+++ b/murphi2xml/src/XMLPrinter.cc
@@ -419,6 +419,23 @@ void XMLPrinter::visit_implication(const Implication &n) {
   visit_bexpr("implication", n);
 }
 
+void XMLPrinter::visit_ismember(const IsMember &n) {
+  sync_to(n);
+  o << "<ismember ";
+  add_location(n);
+  o << ">";
+  sync_to(*n.peg);
+  o << "<arg0>";
+  dispatch(*n.peg);
+  o << "</arg0>";
+  sync_to(*n.hole);
+  o << "<arg1>";
+  dispatch(*n.hole);
+  o << "</arg1>";
+  sync_to(n.loc.end);
+  o << "</ismember>";
+}
+
 void XMLPrinter::visit_isundefined(const IsUndefined &n) {
   visit_uexpr("isundefined", n);
 }
diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h
index 0a36e2cb..2f333577 100644
--- a/murphi2xml/src/XMLPrinter.h
+++ b/murphi2xml/src/XMLPrinter.h
@@ -46,6 +46,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal {
   void visit_if(const rumur::If &n) final;
   void visit_ifclause(const rumur::IfClause &n) final;
   void visit_implication(const rumur::Implication &n) final;
+  void visit_ismember(const rumur::IsMember &n) final;
   void visit_isundefined(const rumur::IsUndefined &n) final;
   void visit_leq(const rumur::Leq &n) final;
   void visit_lsh(const rumur::Lsh &n) final;
diff --git a/rumur/src/check.cc b/rumur/src/check.cc
index 49f78028..25558b47 100644
--- a/rumur/src/check.cc
+++ b/rumur/src/check.cc
@@ -8,6 +8,10 @@ namespace {
 class Check : public ConstTraversal {
 
 public:
+  void visit_ismember(const IsMember &n) final {
+    throw Error("ismember expressions are not supported", n.loc);
+  }
+
   void visit_union(const Union &n) final {
     throw Error("union types are not supported", n.loc);
   }
diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc
index e0547498..e78fa04c 100644
--- a/rumur/src/generate-expr.cc
+++ b/rumur/src/generate-expr.cc
@@ -469,6 +469,11 @@ class Generator : public ConstExprTraversal {
     *this << "(!" << *n.lhs << " || " << *n.rhs << ")";
   }
 
+  void visit_ismember(const IsMember &) final {
+    assert(!"ismember expression not rejected before code generation");
+    __builtin_unreachable();
+  }
+
   void visit_isundefined(const IsUndefined &n) final {
     *this << "handle_isundefined(s, ";
     generate_lvalue(*out, *n.rhs);
diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc
index 87b88273..647ce14b 100644
--- a/rumur/src/smt/simplify.cc
+++ b/rumur/src/smt/simplify.cc
@@ -194,6 +194,13 @@ class Simplifier : public BaseTraversal {
   }
 
   void visit_implication(Implication &n) final { visit_bexpr(n); }
+
+  void visit_ismember(IsMember &n) final {
+    dispatch(*n.peg);
+    simplify(n.peg);
+    dispatch(*n.hole);
+  }
+
   void visit_isundefined(IsUndefined &n) final { visit_uexpr(n); }
   void visit_leq(Leq &n) final { visit_bexpr(n); }
   void visit_lsh(Lsh &n) final { visit_bexpr(n); }
diff --git a/rumur/src/smt/translate.cc b/rumur/src/smt/translate.cc
index ae100961..9089a5b2 100644
--- a/rumur/src/smt/translate.cc
+++ b/rumur/src/smt/translate.cc
@@ -105,6 +105,7 @@ class Translator : public ConstExprTraversal {
     *this << "(=> " << *n.lhs << " " << *n.rhs << ")";
   }
 
+  void visit_ismember(const IsMember &n) final { throw Unsupported(n); }
   void visit_isundefined(const IsUndefined &n) final { throw Unsupported(n); }
 
   void visit_leq(const Leq &n) final {

From 0d62b88d31ca089a273f6b21c2558e3a2be6279d Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Sat, 15 Aug 2026 18:35:27 +1000
Subject: [PATCH 5/7] disable clang formatting on some table-like code

---
 rumur/src/smt/translate.cc | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/rumur/src/smt/translate.cc b/rumur/src/smt/translate.cc
index 9089a5b2..42412d90 100644
--- a/rumur/src/smt/translate.cc
+++ b/rumur/src/smt/translate.cc
@@ -171,6 +171,7 @@ class Translator : public ConstExprTraversal {
 
     // determine the parts of the expression we will construct that depend on
     // forall
+    // clang-format off
     const std::string binder  = forall ? "forall" : "exists";
     const std::string op      = forall ? "or"     : "and";
     const std::string lb_rel  = forall ? lt()     : geq();
@@ -178,6 +179,7 @@ class Translator : public ConstExprTraversal {
     const std::string ub_rel2 = forall ? geq()    : lt();
     const std::string step_o  = forall ? "(not "  : "";
     const std::string step_c  = forall ? ")"      : "";
+    // clang-format on
 
     // “∀q.”/“∃q.”
     *this << "(" << binder << " ((" << qname << " " << qtype << ")) (" << op;

From c8720b77e298e51350be5486829f16f2c2bf15e8 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Sun, 16 Aug 2026 07:22:20 +1000
Subject: [PATCH 6/7] support 'ismember' during lexing
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

There is still no parser support.

Github: #331 “MultiSet support within scope?”
---
 librumur/src/lexer.l   | 1 +
 librumur/src/parser.yy | 1 +
 2 files changed, 2 insertions(+)

diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l
index 647018de..e5bc910b 100644
--- a/librumur/src/lexer.l
+++ b/librumur/src/lexer.l
@@ -96,6 +96,7 @@ forall        { return rumur::parser::token::FORALL;        }
 function      { return rumur::parser::token::FUNCTION;      }
 if            { return rumur::parser::token::IF;            }
 invariant     { return rumur::parser::token::INVARIANT;     }
+ismember      { return rumur::parser::token::ISMEMBER;      }
 isundefined   { return rumur::parser::token::ISUNDEFINED;   }
 liveness      { return rumur::parser::token::LIVENESS;      }
 of            { return rumur::parser::token::OF;            }
diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy
index af03edaa..ca70e0b8 100644
--- a/librumur/src/parser.yy
+++ b/librumur/src/parser.yy
@@ -154,6 +154,7 @@
 %token IF
 %token IMPLIES "->"
 %token INVARIANT
+%token ISMEMBER
 %token ISUNDEFINED
 %token LAND "∧"
 %token LEQ "<="

From c89bd8afdaa1aad2089cecfb7a77d2e28fab68a4 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Sun, 16 Aug 2026 07:36:11 +1000
Subject: [PATCH 7/7] support 'ismember' during parsing
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

At this point, `ismember` support is complete, in the sense we can parse
and manipulate it. This allows ingesting models like sci.m from
CMurphi’s examples. There is still no support for producing a checker
from a model that uses `union` types or `ismember`, and none is planned
right now.

Gitlab: #331 “MultiSet support within scope?”
---
 librumur/src/parser.yy | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy
index ca70e0b8..724fdc8b 100644
--- a/librumur/src/parser.yy
+++ b/librumur/src/parser.yy
@@ -437,6 +437,8 @@ expr: expr '?' expr ':' expr {
   $$->loc = @$;
 } | ID '(' exprlist ')' {
   $$ = rumur::Ptr<rumur::FunctionCall>::make($1, $3, @$);
+} | ISMEMBER '(' expr ',' typeexpr ')' {
+  $$ = rumur::Ptr<rumur::IsMember>::make($3, $5, @$);
 } | ISUNDEFINED '(' designator ')' {
   $$ = rumur::Ptr<rumur::IsUndefined>::make($3, @$);
 };