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/theory/bags/make_bag_op.cpp | |
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/theory/bags/make_bag_op.cpp')
-rw-r--r-- | src/theory/bags/make_bag_op.cpp | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp new file mode 100644 index 000000000..6a535afc2 --- /dev/null +++ b/src/theory/bags/make_bag_op.cpp @@ -0,0 +1,48 @@ +/********************* */ +/*! \file bag_op.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief a class for MK_BAG operator + **/ + +#include <iostream> + +#include "expr/type_node.h" +#include "make_bag_op.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const MakeBagOp& op) +{ + return out << "(mkBag_op " << op.getType() << ')'; +} + +size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const +{ + return TypeNodeHashFunction()(op.getType()); +} + +MakeBagOp::MakeBagOp(const TypeNode& elementType) + : d_type(new TypeNode(elementType)) +{ +} + +MakeBagOp::MakeBagOp(const MakeBagOp& op) : d_type(new TypeNode(op.getType())) +{ +} + +const TypeNode& MakeBagOp::getType() const { return *d_type; } + +bool MakeBagOp::operator==(const MakeBagOp& op) const +{ + return getType() == op.getType(); +} + +} // namespace CVC4 |