diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-21 08:19:55 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-21 08:19:55 -0500 |
commit | 098cee0ea412e24e24caa79307e2950a640279af (patch) | |
tree | e0936bddb8700206d9d0691150b0b4af9dd23dc4 /src/expr/node_manager.h | |
parent | e91077d81183c6c54ff0fdad5c6eb160f16c4205 (diff) |
Add operator MakeBagOp for constructing bags (#5209)
This PR removes subtyping rules for bags and add operator MakeBagOp similar to SingletonOp
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5427c3b6a..8f2237523 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -578,13 +578,23 @@ class NodeManager { /** * Create a singleton set from the given element n. * @param t the element type of the returned set. - * Note that the type of n needs to be a subtype of t. + * Note that the type of n needs to be a subtype of t. * @param n the single element in the singleton. * @return a singleton set constructed from the element n. */ Node mkSingleton(const TypeNode& t, const TNode n); /** + * Create a bag from the given element n along with its multiplicity m. + * @param t the element type of the returned bag. + * Note that the type of n needs to be a subtype of t. + * @param n the element that is used to to construct the bag + * @param m the multiplicity of the element n + * @return a bag that contains m occurrences of n. + */ + Node mkBag(const TypeNode& t, const TNode n, const TNode m); + + /** * Create a constant of type T. It will have the appropriate * CONST_* kind defined for T. */ |