Branch data Line data Source code
1 : : /****************************************************************************** 2 : : * This file is part of the cvc5 project. 3 : : * 4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS 5 : : * in the top-level source directory and their institutional affiliations. 6 : : * All rights reserved. See the file COPYING in the top-level source 7 : : * directory for licensing information. 8 : : * **************************************************************************** 9 : : * 10 : : * The integer AND operator. 11 : : */ 12 : : 13 : : #include "cvc5_public.h" 14 : : 15 : : #ifndef CVC5__IAND_H 16 : : #define CVC5__IAND_H 17 : : 18 : : #include <iosfwd> 19 : : #include <ostream> 20 : : 21 : : #include "base/exception.h" 22 : : #include "util/integer.h" 23 : : 24 : : namespace cvc5::internal { 25 : : 26 : : struct IntAnd 27 : : { 28 : : uint32_t d_size; 29 : 419 : IntAnd(uint32_t size) : d_size(size) {} 30 : 2697 : operator uint32_t() const { return d_size; } 31 : : }; /* struct IntAnd */ 32 : : 33 : : /* ----------------------------------------------------------------------- 34 : : * Output stream 35 : : * ----------------------------------------------------------------------- */ 36 : : 37 : : inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia); 38 : 102 : inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) 39 : : { 40 : 102 : return os << "(_ iand " << ia.d_size << ")"; 41 : : } 42 : : 43 : : } // namespace cvc5::internal 44 : : 45 : : #endif /* CVC5__IAND_H */