GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/backtrackable.h Lines: 2 41 4.9 %
Date: 2021-03-23 Branches: 1 84 1.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file backtrackable.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Contains a backtrackable list
13
 **
14
 ** Contains a backtrackable list.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__UTIL__BACKTRACKABLE_H
20
#define CVC4__UTIL__BACKTRACKABLE_H
21
22
#include <cstdlib>
23
#include <vector>
24
#include "context/cdo.h"
25
26
namespace CVC4 {
27
28
template <class T> class List;
29
template <class T> class List_iterator;
30
template <class T> class Backtracker;
31
32
template <class T>
33
class ListNode {
34
private:
35
  T data;
36
  ListNode<T>* next;
37
38
  bool empty;
39
  ListNode(const T& t, ListNode<T>* n, bool e = false) : data(t), next(n), empty(e) {}
40
  ~ListNode() {
41
    // maybe set to NULL
42
    delete next;
43
  }
44
45
  friend class List<T>;
46
  friend class List_iterator<T>;
47
};/* class ListNode<T> */
48
49
template <class T>
50
class List_iterator : public std::iterator <std::forward_iterator_tag, T> {
51
  friend class List<T>;
52
53
public:
54
  const T& operator*();
55
  List_iterator<T>& operator++();
56
  List_iterator<T> operator++(int);
57
  bool operator!=(const List_iterator<T> & other) const;
58
59
private:
60
  const ListNode<T>* pointee;
61
  List_iterator(const ListNode<T>* p) : pointee(p) {}
62
63
};/* class List_iterator<T> */
64
65
template <class T>
66
const T& List_iterator<T>::operator*() {
67
  return pointee->data;
68
}
69
70
template <class T>
71
List_iterator<T>& List_iterator<T>::operator++() {
72
  Assert(pointee != NULL);
73
  pointee = pointee->next;
74
  while(pointee != NULL && pointee->empty ) {
75
    pointee = pointee->next;
76
  }
77
  return *this;
78
}
79
80
template <class T>
81
List_iterator<T> List_iterator<T>::operator++(int) {
82
  List_iterator<T> it = *this;
83
  ++*this;
84
  return it;
85
}
86
87
template <class T>
88
bool List_iterator<T>::operator!=(const List_iterator<T>& other) const {
89
  return (this->pointee != other.pointee);
90
}
91
92
// !! for the backtracking to work the lists must be allocated on the heap
93
// therefore the hashmap from TNode to List<TNode> should store pointers!
94
template <class T>
95
class List {
96
  ListNode<T>* head;
97
  ListNode<T>* tail;
98
  ListNode<T>* ptr_to_head;
99
  bool uninitialized;
100
  Backtracker<T>* bck;
101
  List (const List&) {}
102
public:
103
  List(Backtracker<T>* b) : ptr_to_head(NULL), uninitialized(true), bck(b) {
104
    head = tail = (ListNode<T>*)calloc(1,sizeof(ListNode<T>));
105
    head->next = NULL;
106
    head->empty = true;
107
  }
108
  ~List() {delete head;}
109
  bool empty() {
110
    bck->checkConsistency();
111
    return head == NULL;
112
  }
113
  void append(const T& d);
114
  //typedef List_iterator<T> iterator;
115
  typedef List_iterator<T> const_iterator;
116
117
  const_iterator begin() {
118
    bck->checkConsistency();
119
    if(head->empty) {
120
      ListNode<T>* temp = head;
121
      // if the head is empty return the first non-empty element or NULL
122
      while(temp != NULL && temp->empty ) {
123
        temp = temp->next;
124
      }
125
      return List_iterator<T>(temp);
126
    }
127
    return List_iterator<T>(head);
128
  }
129
130
  const_iterator end() {
131
    bck->checkConsistency();
132
    return List_iterator<T>(NULL);
133
  }
134
  void concat(List<T>* other);
135
  void unconcat(List<T>* other);
136
};/* class List */
137
138
template <class T>
139
void List<T>::append (const T& d) {
140
  bck->checkConsistency();
141
142
  if(uninitialized) {
143
    new(head)ListNode<T> (d, head->next);
144
    //head->data = d;
145
    head->empty = false;
146
    //Assert(tail == head); FIXME: do I need this because this list might be empty but append to another one
147
    uninitialized = false;
148
149
  } else {
150
    ListNode<T>* new_node = new ListNode<T>(d, head);
151
    head = new_node;
152
  }
153
154
  if(ptr_to_head != NULL) {
155
    ptr_to_head->next = head;
156
  }
157
}
158
159
template <class T>
160
void List<T>::concat (List<T>* other) {
161
  bck->checkConsistency();
162
  bck->notifyConcat(this, other);
163
  Assert(tail->next == NULL);
164
  tail->next = other->head;
165
  Assert(other->ptr_to_head == NULL);
166
  other->ptr_to_head = tail;
167
  tail = other->tail;
168
}
169
170
template <class T>
171
void List<T>::unconcat(List<T>* other) {
172
  // we do not need to check consistency since this is only called by the
173
  // Backtracker when we are inconsistent
174
  Assert(other->ptr_to_head != NULL);
175
  other->ptr_to_head->next = NULL;
176
  tail = other->ptr_to_head;
177
  other->ptr_to_head = NULL;
178
}
179
180
/* Backtrackable Table */
181
182
template <class T>
183
class Backtracker {
184
  friend class List<T>;
185
  std::vector<std::pair<List<T>*,List<T>*> > undo_stack;
186
187
  int curr_level;
188
  context::CDO<int> pop_level;
189
190
  void checkConsistency();
191
  void notifyConcat(List<T>* a, List<T>* b);
192
public:
193
8997
  Backtracker(context::Context* c) : undo_stack(), curr_level(0), pop_level(c, 0) {}
194
8994
  ~Backtracker() {}
195
196
};/* class Backtrackable */
197
198
template <class T>  void Backtracker<T>::notifyConcat(List<T>* a, List<T>* b) {
199
  curr_level++;
200
  pop_level.set(pop_level.get()+1);
201
  undo_stack.push_back( std::make_pair(a, b));
202
}
203
204
template <class T> void Backtracker<T>::checkConsistency() {
205
  if( curr_level == pop_level || pop_level == -1) {
206
    return;
207
  }
208
  Assert(curr_level > pop_level);
209
210
  while (curr_level > pop_level) {
211
    curr_level--;
212
    List<T>* l1 = undo_stack[curr_level].first;
213
    List<T>* l2 = undo_stack[curr_level].second;
214
    l1->unconcat(l2);
215
    undo_stack.pop_back();
216
  }
217
  Assert(curr_level == pop_level);
218
}
219
220
}/* CVC4 namespace */
221
222
#endif /* CVC4__UTIL__BACKTRACKABLE_H */