btor 0.1.0

Rust wrapper for btor
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

/**
 *  Btor2Tools: A tool package for the BTOR format.
 *
 *  Copyright (c) 2013-2016 Mathias Preiner.
 *  Copyright (c) 2015-2018 Aina Niemetz.
 *  Copyright (c) 2018 Armin Biere.
 *  Copyright (c) 2020 Nina Engelhardt.
 *
 *  All rights reserved.
 *
 *  This file is part of the Btor2Tools package.
 *  See LICENSE.txt for more information on using this software.
 */

#ifndef BTOR2AM_H_INCLUDED
#define BTOR2AM_H_INCLUDED

#include <string>
#include <unordered_map>

#include "btorsimbv.h"

struct BtorSimArrayModel
{
  /* length of the array index sort */
  uint64_t index_width = 0;

  /* length of the array element sort */
  uint64_t element_width = 0;

  /* if not 0, uninitialized array elements will have a pseudo-random value */
  uint64_t random_seed = 0;

  /* if not null, global array initialization value from a init <array> <vector>
   * statement */
  BtorSimBitVector* const_init = nullptr;

  /* Only the values of previously accessed memory elements are stored. Indexes
   * are represented as strings of '0' and '1' because they can represent
   * arbitrarily large vectors, have a well-defined length, and do not require
   * custom comparison functions. If a not previously accessed element is read,
   * an entry is created and populated with the first existing value of:
   * - const_init (if the entire array has been initialized with a vector)
   * - a reproducible pseudo-random value provided by get_random_init based on
   * index value and random_seed (if non-zero, i.e. when randomize mode is
   * enabled)
   * - zero.
   * It is important to populate on read and not only on write so that a full
   * account of all accessed memory elements and their values is shown in the
   * trace.
   */
  std::unordered_map<std::string, BtorSimBitVector*> data;

  BtorSimArrayModel (uint64_t index_width, uint64_t element_width)
      : index_width (index_width), element_width (element_width){};
  BtorSimArrayModel (uint64_t index_width,
                     uint64_t element_width,
                     uint64_t random_seed)
      : index_width (index_width),
        element_width (element_width),
        random_seed (random_seed){};
  ~BtorSimArrayModel ();

  /* avoid accidental copies */
  BtorSimArrayModel (const BtorSimArrayModel&) = delete;
  BtorSimArrayModel& operator= (const BtorSimArrayModel&) = delete;

  /* obtain a pseudo-random value for an uninitialized element (always the same
   * for given index and random_seed) */
  uint64_t get_random_init (uint64_t idx) const;

  /* get a copy of the global array init value */
  BtorSimBitVector* get_const_init () const;

  /* set the global array init value (copies the *init argument vector, does not
   * take ownership */
  BtorSimArrayModel* set_const_init (const BtorSimBitVector* init) const;

  /* obtain a copy of the element at index, create entry if not previously
   * accessed and initialize appropriately */
  BtorSimBitVector* read (const BtorSimBitVector* index);

  /* return a copy of the array with the element written at index (copies the
   * *element argument vector, does not take ownership) */
  BtorSimArrayModel* write (const BtorSimBitVector* index,
                            const BtorSimBitVector* element);

  /* obtain a copy of the element at index only if it was already previously
   * accessed, return null otherwise */
  BtorSimBitVector* check (const BtorSimBitVector* index) const;

  /* return a copy of the array */
  BtorSimArrayModel* copy () const;

  /* equality checks test for:
   * - same global init (unless all elements were already accessed)
   * - same random seed (unless all elements were already accessed)
   * - same element values at accessed indices (or equal to init value if
   * accessed only in one: this may happen if one copy has an extra read()
   * called on it)
   */
  bool operator!= (const BtorSimArrayModel& other) const;
  bool operator== (const BtorSimArrayModel& other) const;
};

/* Array variants of polymorphic operators that also exist on vectors */
BtorSimBitVector* btorsim_am_eq (const BtorSimArrayModel* a,
                                 const BtorSimArrayModel* b);
BtorSimBitVector* btorsim_am_neq (const BtorSimArrayModel* a,
                                  const BtorSimArrayModel* b);
BtorSimArrayModel* btorsim_am_ite (const BtorSimBitVector* cond,
                                   const BtorSimArrayModel* a,
                                   const BtorSimArrayModel* b);

#endif