|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
One operand of an nditer: a named array or view and its layout in elements (a negative stride walks backwards, 0 repeats a broadcast axis). More...
#include <numpy_nditer.h>
Public Attributes | |
| nlohmann::json | array |
| bool | writable = false |
| std::vector< long long > | shape |
| std::vector< long long > | strides |
| nlohmann::json | extent |
| nlohmann::json | stride |
| std::vector< long long > | axes |
| The operand axis each iteration axis reads (op_axes), -1 for a new axis; empty for the default alignment on the last axes. | |
| typet | dtype |
| The dtype reads are cast to (op_dtypes); empty for the operand's own. | |
| std::string | buffer |
| A writable operand read through a cast is buffered: the hidden list its items live in, in visiting order, copied back once the iterator is exhausted or closed. | |
One operand of an nditer: a named array or view and its layout in elements (a negative stride walks backwards, 0 repeats a broadcast axis).
A 1-D view whose extent or stride is only known at run time keeps them as expressions in extent and stride.
| nlohmann::json numpy_nditer_operand::array |
| std::vector<long long> numpy_nditer_operand::axes |
The operand axis each iteration axis reads (op_axes), -1 for a new axis; empty for the default alignment on the last axes.
| std::string numpy_nditer_operand::buffer |
A writable operand read through a cast is buffered: the hidden list its items live in, in visiting order, copied back once the iterator is exhausted or closed.
Empty when items are the operand's own elements.
| typet numpy_nditer_operand::dtype |
The dtype reads are cast to (op_dtypes); empty for the operand's own.
| nlohmann::json numpy_nditer_operand::extent |
| std::vector<long long> numpy_nditer_operand::shape |
| nlohmann::json numpy_nditer_operand::stride |
| std::vector<long long> numpy_nditer_operand::strides |