[WIP] syntax-only support for 'multiset'

doc/vs-cmurphi.rst

@@ -37,7 +37,21 @@ 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.
+
+This limitation of syntax-only support applies also to the multiset constructs
+``Choose``, ``MultisetAdd``, ``MultisetCount``, ``MultisetRemove``, and
+``MultisetRemovePred``.
 
 Unions
 ^^^^^^

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<Expr> container;
+  Ptr<Expr> predicate;
+
+  MultisetCount(const std::string &identifier_, const Ptr<Expr> &container_,
+                const Ptr<Expr> &predicate_, const location &loc_);
+  MultisetCount *clone() const override;
+
+  void visit(BaseTraversal &visitor) override;
+  void visit(ConstBaseTraversal &visitor) const override;
+
+  bool constant() const override;
+  Ptr<TypeExpr> type() const override;
+  mpz_class constant_fold() const override;
+  void validate() const override;
+  void to_stream(std::ostream &out) const override;
+  bool is_pure() const override;
+};
+
 } // namespace rumur

librumur/include/rumur/Rule.h

@@ -106,4 +106,20 @@ struct RUMUR_API_WITH_RTTI Ruleset : public Rule {
   std::vector<Ptr<Rule>> flatten() const override;
 };
 
+struct RUMUR_API_WITH_RTTI Choose : public Rule {
+  std::string identifier;
+  Ptr<Expr> container;
+  std::vector<Ptr<Rule>> rules;
+
+  Choose(const std::string &identifier_, const Ptr<Expr> &container_,
+         const std::vector<Ptr<Rule>> &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<Ptr<Rule>> flatten() const override;
+};
+
 } // namespace rumur

librumur/include/rumur/Stmt.h

@@ -130,6 +130,44 @@ struct RUMUR_API_WITH_RTTI If : public Stmt {
   void visit(ConstBaseTraversal &visitor) const override;
 };
 
+struct RUMUR_API_WITH_RTTI MultisetAdd : public Stmt {
+  Ptr<Expr> arg0;
+  Ptr<Expr> arg1;
+
+  MultisetAdd(const Ptr<Expr> &arg0_, const Ptr<Expr> &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 MultisetRemove : public Stmt {
+  Ptr<Expr> arg0;
+  Ptr<Expr> arg1;
+
+  MultisetRemove(const Ptr<Expr> &arg0_, const Ptr<Expr> &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 MultisetRemovePred : public Stmt {
+  std::string identifier;
+  Ptr<Expr> container;
+  Ptr<Expr> predicate;
+
+  MultisetRemovePred(const std::string &identifier_,
+                     const Ptr<Expr> &container_, const Ptr<Expr> &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;

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<Expr> index_bound;
+  Ptr<TypeExpr> element_type;
+
+  Multiset(const Ptr<Expr> &index_bound_, const Ptr<TypeExpr> &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;

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;
@@ -60,6 +61,11 @@ 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_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;

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;
@@ -106,6 +107,11 @@ 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_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;
@@ -167,6 +173,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;
@@ -194,6 +201,11 @@ 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_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;
@@ -247,6 +259,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;
@@ -274,6 +287,11 @@ 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_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;
@@ -327,6 +345,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;
@@ -354,6 +373,11 @@ 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_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;
@@ -405,6 +429,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;
@@ -414,6 +439,10 @@ 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_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;
@@ -452,6 +481,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;
@@ -475,6 +505,8 @@ 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_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;
@@ -517,6 +549,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;
@@ -543,6 +576,10 @@ 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_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;