diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-29 21:55:51 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 19:55:51 -0700 |
commit | 8c794ae1009bf8515b965c1023de188f50b35d60 (patch) | |
tree | 7dcf7bed2aa581fb806c8b23efe77c33f6632754 /src/util | |
parent | 19054b3b1d427e662d30d4322df2b2f2361353da (diff) |
Add internal support for integer and operator (#4668)
Towards merging iand branch to master. This adds internal support for an "integer AND" operator.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/util/iand.h | 47 | ||||
-rw-r--r-- | src/util/iand.i | 9 |
3 files changed, 57 insertions, 0 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index eba5fb8c9..028288dbc 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -17,6 +17,7 @@ libcvc4_add_sources( floatingpoint.cpp gmp_util.h hash.h + iand.h index.cpp index.h maybe.h diff --git a/src/util/iand.h b/src/util/iand.h new file mode 100644 index 000000000..b5bc92960 --- /dev/null +++ b/src/util/iand.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file iand.h + ** \verbatim + ** Top contributors (to current version): + ** Anrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The integer AND operator. + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__IAND_H +#define CVC4__IAND_H + +#include <cstdint> +#include <iosfwd> + +#include "base/exception.h" +#include "util/integer.h" + +namespace CVC4 { + +struct CVC4_PUBLIC IntAnd +{ + unsigned d_size; + IntAnd(unsigned size) : d_size(size) {} + operator unsigned() const { return d_size; } +}; /* struct IntAnd */ + +/* ----------------------------------------------------------------------- + ** Output stream + * ----------------------------------------------------------------------- */ + +inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) +{ + return os << "[" << ia.d_size << "]"; +} + +} // namespace CVC4 + +#endif /* CVC4__IAND_H */ diff --git a/src/util/iand.i b/src/util/iand.i new file mode 100644 index 000000000..92c5a1223 --- /dev/null +++ b/src/util/iand.i @@ -0,0 +1,9 @@ +%{ +#include "util/iand.h" +%} + +%rename(toUnsigned) CVC4::IntAnd::operator unsigned() const; + +%ignore CVC4::operator<<(std::ostream&, const IntAnd&); + +%include "util/iand.h" |