From 9f55ca0ed6fbf0b841130f2c71e5bbf69d4957d0 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 01/21] API BREAK: add preliminary support for multiset types MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/include/rumur/TypeExpr.h | 17 ++++++ librumur/include/rumur/indexer.h | 1 + librumur/include/rumur/traverse.h | 6 ++ librumur/src/TypeExpr.cc | 57 +++++++++++++++++++ librumur/src/indexer.cc | 6 ++ librumur/src/resolve-symbols.cc | 6 ++ librumur/src/traverse.cc | 20 +++++++ librumur/src/validate.cc | 6 ++ misc/murphi2xml.rng | 12 ++++ murphi-format/src/format.c | 5 ++ murphi2c/src/CLikeGenerator.cc | 7 +++ murphi2c/src/CLikeGenerator.h | 1 + murphi2c/src/check.cc | 7 +++ .../src/DecomposeComplexComparisons.cc | 12 +++- murphi2murphi/src/Printer.cc | 9 +++ murphi2murphi/src/Printer.h | 1 + murphi2murphi/src/Stage.cc | 3 + murphi2murphi/src/Stage.h | 1 + murphi2smv/doc/murphi2smv.1 | 2 + murphi2smv/src/codegen.cc | 7 +++ 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/src/check.cc | 4 ++ rumur/src/generate-print.cc | 6 ++ rumur/src/generate-stmt.cc | 3 + rumur/src/smt/define-enum-members.cc | 5 ++ rumur/src/smt/define-records.cc | 5 ++ rumur/src/smt/simplify.cc | 9 +++ rumur/src/smt/typeexpr-to-smt.cc | 4 ++ rumur/src/symmetry-reduction.cc | 8 +++ 33 files changed, 252 insertions(+), 3 deletions(-) diff --git a/librumur/include/rumur/TypeExpr.h b/librumur/include/rumur/TypeExpr.h index f7d90160..ab1dc000 100644 --- a/librumur/include/rumur/TypeExpr.h +++ b/librumur/include/rumur/TypeExpr.h @@ -166,6 +166,23 @@ struct RUMUR_API_WITH_RTTI Array : public TypeExpr { void to_stream(std::ostream &out) const override; }; +struct RUMUR_API_WITH_RTTI Multiset : public TypeExpr { + Ptr index_bound; + Ptr element_type; + + Multiset(const Ptr &index_bound_, const Ptr &element_type_, + const location &loc_); + Multiset *clone() const override; + + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; + + mpz_class width() const override; + mpz_class count() const override; + void validate() const override; + void to_stream(std::ostream &out) const override; +}; + struct RUMUR_API_WITH_RTTI TypeExprID : public TypeExpr { std::string name; diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h index 5aac00bc..34550d66 100644 --- a/librumur/include/rumur/indexer.h +++ b/librumur/include/rumur/indexer.h @@ -60,6 +60,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_model(Model &n) override; void visit_mod(Mod &n) override; void visit_mul(Mul &n) override; + void visit_multiset(Multiset &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h index c92bd0e8..1df46662 100644 --- a/librumur/include/rumur/traverse.h +++ b/librumur/include/rumur/traverse.h @@ -106,6 +106,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_model(Model &n) = 0; virtual void visit_mod(Mod &n) = 0; virtual void visit_mul(Mul &n) = 0; + virtual void visit_multiset(Multiset &n) = 0; virtual void visit_negative(Negative &n) = 0; virtual void visit_neq(Neq &n) = 0; virtual void visit_not(Not &n) = 0; @@ -194,6 +195,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_model(Model &n) override; void visit_mod(Mod &n) override; void visit_mul(Mul &n) override; + void visit_multiset(Multiset &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; @@ -274,6 +276,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_model(const Model &n) = 0; virtual void visit_mod(const Mod &n) = 0; virtual void visit_mul(const Mul &n) = 0; + virtual void visit_multiset(const Multiset &n) = 0; virtual void visit_negative(const Negative &n) = 0; virtual void visit_neq(const Neq &n) = 0; virtual void visit_not(const Not &n) = 0; @@ -354,6 +357,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_model(const Model &n) override; void visit_mod(const Mod &n) override; void visit_mul(const Mul &n) override; + void visit_multiset(const Multiset &n) override; void visit_negative(const Negative &n) override; void visit_neq(const Neq &n) override; void visit_not(const Not &n) override; @@ -414,6 +418,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal { void visit_if(const If &n) final; void visit_ifclause(const IfClause &n) final; void visit_model(const Model &n) final; + void visit_multiset(const Multiset &n) final; void visit_procedurecall(const ProcedureCall &n) final; void visit_property(const Property &n) final; void visit_propertyrule(const PropertyRule &n) final; @@ -475,6 +480,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal { void visit_model(const Model &n) final; void visit_mod(const Mod &n) final; void visit_mul(const Mul &n) final; + void visit_multiset(const Multiset &n) final; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; diff --git a/librumur/src/TypeExpr.cc b/librumur/src/TypeExpr.cc index ff31dd9f..f8f30182 100644 --- a/librumur/src/TypeExpr.cc +++ b/librumur/src/TypeExpr.cc @@ -109,6 +109,18 @@ static bool equal(const TypeExpr &t1, const TypeExpr &t2) { } } + void visit_multiset(const Multiset &n) final { + if (auto m = dynamic_cast(t.get())) { + if (m->index_bound->constant_fold() != n.index_bound->constant_fold()) { + result = false; + } else if (!equal(*m->element_type, *n.element_type)) { + result = false; + } + } else { + result = false; + } + } + void visit_range(const Range &n) final { if (auto r = dynamic_cast(t.get())) { result = r->min->constant_fold() == n.min->constant_fold() && @@ -443,6 +455,51 @@ void Array::to_stream(std::ostream &out) const { out << "array [" << *index_type << "] of " << *element_type; } +Multiset::Multiset(const Ptr &index_bound_, + const Ptr &element_type_, const location &loc_) + : TypeExpr(loc_), index_bound(index_bound_), element_type(element_type_) {} + +Multiset *Multiset::clone() const { return new Multiset(*this); } + +void Multiset::visit(BaseTraversal &visitor) { visitor.visit_multiset(*this); } + +void Multiset::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multiset(*this); +} + +mpz_class Multiset::width() const { + const mpz_class indices = index_bound->constant_fold(); + const mpz_class element_width = element_type->width(); + return indices * element_width; +} + +mpz_class Multiset::count() const { + const mpz_class indices = index_bound->constant_fold(); + + if (indices == 0) + return 0; + + const mpz_class element_count = element_type->count(); + + mpz_class s = 1; + for (mpz_class i = 0; i < indices; ++i) + s *= element_count; + return s; +} + +void Multiset::validate() const { + if (!index_bound->constant()) + throw Error("multiset bound is not a constant", index_bound->loc); + + const mpz_class b = index_bound->constant_fold(); + if (b < 0) + throw Error("multiset bound is negative, " + b.get_str(), index_bound->loc); +} + +void Multiset::to_stream(std::ostream &out) const { + out << "multiset [" << *index_bound << "] of " << *element_type; +} + TypeExprID::TypeExprID(const std::string &name_, const Ptr &referent_, const location &loc_) : TypeExpr(loc_), name(name_), referent(referent_) {} diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc index e2cf265e..fa133948 100644 --- a/librumur/src/indexer.cc +++ b/librumur/src/indexer.cc @@ -185,6 +185,12 @@ void Indexer::visit_model(Model &n) { void Indexer::visit_mul(Mul &n) { visit_bexpr(n); } +void Indexer::visit_multiset(Multiset &n) { + n.unique_id = next++; + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + void Indexer::visit_negative(Negative &n) { visit_uexpr(n); } void Indexer::visit_neq(Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 6c243b71..7565fa97 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -325,6 +325,12 @@ class Resolver : public Traversal { void visit_mul(Mul &n) final { visit_bexpr(n); } + void visit_multiset(Multiset &n) final { + dispatch(*n.index_bound); + dispatch(*n.element_type); + disambiguate(n.index_bound); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc index e3dca41b..c6ff2d1c 100644 --- a/librumur/src/traverse.cc +++ b/librumur/src/traverse.cc @@ -159,6 +159,11 @@ void Traversal::visit_model(Model &n) { void Traversal::visit_mul(Mul &n) { visit_bexpr(n); } +void Traversal::visit_multiset(Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + void Traversal::visit_negative(Negative &n) { visit_uexpr(n); } void Traversal::visit_neq(Neq &n) { visit_bexpr(n); } @@ -438,6 +443,11 @@ void ConstTraversal::visit_model(const Model &n) { void ConstTraversal::visit_mul(const Mul &n) { visit_bexpr(n); } +void ConstTraversal::visit_multiset(const Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + void ConstTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -647,6 +657,11 @@ void ConstExprTraversal::visit_model(const Model &n) { dispatch(*c); } +void ConstExprTraversal::visit_multiset(const Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + void ConstExprTraversal::visit_procedurecall(const ProcedureCall &n) { dispatch(n.call); } @@ -879,6 +894,11 @@ void ConstStmtTraversal::visit_model(const Model &n) { void ConstStmtTraversal::visit_mul(const Mul &n) { visit_bexpr(n); } +void ConstStmtTraversal::visit_multiset(const Multiset &n) { + dispatch(*n.index_bound); + dispatch(*n.element_type); +} + void ConstStmtTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstStmtTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc index 31c7f785..10a3bcaf 100644 --- a/librumur/src/validate.cc +++ b/librumur/src/validate.cc @@ -254,6 +254,12 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_multiset(const Multiset &n) final { + dispatch(*n.index_bound); + dispatch(*n.element_type); + n.validate(); + } + void visit_negative(const Negative &n) final { dispatch(*n.rhs); n.validate(); diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng index ad6fe4f2..dfa4684a 100644 --- a/misc/murphi2xml.rng +++ b/misc/murphi2xml.rng @@ -612,6 +612,17 @@ + + + + + + + + + + + @@ -1096,6 +1107,7 @@ + diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c index 75939879..6928fa67 100644 --- a/murphi-format/src/format.c +++ b/murphi-format/src/format.c @@ -298,6 +298,11 @@ static bool is_keyword(const char *text) { #endif if (streq(text, "liveness")) return true; +#if 0 + // it is more intuitive to suppress space between `multiset` and `[` + if (streq(text, "multiset")) + return true; +#endif if (streq(text, "of")) return true; if (streq(text, "procedure")) diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 013d8639..26ec3a78 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -430,6 +430,11 @@ void CLikeGenerator::visit_mul(const Mul &n) { *this << "(" << *n.lhs << " * " << *n.rhs << ")"; } +void CLikeGenerator::visit_multiset(const Multiset &) { + assert(!"multiset was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_negative(const Negative &n) { *this << "(-" << *n.rhs << ")"; } @@ -526,6 +531,8 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t, const Ptr type = t.resolve(); + assert(!isa(type) && + "multiset type was not rejected during check()"); assert(!isa(type) && "union type was not rejected during check()"); // if this is boolean, handle it separately to other Enums to avoid diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h index fe0d6d09..139413f3 100644 --- a/murphi2c/src/CLikeGenerator.h +++ b/murphi2c/src/CLikeGenerator.h @@ -72,6 +72,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_mod(const rumur::Mod &n) final; void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; + void visit_multiset(const rumur::Multiset &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index b57f824d..ed410ffe 100644 --- a/murphi2c/src/check.cc +++ b/murphi2c/src/check.cc @@ -27,6 +27,13 @@ class Check : public ConstTraversal { } } + void visit_multiset(const Multiset &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + void visit_union(const Union &) final { if (ok) { std::cerr << "union types are not supported\n"; diff --git a/murphi2murphi/src/DecomposeComplexComparisons.cc b/murphi2murphi/src/DecomposeComplexComparisons.cc index 83eb7f44..4c2d65d2 100644 --- a/murphi2murphi/src/DecomposeComplexComparisons.cc +++ b/murphi2murphi/src/DecomposeComplexComparisons.cc @@ -67,9 +67,9 @@ static std::string explode(std::unordered_set &ids, const Ptr t = type.resolve(); - // if this is a union, assume there is no reasonable way to decompose its - // comparison - if (isa(t)) { + // if this is a multiset or union, assume there is no reasonable way to + // decompose its comparison + if (isa(t) || isa(t)) { buf << prefix_a << stem << (is_eq ? " = " : " != ") << prefix_b << stem; return buf.str(); } @@ -114,6 +114,12 @@ void DecomposeComplexComparisons::rewrite(const EquatableBinaryExpr &n, return; } + // if either side is of multiset type, we cannot decompose this + if (isa(lhs_type) || isa(rhs_type)) { + next.dispatch(n); + return; + } + // if either side is of union type, we cannot decompose this if (isa(lhs_type) || isa(rhs_type)) { next.dispatch(n); diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc index aba94151..8423bf8f 100644 --- a/murphi2murphi/src/Printer.cc +++ b/murphi2murphi/src/Printer.cc @@ -269,6 +269,15 @@ void Printer::visit_model(const Model &n) { void Printer::visit_mul(const Mul &n) { visit_bexpr(n); } +void Printer::visit_multiset(const Multiset &n) { + top->sync_to(n); + top->sync_to(*n.index_bound); + top->dispatch(*n.index_bound); + top->sync_to(*n.element_type); + top->dispatch(*n.element_type); + top->sync_to(n.loc.end); +} + void Printer::visit_negative(const Negative &n) { visit_uexpr(n); } void Printer::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h index c1bc53d6..57164601 100644 --- a/murphi2murphi/src/Printer.h +++ b/murphi2murphi/src/Printer.h @@ -55,6 +55,7 @@ class Printer : public Stage { void visit_mod(const rumur::Mod &n) final; void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; + void visit_multiset(const rumur::Multiset &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc index 51839870..540862ad 100644 --- a/murphi2murphi/src/Stage.cc +++ b/murphi2murphi/src/Stage.cc @@ -132,6 +132,9 @@ void IntermediateStage::visit_lt(const Lt &n) { next.visit_lt(n); } void IntermediateStage::visit_mod(const Mod &n) { next.visit_mod(n); } void IntermediateStage::visit_model(const Model &n) { next.visit_model(n); } void IntermediateStage::visit_mul(const Mul &n) { next.visit_mul(n); } +void IntermediateStage::visit_multiset(const Multiset &n) { + next.visit_multiset(n); +} void IntermediateStage::visit_negative(const Negative &n) { next.visit_negative(n); } diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h index 635d736f..1ca92c4a 100644 --- a/murphi2murphi/src/Stage.h +++ b/murphi2murphi/src/Stage.h @@ -97,6 +97,7 @@ class IntermediateStage : public Stage { void visit_mod(const rumur::Mod &n) override; void visit_model(const rumur::Model &n) override; void visit_mul(const rumur::Mul &n) override; + void visit_multiset(const rumur::Multiset &n) override; void visit_negative(const rumur::Negative &n) override; void visit_neq(const rumur::Neq &n) override; void visit_not(const rumur::Not &n) override; diff --git a/murphi2smv/doc/murphi2smv.1 b/murphi2smv/doc/murphi2smv.1 index 0238859a..1b0e139a 100644 --- a/murphi2smv/doc/murphi2smv.1 +++ b/murphi2smv/doc/murphi2smv.1 @@ -83,6 +83,8 @@ placeholder comment: .IP \[bu] \fBisundefined\fR statements .IP \[bu] +\fBmultiset\fR types +.IP \[bu] \fBproperty\fR statements .IP \[bu] quantifiers diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc index 0abd922a..2c5448d4 100644 --- a/murphi2smv/src/codegen.cc +++ b/murphi2smv/src/codegen.cc @@ -296,6 +296,13 @@ class Printer : public ConstBaseTraversal { *this << '(' << *n.lhs << " * " << *n.rhs << ')'; } + void visit_multiset(const Multiset &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "index: " + << *n.index_bound << "; element type: " << *n.element_type + << " /-- FIXME: end of Murphi multiset type --/"; + } + void visit_negative(const Negative &n) final { *this << '-' << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2uclid/doc/murphi2uclid.1 b/murphi2uclid/doc/murphi2uclid.1 index 1a353fc3..b3896f64 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] +\fBmultiset\fR types +.IP \[bu] \fBunion\fR types .IP \[bu] The modulo operator, \fB%\fR diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc index 4a65a048..e4099818 100644 --- a/murphi2uclid/src/check.cc +++ b/murphi2uclid/src/check.cc @@ -131,6 +131,10 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of the modulo operator", n.loc); } + void visit_multiset(const Multiset &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + void visit_propertyrule(const PropertyRule &n) final { if (n.property.category == Property::COVER) throw Error("cover properties have no LTL equivalent in Uclid5", n.loc); diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc index f9d56bfa..697a5d01 100644 --- a/murphi2uclid/src/codegen.cc +++ b/murphi2uclid/src/codegen.cc @@ -486,6 +486,11 @@ class Printer : public ConstBaseTraversal { *this << "(" << *n.lhs << " * " << *n.rhs << ")"; } + void visit_multiset(const Multiset &) final { + assert(!"multiset not rejected during check()"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { *this << "-" << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc index 0dad71c5..be457157 100644 --- a/murphi2xml/src/XMLPrinter.cc +++ b/murphi2xml/src/XMLPrinter.cc @@ -465,6 +465,19 @@ void XMLPrinter::visit_model(const Model &n) { void XMLPrinter::visit_mul(const Mul &n) { visit_bexpr("mul", n); } +void XMLPrinter::visit_multiset(const Multiset &n) { + sync_to(n); + o << "'; + sync_to(*n.index_bound); + dispatch(*n.index_bound); + sync_to(*n.element_type); + dispatch(*n.element_type); + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_negative(const Negative &n) { visit_uexpr("negative", n); } diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h index 2f333577..69f6e28a 100644 --- a/murphi2xml/src/XMLPrinter.h +++ b/murphi2xml/src/XMLPrinter.h @@ -54,6 +54,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal { void visit_mod(const rumur::Mod &n) final; void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; + void visit_multiset(const rumur::Multiset &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/rumur/src/check.cc b/rumur/src/check.cc index 25558b47..c0359c13 100644 --- a/rumur/src/check.cc +++ b/rumur/src/check.cc @@ -12,6 +12,10 @@ class Check : public ConstTraversal { throw Error("ismember expressions are not supported", n.loc); } + void visit_multiset(const Multiset &n) final { + throw Error("multiset types 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-print.cc b/rumur/src/generate-print.cc index 0c25e4e2..181a3427 100644 --- a/rumur/src/generate-print.cc +++ b/rumur/src/generate-print.cc @@ -317,6 +317,8 @@ class Generator : public ConstTypeTraversal { return; } + assert(!isa(t) && + "multiset type not rejected before code generation"); assert(!isa(t) && "union type not rejected before code generation"); assert(!"non-range, non-enum used as array index"); @@ -361,6 +363,10 @@ class Generator : public ConstTypeTraversal { << "}\n"; } + void visit_multiset(const Multiset &n) final { + throw Error("multiset types are not supported", n.loc); + } + void visit_range(const Range &n) final { const std::string lb = "VALUE_C(" + n.lower_bound().get_str() + ")"; diff --git a/rumur/src/generate-stmt.cc b/rumur/src/generate-stmt.cc index ed3bdd28..aee22397 100644 --- a/rumur/src/generate-stmt.cc +++ b/rumur/src/generate-stmt.cc @@ -79,6 +79,9 @@ static void clear(std::ostream &out, const TypeExpr &t, clear(out, *m, offset, depth); } + assert(!isa(type) && + "multiset not rejected prior to code generation"); + assert(!"unreachable"); } diff --git a/rumur/src/smt/define-enum-members.cc b/rumur/src/smt/define-enum-members.cc index 4f1948d3..9bafbc28 100644 --- a/rumur/src/smt/define-enum-members.cc +++ b/rumur/src/smt/define-enum-members.cc @@ -49,6 +49,11 @@ class Definer : public ConstTypeTraversal { } } + void visit_multiset(const Multiset &n) final { + // define any enum members that occur within the multiset element type + dispatch(*n.element_type); + } + void visit_range(const Range &) final { // as a primitive, ranges can't contain any enum members } diff --git a/rumur/src/smt/define-records.cc b/rumur/src/smt/define-records.cc index 49db5700..ea47eccb 100644 --- a/rumur/src/smt/define-records.cc +++ b/rumur/src/smt/define-records.cc @@ -29,6 +29,11 @@ class Definer : public ConstTypeTraversal { // nothing to do } + void visit_multiset(const Multiset &n) final { + // define any records that are defined within this multiset + dispatch(*n.element_type); + } + void visit_range(const Range &) final { // nothing to do } diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc index 647ce14b..05920ba3 100644 --- a/rumur/src/smt/simplify.cc +++ b/rumur/src/smt/simplify.cc @@ -220,6 +220,13 @@ class Simplifier : public BaseTraversal { } void visit_mul(Mul &n) final { visit_bexpr(n); } + + void visit_multiset(Multiset &n) final { + dispatch(*n.index_bound); + simplify(n.index_bound); + dispatch(*n.element_type); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } void visit_not(Not &n) final { visit_uexpr(n); } @@ -569,6 +576,8 @@ class Simplifier : public BaseTraversal { *solver << "(assert (" << lt() << " " << name << " " << size << "))\n"; } + void visit_multiset(const Multiset &) final { throw Unsupported(); } + void visit_range(const Range &n) final { // if this range's bounds are static, make them known to the solver diff --git a/rumur/src/smt/typeexpr-to-smt.cc b/rumur/src/smt/typeexpr-to-smt.cc index 13105337..4bca7452 100644 --- a/rumur/src/smt/typeexpr-to-smt.cc +++ b/rumur/src/smt/typeexpr-to-smt.cc @@ -49,6 +49,10 @@ class Translator : public ConstTypeTraversal { *this << integer_type(); } + void visit_multiset(const Multiset &) final { + throw Unsupported("multiset types are not supported in SMT translation"); + } + void visit_range(const Range &) final { /* we assume our caller will eventually set the lower and upper bound * constraints for this integer if it is relevant to them diff --git a/rumur/src/symmetry-reduction.cc b/rumur/src/symmetry-reduction.cc index b48a0613..e512c5eb 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(t) && + "multiset type not rejected before symmetry reduction"); assert(!isa(t) && "union type not rejected before symmetry reduction"); assert(!"missed case in generate_apply_swap"); @@ -200,6 +202,8 @@ static void generate_swap_chunk(std::ostream &out, const TypeExpr &t, return; } + assert(!isa(type) && + "multiset type not rejected before symmetry reduction"); assert(!isa(type) && "union type not rejected before symmetry reduction"); @@ -472,6 +476,8 @@ static void generate_apply_compare(std::ostream &out, const TypeExpr &type, return; } + assert(!isa(t) && + "multiset type not rejected before symmetry reduction"); assert(!isa(t) && "union type not rejected before symmetry reduction"); assert(!"missed case in generate_apply_compare"); @@ -583,6 +589,8 @@ static void generate_compare_chunk(std::ostream &out, const TypeExpr &t, return; } + assert(!isa(type) && + "multiset type not rejected before symmetry reduction"); assert(!isa(type) && "union type not rejected before symmetry reduction"); From 0b3e81a6b425d10f5847e8907cf36487944cc017 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 02/21] support 'multiset' during lexing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- 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 e5bc910b..3cf52311 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -99,6 +99,7 @@ invariant { return rumur::parser::token::INVARIANT; } ismember { return rumur::parser::token::ISMEMBER; } isundefined { return rumur::parser::token::ISUNDEFINED; } liveness { return rumur::parser::token::LIVENESS; } +multiset { return rumur::parser::token::MULTISET; } of { return rumur::parser::token::OF; } procedure { return rumur::parser::token::PROCEDURE; } put { return rumur::parser::token::PUT; } diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 724fdc8b..29a49e87 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -161,6 +161,7 @@ %token LIVENESS %token LOR "∨" %token LSH "<<" +%token MULTISET %token NEQ "!=" %token NUMBER %token OF From 0639e869deb55f9930e485a5029c82316eafc950 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 03/21] support 'multiset' during parsing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- doc/vs-cmurphi.rst | 12 +++++++++++- librumur/src/parser.yy | 2 ++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst index 39896992..15c24e90 100644 --- a/doc/vs-cmurphi.rst +++ b/doc/vs-cmurphi.rst @@ -37,7 +37,17 @@ 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 ``multiset`` type. +support. + +Multisets +^^^^^^^^^ +Models that use the ``multiset`` type can be parsed with librumur, but +generation of a checker using ``rumur`` is not supported. Some of the Rumur +tools fully support multiset types, e.g. ``murphi2xml``, but others reject +models with multiset types, e.g. ``murphi2uclid``. + +CMurphi requires the index of multiset to be a scalarset bound. Rumur supports +any constant expression as a bound. Unions ^^^^^^ diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 29a49e87..9dd7070f 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -681,6 +681,8 @@ typeexpr: BOOLEAN { $$ = rumur::Ptr::make($2, @$); } | ARRAY '[' typeexpr ']' OF typeexpr { $$ = rumur::Ptr::make($3, $6, @$); +} | MULTISET '[' expr ']' OF typeexpr { + $$ = rumur::Ptr::make($3, $6, @$); } | SCALARSET '(' expr ')' { $$ = rumur::Ptr::make($3, @$); } | UNION '{' typeexprs '}' { From 1942fbaab08493e2a02a02cb1ef3af40b1901cd9 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 04/21] API BREAK: preliminary support for 'MultisetAdd' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One might think this could just be implemented as a built-in name for a procedure. But this needs to have a generic type (type constraint of its first parameter depends on its second parameter) that we cannot describe in the usual type system. Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/include/rumur/Stmt.h | 12 ++++++++++++ librumur/include/rumur/indexer.h | 1 + librumur/include/rumur/traverse.h | 6 ++++++ librumur/src/Function.cc | 6 ++++++ librumur/src/Stmt.cc | 24 ++++++++++++++++++++++++ librumur/src/indexer.cc | 6 ++++++ librumur/src/resolve-symbols.cc | 7 +++++++ librumur/src/traverse.cc | 20 ++++++++++++++++++++ librumur/src/validate.cc | 6 ++++++ misc/murphi2xml.rng | 26 +++++++++++++++++++++----- 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-stmt.cc | 5 +++++ rumur/src/smt/simplify.cc | 7 +++++++ 26 files changed, 188 insertions(+), 5 deletions(-) diff --git a/librumur/include/rumur/Stmt.h b/librumur/include/rumur/Stmt.h index 1a8a4c25..cf48f564 100644 --- a/librumur/include/rumur/Stmt.h +++ b/librumur/include/rumur/Stmt.h @@ -130,6 +130,18 @@ struct RUMUR_API_WITH_RTTI If : public Stmt { void visit(ConstBaseTraversal &visitor) const override; }; +struct RUMUR_API_WITH_RTTI MultisetAdd : public Stmt { + Ptr arg0; + Ptr arg1; + + MultisetAdd(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_); + MultisetAdd *clone() const override; + void validate() const override; + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; +}; + struct RUMUR_API_WITH_RTTI ProcedureCall : public Stmt { FunctionCall call; diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h index 34550d66..ae77383f 100644 --- a/librumur/include/rumur/indexer.h +++ b/librumur/include/rumur/indexer.h @@ -61,6 +61,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_mod(Mod &n) override; void visit_mul(Mul &n) override; void visit_multiset(Multiset &n) override; + void visit_multisetadd(MultisetAdd &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h index 1df46662..190dbbfd 100644 --- a/librumur/include/rumur/traverse.h +++ b/librumur/include/rumur/traverse.h @@ -107,6 +107,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_mod(Mod &n) = 0; virtual void visit_mul(Mul &n) = 0; virtual void visit_multiset(Multiset &n) = 0; + virtual void visit_multisetadd(MultisetAdd &n) = 0; virtual void visit_negative(Negative &n) = 0; virtual void visit_neq(Neq &n) = 0; virtual void visit_not(Not &n) = 0; @@ -196,6 +197,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_mod(Mod &n) override; void visit_mul(Mul &n) override; void visit_multiset(Multiset &n) override; + void visit_multisetadd(MultisetAdd &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; @@ -277,6 +279,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_mod(const Mod &n) = 0; virtual void visit_mul(const Mul &n) = 0; virtual void visit_multiset(const Multiset &n) = 0; + virtual void visit_multisetadd(const MultisetAdd &n) = 0; virtual void visit_negative(const Negative &n) = 0; virtual void visit_neq(const Neq &n) = 0; virtual void visit_not(const Not &n) = 0; @@ -358,6 +361,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_mod(const Mod &n) override; void visit_mul(const Mul &n) override; void visit_multiset(const Multiset &n) override; + void visit_multisetadd(const MultisetAdd &n) override; void visit_negative(const Negative &n) override; void visit_neq(const Neq &n) override; void visit_not(const Not &n) override; @@ -419,6 +423,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal { void visit_ifclause(const IfClause &n) final; void visit_model(const Model &n) final; void visit_multiset(const Multiset &n) final; + void visit_multisetadd(const MultisetAdd &n) final; void visit_procedurecall(const ProcedureCall &n) final; void visit_property(const Property &n) final; void visit_propertyrule(const PropertyRule &n) final; @@ -549,6 +554,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal { void visit_model(const Model &n) final; void visit_mod(const Mod &n) final; void visit_mul(const Mul &n) final; + void visit_multisetadd(const MultisetAdd &n) final; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; diff --git a/librumur/src/Function.cc b/librumur/src/Function.cc index a1bb2c92..d75ecac7 100644 --- a/librumur/src/Function.cc +++ b/librumur/src/Function.cc @@ -141,6 +141,12 @@ bool Function::is_pure() const { pure &= n.function->is_pure(); } + void visit_multisetadd(const MultisetAdd &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + pure &= !is_global_ref(*n.arg1); + } + void visit_propertystmt(const PropertyStmt &) final { // treat any property statement as a side effect pure = false; diff --git a/librumur/src/Stmt.cc b/librumur/src/Stmt.cc index adad9287..e8b21ee2 100644 --- a/librumur/src/Stmt.cc +++ b/librumur/src/Stmt.cc @@ -155,6 +155,30 @@ void If::visit(BaseTraversal &visitor) { visitor.visit_if(*this); } void If::visit(ConstBaseTraversal &visitor) const { visitor.visit_if(*this); } +MultisetAdd::MultisetAdd(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_) + : Stmt(loc_), arg0(arg0_), arg1(arg1_) {} + +MultisetAdd *MultisetAdd::clone() const { return new MultisetAdd(*this); } + +void MultisetAdd::validate() const { + const Ptr t1 = arg1->type()->resolve(); + auto m = dynamic_cast(t1.get()); + if (m == nullptr) + throw Error("second argument to multisetadd is not a multiset", arg1->loc); + + if (!arg0->type()->coerces_to(*m->element_type)) + throw Error("incompatible multisetadd arguments", loc); +} + +void MultisetAdd::visit(BaseTraversal &visitor) { + visitor.visit_multisetadd(*this); +} + +void MultisetAdd::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetadd(*this); +} + ProcedureCall::ProcedureCall(const std::string &name, const std::vector> &arguments, const location &loc_) diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc index fa133948..c4e06c15 100644 --- a/librumur/src/indexer.cc +++ b/librumur/src/indexer.cc @@ -191,6 +191,12 @@ void Indexer::visit_multiset(Multiset &n) { dispatch(*n.element_type); } +void Indexer::visit_multisetadd(MultisetAdd &n) { + n.unique_id = next++; + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void Indexer::visit_negative(Negative &n) { visit_uexpr(n); } void Indexer::visit_neq(Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 7565fa97..54906577 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -331,6 +331,13 @@ class Resolver : public Traversal { disambiguate(n.index_bound); } + void visit_multisetadd(MultisetAdd &n) final { + dispatch(*n.arg0); + disambiguate(n.arg0); + dispatch(*n.arg1); + disambiguate(n.arg1); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc index c6ff2d1c..8eda7f8d 100644 --- a/librumur/src/traverse.cc +++ b/librumur/src/traverse.cc @@ -164,6 +164,11 @@ void Traversal::visit_multiset(Multiset &n) { dispatch(*n.element_type); } +void Traversal::visit_multisetadd(MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void Traversal::visit_negative(Negative &n) { visit_uexpr(n); } void Traversal::visit_neq(Neq &n) { visit_bexpr(n); } @@ -448,6 +453,11 @@ void ConstTraversal::visit_multiset(const Multiset &n) { dispatch(*n.element_type); } +void ConstTraversal::visit_multisetadd(const MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void ConstTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -662,6 +672,11 @@ void ConstExprTraversal::visit_multiset(const Multiset &n) { dispatch(*n.element_type); } +void ConstExprTraversal::visit_multisetadd(const MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void ConstExprTraversal::visit_procedurecall(const ProcedureCall &n) { dispatch(n.call); } @@ -1143,6 +1158,11 @@ void ConstTypeTraversal::visit_model(const Model &n) { void ConstTypeTraversal::visit_mul(const Mul &n) { visit_bexpr(n); } +void ConstTypeTraversal::visit_multisetadd(const MultisetAdd &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void ConstTypeTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTypeTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc index 10a3bcaf..5e5294c5 100644 --- a/librumur/src/validate.cc +++ b/librumur/src/validate.cc @@ -260,6 +260,12 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_multisetadd(const MultisetAdd &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + n.validate(); + } + void visit_negative(const Negative &n) final { dispatch(*n.rhs); n.validate(); diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng index dfa4684a..445e6498 100644 --- a/misc/murphi2xml.rng +++ b/misc/murphi2xml.rng @@ -83,6 +83,14 @@ + + + + + + + + @@ -419,11 +427,7 @@ - - - - - + @@ -623,6 +627,17 @@ + + + + + + + + + + + @@ -1000,6 +1015,7 @@ + diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c index 6928fa67..94cb58f6 100644 --- a/murphi-format/src/format.c +++ b/murphi-format/src/format.c @@ -302,6 +302,9 @@ static bool is_keyword(const char *text) { // it is more intuitive to suppress space between `multiset` and `[` if (streq(text, "multiset")) return true; + // `multisetadd` is a keyword, but is used as if it were a function + if (streq(text, "multisetadd")) + return true; #endif if (streq(text, "of")) return true; diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 26ec3a78..05b1714d 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -435,6 +435,11 @@ void CLikeGenerator::visit_multiset(const Multiset &) { __builtin_unreachable(); } +void CLikeGenerator::visit_multisetadd(const MultisetAdd &) { + assert(!"multisetadd was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_negative(const Negative &n) { *this << "(-" << *n.rhs << ")"; } diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h index 139413f3..a0ffdb76 100644 --- a/murphi2c/src/CLikeGenerator.h +++ b/murphi2c/src/CLikeGenerator.h @@ -73,6 +73,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; void visit_multiset(const rumur::Multiset &n) final; + void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index ed410ffe..78bf3767 100644 --- a/murphi2c/src/check.cc +++ b/murphi2c/src/check.cc @@ -34,6 +34,13 @@ class Check : public ConstTraversal { } } + void visit_multisetadd(const MultisetAdd &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + void visit_union(const Union &) final { if (ok) { std::cerr << "union types are not supported\n"; diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc index 8423bf8f..008021e9 100644 --- a/murphi2murphi/src/Printer.cc +++ b/murphi2murphi/src/Printer.cc @@ -278,6 +278,15 @@ void Printer::visit_multiset(const Multiset &n) { top->sync_to(n.loc.end); } +void Printer::visit_multisetadd(const MultisetAdd &n) { + top->sync_to(n); + top->sync_to(*n.arg0); + top->dispatch(*n.arg0); + top->sync_to(*n.arg1); + top->dispatch(*n.arg1); + top->sync_to(n.loc.end); +} + void Printer::visit_negative(const Negative &n) { visit_uexpr(n); } void Printer::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h index 57164601..02e9c5d9 100644 --- a/murphi2murphi/src/Printer.h +++ b/murphi2murphi/src/Printer.h @@ -56,6 +56,7 @@ class Printer : public Stage { void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; void visit_multiset(const rumur::Multiset &n) final; + void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc index 540862ad..996ff489 100644 --- a/murphi2murphi/src/Stage.cc +++ b/murphi2murphi/src/Stage.cc @@ -135,6 +135,9 @@ void IntermediateStage::visit_mul(const Mul &n) { next.visit_mul(n); } void IntermediateStage::visit_multiset(const Multiset &n) { next.visit_multiset(n); } +void IntermediateStage::visit_multisetadd(const MultisetAdd &n) { + next.visit_multisetadd(n); +} void IntermediateStage::visit_negative(const Negative &n) { next.visit_negative(n); } diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h index 1ca92c4a..a181370c 100644 --- a/murphi2murphi/src/Stage.h +++ b/murphi2murphi/src/Stage.h @@ -98,6 +98,7 @@ class IntermediateStage : public Stage { void visit_model(const rumur::Model &n) override; void visit_mul(const rumur::Mul &n) override; void visit_multiset(const rumur::Multiset &n) override; + void visit_multisetadd(const rumur::MultisetAdd &n) override; void visit_negative(const rumur::Negative &n) override; void visit_neq(const rumur::Neq &n) override; void visit_not(const rumur::Not &n) override; diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc index 2c5448d4..8e79e07c 100644 --- a/murphi2smv/src/codegen.cc +++ b/murphi2smv/src/codegen.cc @@ -303,6 +303,12 @@ class Printer : public ConstBaseTraversal { << " /-- FIXME: end of Murphi multiset type --/"; } + void visit_multisetadd(const MultisetAdd &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetAdd(" + << *n.arg0 << ", " << *n.arg1 << ')'; + } + void visit_negative(const Negative &n) final { *this << '-' << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc index e4099818..b7c82344 100644 --- a/murphi2uclid/src/check.cc +++ b/murphi2uclid/src/check.cc @@ -135,6 +135,10 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of the multiset type", n.loc); } + void visit_multisetadd(const MultisetAdd &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + void visit_propertyrule(const PropertyRule &n) final { if (n.property.category == Property::COVER) throw Error("cover properties have no LTL equivalent in Uclid5", n.loc); diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc index 697a5d01..3cd2216e 100644 --- a/murphi2uclid/src/codegen.cc +++ b/murphi2uclid/src/codegen.cc @@ -491,6 +491,11 @@ class Printer : public ConstBaseTraversal { __builtin_unreachable(); } + void visit_multisetadd(const MultisetAdd &) final { + assert(!"multisetadd not rejected during check()"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { *this << "-" << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc index be457157..99bb53a2 100644 --- a/murphi2xml/src/XMLPrinter.cc +++ b/murphi2xml/src/XMLPrinter.cc @@ -478,6 +478,23 @@ void XMLPrinter::visit_multiset(const Multiset &n) { o << ""; } +void XMLPrinter::visit_multisetadd(const MultisetAdd &n) { + sync_to(n); + o << "'; + sync_to(*n.arg0); + o << ""; + dispatch(*n.arg0); + o << ""; + sync_to(*n.arg1); + o << ""; + dispatch(*n.arg1); + o << ""; + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_negative(const Negative &n) { visit_uexpr("negative", n); } diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h index 69f6e28a..4ddef884 100644 --- a/murphi2xml/src/XMLPrinter.h +++ b/murphi2xml/src/XMLPrinter.h @@ -55,6 +55,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal { void visit_model(const rumur::Model &n) final; void visit_mul(const rumur::Mul &n) final; void visit_multiset(const rumur::Multiset &n) final; + void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/rumur/src/check.cc b/rumur/src/check.cc index c0359c13..de87847d 100644 --- a/rumur/src/check.cc +++ b/rumur/src/check.cc @@ -16,6 +16,10 @@ class Check : public ConstTraversal { throw Error("multiset types are not supported", n.loc); } + void visit_multisetadd(const MultisetAdd &n) final { + throw Error("multiset types 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-stmt.cc b/rumur/src/generate-stmt.cc index aee22397..e2aaab84 100644 --- a/rumur/src/generate-stmt.cc +++ b/rumur/src/generate-stmt.cc @@ -208,6 +208,11 @@ class Generator : public ConstStmtTraversal { } } + void visit_multisetadd(const MultisetAdd &) final { + assert(!"multisetadd not rejected during check()"); + __builtin_unreachable(); + } + void visit_procedurecall(const ProcedureCall &s) final { generate_rvalue(*out, s.call); } diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc index 05920ba3..2f362283 100644 --- a/rumur/src/smt/simplify.cc +++ b/rumur/src/smt/simplify.cc @@ -227,6 +227,13 @@ class Simplifier : public BaseTraversal { dispatch(*n.element_type); } + void visit_multisetadd(MultisetAdd &n) final { + dispatch(*n.arg0); + simplify(n.arg0); + dispatch(*n.arg1); + simplify(n.arg1); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } void visit_not(Not &n) final { visit_uexpr(n); } From b9d77afccfc01ce9be1287580714c8dd3934493c Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 05/21] support 'multisetadd' during lexing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- 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 3cf52311..140a7356 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -100,6 +100,7 @@ ismember { return rumur::parser::token::ISMEMBER; } isundefined { return rumur::parser::token::ISUNDEFINED; } liveness { return rumur::parser::token::LIVENESS; } multiset { return rumur::parser::token::MULTISET; } +multisetadd { return rumur::parser::token::MULTISETADD; } of { return rumur::parser::token::OF; } procedure { return rumur::parser::token::PROCEDURE; } put { return rumur::parser::token::PUT; } diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 9dd7070f..8f893b5f 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -162,6 +162,7 @@ %token LOR "∨" %token LSH "<<" %token MULTISET +%token MULTISETADD %token NEQ "!=" %token NUMBER %token OF From dbd173eefe7ab88b329330d58c214169133aca46 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 06/21] support 'multisetadd' during parsing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- doc/vs-cmurphi.rst | 3 +++ librumur/src/parser.yy | 2 ++ 2 files changed, 5 insertions(+) diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst index 15c24e90..d030c6f1 100644 --- a/doc/vs-cmurphi.rst +++ b/doc/vs-cmurphi.rst @@ -49,6 +49,9 @@ models with multiset types, e.g. ``murphi2uclid``. CMurphi requires the index of multiset to be a scalarset bound. Rumur supports any constant expression as a bound. +This limitation of syntax-only support applies also to the multiset construct +``MultisetAdd``. + Unions ^^^^^^ Models that use the ``union`` type can be parsed with librumur, but generation diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 8f893b5f..c0646b63 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -600,6 +600,8 @@ stmt: category STRING expr { cs.insert(cs.end(), $5.begin(), $5.end()); cs.insert(cs.end(), $6.begin(), $6.end()); $$ = rumur::Ptr::make(cs, @$); +} | MULTISETADD '(' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, @$); } | PUT STRING { $$ = rumur::Ptr::make($2, @$); } | PUT expr { From df05e0f8df35146f535cc42cc134cd2efbb47735 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 07/21] API BREAK: preliminary support for 'MultisetCount' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Despite being phrased like a function call, this actually acts more like a quantified expression. Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/include/rumur/Expr.h | 20 ++++++++++++ librumur/include/rumur/indexer.h | 1 + librumur/include/rumur/traverse.h | 6 ++++ librumur/src/Expr.cc | 53 +++++++++++++++++++++++++++++++ librumur/src/indexer.cc | 6 ++++ librumur/src/resolve-symbols.cc | 21 ++++++++++++ librumur/src/traverse.cc | 20 ++++++++++++ librumur/src/validate.cc | 6 ++++ misc/murphi2xml.rng | 15 +++++++++ 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 | 7 ++++ 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 | 19 +++++++++++ rumur/src/smt/translate.cc | 4 +++ 26 files changed, 244 insertions(+) diff --git a/librumur/include/rumur/Expr.h b/librumur/include/rumur/Expr.h index 88e86350..65c2b03f 100644 --- a/librumur/include/rumur/Expr.h +++ b/librumur/include/rumur/Expr.h @@ -710,4 +710,24 @@ struct RUMUR_API_WITH_RTTI IsUndefined : public UnaryExpr { void to_stream(std::ostream &out) const override; }; +struct RUMUR_API_WITH_RTTI MultisetCount : public Expr { + std::string identifier; + Ptr container; + Ptr predicate; + + MultisetCount(const std::string &identifier_, const Ptr &container_, + const Ptr &predicate_, const location &loc_); + MultisetCount *clone() const override; + + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; + + bool constant() const override; + Ptr type() const override; + mpz_class constant_fold() const override; + void validate() const override; + void to_stream(std::ostream &out) const override; + bool is_pure() const override; +}; + } // namespace rumur diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h index ae77383f..21f74043 100644 --- a/librumur/include/rumur/indexer.h +++ b/librumur/include/rumur/indexer.h @@ -62,6 +62,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_mul(Mul &n) override; void visit_multiset(Multiset &n) override; void visit_multisetadd(MultisetAdd &n) override; + void visit_multisetcount(MultisetCount &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h index 190dbbfd..e06da814 100644 --- a/librumur/include/rumur/traverse.h +++ b/librumur/include/rumur/traverse.h @@ -108,6 +108,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_mul(Mul &n) = 0; virtual void visit_multiset(Multiset &n) = 0; virtual void visit_multisetadd(MultisetAdd &n) = 0; + virtual void visit_multisetcount(MultisetCount &n) = 0; virtual void visit_negative(Negative &n) = 0; virtual void visit_neq(Neq &n) = 0; virtual void visit_not(Not &n) = 0; @@ -198,6 +199,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_mul(Mul &n) override; void visit_multiset(Multiset &n) override; void visit_multisetadd(MultisetAdd &n) override; + void visit_multisetcount(MultisetCount &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; @@ -280,6 +282,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_mul(const Mul &n) = 0; virtual void visit_multiset(const Multiset &n) = 0; virtual void visit_multisetadd(const MultisetAdd &n) = 0; + virtual void visit_multisetcount(const MultisetCount &n) = 0; virtual void visit_negative(const Negative &n) = 0; virtual void visit_neq(const Neq &n) = 0; virtual void visit_not(const Not &n) = 0; @@ -362,6 +365,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_mul(const Mul &n) override; void visit_multiset(const Multiset &n) override; void visit_multisetadd(const MultisetAdd &n) override; + void visit_multisetcount(const MultisetCount &n) override; void visit_negative(const Negative &n) override; void visit_neq(const Neq &n) override; void visit_not(const Not &n) override; @@ -486,6 +490,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal { void visit_mod(const Mod &n) final; void visit_mul(const Mul &n) final; void visit_multiset(const Multiset &n) final; + void visit_multisetcount(const MultisetCount &n) final; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; @@ -555,6 +560,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal { void visit_mod(const Mod &n) final; void visit_mul(const Mul &n) final; void visit_multisetadd(const MultisetAdd &n) final; + void visit_multisetcount(const MultisetCount &n) final; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc index c4b9138f..ed2aef41 100644 --- a/librumur/src/Expr.cc +++ b/librumur/src/Expr.cc @@ -12,6 +12,7 @@ #include #include #include +#include #include #include #include @@ -1744,4 +1745,56 @@ void IsUndefined::to_stream(std::ostream &out) const { out << "isundefined(" << *rhs << ')'; } +MultisetCount::MultisetCount(const std::string &identifier_, + const Ptr &container_, + const Ptr &predicate_, const location &loc_) + : Expr(loc_), identifier(identifier_), container(container_), + predicate(predicate_) {} + +MultisetCount *MultisetCount::clone() const { return new MultisetCount(*this); } + +void MultisetCount::visit(BaseTraversal &visitor) { + visitor.visit_multisetcount(*this); +} + +void MultisetCount::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetcount(*this); +} + +bool MultisetCount::constant() const { return false; } + +Ptr MultisetCount::type() const { + const Ptr c = container->type()->resolve(); + auto m = dynamic_cast(c.get()); + if (m == nullptr) + throw Error("multisetcount container is not a multiset", container->loc); + + const Ptr lb = Ptr::make(0, loc); + const Ptr ub = + Ptr::make(m->index_bound->constant_fold() - 1, loc); + return Ptr::make(lb, ub, loc); +} + +mpz_class MultisetCount::constant_fold() const { + throw Error("multisetcount used in constant expression", loc); +} + +void MultisetCount::validate() const { + const Ptr c = container->type()->resolve(); + if (!isa(c)) + throw Error("multisetcount container is not a multiset", container->loc); + + const Ptr p = predicate->type()->resolve(); + if (!p->is_boolean()) + throw Error("multisetcount predicate is not a boolean expression", + predicate->loc); +} + +void MultisetCount::to_stream(std::ostream &out) const { + out << "multisetcount(" << identifier << ": " << *container << ", " + << *predicate << ')'; +} + +bool MultisetCount::is_pure() const { return true; } + } // namespace rumur diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc index c4e06c15..4e46f4ca 100644 --- a/librumur/src/indexer.cc +++ b/librumur/src/indexer.cc @@ -197,6 +197,12 @@ void Indexer::visit_multisetadd(MultisetAdd &n) { dispatch(*n.arg1); } +void Indexer::visit_multisetcount(MultisetCount &n) { + n.unique_id = next++; + dispatch(*n.container); + dispatch(*n.predicate); +} + void Indexer::visit_negative(Negative &n) { visit_uexpr(n); } void Indexer::visit_neq(Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 54906577..92d4deba 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -338,6 +338,27 @@ class Resolver : public Traversal { disambiguate(n.arg1); } + void visit_multisetcount(MultisetCount &n) final { + dispatch(*n.container); + disambiguate(n.container); + + symtab.open_scope(); + + const Ptr id_type = n.container->type()->resolve(); + auto m = dynamic_cast(id_type.get()); + if (m == nullptr) + throw Error("multisetcount container is not a multiset", + n.container->loc); + const Ptr s = Ptr::make(m->index_bound, n.loc); + VarDecl *const i = make(n.identifier, s, n.loc); + symtab.declare(n.identifier, i); + + dispatch(*n.predicate); + symtab.close_scope(); + + disambiguate(n.predicate); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc index 8eda7f8d..3a4c5e16 100644 --- a/librumur/src/traverse.cc +++ b/librumur/src/traverse.cc @@ -169,6 +169,11 @@ void Traversal::visit_multisetadd(MultisetAdd &n) { dispatch(*n.arg1); } +void Traversal::visit_multisetcount(MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void Traversal::visit_negative(Negative &n) { visit_uexpr(n); } void Traversal::visit_neq(Neq &n) { visit_bexpr(n); } @@ -458,6 +463,11 @@ void ConstTraversal::visit_multisetadd(const MultisetAdd &n) { dispatch(*n.arg1); } +void ConstTraversal::visit_multisetcount(const MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -914,6 +924,11 @@ void ConstStmtTraversal::visit_multiset(const Multiset &n) { dispatch(*n.element_type); } +void ConstStmtTraversal::visit_multisetcount(const MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstStmtTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstStmtTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -1163,6 +1178,11 @@ void ConstTypeTraversal::visit_multisetadd(const MultisetAdd &n) { dispatch(*n.arg1); } +void ConstTypeTraversal::visit_multisetcount(const MultisetCount &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstTypeTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTypeTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc index 5e5294c5..5363a2b7 100644 --- a/librumur/src/validate.cc +++ b/librumur/src/validate.cc @@ -266,6 +266,12 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_multisetcount(const MultisetCount &n) final { + dispatch(*n.container); + dispatch(*n.predicate); + n.validate(); + } + void visit_negative(const Negative &n) final { dispatch(*n.rhs); n.validate(); diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng index 445e6498..5ce7f104 100644 --- a/misc/murphi2xml.rng +++ b/misc/murphi2xml.rng @@ -305,6 +305,7 @@ + @@ -638,6 +639,20 @@ + + + + + + + + + + + + + + diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c index 94cb58f6..afe0216f 100644 --- a/murphi-format/src/format.c +++ b/murphi-format/src/format.c @@ -305,6 +305,9 @@ static bool is_keyword(const char *text) { // `multisetadd` is a keyword, but is used as if it were a function if (streq(text, "multisetadd")) return true; + // `multisetcount` is a keyword, but is used as if it were a function + if (streq(text, "multisetcount")) + return true; #endif if (streq(text, "of")) return true; diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 05b1714d..fbd80b26 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -440,6 +440,11 @@ void CLikeGenerator::visit_multisetadd(const MultisetAdd &) { __builtin_unreachable(); } +void CLikeGenerator::visit_multisetcount(const MultisetCount &) { + assert(!"multisetcount was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_negative(const Negative &n) { *this << "(-" << *n.rhs << ")"; } diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h index a0ffdb76..53481a5b 100644 --- a/murphi2c/src/CLikeGenerator.h +++ b/murphi2c/src/CLikeGenerator.h @@ -74,6 +74,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_mul(const rumur::Mul &n) final; void visit_multiset(const rumur::Multiset &n) final; void visit_multisetadd(const rumur::MultisetAdd &n) final; + void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index 78bf3767..51ce55d3 100644 --- a/murphi2c/src/check.cc +++ b/murphi2c/src/check.cc @@ -41,6 +41,13 @@ class Check : public ConstTraversal { } } + void visit_multisetcount(const MultisetCount &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + void visit_union(const Union &) final { if (ok) { std::cerr << "union types are not supported\n"; diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc index 008021e9..de8b7874 100644 --- a/murphi2murphi/src/Printer.cc +++ b/murphi2murphi/src/Printer.cc @@ -287,6 +287,15 @@ void Printer::visit_multisetadd(const MultisetAdd &n) { top->sync_to(n.loc.end); } +void Printer::visit_multisetcount(const MultisetCount &n) { + top->sync_to(n); + top->sync_to(*n.container); + top->dispatch(*n.container); + top->sync_to(*n.predicate); + top->dispatch(*n.predicate); + top->sync_to(n.loc.end); +} + void Printer::visit_negative(const Negative &n) { visit_uexpr(n); } void Printer::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h index 02e9c5d9..3e96ada7 100644 --- a/murphi2murphi/src/Printer.h +++ b/murphi2murphi/src/Printer.h @@ -57,6 +57,7 @@ class Printer : public Stage { void visit_mul(const rumur::Mul &n) final; void visit_multiset(const rumur::Multiset &n) final; void visit_multisetadd(const rumur::MultisetAdd &n) final; + void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc index 996ff489..0b944a2d 100644 --- a/murphi2murphi/src/Stage.cc +++ b/murphi2murphi/src/Stage.cc @@ -138,6 +138,9 @@ void IntermediateStage::visit_multiset(const Multiset &n) { void IntermediateStage::visit_multisetadd(const MultisetAdd &n) { next.visit_multisetadd(n); } +void IntermediateStage::visit_multisetcount(const MultisetCount &n) { + next.visit_multisetcount(n); +} void IntermediateStage::visit_negative(const Negative &n) { next.visit_negative(n); } diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h index a181370c..2e41bf1f 100644 --- a/murphi2murphi/src/Stage.h +++ b/murphi2murphi/src/Stage.h @@ -99,6 +99,7 @@ class IntermediateStage : public Stage { void visit_mul(const rumur::Mul &n) override; void visit_multiset(const rumur::Multiset &n) override; void visit_multisetadd(const rumur::MultisetAdd &n) override; + void visit_multisetcount(const rumur::MultisetCount &n) override; void visit_negative(const rumur::Negative &n) override; void visit_neq(const rumur::Neq &n) override; void visit_not(const rumur::Not &n) override; diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc index 8e79e07c..c67f3be0 100644 --- a/murphi2smv/src/codegen.cc +++ b/murphi2smv/src/codegen.cc @@ -309,6 +309,13 @@ class Printer : public ConstBaseTraversal { << *n.arg0 << ", " << *n.arg1 << ')'; } + void visit_multisetcount(const MultisetCount &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetCount(" + << n.identifier << ": " << *n.container << ", " << *n.predicate + << ')'; + } + void visit_negative(const Negative &n) final { *this << '-' << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc index b7c82344..4dd89614 100644 --- a/murphi2uclid/src/check.cc +++ b/murphi2uclid/src/check.cc @@ -139,6 +139,10 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of the multiset type", n.loc); } + void visit_multisetcount(const MultisetCount &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + void visit_propertyrule(const PropertyRule &n) final { if (n.property.category == Property::COVER) throw Error("cover properties have no LTL equivalent in Uclid5", n.loc); diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc index 3cd2216e..20a048db 100644 --- a/murphi2uclid/src/codegen.cc +++ b/murphi2uclid/src/codegen.cc @@ -496,6 +496,11 @@ class Printer : public ConstBaseTraversal { __builtin_unreachable(); } + void visit_multisetcount(const MultisetCount &) final { + assert(!"multisetcount not rejected during check()"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { *this << "-" << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc index 99bb53a2..ccb95753 100644 --- a/murphi2xml/src/XMLPrinter.cc +++ b/murphi2xml/src/XMLPrinter.cc @@ -495,6 +495,23 @@ void XMLPrinter::visit_multisetadd(const MultisetAdd &n) { o << ""; } +void XMLPrinter::visit_multisetcount(const MultisetCount &n) { + sync_to(n); + o << "'; + sync_to(*n.container); + o << ""; + dispatch(*n.container); + o << ""; + sync_to(*n.predicate); + o << ""; + dispatch(*n.predicate); + o << ""; + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_negative(const Negative &n) { visit_uexpr("negative", n); } diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h index 4ddef884..e5887f15 100644 --- a/murphi2xml/src/XMLPrinter.h +++ b/murphi2xml/src/XMLPrinter.h @@ -56,6 +56,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal { void visit_mul(const rumur::Mul &n) final; void visit_multiset(const rumur::Multiset &n) final; void visit_multisetadd(const rumur::MultisetAdd &n) final; + void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/rumur/src/check.cc b/rumur/src/check.cc index de87847d..2505e1d5 100644 --- a/rumur/src/check.cc +++ b/rumur/src/check.cc @@ -20,6 +20,10 @@ class Check : public ConstTraversal { throw Error("multiset types are not supported", n.loc); } + void visit_multisetcount(const MultisetCount &n) final { + throw Error("multiset types 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 e78fa04c..ea8633ef 100644 --- a/rumur/src/generate-expr.cc +++ b/rumur/src/generate-expr.cc @@ -512,6 +512,11 @@ class Generator : public ConstExprTraversal { << ", s, " << *n.lhs << ", " << *n.rhs << ")"; } + void visit_multisetcount(const MultisetCount &) final { + assert(!"multisetcount not rejected before code generation"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { if (lvalue) invalid(n); diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc index 2f362283..b2149fca 100644 --- a/rumur/src/smt/simplify.cc +++ b/rumur/src/smt/simplify.cc @@ -234,6 +234,25 @@ class Simplifier : public BaseTraversal { simplify(n.arg1); } + void visit_multisetcount(MultisetCount &n) final { + dispatch(*n.container); + simplify(n.container); + + solver->open_scope(); + + const Ptr c = n.container->type()->resolve(); + auto m = dynamic_cast(c.get()); + if (m == nullptr) + throw Error("multisetcount container is not a multiset", + n.container->loc); + const Scalarset s{m->index_bound, n.loc}; + declare_var(n.identifier, n.unique_id, s); + + dispatch(*n.predicate); + simplify(n.predicate); + solver->close_scope(); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } void visit_not(Not &n) final { visit_uexpr(n); } diff --git a/rumur/src/smt/translate.cc b/rumur/src/smt/translate.cc index 42412d90..b16f8651 100644 --- a/rumur/src/smt/translate.cc +++ b/rumur/src/smt/translate.cc @@ -128,6 +128,10 @@ class Translator : public ConstExprTraversal { *this << "(" << mul() << " " << *n.lhs << " " << *n.rhs << ")"; } + void visit_multisetcount(const MultisetCount &n) final { + throw Unsupported(n); + } + void visit_negative(const Negative &n) final { *this << "(" << neg() << " " << *n.rhs << ")"; } From c12c449c53600e8de09fb40459f67590d8399990 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 08/21] support 'MultisetCount' during lexing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- 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 140a7356..7145ec18 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -101,6 +101,7 @@ isundefined { return rumur::parser::token::ISUNDEFINED; } liveness { return rumur::parser::token::LIVENESS; } multiset { return rumur::parser::token::MULTISET; } multisetadd { return rumur::parser::token::MULTISETADD; } +multisetcount { return rumur::parser::token::MULTISETCOUNT; } of { return rumur::parser::token::OF; } procedure { return rumur::parser::token::PROCEDURE; } put { return rumur::parser::token::PUT; } diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index c0646b63..2129318d 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -163,6 +163,7 @@ %token LSH "<<" %token MULTISET %token MULTISETADD +%token MULTISETCOUNT %token NEQ "!=" %token NUMBER %token OF From ba7239c495f448f60977c6059af2f14d16fb509a Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 09/21] support 'MultisetCount' during parsing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- doc/vs-cmurphi.rst | 4 ++-- librumur/src/parser.yy | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst index d030c6f1..6006d780 100644 --- a/doc/vs-cmurphi.rst +++ b/doc/vs-cmurphi.rst @@ -49,8 +49,8 @@ models with multiset types, e.g. ``murphi2uclid``. CMurphi requires the index of multiset to be a scalarset bound. Rumur supports any constant expression as a bound. -This limitation of syntax-only support applies also to the multiset construct -``MultisetAdd``. +This limitation of syntax-only support applies also to the multiset constructs +``MultisetAdd`` and ``MultisetCount``. Unions ^^^^^^ diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 2129318d..f89e244e 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -444,6 +444,8 @@ expr: expr '?' expr ':' expr { $$ = rumur::Ptr::make($3, $5, @$); } | ISUNDEFINED '(' designator ')' { $$ = rumur::Ptr::make($3, @$); +} | MULTISETCOUNT '(' ID ':' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, $7, @$); }; exprdecl: id_list_opt ':' expr { From 8eb2b08949f5c2c97ee3dc5f22594c5ffbd1fc39 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 10/21] API BREAK: preliminary support for 'Choose' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/include/rumur/Rule.h | 16 ++++++++++ librumur/include/rumur/indexer.h | 1 + librumur/include/rumur/traverse.h | 7 +++++ librumur/src/Model.cc | 21 +++++++++++++ librumur/src/Rule.cc | 39 +++++++++++++++++++++++++ librumur/src/indexer.cc | 7 +++++ librumur/src/resolve-symbols.cc | 21 +++++++++++++ librumur/src/sanitise_rule_names.cc | 6 ++++ librumur/src/traverse.cc | 30 +++++++++++++++++++ librumur/src/validate.cc | 6 ++++ misc/murphi2xml.rng | 18 ++++++++++++ murphi-format/src/format.c | 8 +++++ murphi2c/src/CLikeGenerator.cc | 5 ++++ murphi2c/src/CLikeGenerator.h | 1 + murphi2c/src/check.cc | 7 +++++ murphi2murphi/src/ExplicitSemicolons.cc | 4 +++ murphi2murphi/src/ExplicitSemicolons.h | 1 + murphi2murphi/src/Printer.cc | 11 +++++++ murphi2murphi/src/Printer.h | 1 + murphi2murphi/src/Stage.cc | 1 + murphi2murphi/src/Stage.h | 1 + murphi2smv/src/codegen.cc | 5 ++++ murphi2uclid/src/check.cc | 4 +++ murphi2uclid/src/codegen.cc | 5 ++++ murphi2xml/src/XMLPrinter.cc | 20 +++++++++++++ murphi2xml/src/XMLPrinter.h | 1 + rumur/src/check.cc | 4 +++ rumur/src/smt/simplify.cc | 19 ++++++++++++ 28 files changed, 270 insertions(+) diff --git a/librumur/include/rumur/Rule.h b/librumur/include/rumur/Rule.h index a06b93ae..0f54e7f5 100644 --- a/librumur/include/rumur/Rule.h +++ b/librumur/include/rumur/Rule.h @@ -106,4 +106,20 @@ struct RUMUR_API_WITH_RTTI Ruleset : public Rule { std::vector> flatten() const override; }; +struct RUMUR_API_WITH_RTTI Choose : public Rule { + std::string identifier; + Ptr container; + std::vector> rules; + + Choose(const std::string &identifier_, const Ptr &container_, + const std::vector> &rules_, const location &loc_); + Choose *clone() const override; + void validate() const override; + + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; + + std::vector> flatten() const override; +}; + } // namespace rumur diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h index 21f74043..8f502da1 100644 --- a/librumur/include/rumur/indexer.h +++ b/librumur/include/rumur/indexer.h @@ -33,6 +33,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_band(Band &n) override; void visit_bnot(Bnot &n) override; void visit_bor(Bor &n) override; + void visit_choose(Choose &n) override; void visit_clear(Clear &n) override; void visit_constdecl(ConstDecl &n) override; void visit_div(Div &n) override; diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h index e06da814..491f7e36 100644 --- a/librumur/include/rumur/traverse.h +++ b/librumur/include/rumur/traverse.h @@ -79,6 +79,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_band(Band &n) = 0; virtual void visit_bnot(Bnot &n) = 0; virtual void visit_bor(Bor &n) = 0; + virtual void visit_choose(Choose &n) = 0; virtual void visit_clear(Clear &n) = 0; virtual void visit_constdecl(ConstDecl &n) = 0; virtual void visit_div(Div &n) = 0; @@ -170,6 +171,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_band(Band &n) override; void visit_bnot(Bnot &n) override; void visit_bor(Bor &n) override; + void visit_choose(Choose &n) override; void visit_clear(Clear &n) override; void visit_constdecl(ConstDecl &n) override; void visit_div(Div &n) override; @@ -253,6 +255,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_band(const Band &n) = 0; virtual void visit_bnot(const Bnot &n) = 0; virtual void visit_bor(const Bor &n) = 0; + virtual void visit_choose(const Choose &n) = 0; virtual void visit_clear(const Clear &n) = 0; virtual void visit_constdecl(const ConstDecl &n) = 0; virtual void visit_div(const Div &n) = 0; @@ -336,6 +339,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_band(const Band &n) override; void visit_bnot(const Bnot &n) override; void visit_bor(const Bor &n) override; + void visit_choose(const Choose &n) override; void visit_clear(const Clear &n) override; void visit_constdecl(const ConstDecl &n) override; void visit_div(const Div &n) override; @@ -417,6 +421,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal { void visit_aliasstmt(const AliasStmt &n) final; void visit_array(const Array &n) final; void visit_assignment(const Assignment &n) final; + void visit_choose(const Choose &n) final; void visit_clear(const Clear &n) final; void visit_constdecl(const ConstDecl &n) final; void visit_enum(const Enum &n) final; @@ -466,6 +471,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal { void visit_band(const Band &n) final; void visit_bnot(const Bnot &n) final; void visit_bor(const Bor &n) final; + void visit_choose(const Choose &n) final; void visit_constdecl(const ConstDecl &n) final; void visit_div(const Div &n) final; void visit_element(const Element &n) final; @@ -533,6 +539,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal { void visit_band(const Band &n) final; void visit_bnot(const Bnot &n) final; void visit_bor(const Bor &n) final; + void visit_choose(const Choose &n) final; void visit_clear(const Clear &n) final; void visit_constdecl(const ConstDecl &n) final; void visit_div(const Div &n) final; diff --git a/librumur/src/Model.cc b/librumur/src/Model.cc index 4bcee137..0886e2ff 100644 --- a/librumur/src/Model.cc +++ b/librumur/src/Model.cc @@ -66,6 +66,27 @@ mpz_class Model::liveness_count() const { mpz_class count = 0; mpz_class multiplier = 1; + void visit_choose(const Choose &n) final { + // adjust the multiplier for the number of copies of the contained rules + // we will eventually generate + const Ptr t = n.container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in choose rule is not a multiset", + n.container->loc); + const mpz_class bound = m->index_bound->constant_fold(); + if (bound > 0) + multiplier *= bound; + + // descend into our rule children + for (const Ptr &r : n.rules) + dispatch(*r); + + // undo the multiplier effect + if (bound > 0) + multiplier /= bound; + } + void visit_ruleset(const Ruleset &n) final { /* Adjust the multiplier for the number of copies of the contained rules * we will eventually generate. diff --git a/librumur/src/Rule.cc b/librumur/src/Rule.cc index af54ffc1..6bcb5f86 100644 --- a/librumur/src/Rule.cc +++ b/librumur/src/Rule.cc @@ -1,6 +1,8 @@ +#include "../../common/isa.h" #include "location.hh" #include #include +#include #include #include #include @@ -9,6 +11,7 @@ #include #include #include +#include #include #include #include @@ -162,4 +165,40 @@ std::vector> Ruleset::flatten() const { return rs; } +Choose::Choose(const std::string &identifier_, const Ptr &container_, + const std::vector> &rules_, const location &loc_) + : Rule("", loc_), identifier(identifier_), container(container_), + rules(rules_) {} + +Choose *Choose::clone() const { return new Choose(*this); } + +void Choose::validate() const { + const Ptr t = container->type()->resolve(); + if (!isa(t)) + throw Error("choose rule container is not a multiset", container->loc); +} + +void Choose::visit(BaseTraversal &visitor) { visitor.visit_choose(*this); } + +void Choose::visit(ConstBaseTraversal &visitor) const { + visitor.visit_choose(*this); +} + +std::vector> Choose::flatten() const { + const Ptr t = container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in choose rule is not a multiset", container->loc); + const mpz_class multiplier = m->index_bound->constant_fold(); + + std::vector> rs; + for (const Ptr &r : rules) { + for (Ptr &f : r->flatten()) { + for (mpz_class i = 0; i < multiplier; ++i) + rs.push_back(f); + } + } + return rs; +} + } // namespace rumur diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc index 4e46f4ca..7523740f 100644 --- a/librumur/src/indexer.cc +++ b/librumur/src/indexer.cc @@ -67,6 +67,13 @@ void Indexer::visit_bexpr(BinaryExpr &n) { dispatch(*n.rhs); } +void Indexer::visit_choose(Choose &n) { + n.unique_id = next++; + dispatch(*n.container); + for (Ptr &r : n.rules) + dispatch(*r); +} + void Indexer::visit_clear(Clear &n) { n.unique_id = next++; dispatch(*n.rhs); diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 92d4deba..45da8a83 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -124,6 +124,27 @@ class Resolver : public Traversal { void visit_bor(Bor &n) final { visit_bexpr(n); } + void visit_choose(Choose &n) final { + dispatch(*n.container); + + // register our quantified variable + symtab.open_scope(); + const Ptr t = n.container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container of choose rule is not a multiset", + n.container->loc); + const Ptr s = + Ptr::make(m->index_bound, n.container->loc); + VarDecl *const i = make(n.identifier, s, n.loc); + symtab.declare(n.identifier, i); + + for (Ptr &r : n.rules) + dispatch(*r); + + symtab.close_scope(); + } + void visit_clear(Clear &n) final { dispatch(*n.rhs); disambiguate(n.rhs); diff --git a/librumur/src/sanitise_rule_names.cc b/librumur/src/sanitise_rule_names.cc index 73b1d953..a76d9274 100644 --- a/librumur/src/sanitise_rule_names.cc +++ b/librumur/src/sanitise_rule_names.cc @@ -52,6 +52,12 @@ class RuleNamer : public Traversal { } } + void visit_choose(Choose &n) final { + name(n, "choose"); + for (Ptr &r : n.rules) + dispatch(*r); + } + void visit_propertyrule(PropertyRule &n) final { name(n, "property"); } void visit_ruleset(Ruleset &n) final { diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc index 3a4c5e16..c9388577 100644 --- a/librumur/src/traverse.cc +++ b/librumur/src/traverse.cc @@ -66,6 +66,12 @@ void Traversal::visit_bexpr(BinaryExpr &n) { dispatch(*n.rhs); } +void Traversal::visit_choose(Choose &n) { + dispatch(*n.container); + for (Ptr &r : n.rules) + dispatch(*r); +} + void Traversal::visit_clear(Clear &n) { dispatch(*n.rhs); } void Traversal::visit_constdecl(ConstDecl &n) { dispatch(*n.value); } @@ -360,6 +366,12 @@ void ConstTraversal::visit_bexpr(const BinaryExpr &n) { dispatch(*n.rhs); } +void ConstTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstTraversal::visit_clear(const Clear &n) { dispatch(*n.rhs); } void ConstTraversal::visit_constdecl(const ConstDecl &n) { dispatch(*n.value); } @@ -633,6 +645,12 @@ void ConstExprTraversal::visit_assignment(const Assignment &n) { dispatch(*n.rhs); } +void ConstExprTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstExprTraversal::visit_clear(const Clear &n) { dispatch(*n.rhs); } void ConstExprTraversal::visit_constdecl(const ConstDecl &n) { @@ -835,6 +853,12 @@ void ConstStmtTraversal::visit_bexpr(const BinaryExpr &n) { dispatch(*n.rhs); } +void ConstStmtTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstStmtTraversal::visit_constdecl(const ConstDecl &n) { dispatch(*n.value); } @@ -1076,6 +1100,12 @@ void ConstTypeTraversal::visit_bexpr(const BinaryExpr &n) { dispatch(*n.rhs); } +void ConstTypeTraversal::visit_choose(const Choose &n) { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); +} + void ConstTypeTraversal::visit_clear(const Clear &n) { dispatch(*n.rhs); } void ConstTypeTraversal::visit_constdecl(const ConstDecl &n) { diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc index 5363a2b7..e487e9f3 100644 --- a/librumur/src/validate.cc +++ b/librumur/src/validate.cc @@ -95,6 +95,12 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_choose(const Choose &n) final { + dispatch(*n.container); + for (const Ptr &r : n.rules) + dispatch(*r); + } + void visit_clear(const Clear &n) final { dispatch(*n.rhs); n.validate(); diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng index 5ce7f104..7f0a44e4 100644 --- a/misc/murphi2xml.rng +++ b/misc/murphi2xml.rng @@ -168,6 +168,22 @@ + + + + + + + + + + + + + + + + @@ -600,6 +616,7 @@ + @@ -866,6 +883,7 @@ + diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c index afe0216f..d3281d1d 100644 --- a/murphi-format/src/format.c +++ b/murphi-format/src/format.c @@ -232,6 +232,8 @@ static bool is_keyword(const char *text) { return true; if (streq(text, "case")) return true; + if (streq(text, "choose")) + return true; if (streq(text, "clear")) return true; if (streq(text, "const")) @@ -248,6 +250,8 @@ static bool is_keyword(const char *text) { return true; if (streq(text, "endalias")) return true; + if (streq(text, "endchoose")) + return true; if (streq(text, "endexists")) return true; if (streq(text, "endfor")) @@ -388,6 +392,8 @@ static bool is_block_starter(state_t st, const char *text) { return true; if (streq(text, "case")) return true; + if (streq(text, "choose")) + return true; if (streq(text, "const")) return true; if (streq(text, "invariant")) @@ -453,6 +459,8 @@ static bool is_dedenter(const char *text) { return true; if (streq(text, "endalias")) return true; + if (streq(text, "endchoose")) + return true; if (streq(text, "endexists")) return true; if (streq(text, "endfor")) diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index fbd80b26..7a7482bf 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -181,6 +181,11 @@ void CLikeGenerator::visit_bor(const Bor &n) { *this << "(" << *n.lhs << " | " << *n.rhs << ")"; } +void CLikeGenerator::visit_choose(const Choose &) { + assert(!"choose was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_clear(const Clear &n) { *this << indentation() << "memset(&" << *n.rhs << ", 0, sizeof(" << *n.rhs << "));"; diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h index 53481a5b..f8ba4749 100644 --- a/murphi2c/src/CLikeGenerator.h +++ b/murphi2c/src/CLikeGenerator.h @@ -47,6 +47,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_band(const rumur::Band &n) final; void visit_bnot(const rumur::Bnot &n) final; void visit_bor(const rumur::Bor &n) final; + void visit_choose(const rumur::Choose &n) final; void visit_clear(const rumur::Clear &n) final; void visit_div(const rumur::Div &n) final; void visit_element(const rumur::Element &n) final; diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index 51ce55d3..15e9d1a4 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_choose(const Choose &) final { + if (ok) { + std::cerr << "choose rules are not supported\n"; + ok = false; + } + } + void visit_ismember(const IsMember &) final { if (ok) { std::cerr << "ismember expressions are not supported\n"; diff --git a/murphi2murphi/src/ExplicitSemicolons.cc b/murphi2murphi/src/ExplicitSemicolons.cc index d146dc0f..4c699d89 100644 --- a/murphi2murphi/src/ExplicitSemicolons.cc +++ b/murphi2murphi/src/ExplicitSemicolons.cc @@ -63,6 +63,10 @@ void ExplicitSemicolons::visit_aliasrule(const AliasRule &n) { next.visit_aliasrule(n); set_pending_semi(); } +void ExplicitSemicolons::visit_choose(const Choose &n) { + next.visit_choose(n); + set_pending_semi(); +} void ExplicitSemicolons::visit_constdecl(const ConstDecl &n) { next.visit_constdecl(n); set_pending_semi(); diff --git a/murphi2murphi/src/ExplicitSemicolons.h b/murphi2murphi/src/ExplicitSemicolons.h index d069b65e..a23e9948 100644 --- a/murphi2murphi/src/ExplicitSemicolons.h +++ b/murphi2murphi/src/ExplicitSemicolons.h @@ -25,6 +25,7 @@ class ExplicitSemicolons : public IntermediateStage { // override visitors for all nodes that can have an omitted semicolon void visit_aliasrule(const rumur::AliasRule &n) final; + void visit_choose(const rumur::Choose &n) final; void visit_constdecl(const rumur::ConstDecl &n) final; void visit_function(const rumur::Function &n) final; void visit_propertyrule(const rumur::PropertyRule &n) final; diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc index de8b7874..31f89322 100644 --- a/murphi2murphi/src/Printer.cc +++ b/murphi2murphi/src/Printer.cc @@ -82,6 +82,17 @@ void Printer::visit_assignment(const Assignment &n) { top->sync_to(n.loc.end); } +void Printer::visit_choose(const Choose &n) { + top->sync_to(n); + top->sync_to(*n.container); + top->dispatch(*n.container); + for (const Ptr &r : n.rules) { + top->sync_to(*r); + top->dispatch(*r); + } + top->sync_to(n.loc.end); +} + void Printer::visit_clear(const Clear &n) { top->sync_to(n); top->sync_to(*n.rhs); diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h index 3e96ada7..c415e1ba 100644 --- a/murphi2murphi/src/Printer.h +++ b/murphi2murphi/src/Printer.h @@ -28,6 +28,7 @@ class Printer : public Stage { void visit_band(const rumur::Band &n) final; void visit_bnot(const rumur::Bnot &n) final; void visit_bor(const rumur::Bor &n) final; + void visit_choose(const rumur::Choose &n) final; void visit_clear(const rumur::Clear &n) final; void visit_constdecl(const rumur::ConstDecl &n) final; void visit_div(const rumur::Div &n) final; diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc index 0b944a2d..b04a16c8 100644 --- a/murphi2murphi/src/Stage.cc +++ b/murphi2murphi/src/Stage.cc @@ -87,6 +87,7 @@ void IntermediateStage::visit_assignment(const Assignment &n) { void IntermediateStage::visit_band(const Band &n) { next.visit_band(n); } void IntermediateStage::visit_bnot(const Bnot &n) { next.visit_bnot(n); } void IntermediateStage::visit_bor(const Bor &n) { next.visit_bor(n); } +void IntermediateStage::visit_choose(const Choose &n) { next.visit_choose(n); } void IntermediateStage::visit_clear(const Clear &n) { next.visit_clear(n); } void IntermediateStage::visit_constdecl(const ConstDecl &n) { next.visit_constdecl(n); diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h index 2e41bf1f..93bc1bd3 100644 --- a/murphi2murphi/src/Stage.h +++ b/murphi2murphi/src/Stage.h @@ -70,6 +70,7 @@ class IntermediateStage : public Stage { void visit_band(const rumur::Band &n) override; void visit_bnot(const rumur::Bnot &n) override; void visit_bor(const rumur::Bor &n) override; + void visit_choose(const rumur::Choose &n) override; void visit_clear(const rumur::Clear &n) override; void visit_constdecl(const rumur::ConstDecl &n) override; void visit_div(const rumur::Div &n) override; diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc index c67f3be0..59bae550 100644 --- a/murphi2smv/src/codegen.cc +++ b/murphi2smv/src/codegen.cc @@ -109,6 +109,11 @@ class Printer : public ConstBaseTraversal { *this << '(' << *n.lhs << " | " << *n.rhs << ')'; } + void visit_choose(const Choose &) final { + *this << tab() + << "/-- FIXME: Murphi choose rules have no equivalent in SMV --/\n"; + } + void visit_clear(const Clear &) final { *this << tab() diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc index 4dd89614..859fcea4 100644 --- a/murphi2uclid/src/check.cc +++ b/murphi2uclid/src/check.cc @@ -32,6 +32,10 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of alias statements", n.loc); } + void visit_choose(const Choose &n) final { + throw Error("Uclid5 has no equivalent of choose rules", n.loc); + } + void visit_clear(const Clear &n) final { const Ptr type = n.rhs->type(); diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc index 20a048db..c6014bb3 100644 --- a/murphi2uclid/src/codegen.cc +++ b/murphi2uclid/src/codegen.cc @@ -114,6 +114,11 @@ class Printer : public ConstBaseTraversal { *this << "(" << *n.lhs << " | " << *n.rhs << ")"; } + void visit_choose(const Choose &) final { + assert(!"choose rule not rejected during check()"); + __builtin_unreachable(); + } + void visit_clear(const Clear &n) final { const Ptr type = n.rhs->type()->resolve(); diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc index ccb95753..4cc0bc5f 100644 --- a/murphi2xml/src/XMLPrinter.cc +++ b/murphi2xml/src/XMLPrinter.cc @@ -156,6 +156,26 @@ void XMLPrinter::visit_bnot(const Bnot &n) { visit_uexpr("bnot", n); } void XMLPrinter::visit_bor(const Bor &n) { visit_bexpr("bor", n); } +void XMLPrinter::visit_choose(const Choose &n) { + sync_to(n); + o << "'; + sync_to(*n.container); + dispatch(*n.container); + if (!n.rules.empty()) { + sync_to(*n.rules[0]); + o << ""; + for (const Ptr &r : n.rules) { + sync_to(*r); + dispatch(*r); + } + o << ""; + } + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_clear(const Clear &n) { sync_to(n); o << "open_scope(); + const Ptr t = n.container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in choose rule is not a multiset", + n.container->loc); + const Scalarset s{m->index_bound, n.container->loc}; + declare_var(n.identifier, n.unique_id, s); + + for (Ptr &r : n.rules) + dispatch(*r); + + solver->close_scope(); + } + void visit_clear(Clear &n) final { dispatch(*n.rhs); From 1076e5f55a0e164824a4e1c23f0ad0fd33528dd1 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 11/21] support 'choose' during lexing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/src/lexer.l | 2 ++ librumur/src/parser.yy | 2 ++ 2 files changed, 4 insertions(+) diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l index 7145ec18..8e279ed0 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -68,6 +68,7 @@ begin { return rumur::parser::token::BEGIN_TOK; } boolean { return rumur::parser::token::BOOLEAN; } by { return rumur::parser::token::BY; } case { return rumur::parser::token::CASE; } +choose { return rumur::parser::token::CHOOSE; } clear { return rumur::parser::token::CLEAR; } const { return rumur::parser::token::CONST; } cover { return rumur::parser::token::COVER; } @@ -76,6 +77,7 @@ else { return rumur::parser::token::ELSE; } elsif { return rumur::parser::token::ELSIF; } end { return rumur::parser::token::END; } endalias { return rumur::parser::token::ENDALIAS; } +endchoose { return rumur::parser::token::ENDCHOOSE; } endexists { return rumur::parser::token::ENDEXISTS; } endfor { return rumur::parser::token::ENDFOR; } endforall { return rumur::parser::token::ENDFORALL; } diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index f89e244e..2675b2d8 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -120,6 +120,7 @@ %token BOOLEAN %token BY %token CASE +%token CHOOSE %token CLEAR %token COLON_EQ ":=" %token CONST @@ -131,6 +132,7 @@ %token ELSIF %token END %token ENDALIAS +%token ENDCHOOSE %token ENDEXISTS %token ENDFOR %token ENDFORALL From d1cfbdd8a8b1cf96e9f265bcc4061b2ecb26205f Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 12/21] support 'choose' during parsing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- doc/vs-cmurphi.rst | 2 +- librumur/src/parser.yy | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst index 6006d780..045a2187 100644 --- a/doc/vs-cmurphi.rst +++ b/doc/vs-cmurphi.rst @@ -50,7 +50,7 @@ CMurphi requires the index of multiset to be a scalarset bound. Rumur supports any constant expression as a bound. This limitation of syntax-only support applies also to the multiset constructs -``MultisetAdd`` and ``MultisetCount``. +``Choose``, ``MultisetAdd``, and ``MultisetCount``. Unions ^^^^^^ diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 2675b2d8..a6ae5a11 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -211,6 +211,7 @@ %type > aliasrule %type > category +%type > choose %type >> decl %type >> decls %type >> decls_header @@ -312,6 +313,10 @@ category: ASSERT { $$ = std::make_shared(rumur::Property::LIVENESS); }; +choose: CHOOSE ID ':' expr DO rules endchoose { + $$ = rumur::Ptr::make($2, $4, $6, @$); +}; + comma_opt: ',' | %empty; decl: CONST exprdecls { @@ -356,6 +361,7 @@ elsifs: elsifs ELSIF expr THEN stmts { }; endalias: END | ENDALIAS; +endchoose: END | ENDCHOOSE; endexists: END | ENDEXISTS; endfor: END | ENDFOR; endforall: END | ENDFORALL; @@ -555,6 +561,8 @@ rule: startstate { $$ = $1; } | aliasrule { $$ = $1; +} | choose { + $$ = $1; }; rules: rules rule semi_opt { From d70d11730bd472b36f96fc6539a4a05b2c881fd4 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 13/21] API BREAK: preliminary support for 'MultisetRemove' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/include/rumur/Stmt.h | 12 ++++++++++++ librumur/include/rumur/indexer.h | 1 + librumur/include/rumur/traverse.h | 6 ++++++ librumur/src/Function.cc | 6 ++++++ librumur/src/Stmt.cc | 29 +++++++++++++++++++++++++++++ librumur/src/indexer.cc | 6 ++++++ librumur/src/resolve-symbols.cc | 7 +++++++ librumur/src/traverse.cc | 20 ++++++++++++++++++++ librumur/src/validate.cc | 6 ++++++ misc/murphi2xml.rng | 12 ++++++++++++ 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-stmt.cc | 5 +++++ rumur/src/smt/simplify.cc | 7 +++++++ 26 files changed, 184 insertions(+) diff --git a/librumur/include/rumur/Stmt.h b/librumur/include/rumur/Stmt.h index cf48f564..14659bae 100644 --- a/librumur/include/rumur/Stmt.h +++ b/librumur/include/rumur/Stmt.h @@ -142,6 +142,18 @@ struct RUMUR_API_WITH_RTTI MultisetAdd : public Stmt { void visit(ConstBaseTraversal &visitor) const override; }; +struct RUMUR_API_WITH_RTTI MultisetRemove : public Stmt { + Ptr arg0; + Ptr arg1; + + MultisetRemove(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_); + MultisetRemove *clone() const override; + void validate() const override; + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; +}; + struct RUMUR_API_WITH_RTTI ProcedureCall : public Stmt { FunctionCall call; diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h index 8f502da1..56bb578b 100644 --- a/librumur/include/rumur/indexer.h +++ b/librumur/include/rumur/indexer.h @@ -64,6 +64,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_multiset(Multiset &n) override; void visit_multisetadd(MultisetAdd &n) override; void visit_multisetcount(MultisetCount &n) override; + void visit_multisetremove(MultisetRemove &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h index 491f7e36..e18edeb3 100644 --- a/librumur/include/rumur/traverse.h +++ b/librumur/include/rumur/traverse.h @@ -110,6 +110,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_multiset(Multiset &n) = 0; virtual void visit_multisetadd(MultisetAdd &n) = 0; virtual void visit_multisetcount(MultisetCount &n) = 0; + virtual void visit_multisetremove(MultisetRemove &n) = 0; virtual void visit_negative(Negative &n) = 0; virtual void visit_neq(Neq &n) = 0; virtual void visit_not(Not &n) = 0; @@ -202,6 +203,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_multiset(Multiset &n) override; void visit_multisetadd(MultisetAdd &n) override; void visit_multisetcount(MultisetCount &n) override; + void visit_multisetremove(MultisetRemove &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; @@ -286,6 +288,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_multiset(const Multiset &n) = 0; virtual void visit_multisetadd(const MultisetAdd &n) = 0; virtual void visit_multisetcount(const MultisetCount &n) = 0; + virtual void visit_multisetremove(const MultisetRemove &n) = 0; virtual void visit_negative(const Negative &n) = 0; virtual void visit_neq(const Neq &n) = 0; virtual void visit_not(const Not &n) = 0; @@ -370,6 +373,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_multiset(const Multiset &n) override; void visit_multisetadd(const MultisetAdd &n) override; void visit_multisetcount(const MultisetCount &n) override; + void visit_multisetremove(const MultisetRemove &n) override; void visit_negative(const Negative &n) override; void visit_neq(const Neq &n) override; void visit_not(const Not &n) override; @@ -433,6 +437,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal { void visit_model(const Model &n) final; void visit_multiset(const Multiset &n) final; void visit_multisetadd(const MultisetAdd &n) final; + void visit_multisetremove(const MultisetRemove &n) override; void visit_procedurecall(const ProcedureCall &n) final; void visit_property(const Property &n) final; void visit_propertyrule(const PropertyRule &n) final; @@ -568,6 +573,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal { void visit_mul(const Mul &n) final; void visit_multisetadd(const MultisetAdd &n) final; void visit_multisetcount(const MultisetCount &n) final; + void visit_multisetremove(const MultisetRemove &n) override; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; diff --git a/librumur/src/Function.cc b/librumur/src/Function.cc index d75ecac7..a69ada47 100644 --- a/librumur/src/Function.cc +++ b/librumur/src/Function.cc @@ -147,6 +147,12 @@ bool Function::is_pure() const { pure &= !is_global_ref(*n.arg1); } + void visit_multisetremove(const MultisetRemove &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + pure &= !is_global_ref(*n.arg1); + } + void visit_propertystmt(const PropertyStmt &) final { // treat any property statement as a side effect pure = false; diff --git a/librumur/src/Stmt.cc b/librumur/src/Stmt.cc index e8b21ee2..b898b1f7 100644 --- a/librumur/src/Stmt.cc +++ b/librumur/src/Stmt.cc @@ -179,6 +179,35 @@ void MultisetAdd::visit(ConstBaseTraversal &visitor) const { visitor.visit_multisetadd(*this); } +MultisetRemove::MultisetRemove(const Ptr &arg0_, const Ptr &arg1_, + const location &loc_) + : Stmt(loc_), arg0(arg0_), arg1(arg1_) {} + +MultisetRemove *MultisetRemove::clone() const { + return new MultisetRemove(*this); +} + +void MultisetRemove::validate() const { + const Ptr t1 = arg1->type()->resolve(); + auto m = dynamic_cast(t1.get()); + if (m == nullptr) + throw Error("second argument to MultisetRemove is not a multiset", + arg1->loc); + + const Scalarset s{m->index_bound, m->index_bound->loc}; + + if (!arg0->type()->coerces_to(s)) + throw Error("incompatible MultisetRemove arguments", loc); +} + +void MultisetRemove::visit(BaseTraversal &visitor) { + visitor.visit_multisetremove(*this); +} + +void MultisetRemove::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetremove(*this); +} + ProcedureCall::ProcedureCall(const std::string &name, const std::vector> &arguments, const location &loc_) diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc index 7523740f..8d07eb41 100644 --- a/librumur/src/indexer.cc +++ b/librumur/src/indexer.cc @@ -210,6 +210,12 @@ void Indexer::visit_multisetcount(MultisetCount &n) { dispatch(*n.predicate); } +void Indexer::visit_multisetremove(MultisetRemove &n) { + n.unique_id = next++; + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void Indexer::visit_negative(Negative &n) { visit_uexpr(n); } void Indexer::visit_neq(Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 45da8a83..618a5a5e 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -380,6 +380,13 @@ class Resolver : public Traversal { disambiguate(n.predicate); } + void visit_multisetremove(MultisetRemove &n) final { + dispatch(*n.arg0); + disambiguate(n.arg0); + dispatch(*n.arg1); + disambiguate(n.arg1); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc index c9388577..44c70138 100644 --- a/librumur/src/traverse.cc +++ b/librumur/src/traverse.cc @@ -180,6 +180,11 @@ void Traversal::visit_multisetcount(MultisetCount &n) { dispatch(*n.predicate); } +void Traversal::visit_multisetremove(MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void Traversal::visit_negative(Negative &n) { visit_uexpr(n); } void Traversal::visit_neq(Neq &n) { visit_bexpr(n); } @@ -480,6 +485,11 @@ void ConstTraversal::visit_multisetcount(const MultisetCount &n) { dispatch(*n.predicate); } +void ConstTraversal::visit_multisetremove(const MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void ConstTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -705,6 +715,11 @@ void ConstExprTraversal::visit_multisetadd(const MultisetAdd &n) { dispatch(*n.arg1); } +void ConstExprTraversal::visit_multisetremove(const MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void ConstExprTraversal::visit_procedurecall(const ProcedureCall &n) { dispatch(n.call); } @@ -1213,6 +1228,11 @@ void ConstTypeTraversal::visit_multisetcount(const MultisetCount &n) { dispatch(*n.predicate); } +void ConstTypeTraversal::visit_multisetremove(const MultisetRemove &n) { + dispatch(*n.arg0); + dispatch(*n.arg1); +} + void ConstTypeTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTypeTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc index e487e9f3..ec2d8706 100644 --- a/librumur/src/validate.cc +++ b/librumur/src/validate.cc @@ -278,6 +278,12 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_multisetremove(const MultisetRemove &n) final { + dispatch(*n.arg0); + dispatch(*n.arg1); + n.validate(); + } + void visit_negative(const Negative &n) final { dispatch(*n.rhs); n.validate(); diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng index 7f0a44e4..22836ab8 100644 --- a/misc/murphi2xml.rng +++ b/misc/murphi2xml.rng @@ -670,6 +670,17 @@ + + + + + + + + + + + @@ -1049,6 +1060,7 @@ + diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c index d3281d1d..611e1d0c 100644 --- a/murphi-format/src/format.c +++ b/murphi-format/src/format.c @@ -312,6 +312,9 @@ static bool is_keyword(const char *text) { // `multisetcount` is a keyword, but is used as if it were a function if (streq(text, "multisetcount")) return true; + // `multisetremove` is a keyword, but is used as if it were a function + if (streq(text, "multisetremove")) + return true; #endif if (streq(text, "of")) return true; diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 7a7482bf..fff78c78 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -450,6 +450,11 @@ void CLikeGenerator::visit_multisetcount(const MultisetCount &) { __builtin_unreachable(); } +void CLikeGenerator::visit_multisetremove(const MultisetRemove &) { + assert(!"multisetremove was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_negative(const Negative &n) { *this << "(-" << *n.rhs << ")"; } diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h index f8ba4749..e3112f15 100644 --- a/murphi2c/src/CLikeGenerator.h +++ b/murphi2c/src/CLikeGenerator.h @@ -76,6 +76,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_multiset(const rumur::Multiset &n) final; void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_multisetcount(const rumur::MultisetCount &n) final; + void visit_multisetremove(const rumur::MultisetRemove &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index 15e9d1a4..0613ffdc 100644 --- a/murphi2c/src/check.cc +++ b/murphi2c/src/check.cc @@ -55,6 +55,13 @@ class Check : public ConstTraversal { } } + void visit_multisetremove(const MultisetRemove &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + void visit_union(const Union &) final { if (ok) { std::cerr << "union types are not supported\n"; diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc index 31f89322..28f2767d 100644 --- a/murphi2murphi/src/Printer.cc +++ b/murphi2murphi/src/Printer.cc @@ -307,6 +307,15 @@ void Printer::visit_multisetcount(const MultisetCount &n) { top->sync_to(n.loc.end); } +void Printer::visit_multisetremove(const MultisetRemove &n) { + top->sync_to(n); + top->sync_to(*n.arg0); + top->dispatch(*n.arg0); + top->sync_to(*n.arg1); + top->dispatch(*n.arg1); + top->sync_to(n.loc.end); +} + void Printer::visit_negative(const Negative &n) { visit_uexpr(n); } void Printer::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h index c415e1ba..fdb66756 100644 --- a/murphi2murphi/src/Printer.h +++ b/murphi2murphi/src/Printer.h @@ -58,6 +58,7 @@ class Printer : public Stage { void visit_mul(const rumur::Mul &n) final; void visit_multiset(const rumur::Multiset &n) final; void visit_multisetadd(const rumur::MultisetAdd &n) final; + void visit_multisetremove(const rumur::MultisetRemove &n) final; void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc index b04a16c8..23261bcc 100644 --- a/murphi2murphi/src/Stage.cc +++ b/murphi2murphi/src/Stage.cc @@ -142,6 +142,9 @@ void IntermediateStage::visit_multisetadd(const MultisetAdd &n) { void IntermediateStage::visit_multisetcount(const MultisetCount &n) { next.visit_multisetcount(n); } +void IntermediateStage::visit_multisetremove(const MultisetRemove &n) { + next.visit_multisetremove(n); +} void IntermediateStage::visit_negative(const Negative &n) { next.visit_negative(n); } diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h index 93bc1bd3..aaa38600 100644 --- a/murphi2murphi/src/Stage.h +++ b/murphi2murphi/src/Stage.h @@ -101,6 +101,7 @@ class IntermediateStage : public Stage { void visit_multiset(const rumur::Multiset &n) override; void visit_multisetadd(const rumur::MultisetAdd &n) override; void visit_multisetcount(const rumur::MultisetCount &n) override; + void visit_multisetremove(const rumur::MultisetRemove &n) override; void visit_negative(const rumur::Negative &n) override; void visit_neq(const rumur::Neq &n) override; void visit_not(const rumur::Not &n) override; diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc index 59bae550..a0985de9 100644 --- a/murphi2smv/src/codegen.cc +++ b/murphi2smv/src/codegen.cc @@ -321,6 +321,12 @@ class Printer : public ConstBaseTraversal { << ')'; } + void visit_multisetremove(const MultisetRemove &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetRemove(" + << *n.arg0 << ", " << *n.arg1 << ')'; + } + void visit_negative(const Negative &n) final { *this << '-' << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc index 859fcea4..2cd6470e 100644 --- a/murphi2uclid/src/check.cc +++ b/murphi2uclid/src/check.cc @@ -147,6 +147,10 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of the multiset type", n.loc); } + void visit_multisetremove(const MultisetRemove &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + void visit_propertyrule(const PropertyRule &n) final { if (n.property.category == Property::COVER) throw Error("cover properties have no LTL equivalent in Uclid5", n.loc); diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc index c6014bb3..69955b87 100644 --- a/murphi2uclid/src/codegen.cc +++ b/murphi2uclid/src/codegen.cc @@ -506,6 +506,11 @@ class Printer : public ConstBaseTraversal { __builtin_unreachable(); } + void visit_multisetremove(const MultisetRemove &) final { + assert(!"multisetremove not rejected during check()"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { *this << "-" << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc index 4cc0bc5f..1d61f572 100644 --- a/murphi2xml/src/XMLPrinter.cc +++ b/murphi2xml/src/XMLPrinter.cc @@ -532,6 +532,23 @@ void XMLPrinter::visit_multisetcount(const MultisetCount &n) { o << ""; } +void XMLPrinter::visit_multisetremove(const MultisetRemove &n) { + sync_to(n); + o << "'; + sync_to(*n.arg0); + o << ""; + dispatch(*n.arg0); + o << ""; + sync_to(*n.arg1); + o << ""; + dispatch(*n.arg1); + o << ""; + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_negative(const Negative &n) { visit_uexpr("negative", n); } diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h index 361c9b16..8636cfb8 100644 --- a/murphi2xml/src/XMLPrinter.h +++ b/murphi2xml/src/XMLPrinter.h @@ -58,6 +58,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal { void visit_multiset(const rumur::Multiset &n) final; void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_multisetcount(const rumur::MultisetCount &n) final; + void visit_multisetremove(const rumur::MultisetRemove &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/rumur/src/check.cc b/rumur/src/check.cc index db8b3f89..9bb1d987 100644 --- a/rumur/src/check.cc +++ b/rumur/src/check.cc @@ -28,6 +28,10 @@ class Check : public ConstTraversal { throw Error("multiset types are not supported", n.loc); } + void visit_multisetremove(const MultisetRemove &n) final { + throw Error("multiset types 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-stmt.cc b/rumur/src/generate-stmt.cc index e2aaab84..794d1e59 100644 --- a/rumur/src/generate-stmt.cc +++ b/rumur/src/generate-stmt.cc @@ -213,6 +213,11 @@ class Generator : public ConstStmtTraversal { __builtin_unreachable(); } + void visit_multisetremove(const MultisetRemove &) final { + assert(!"multisetremove not rejected during check()"); + __builtin_unreachable(); + } + void visit_procedurecall(const ProcedureCall &s) final { generate_rvalue(*out, s.call); } diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc index 9c0fd394..c8ee3593 100644 --- a/rumur/src/smt/simplify.cc +++ b/rumur/src/smt/simplify.cc @@ -272,6 +272,13 @@ class Simplifier : public BaseTraversal { solver->close_scope(); } + void visit_multisetremove(MultisetRemove &n) final { + dispatch(*n.arg0); + simplify(n.arg0); + dispatch(*n.arg1); + simplify(n.arg1); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } void visit_not(Not &n) final { visit_uexpr(n); } From 67127631f48b6f495d858bae6a52de4b0dcaf0ae Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 14/21] support 'multisetremove' during lexing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/src/lexer.l | 131 +++++++++++++++++++++-------------------- librumur/src/parser.yy | 1 + 2 files changed, 67 insertions(+), 65 deletions(-) diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l index 8e279ed0..4b03f4bd 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -60,71 +60,72 @@ throw rumur::Error("real types are not supported", *loc); } -alias { return rumur::parser::token::ALIAS; } -array { return rumur::parser::token::ARRAY; } -assert { return rumur::parser::token::ASSERT; } -assume { return rumur::parser::token::ASSUME; } -begin { return rumur::parser::token::BEGIN_TOK; } -boolean { return rumur::parser::token::BOOLEAN; } -by { return rumur::parser::token::BY; } -case { return rumur::parser::token::CASE; } -choose { return rumur::parser::token::CHOOSE; } -clear { return rumur::parser::token::CLEAR; } -const { return rumur::parser::token::CONST; } -cover { return rumur::parser::token::COVER; } -do { return rumur::parser::token::DO; } -else { return rumur::parser::token::ELSE; } -elsif { return rumur::parser::token::ELSIF; } -end { return rumur::parser::token::END; } -endalias { return rumur::parser::token::ENDALIAS; } -endchoose { return rumur::parser::token::ENDCHOOSE; } -endexists { return rumur::parser::token::ENDEXISTS; } -endfor { return rumur::parser::token::ENDFOR; } -endforall { return rumur::parser::token::ENDFORALL; } -endfunction { return rumur::parser::token::ENDFUNCTION; } -endif { return rumur::parser::token::ENDIF; } -endprocedure { return rumur::parser::token::ENDPROCEDURE; } -endrecord { return rumur::parser::token::ENDRECORD; } -endrule { return rumur::parser::token::ENDRULE; } -endruleset { return rumur::parser::token::ENDRULESET; } -endstartstate { return rumur::parser::token::ENDSTARTSTATE; } -endswitch { return rumur::parser::token::ENDSWITCH; } -endwhile { return rumur::parser::token::ENDWHILE; } -enum { return rumur::parser::token::ENUM; } -error { return rumur::parser::token::ERROR; } -exists { return rumur::parser::token::EXISTS; } -for { return rumur::parser::token::FOR; } -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; } -multiset { return rumur::parser::token::MULTISET; } -multisetadd { return rumur::parser::token::MULTISETADD; } -multisetcount { return rumur::parser::token::MULTISETCOUNT; } -of { return rumur::parser::token::OF; } -procedure { return rumur::parser::token::PROCEDURE; } -put { return rumur::parser::token::PUT; } -real { throw rumur::Error("real types are not supported", *loc); } -record { return rumur::parser::token::RECORD; } -return { return rumur::parser::token::RETURN; } -rule { return rumur::parser::token::RULE; } -ruleset { return rumur::parser::token::RULESET; } -scalarset { return rumur::parser::token::SCALARSET; } -startstate { return rumur::parser::token::STARTSTATE; } -switch { return rumur::parser::token::SWITCH; } -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 { return rumur::parser::token::UNION; } -var { return rumur::parser::token::VAR; } -while { return rumur::parser::token::WHILE; } - -"∀" { return rumur::parser::token::FORALL; } -"∃" { return rumur::parser::token::EXISTS; } +alias { return rumur::parser::token::ALIAS; } +array { return rumur::parser::token::ARRAY; } +assert { return rumur::parser::token::ASSERT; } +assume { return rumur::parser::token::ASSUME; } +begin { return rumur::parser::token::BEGIN_TOK; } +boolean { return rumur::parser::token::BOOLEAN; } +by { return rumur::parser::token::BY; } +case { return rumur::parser::token::CASE; } +choose { return rumur::parser::token::CHOOSE; } +clear { return rumur::parser::token::CLEAR; } +const { return rumur::parser::token::CONST; } +cover { return rumur::parser::token::COVER; } +do { return rumur::parser::token::DO; } +else { return rumur::parser::token::ELSE; } +elsif { return rumur::parser::token::ELSIF; } +end { return rumur::parser::token::END; } +endalias { return rumur::parser::token::ENDALIAS; } +endchoose { return rumur::parser::token::ENDCHOOSE; } +endexists { return rumur::parser::token::ENDEXISTS; } +endfor { return rumur::parser::token::ENDFOR; } +endforall { return rumur::parser::token::ENDFORALL; } +endfunction { return rumur::parser::token::ENDFUNCTION; } +endif { return rumur::parser::token::ENDIF; } +endprocedure { return rumur::parser::token::ENDPROCEDURE; } +endrecord { return rumur::parser::token::ENDRECORD; } +endrule { return rumur::parser::token::ENDRULE; } +endruleset { return rumur::parser::token::ENDRULESET; } +endstartstate { return rumur::parser::token::ENDSTARTSTATE; } +endswitch { return rumur::parser::token::ENDSWITCH; } +endwhile { return rumur::parser::token::ENDWHILE; } +enum { return rumur::parser::token::ENUM; } +error { return rumur::parser::token::ERROR; } +exists { return rumur::parser::token::EXISTS; } +for { return rumur::parser::token::FOR; } +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; } +multiset { return rumur::parser::token::MULTISET; } +multisetadd { return rumur::parser::token::MULTISETADD; } +multisetcount { return rumur::parser::token::MULTISETCOUNT; } +multisetremove { return rumur::parser::token::MULTISETREMOVE; } +of { return rumur::parser::token::OF; } +procedure { return rumur::parser::token::PROCEDURE; } +put { return rumur::parser::token::PUT; } +real { throw rumur::Error("real types are not supported", *loc); } +record { return rumur::parser::token::RECORD; } +return { return rumur::parser::token::RETURN; } +rule { return rumur::parser::token::RULE; } +ruleset { return rumur::parser::token::RULESET; } +scalarset { return rumur::parser::token::SCALARSET; } +startstate { return rumur::parser::token::STARTSTATE; } +switch { return rumur::parser::token::SWITCH; } +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 { return rumur::parser::token::UNION; } +var { return rumur::parser::token::VAR; } +while { return rumur::parser::token::WHILE; } + +"∀" { return rumur::parser::token::FORALL; } +"∃" { return rumur::parser::token::EXISTS; } /* Recognise true and false explicitly rather than as generic IDs (below). The * purpose of this is so that we match them case-insensitively. diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index a6ae5a11..6b018360 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -166,6 +166,7 @@ %token MULTISET %token MULTISETADD %token MULTISETCOUNT +%token MULTISETREMOVE %token NEQ "!=" %token NUMBER %token OF From e534adfddbfa43ee0d572a96a3aa718d8a7bfec2 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 15/21] support 'multisetremove' during parsing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- doc/vs-cmurphi.rst | 2 +- librumur/src/parser.yy | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst index 045a2187..5aaee30a 100644 --- a/doc/vs-cmurphi.rst +++ b/doc/vs-cmurphi.rst @@ -50,7 +50,7 @@ CMurphi requires the index of multiset to be a scalarset bound. Rumur supports any constant expression as a bound. This limitation of syntax-only support applies also to the multiset constructs -``Choose``, ``MultisetAdd``, and ``MultisetCount``. +``Choose``, ``MultisetAdd``, ``MultisetCount``, and ``MultisetRemove``. Unions ^^^^^^ diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 6b018360..edd4a719 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -616,6 +616,8 @@ stmt: category STRING expr { $$ = rumur::Ptr::make(cs, @$); } | MULTISETADD '(' expr ',' expr ')' { $$ = rumur::Ptr::make($3, $5, @$); +} | MULTISETREMOVE '(' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, @$); } | PUT STRING { $$ = rumur::Ptr::make($2, @$); } | PUT expr { From 745ce5eec26b43a123ba27e9f7403fd511022307 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 16/21] API BREAK: preliminary support for 'MultisetRemovePred' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/include/rumur/Stmt.h | 14 ++++++++++++++ librumur/include/rumur/indexer.h | 1 + librumur/include/rumur/traverse.h | 6 ++++++ librumur/src/Function.cc | 6 ++++++ librumur/src/Stmt.cc | 31 +++++++++++++++++++++++++++++++ librumur/src/indexer.cc | 6 ++++++ librumur/src/resolve-symbols.cc | 21 +++++++++++++++++++++ librumur/src/traverse.cc | 20 ++++++++++++++++++++ librumur/src/validate.cc | 6 ++++++ misc/murphi2xml.rng | 15 +++++++++++++++ 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-stmt.cc | 5 +++++ rumur/src/smt/simplify.cc | 7 +++++++ 26 files changed, 205 insertions(+) diff --git a/librumur/include/rumur/Stmt.h b/librumur/include/rumur/Stmt.h index 14659bae..c22967c2 100644 --- a/librumur/include/rumur/Stmt.h +++ b/librumur/include/rumur/Stmt.h @@ -154,6 +154,20 @@ struct RUMUR_API_WITH_RTTI MultisetRemove : public Stmt { void visit(ConstBaseTraversal &visitor) const override; }; +struct RUMUR_API_WITH_RTTI MultisetRemovePred : public Stmt { + std::string identifier; + Ptr container; + Ptr predicate; + + MultisetRemovePred(const std::string &identifier_, + const Ptr &container_, const Ptr &predicate_, + const location &loc_); + MultisetRemovePred *clone() const override; + void validate() const override; + void visit(BaseTraversal &visitor) override; + void visit(ConstBaseTraversal &visitor) const override; +}; + struct RUMUR_API_WITH_RTTI ProcedureCall : public Stmt { FunctionCall call; diff --git a/librumur/include/rumur/indexer.h b/librumur/include/rumur/indexer.h index 56bb578b..d0fb3447 100644 --- a/librumur/include/rumur/indexer.h +++ b/librumur/include/rumur/indexer.h @@ -65,6 +65,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal { void visit_multisetadd(MultisetAdd &n) override; void visit_multisetcount(MultisetCount &n) override; void visit_multisetremove(MultisetRemove &n) override; + void visit_multisetremovepred(MultisetRemovePred &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; diff --git a/librumur/include/rumur/traverse.h b/librumur/include/rumur/traverse.h index e18edeb3..01272571 100644 --- a/librumur/include/rumur/traverse.h +++ b/librumur/include/rumur/traverse.h @@ -111,6 +111,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal { virtual void visit_multisetadd(MultisetAdd &n) = 0; virtual void visit_multisetcount(MultisetCount &n) = 0; virtual void visit_multisetremove(MultisetRemove &n) = 0; + virtual void visit_multisetremovepred(MultisetRemovePred &n) = 0; virtual void visit_negative(Negative &n) = 0; virtual void visit_neq(Neq &n) = 0; virtual void visit_not(Not &n) = 0; @@ -204,6 +205,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal { void visit_multisetadd(MultisetAdd &n) override; void visit_multisetcount(MultisetCount &n) override; void visit_multisetremove(MultisetRemove &n) override; + void visit_multisetremovepred(MultisetRemovePred &n) override; void visit_negative(Negative &n) override; void visit_neq(Neq &n) override; void visit_not(Not &n) override; @@ -289,6 +291,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal { virtual void visit_multisetadd(const MultisetAdd &n) = 0; virtual void visit_multisetcount(const MultisetCount &n) = 0; virtual void visit_multisetremove(const MultisetRemove &n) = 0; + virtual void visit_multisetremovepred(const MultisetRemovePred &n) = 0; virtual void visit_negative(const Negative &n) = 0; virtual void visit_neq(const Neq &n) = 0; virtual void visit_not(const Not &n) = 0; @@ -374,6 +377,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal { void visit_multisetadd(const MultisetAdd &n) override; void visit_multisetcount(const MultisetCount &n) override; void visit_multisetremove(const MultisetRemove &n) override; + void visit_multisetremovepred(const MultisetRemovePred &n) override; void visit_negative(const Negative &n) override; void visit_neq(const Neq &n) override; void visit_not(const Not &n) override; @@ -438,6 +442,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal { void visit_multiset(const Multiset &n) final; void visit_multisetadd(const MultisetAdd &n) final; void visit_multisetremove(const MultisetRemove &n) override; + void visit_multisetremovepred(const MultisetRemovePred &n) override; void visit_procedurecall(const ProcedureCall &n) final; void visit_property(const Property &n) final; void visit_propertyrule(const PropertyRule &n) final; @@ -574,6 +579,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal { void visit_multisetadd(const MultisetAdd &n) final; void visit_multisetcount(const MultisetCount &n) final; void visit_multisetremove(const MultisetRemove &n) override; + void visit_multisetremovepred(const MultisetRemovePred &n) override; void visit_negative(const Negative &n) final; void visit_neq(const Neq &n) final; void visit_not(const Not &n) final; diff --git a/librumur/src/Function.cc b/librumur/src/Function.cc index a69ada47..ae705e5f 100644 --- a/librumur/src/Function.cc +++ b/librumur/src/Function.cc @@ -153,6 +153,12 @@ bool Function::is_pure() const { pure &= !is_global_ref(*n.arg1); } + void visit_multisetremovepred(const MultisetRemovePred &n) final { + dispatch(*n.container); + dispatch(*n.predicate); + pure &= !is_global_ref(*n.container); + } + void visit_propertystmt(const PropertyStmt &) final { // treat any property statement as a side effect pure = false; diff --git a/librumur/src/Stmt.cc b/librumur/src/Stmt.cc index b898b1f7..4b6162f9 100644 --- a/librumur/src/Stmt.cc +++ b/librumur/src/Stmt.cc @@ -208,6 +208,37 @@ void MultisetRemove::visit(ConstBaseTraversal &visitor) const { visitor.visit_multisetremove(*this); } +MultisetRemovePred::MultisetRemovePred(const std::string &identifier_, + const Ptr &container_, + const Ptr &predicate_, + const location &loc_) + : Stmt(loc_), identifier(identifier_), container(container_), + predicate(predicate_) {} + +MultisetRemovePred *MultisetRemovePred::clone() const { + return new MultisetRemovePred(*this); +} + +void MultisetRemovePred::validate() const { + const Ptr t = container->type()->resolve(); + auto m = dynamic_cast(t.get()); + if (m == nullptr) + throw Error("container in MultisetRemovePred is not a multiset", + container->loc); + + if (!predicate->type()->resolve()->is_boolean()) + throw Error("MultisetRemovePred predicate is not a boolean expression", + predicate->loc); +} + +void MultisetRemovePred::visit(BaseTraversal &visitor) { + visitor.visit_multisetremovepred(*this); +} + +void MultisetRemovePred::visit(ConstBaseTraversal &visitor) const { + visitor.visit_multisetremovepred(*this); +} + ProcedureCall::ProcedureCall(const std::string &name, const std::vector> &arguments, const location &loc_) diff --git a/librumur/src/indexer.cc b/librumur/src/indexer.cc index 8d07eb41..9b871d67 100644 --- a/librumur/src/indexer.cc +++ b/librumur/src/indexer.cc @@ -216,6 +216,12 @@ void Indexer::visit_multisetremove(MultisetRemove &n) { dispatch(*n.arg1); } +void Indexer::visit_multisetremovepred(MultisetRemovePred &n) { + n.unique_id = next++; + dispatch(*n.container); + dispatch(*n.predicate); +} + void Indexer::visit_negative(Negative &n) { visit_uexpr(n); } void Indexer::visit_neq(Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 618a5a5e..1bc788a4 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -387,6 +387,27 @@ class Resolver : public Traversal { disambiguate(n.arg1); } + void visit_multisetremovepred(MultisetRemovePred &n) final { + dispatch(*n.container); + disambiguate(n.container); + + symtab.open_scope(); + + const Ptr id_type = n.container->type()->resolve(); + auto m = dynamic_cast(id_type.get()); + if (m == nullptr) + throw Error("multisetremovepred container is not a multiset", + n.container->loc); + const Ptr s = Ptr::make(m->index_bound, n.loc); + VarDecl *const i = make(n.identifier, s, n.loc); + symtab.declare(n.identifier, i); + + dispatch(*n.predicate); + symtab.close_scope(); + + disambiguate(n.predicate); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } diff --git a/librumur/src/traverse.cc b/librumur/src/traverse.cc index 44c70138..40f6ae48 100644 --- a/librumur/src/traverse.cc +++ b/librumur/src/traverse.cc @@ -185,6 +185,11 @@ void Traversal::visit_multisetremove(MultisetRemove &n) { dispatch(*n.arg1); } +void Traversal::visit_multisetremovepred(MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void Traversal::visit_negative(Negative &n) { visit_uexpr(n); } void Traversal::visit_neq(Neq &n) { visit_bexpr(n); } @@ -490,6 +495,11 @@ void ConstTraversal::visit_multisetremove(const MultisetRemove &n) { dispatch(*n.arg1); } +void ConstTraversal::visit_multisetremovepred(const MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } @@ -720,6 +730,11 @@ void ConstExprTraversal::visit_multisetremove(const MultisetRemove &n) { dispatch(*n.arg1); } +void ConstExprTraversal::visit_multisetremovepred(const MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstExprTraversal::visit_procedurecall(const ProcedureCall &n) { dispatch(n.call); } @@ -1233,6 +1248,11 @@ void ConstTypeTraversal::visit_multisetremove(const MultisetRemove &n) { dispatch(*n.arg1); } +void ConstTypeTraversal::visit_multisetremovepred(const MultisetRemovePred &n) { + dispatch(*n.container); + dispatch(*n.predicate); +} + void ConstTypeTraversal::visit_negative(const Negative &n) { visit_uexpr(n); } void ConstTypeTraversal::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/librumur/src/validate.cc b/librumur/src/validate.cc index ec2d8706..9f387946 100644 --- a/librumur/src/validate.cc +++ b/librumur/src/validate.cc @@ -284,6 +284,12 @@ class Validator : public ConstBaseTraversal { n.validate(); } + void visit_multisetremovepred(const MultisetRemovePred &n) final { + dispatch(*n.container); + dispatch(*n.predicate); + n.validate(); + } + void visit_negative(const Negative &n) final { dispatch(*n.rhs); n.validate(); diff --git a/misc/murphi2xml.rng b/misc/murphi2xml.rng index 22836ab8..42ac9e11 100644 --- a/misc/murphi2xml.rng +++ b/misc/murphi2xml.rng @@ -681,6 +681,20 @@ + + + + + + + + + + + + + + @@ -1061,6 +1075,7 @@ + diff --git a/murphi-format/src/format.c b/murphi-format/src/format.c index 611e1d0c..e3524b17 100644 --- a/murphi-format/src/format.c +++ b/murphi-format/src/format.c @@ -315,6 +315,9 @@ static bool is_keyword(const char *text) { // `multisetremove` is a keyword, but is used as if it were a function if (streq(text, "multisetremove")) return true; + // `multisetremovepred` is a keyword, but is used as if it were a function + if (streq(text, "multisetremovepred")) + return true; #endif if (streq(text, "of")) return true; diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index fff78c78..2e5c0f5a 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -455,6 +455,11 @@ void CLikeGenerator::visit_multisetremove(const MultisetRemove &) { __builtin_unreachable(); } +void CLikeGenerator::visit_multisetremovepred(const MultisetRemovePred &) { + assert(!"multisetremovepred was not rejected during check()"); + __builtin_unreachable(); +} + void CLikeGenerator::visit_negative(const Negative &n) { *this << "(-" << *n.rhs << ")"; } diff --git a/murphi2c/src/CLikeGenerator.h b/murphi2c/src/CLikeGenerator.h index e3112f15..4470c02d 100644 --- a/murphi2c/src/CLikeGenerator.h +++ b/murphi2c/src/CLikeGenerator.h @@ -77,6 +77,7 @@ class __attribute__((visibility("hidden"))) CLikeGenerator void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_multisetremove(const rumur::MultisetRemove &n) final; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index 0613ffdc..f7231a86 100644 --- a/murphi2c/src/check.cc +++ b/murphi2c/src/check.cc @@ -62,6 +62,13 @@ class Check : public ConstTraversal { } } + void visit_multisetremovepred(const MultisetRemovePred &) final { + if (ok) { + std::cerr << "multiset types are not supported\n"; + ok = false; + } + } + void visit_union(const Union &) final { if (ok) { std::cerr << "union types are not supported\n"; diff --git a/murphi2murphi/src/Printer.cc b/murphi2murphi/src/Printer.cc index 28f2767d..e7ec8ac9 100644 --- a/murphi2murphi/src/Printer.cc +++ b/murphi2murphi/src/Printer.cc @@ -316,6 +316,15 @@ void Printer::visit_multisetremove(const MultisetRemove &n) { top->sync_to(n.loc.end); } +void Printer::visit_multisetremovepred(const MultisetRemovePred &n) { + top->sync_to(n); + top->sync_to(*n.container); + top->dispatch(*n.container); + top->sync_to(*n.predicate); + top->dispatch(*n.predicate); + top->sync_to(n.loc.end); +} + void Printer::visit_negative(const Negative &n) { visit_uexpr(n); } void Printer::visit_neq(const Neq &n) { visit_bexpr(n); } diff --git a/murphi2murphi/src/Printer.h b/murphi2murphi/src/Printer.h index fdb66756..9a428531 100644 --- a/murphi2murphi/src/Printer.h +++ b/murphi2murphi/src/Printer.h @@ -59,6 +59,7 @@ class Printer : public Stage { void visit_multiset(const rumur::Multiset &n) final; void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_multisetremove(const rumur::MultisetRemove &n) final; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) final; void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; diff --git a/murphi2murphi/src/Stage.cc b/murphi2murphi/src/Stage.cc index 23261bcc..9ff638a7 100644 --- a/murphi2murphi/src/Stage.cc +++ b/murphi2murphi/src/Stage.cc @@ -145,6 +145,9 @@ void IntermediateStage::visit_multisetcount(const MultisetCount &n) { void IntermediateStage::visit_multisetremove(const MultisetRemove &n) { next.visit_multisetremove(n); } +void IntermediateStage::visit_multisetremovepred(const MultisetRemovePred &n) { + next.visit_multisetremovepred(n); +} void IntermediateStage::visit_negative(const Negative &n) { next.visit_negative(n); } diff --git a/murphi2murphi/src/Stage.h b/murphi2murphi/src/Stage.h index aaa38600..c0db88c9 100644 --- a/murphi2murphi/src/Stage.h +++ b/murphi2murphi/src/Stage.h @@ -102,6 +102,7 @@ class IntermediateStage : public Stage { void visit_multisetadd(const rumur::MultisetAdd &n) override; void visit_multisetcount(const rumur::MultisetCount &n) override; void visit_multisetremove(const rumur::MultisetRemove &n) override; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) override; void visit_negative(const rumur::Negative &n) override; void visit_neq(const rumur::Neq &n) override; void visit_not(const rumur::Not &n) override; diff --git a/murphi2smv/src/codegen.cc b/murphi2smv/src/codegen.cc index a0985de9..481c3502 100644 --- a/murphi2smv/src/codegen.cc +++ b/murphi2smv/src/codegen.cc @@ -327,6 +327,12 @@ class Printer : public ConstBaseTraversal { << *n.arg0 << ", " << *n.arg1 << ')'; } + void visit_multisetremovepred(const MultisetRemovePred &n) final { + *this << "/-- FIXME: Murphi multiset types have no equivalent in SMV --/ " + "MultisetRemovePred(" + << *n.container << ", " << *n.predicate << ')'; + } + void visit_negative(const Negative &n) final { *this << '-' << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2uclid/src/check.cc b/murphi2uclid/src/check.cc index 2cd6470e..90d0e3bd 100644 --- a/murphi2uclid/src/check.cc +++ b/murphi2uclid/src/check.cc @@ -151,6 +151,10 @@ class Checker : public ConstTraversal { throw Error("Uclid5 has no equivalent of the multiset type", n.loc); } + void visit_multisetremovepred(const MultisetRemovePred &n) final { + throw Error("Uclid5 has no equivalent of the multiset type", n.loc); + } + void visit_propertyrule(const PropertyRule &n) final { if (n.property.category == Property::COVER) throw Error("cover properties have no LTL equivalent in Uclid5", n.loc); diff --git a/murphi2uclid/src/codegen.cc b/murphi2uclid/src/codegen.cc index 69955b87..b91dc481 100644 --- a/murphi2uclid/src/codegen.cc +++ b/murphi2uclid/src/codegen.cc @@ -511,6 +511,11 @@ class Printer : public ConstBaseTraversal { __builtin_unreachable(); } + void visit_multisetremovepred(const MultisetRemovePred &) final { + assert(!"multisetremovepred not rejected during check()"); + __builtin_unreachable(); + } + void visit_negative(const Negative &n) final { *this << "-" << *n.rhs; } void visit_neq(const Neq &n) final { diff --git a/murphi2xml/src/XMLPrinter.cc b/murphi2xml/src/XMLPrinter.cc index 1d61f572..1a447a6c 100644 --- a/murphi2xml/src/XMLPrinter.cc +++ b/murphi2xml/src/XMLPrinter.cc @@ -549,6 +549,23 @@ void XMLPrinter::visit_multisetremove(const MultisetRemove &n) { o << ""; } +void XMLPrinter::visit_multisetremovepred(const MultisetRemovePred &n) { + sync_to(n); + o << "'; + sync_to(*n.container); + o << ""; + dispatch(*n.container); + o << ""; + sync_to(*n.predicate); + o << ""; + dispatch(*n.predicate); + o << ""; + sync_to(n.loc.end); + o << ""; +} + void XMLPrinter::visit_negative(const Negative &n) { visit_uexpr("negative", n); } diff --git a/murphi2xml/src/XMLPrinter.h b/murphi2xml/src/XMLPrinter.h index 8636cfb8..c6700ef6 100644 --- a/murphi2xml/src/XMLPrinter.h +++ b/murphi2xml/src/XMLPrinter.h @@ -59,6 +59,7 @@ class XMLPrinter : public rumur::ConstBaseTraversal { void visit_multisetadd(const rumur::MultisetAdd &n) final; void visit_multisetcount(const rumur::MultisetCount &n) final; void visit_multisetremove(const rumur::MultisetRemove &n) final; + void visit_multisetremovepred(const rumur::MultisetRemovePred &n) final; void visit_negative(const rumur::Negative &n) final; void visit_neq(const rumur::Neq &n) final; void visit_not(const rumur::Not &n) final; diff --git a/rumur/src/check.cc b/rumur/src/check.cc index 9bb1d987..15aa511d 100644 --- a/rumur/src/check.cc +++ b/rumur/src/check.cc @@ -32,6 +32,10 @@ class Check : public ConstTraversal { throw Error("multiset types are not supported", n.loc); } + void visit_multisetremovepred(const MultisetRemovePred &n) final { + throw Error("multiset types 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-stmt.cc b/rumur/src/generate-stmt.cc index 794d1e59..ccb6c43a 100644 --- a/rumur/src/generate-stmt.cc +++ b/rumur/src/generate-stmt.cc @@ -218,6 +218,11 @@ class Generator : public ConstStmtTraversal { __builtin_unreachable(); } + void visit_multisetremovepred(const MultisetRemovePred &) final { + assert(!"multisetremovepred not rejected during check()"); + __builtin_unreachable(); + } + void visit_procedurecall(const ProcedureCall &s) final { generate_rvalue(*out, s.call); } diff --git a/rumur/src/smt/simplify.cc b/rumur/src/smt/simplify.cc index c8ee3593..61f94390 100644 --- a/rumur/src/smt/simplify.cc +++ b/rumur/src/smt/simplify.cc @@ -279,6 +279,13 @@ class Simplifier : public BaseTraversal { simplify(n.arg1); } + void visit_multisetremovepred(MultisetRemovePred &n) final { + dispatch(*n.container); + simplify(n.container); + dispatch(*n.predicate); + simplify(n.predicate); + } + void visit_negative(Negative &n) final { visit_uexpr(n); } void visit_neq(Neq &n) final { visit_bexpr(n); } void visit_not(Not &n) final { visit_uexpr(n); } From 666b89cdfb62af4d39fb292ebe74625715c7a69b Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 17/21] support 'multisetremovepred' during lexing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/src/lexer.l | 133 +++++++++++++++++++++-------------------- librumur/src/parser.yy | 1 + 2 files changed, 68 insertions(+), 66 deletions(-) diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l index 4b03f4bd..9fc67d1f 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -60,72 +60,73 @@ throw rumur::Error("real types are not supported", *loc); } -alias { return rumur::parser::token::ALIAS; } -array { return rumur::parser::token::ARRAY; } -assert { return rumur::parser::token::ASSERT; } -assume { return rumur::parser::token::ASSUME; } -begin { return rumur::parser::token::BEGIN_TOK; } -boolean { return rumur::parser::token::BOOLEAN; } -by { return rumur::parser::token::BY; } -case { return rumur::parser::token::CASE; } -choose { return rumur::parser::token::CHOOSE; } -clear { return rumur::parser::token::CLEAR; } -const { return rumur::parser::token::CONST; } -cover { return rumur::parser::token::COVER; } -do { return rumur::parser::token::DO; } -else { return rumur::parser::token::ELSE; } -elsif { return rumur::parser::token::ELSIF; } -end { return rumur::parser::token::END; } -endalias { return rumur::parser::token::ENDALIAS; } -endchoose { return rumur::parser::token::ENDCHOOSE; } -endexists { return rumur::parser::token::ENDEXISTS; } -endfor { return rumur::parser::token::ENDFOR; } -endforall { return rumur::parser::token::ENDFORALL; } -endfunction { return rumur::parser::token::ENDFUNCTION; } -endif { return rumur::parser::token::ENDIF; } -endprocedure { return rumur::parser::token::ENDPROCEDURE; } -endrecord { return rumur::parser::token::ENDRECORD; } -endrule { return rumur::parser::token::ENDRULE; } -endruleset { return rumur::parser::token::ENDRULESET; } -endstartstate { return rumur::parser::token::ENDSTARTSTATE; } -endswitch { return rumur::parser::token::ENDSWITCH; } -endwhile { return rumur::parser::token::ENDWHILE; } -enum { return rumur::parser::token::ENUM; } -error { return rumur::parser::token::ERROR; } -exists { return rumur::parser::token::EXISTS; } -for { return rumur::parser::token::FOR; } -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; } -multiset { return rumur::parser::token::MULTISET; } -multisetadd { return rumur::parser::token::MULTISETADD; } -multisetcount { return rumur::parser::token::MULTISETCOUNT; } -multisetremove { return rumur::parser::token::MULTISETREMOVE; } -of { return rumur::parser::token::OF; } -procedure { return rumur::parser::token::PROCEDURE; } -put { return rumur::parser::token::PUT; } -real { throw rumur::Error("real types are not supported", *loc); } -record { return rumur::parser::token::RECORD; } -return { return rumur::parser::token::RETURN; } -rule { return rumur::parser::token::RULE; } -ruleset { return rumur::parser::token::RULESET; } -scalarset { return rumur::parser::token::SCALARSET; } -startstate { return rumur::parser::token::STARTSTATE; } -switch { return rumur::parser::token::SWITCH; } -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 { return rumur::parser::token::UNION; } -var { return rumur::parser::token::VAR; } -while { return rumur::parser::token::WHILE; } - -"∀" { return rumur::parser::token::FORALL; } -"∃" { return rumur::parser::token::EXISTS; } +alias { return rumur::parser::token::ALIAS; } +array { return rumur::parser::token::ARRAY; } +assert { return rumur::parser::token::ASSERT; } +assume { return rumur::parser::token::ASSUME; } +begin { return rumur::parser::token::BEGIN_TOK; } +boolean { return rumur::parser::token::BOOLEAN; } +by { return rumur::parser::token::BY; } +case { return rumur::parser::token::CASE; } +choose { return rumur::parser::token::CHOOSE; } +clear { return rumur::parser::token::CLEAR; } +const { return rumur::parser::token::CONST; } +cover { return rumur::parser::token::COVER; } +do { return rumur::parser::token::DO; } +else { return rumur::parser::token::ELSE; } +elsif { return rumur::parser::token::ELSIF; } +end { return rumur::parser::token::END; } +endalias { return rumur::parser::token::ENDALIAS; } +endchoose { return rumur::parser::token::ENDCHOOSE; } +endexists { return rumur::parser::token::ENDEXISTS; } +endfor { return rumur::parser::token::ENDFOR; } +endforall { return rumur::parser::token::ENDFORALL; } +endfunction { return rumur::parser::token::ENDFUNCTION; } +endif { return rumur::parser::token::ENDIF; } +endprocedure { return rumur::parser::token::ENDPROCEDURE; } +endrecord { return rumur::parser::token::ENDRECORD; } +endrule { return rumur::parser::token::ENDRULE; } +endruleset { return rumur::parser::token::ENDRULESET; } +endstartstate { return rumur::parser::token::ENDSTARTSTATE; } +endswitch { return rumur::parser::token::ENDSWITCH; } +endwhile { return rumur::parser::token::ENDWHILE; } +enum { return rumur::parser::token::ENUM; } +error { return rumur::parser::token::ERROR; } +exists { return rumur::parser::token::EXISTS; } +for { return rumur::parser::token::FOR; } +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; } +multiset { return rumur::parser::token::MULTISET; } +multisetadd { return rumur::parser::token::MULTISETADD; } +multisetcount { return rumur::parser::token::MULTISETCOUNT; } +multisetremove { return rumur::parser::token::MULTISETREMOVE; } +multisetremovepred { return rumur::parser::token::MULTISETREMOVEPRED; } +of { return rumur::parser::token::OF; } +procedure { return rumur::parser::token::PROCEDURE; } +put { return rumur::parser::token::PUT; } +real { throw rumur::Error("real types are not supported", *loc); } +record { return rumur::parser::token::RECORD; } +return { return rumur::parser::token::RETURN; } +rule { return rumur::parser::token::RULE; } +ruleset { return rumur::parser::token::RULESET; } +scalarset { return rumur::parser::token::SCALARSET; } +startstate { return rumur::parser::token::STARTSTATE; } +switch { return rumur::parser::token::SWITCH; } +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 { return rumur::parser::token::UNION; } +var { return rumur::parser::token::VAR; } +while { return rumur::parser::token::WHILE; } + +"∀" { return rumur::parser::token::FORALL; } +"∃" { return rumur::parser::token::EXISTS; } /* Recognise true and false explicitly rather than as generic IDs (below). The * purpose of this is so that we match them case-insensitively. diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index edd4a719..0c4221fc 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -167,6 +167,7 @@ %token MULTISETADD %token MULTISETCOUNT %token MULTISETREMOVE +%token MULTISETREMOVEPRED %token NEQ "!=" %token NUMBER %token OF From 2a686b72ac14948168f58957bff44a7898891cec Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 18/21] support 'multisetremovepred' during parsing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- doc/vs-cmurphi.rst | 3 ++- librumur/src/parser.yy | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/doc/vs-cmurphi.rst b/doc/vs-cmurphi.rst index 5aaee30a..2f986ac9 100644 --- a/doc/vs-cmurphi.rst +++ b/doc/vs-cmurphi.rst @@ -50,7 +50,8 @@ CMurphi requires the index of multiset to be a scalarset bound. Rumur supports any constant expression as a bound. This limitation of syntax-only support applies also to the multiset constructs -``Choose``, ``MultisetAdd``, ``MultisetCount``, and ``MultisetRemove``. +``Choose``, ``MultisetAdd``, ``MultisetCount``, ``MultisetRemove``, and +``MultisetRemovePred``. Unions ^^^^^^ diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index 0c4221fc..2ffc5dbd 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -619,6 +619,8 @@ stmt: category STRING expr { $$ = rumur::Ptr::make($3, $5, @$); } | MULTISETREMOVE '(' expr ',' expr ')' { $$ = rumur::Ptr::make($3, $5, @$); +} | MULTISETREMOVEPRED '(' ID ':' expr ',' expr ')' { + $$ = rumur::Ptr::make($3, $5, $7, @$); } | PUT STRING { $$ = rumur::Ptr::make($2, @$); } | PUT expr { From f6617bef7bab564139822149caafd67b0c722614 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:03:04 +1000 Subject: [PATCH 19/21] support array indexing syntax on multisets MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #331 “MultiSet support within scope?” Reported-by: Markus Alexander Kuppe --- librumur/src/Expr.cc | 49 ++++++++++++++++++++++++++-------- murphi2c/src/CLikeGenerator.cc | 1 + rumur/src/generate-expr.cc | 3 +++ 3 files changed, 42 insertions(+), 11 deletions(-) diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc index ed2aef41..170d90d5 100644 --- a/librumur/src/Expr.cc +++ b/librumur/src/Expr.cc @@ -1288,14 +1288,24 @@ bool Element::constant() const { return false; } Ptr Element::type() const { const Ptr t = array->type()->resolve(); - const Array *a = dynamic_cast(t.get()); - // if we are called during symbol resolution on a malformed expression, our - // left hand side may not be an array - if (a == nullptr) - throw Error("array reference based on something that is not an array", loc); + { + auto a = dynamic_cast(t.get()); + if (a != nullptr) + return a->element_type; + } + + { + auto m = dynamic_cast(t.get()); + if (m != nullptr) + return m->element_type; + } - return a->element_type; + // if we are called during symbol resolution on a malformed expression, our + // left hand side may not be an array or a multiset + throw Error("array reference based on something that is neither an array nor " + "a multiset", + loc); } mpz_class Element::constant_fold() const { @@ -1306,13 +1316,30 @@ void Element::validate() const { const Ptr t = array->type()->resolve(); - if (!isa(t)) - throw Error("array index on an expression that is not an array", loc); + { + auto a = dynamic_cast(t.get()); + if (a != nullptr) { + + if (!index->type()->coerces_to(*a->index_type)) + throw Error("array indexed using an expression of incorrect type", loc); + return; + } + } - auto a = dynamic_cast(*t); + { + auto m = dynamic_cast(t.get()); + if (m != nullptr) { + const Scalarset s{m->index_bound, m->index_bound->loc}; + if (!index->type()->coerces_to(s)) + throw Error("multiset indexed using an expression of incorrect type", + loc); + return; + } + } - if (!index->type()->coerces_to(*a.index_type)) - throw Error("array indexed using an expression of incorrect type", loc); + throw Error( + "array index on an expression that is neither an array nor a multiset", + loc); } bool Element::is_lvalue() const { return array->is_lvalue(); } diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 2e5c0f5a..8949c167 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -205,6 +205,7 @@ void CLikeGenerator::visit_element(const Element &n) { // find the type of the array expression const Ptr t = n.array->type()->resolve(); + assert(!isa(t) && "multiset was not rejected during check()"); auto a = dynamic_cast(t.get()); assert(a != nullptr && "non-array on LHS of array indexing expression"); diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc index ea8633ef..ebaa1787 100644 --- a/rumur/src/generate-expr.cc +++ b/rumur/src/generate-expr.cc @@ -84,6 +84,9 @@ class Generator : public ConstExprTraversal { const Ptr t2 = t1->resolve(); assert(t2 != nullptr && "array with invalid type"); + assert(!isa(t2) && + "multiset not rejected prior to code generation"); + auto a = dynamic_cast(*t2); mpz_class element_width = a.element_type->width(); From 1c419e523f625b8ff4d31cd33f9a9fb021f6ed42 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Fri, 21 Aug 2026 17:48:36 +1000 Subject: [PATCH 20/21] support 'foo := undefined' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CMurphi supports `undefined` in two situations: 1. assignment, `foo := undefined;` 2. function calls, `foo(…, undefined, …)` This change adds support for (1). Github: #331 “MultiSet support within scope?” --- librumur/src/lexer.l | 1 + librumur/src/parser.yy | 3 +++ tests/tests.py | 1 + tests/undefined-assign.m | 19 +++++++++++++++++++ 4 files changed, 24 insertions(+) create mode 100644 tests/undefined-assign.m diff --git a/librumur/src/lexer.l b/librumur/src/lexer.l index 9fc67d1f..219e20bd 100644 --- a/librumur/src/lexer.l +++ b/librumur/src/lexer.l @@ -121,6 +121,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; } +undefined { return rumur::parser::token::UNDEFINED; } 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 2ffc5dbd..ca5273bd 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -193,6 +193,7 @@ %token TO %token TYPE %token UNDEFINE +%token UNDEFINED %token UNION %token VAR %token WHILE @@ -597,6 +598,8 @@ stmt: category STRING expr { $$ = rumur::Ptr::make(p, $3, @$); } | designator COLON_EQ expr { $$ = rumur::Ptr::make($1, $3, @$); +} | designator COLON_EQ UNDEFINED { + $$ = rumur::Ptr::make($1, @$); } | ALIAS exprdecls DO stmts endalias { std::vector> decls; for (const std::tuple, rumur::location> &d : $2) { diff --git a/tests/tests.py b/tests/tests.py index 2d53071e..59c81222 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1552,6 +1552,7 @@ def test_murphi2uclid(model, tmp_path): "scalarset-cex.m", "scalarset-schedules-off.m", "scalarset-schedules-off-2.m", + "undefined-assign.m", # contains `put` "for-step-0-dynamic.m", "put-stmt.m", diff --git a/tests/undefined-assign.m b/tests/undefined-assign.m new file mode 100644 index 00000000..fb4819ce --- /dev/null +++ b/tests/undefined-assign.m @@ -0,0 +1,19 @@ +-- can we handle the 'undefined' token in an assignment? +-- +-- This seems to be an extension added to CMurphi after its initial release. + +var + x: boolean; + +startstate begin + x := false; +end; + +rule + var y: boolean; +begin + y := x; + x := undefined; + assert isundefined(x); + x := !y; +end; From dd3bc59f781c8ae587f3a5753b80ed06ac033c8b Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sun, 23 Aug 2026 07:12:25 +1000 Subject: [PATCH 21/21] =?UTF-8?q?support=20'foo(=E2=80=A6,=20undefined,=20?= =?UTF-8?q?=E2=80=A6)'?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This completes (2) described in the previous commit. This looks pretty hacky – supporting `undefined` exactly within function calls and not elsewhere – but this appears to match CMurphi behaviour. Github: #331 “MultiSet support within scope?” --- librumur/src/parser.yy | 34 ++++++++++++---- librumur/src/resolve-symbols.cc | 17 +++++++- rumur/src/generate-expr.cc | 62 ++++++++++++++++++------------ tests/tests.py | 4 ++ tests/undefined-call-complex.m | 22 +++++++++++ tests/undefined-call.m | 45 ++++++++++++++++++++++ tests/undefined-var-call-complex.m | 22 +++++++++++ tests/undefined-var-call.m | 45 ++++++++++++++++++++++ 8 files changed, 218 insertions(+), 33 deletions(-) create mode 100644 tests/undefined-call-complex.m create mode 100644 tests/undefined-call.m create mode 100644 tests/undefined-var-call-complex.m create mode 100644 tests/undefined-var-call.m diff --git a/librumur/src/parser.yy b/librumur/src/parser.yy index ca5273bd..6a21264f 100644 --- a/librumur/src/parser.yy +++ b/librumur/src/parser.yy @@ -224,8 +224,10 @@ %type > expr %type , rumur::location>>> exprdecl %type , rumur::location>>> exprdecls -%type >> exprlist -%type >> exprlist_cont +%type >> exprlist_fn +%type >> exprlist_fn_cont +%type >> exprlist_sw +%type >> exprlist_sw_cont %type > guard_opt %type >> id_list %type >> id_list_opt @@ -449,7 +451,7 @@ expr: expr '?' expr ':' expr { } | '(' expr ')' { $$ = $2; $$->loc = @$; -} | ID '(' exprlist ')' { +} | ID '(' exprlist_fn ')' { $$ = rumur::Ptr::make($1, $3, @$); } | ISMEMBER '(' expr ',' typeexpr ')' { $$ = rumur::Ptr::make($3, $5, @$); @@ -472,13 +474,31 @@ exprdecls: exprdecls exprdecl semi_opt { /* nothing required */ }; -exprlist: exprlist_cont expr comma_opt { +exprlist_fn: exprlist_fn_cont expr comma_opt { + $$ = $1; + $$.push_back($2); +} | exprlist_fn_cont UNDEFINED comma_opt { + $$ = $1; + $$.push_back(rumur::Ptr::make("undefined", nullptr, @2)); +} | %empty { +}; + +exprlist_fn_cont: exprlist_fn_cont expr ',' { + $$ = $1; + $$.push_back($2); +} | exprlist_fn_cont UNDEFINED ',' { + $$ = $1; + $$.push_back(rumur::Ptr::make("undefined", nullptr, @2)); +} | %empty { +}; + +exprlist_sw: exprlist_sw_cont expr comma_opt { $$ = $1; $$.push_back($2); } | %empty { }; -exprlist_cont: exprlist_cont expr ',' { +exprlist_sw_cont: exprlist_sw_cont expr ',' { $$ = $1; $$.push_back($2); } | %empty { @@ -634,7 +654,7 @@ stmt: category STRING expr { $$ = rumur::Ptr::make($2, @$); } | UNDEFINE designator { $$ = rumur::Ptr::make($2, @$); -} | ID '(' exprlist ')' { +} | ID '(' exprlist_fn ')' { $$ = rumur::Ptr::make($1, $3, @$); } | WHILE expr DO stmts endwhile { $$ = rumur::Ptr::make($2, $4, @$); @@ -670,7 +690,7 @@ switchcases: switchcases_cont ELSE stmts { $$ = $1; }; -switchcases_cont: switchcases_cont CASE exprlist ':' stmts { +switchcases_cont: switchcases_cont CASE exprlist_sw ':' stmts { $$ = $1; $$.push_back(rumur::SwitchCase($3, $5, @$)); } | %empty { diff --git a/librumur/src/resolve-symbols.cc b/librumur/src/resolve-symbols.cc index 1bc788a4..5f58bf04 100644 --- a/librumur/src/resolve-symbols.cc +++ b/librumur/src/resolve-symbols.cc @@ -260,8 +260,23 @@ class Resolver : public Traversal { n.function = f; } - for (auto &a : n.arguments) + + size_t i = 0; + for (auto &a : n.arguments) { + symtab.open_scope(); + + // if this argument is `undefined`, create something it can resolve to + auto id = dynamic_cast(a.get()); + if (id != nullptr && id->id == "undefined") { + VarDecl *const undef = + make("undefined", n.function->parameters[i]->type, n.loc); + symtab.declare("undefined", undef); + } + dispatch(*a); + symtab.close_scope(); + ++i; + } for (Ptr &a : n.arguments) disambiguate(a); diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc index ebaa1787..69adb4d7 100644 --- a/rumur/src/generate-expr.cc +++ b/rumur/src/generate-expr.cc @@ -270,22 +270,23 @@ class Generator : public ConstExprTraversal { } } - /* Now for each parameter we need to consider five distinct methods, based - * on the parameter's circumstance as described in the following table: + /* Now for each parameter we need to consider six distinct methods, based on + * the parameter’s circumstance as described in the following table: * - * ┌──────┬────────────────┬─────────┬────────────╥────────┐ - * │ var? │ simple/complex │ lvalue? │ read-only? ║ method │ - * ├──────┼────────────────┼─────────┼────────────╫────────┤ - * │ no │ simple │ no │ - ║ 1 │ - * │ no │ simple │ yes │ no ║ 2 │ - * │ no │ simple │ yes │ yes ║ 2 │ - * │ no │ complex │ no │ - ║ 5 │ - * │ no │ complex │ yes │ no ║ 3 │ - * │ no │ complex │ yes │ yes ║ 3 │ - * │ yes │ simple │ no │ no ║ 1 │ - * │ yes │ simple │ yes │ no ║ 4 │ - * │ yes │ complex │ yes │ no ║ 4 │ - * └──────┴────────────────┴─────────┴────────────╨────────┘ + * ┌──────┬────────────────┬─────────┬────────────┬────────────╥────────┐ + * │ var? │ simple/complex │ lvalue? │ read-only? │ undefined? ║ method │ + * ├──────┼────────────────┼─────────┼────────────┼────────────╫────────┤ + * │ no │ simple │ no │ - │ no ║ 1 │ + * │ no │ simple │ yes │ no │ no ║ 2 │ + * │ no │ simple │ yes │ yes │ no ║ 2 │ + * │ no │ complex │ no │ - │ no ║ 5 │ + * │ no │ complex │ yes │ no │ no ║ 3 │ + * │ no │ complex │ yes │ yes │ no ║ 3 │ + * │ yes │ simple │ no │ no │ no ║ 1 │ + * │ yes │ simple │ yes │ no │ no ║ 4 │ + * │ yes │ complex │ yes │ no │ no ║ 4 │ + * │ - │ - │ - │ - │ yes ║ 6 │ + * └──────┴────────────────┴─────────┴────────────┴────────────╨────────┘ * * 1. We can create a temporary handle and backing storage, then extract * the value of the argument as an rvalue and write it to this @@ -307,6 +308,8 @@ class Generator : public ConstExprTraversal { * 4. We just pass the original handle, the lvalue of the argument. * * 5. We pass the original (rvalue) handle. + * + * 6. We pass a zeroed C99 compound literal. */ // clang-format off @@ -318,15 +321,19 @@ class Generator : public ConstExprTraversal { bool is_lvalue = argument->is_lvalue(); bool readonly = argument->is_readonly(); - if (!var && simple && !is_lvalue ) return 1; - if (!var && simple && is_lvalue && !readonly) return 2; - if (!var && simple && is_lvalue && readonly) return 2; - if (!var && !simple && !is_lvalue ) return 5; - if (!var && !simple && is_lvalue && !readonly) return 3; - if (!var && !simple && is_lvalue && readonly) return 3; - if ( var && simple && !is_lvalue ) return 1; - if ( var && simple && is_lvalue && !readonly) return 4; - if ( var && !simple && !readonly) return 4; + auto id = dynamic_cast(argument.get()); + const bool is_undef = id != nullptr && id->id == "undefined"; + + if (!var && simple && !is_lvalue && !is_undef) return 1; + if (!var && simple && is_lvalue && !readonly && !is_undef) return 2; + if (!var && simple && is_lvalue && readonly && !is_undef) return 2; + if (!var && !simple && !is_lvalue && !is_undef) return 5; + if (!var && !simple && is_lvalue && !readonly && !is_undef) return 3; + if (!var && !simple && is_lvalue && readonly && !is_undef) return 3; + if ( var && simple && !is_lvalue && !is_undef) return 1; + if ( var && simple && is_lvalue && !readonly && !is_undef) return 4; + if ( var && !simple && !readonly && !is_undef) return 4; + if ( is_undef) return 6; assert(!"unreachable"); __builtin_unreachable(); @@ -346,7 +353,7 @@ class Generator : public ConstExprTraversal { "v" + std::to_string(n.unique_id) + "_" + std::to_string(index); auto method = get_method(p, a); - assert(method >= 1 && method <= 5); + assert(method >= 1 && method <= 6); if (method == 1 || method == 2 || method == 3) *out << "unsigned char " << storage << "[BITS_TO_BYTES(" << p->width() @@ -438,6 +445,11 @@ class Generator : public ConstExprTraversal { generate_rvalue(*out, *a); break; + case 6: + *out << "((struct handle){ .base = (unsigned char[BITS_TO_BYTES(" + << p->width() << ")]){0}, .width = " << p->width() << "ull })"; + break; + default: *out << handle; break; diff --git a/tests/tests.py b/tests/tests.py index 59c81222..d616ecbd 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1553,6 +1553,10 @@ def test_murphi2uclid(model, tmp_path): "scalarset-schedules-off.m", "scalarset-schedules-off-2.m", "undefined-assign.m", + "undefined-call.m", + "undefined-call-complex.m", + "undefined-var-call.m", + "undefined-var-call-complex.m", # contains `put` "for-step-0-dynamic.m", "put-stmt.m", diff --git a/tests/undefined-call-complex.m b/tests/undefined-call-complex.m new file mode 100644 index 00000000..b3886b1a --- /dev/null +++ b/tests/undefined-call-complex.m @@ -0,0 +1,22 @@ +-- a model that passes `undefined` to a function taking complex type + +type + t: record + a: 0..1; + end; + +var + x: boolean; + +function foo(y: t): boolean; begin + assert isundefined(y.a); + return !x; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; diff --git a/tests/undefined-call.m b/tests/undefined-call.m new file mode 100644 index 00000000..17cbede7 --- /dev/null +++ b/tests/undefined-call.m @@ -0,0 +1,45 @@ +-- a model that passes `undefined` to a function + +var + x: boolean; + +function foo(y: 0..1): boolean; begin + assert isundefined(y); + return !x; +end; + +function bar(a: boolean; y: 0..1): boolean; begin + assert isundefined(y); + return !a; +end; + +function baz(y: 0..1; a: boolean): boolean; begin + assert isundefined(y); + return !a; +end; + +function qux(a: boolean; y: 0..1; b: boolean): boolean; begin + assert isundefined(y); + assert a = b; + return !a; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; + +rule begin + x := bar(x, undefined); +end; + +rule begin + x := baz(undefined, x); +end; + +rule begin + x := qux(x, undefined, x); +end; diff --git a/tests/undefined-var-call-complex.m b/tests/undefined-var-call-complex.m new file mode 100644 index 00000000..b41b26de --- /dev/null +++ b/tests/undefined-var-call-complex.m @@ -0,0 +1,22 @@ +-- a model that passes `undefined` to a function taking complex type + +type + t: record + a: 0..1; + end; + +var + x: boolean; + +function foo(var y: t): boolean; begin + assert isundefined(y.a); + return !x; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; diff --git a/tests/undefined-var-call.m b/tests/undefined-var-call.m new file mode 100644 index 00000000..78122b83 --- /dev/null +++ b/tests/undefined-var-call.m @@ -0,0 +1,45 @@ +-- a model that passes `undefined` to a function as a `var` parameter + +var + x: boolean; + +function foo(var y: 0..1): boolean; begin + assert isundefined(y); + return !x; +end; + +function bar(a: boolean; var y: 0..1): boolean; begin + assert isundefined(y); + return !a; +end; + +function baz(var y: 0..1; a: boolean): boolean; begin + assert isundefined(y); + return !a; +end; + +function qux(a: boolean; var y: 0..1; b: boolean): boolean; begin + assert isundefined(y); + assert a = b; + return !a; +end; + +startstate begin + x := false; +end; + +rule begin + x := foo(undefined); +end; + +rule begin + x := bar(x, undefined); +end; + +rule begin + x := baz(undefined, x); +end; + +rule begin + x := qux(x, undefined, x); +end;