Struct haybale::simple_memory::Memory

pub struct Memory { /* fields omitted */ }

Implementations

impl Memory

pub const CELL_BITS: u32

pub const BITS_IN_BYTE: u32

pub const LOG_BITS_IN_BYTE: u32

pub const CELL_BYTES: u32

pub fn new_uninitialized(
    btor: Rc<Btor>,
    null_detection: bool,
    name: Option<&str>,
    addr_bits: u32
) -> Self

A new Memory, whose contents at all addresses are completely uninitialized (unconstrained)

null_detection: if true, all memory accesses will be checked to ensure their addresses cannot be NULL, throwing Error::NullPointerDereference if NULL is a possible solution for the address

name: a name for this Memory, or None to use the default name (as of this writing, 'mem')

addr_bits: e.g. 64 for a Memory which uses 64-bit addresses

pub fn new_zero_initialized(
    btor: Rc<Btor>,
    null_detection: bool,
    name: Option<&str>,
    addr_bits: u32
) -> Self

A new Memory, whose contents at all addresses are initialized to be 0

null_detection: if true, all memory accesses will be checked to ensure their addresses cannot be NULL, throwing Error::NullPointerDereference if NULL is a possible solution for the address

name: a name for this Memory, or None to use the default name (as of this writing, 'mem_initialized')

addr_bits: e.g. 64 for a Memory which uses 64-bit addresses

pub fn get_solver(&self) -> Rc<Btor>

Get a reference to the Btor instance this Memory belongs to

pub fn change_solver(&mut self, new_btor: Rc<Btor>)

Adapt the Memory to a new Btor instance.

The new Btor instance should have been created (possibly transitively) via Btor::duplicate() from the Btor this Memory was originally created with (or most recently changed to). Further, no new variables should have been added since the call to Btor::duplicate().

pub fn read(&self, addr: &BV<Rc<Btor>>, bits: u32) -> Result<BV<Rc<Btor>>>

Read any number (>0) of bits of memory, at any alignment. Returned BV will have size bits.

pub fn write(&mut self, addr: &BV<Rc<Btor>>, val: BV<Rc<Btor>>) -> Result<()>

Write any number (>0) of bits of memory, at any alignment.

Trait Implementations

impl Clone for Memory

fn clone(&self) -> Memory

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Memory

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Memory

impl Memory for Memory

type SolverRef = Rc<Btor>

type Index = BV<Rc<Btor>>

type Value = BV<Rc<Btor>>

fn new_uninitialized(
    btor: Rc<Btor>,
    null_detection: bool,
    name: Option<&str>,
    addr_bits: u32
) -> Self

A new Memory, whose contents at all addresses are completely uninitialized (unconstrained)

fn new_zero_initialized(
    btor: Rc<Btor>,
    null_detection: bool,
    name: Option<&str>,
    addr_bits: u32
) -> Self

A new Memory, whose contents at all addresses are initialized to be 0

fn read(&self, index: &Self::Index, bits: u32) -> Result<Self::Value>

Read any number (>0) of bits of memory, at any alignment. Returned BV will have size bits.

fn write(&mut self, index: &Self::Index, value: Self::Value) -> Result<()>

Write any number (>0) of bits of memory, at any alignment.

fn get_solver(&self) -> Rc<Btor>

Get a reference to the solver instance this Memory belongs to

fn change_solver(&mut self, new_btor: Rc<Btor>)

Adapt the Memory to a new solver instance.

impl PartialEq<Memory> for Memory

fn eq(&self, other: &Memory) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Memory) -> bool

This method tests for !=.

impl StructuralEq for Memory

impl StructuralPartialEq for Memory