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

/**
 *  Btor2Tools: A tool package for the BTOR format.
 *
 *  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.
 */

#include "btorsimstate.h"

#include <assert.h>

#include "btorsimhelpers.h"

void
BtorSimState::update (BtorSimBitVector *bv)
{
  assert (type == BtorSimState::Type::BITVEC);
  if (bv_state) btorsim_bv_free (bv_state);
  bv_state = bv;
}

void
BtorSimState::update (BtorSimArrayModel *am)
{
  assert (type == ARRAY);
  if (array_state) delete array_state;
  array_state = am;
}

void
BtorSimState::update (BtorSimState &s)
{
  switch (type)
  {
    case ARRAY:
      assert (s.type == ARRAY);
      update (s.array_state);
      break;
    case BtorSimState::Type::BITVEC:
      assert (s.type == BITVEC);
      update (s.bv_state);
      break;
    default: die ("Updating invalid state!");
  }
}

void
BtorSimState::remove ()
{
  switch (type)
  {
    case ARRAY:
      if (array_state) delete array_state;
      array_state = nullptr;
      break;
    case BtorSimState::Type::BITVEC:
      if (bv_state) btorsim_bv_free (bv_state);
      bv_state = nullptr;
      break;
    default: die ("Removing invalid state!");
  }
}

bool
BtorSimState::is_set ()
{
  switch (type)
  {
    case ARRAY: return array_state != nullptr;
    case BtorSimState::Type::BITVEC: return bv_state != nullptr;
    default:
      die ("Checking invalid state!");
      return false;  // compiler can't tell that die contains exit, complains
                     // about lack of return value
  }
}