Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/backtrackable.h	Lines:	2	41	4.9 %
Date:	2021-05-22	Branches:	1	84	1.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Contains a backtrackable list.
 */

#include "cvc5_private.h"

#ifndef CVC5__UTIL__BACKTRACKABLE_H
#define CVC5__UTIL__BACKTRACKABLE_H

#include <cstdlib>
#include <vector>
#include "context/cdo.h"

namespace cvc5 {

template <class T> class List;
template <class T> class List_iterator;
template <class T> class Backtracker;

template <class T>
class ListNode {
private:
  T data;
  ListNode<T>* next;

  bool empty;
  ListNode(const T& t, ListNode<T>* n, bool e = false) : data(t), next(n), empty(e) {}
  ~ListNode() {
    // maybe set to NULL
    delete next;
  }

  friend class List<T>;
  friend class List_iterator<T>;
};/* class ListNode<T> */

template <class T>
class List_iterator : public std::iterator <std::forward_iterator_tag, T> {
  friend class List<T>;

public:
  const T& operator*();
  List_iterator<T>& operator++();
  List_iterator<T> operator++(int);
  bool operator!=(const List_iterator<T> & other) const;

private:
  const ListNode<T>* pointee;
  List_iterator(const ListNode<T>* p) : pointee(p) {}

};/* class List_iterator<T> */

template <class T>
const T& List_iterator<T>::operator*() {
  return pointee->data;
}

template <class T>
List_iterator<T>& List_iterator<T>::operator++() {
  Assert(pointee != NULL);
  pointee = pointee->next;
  while(pointee != NULL && pointee->empty ) {
    pointee = pointee->next;
  }
  return *this;
}

template <class T>
List_iterator<T> List_iterator<T>::operator++(int) {
  List_iterator<T> it = *this;
  ++*this;
  return it;
}

template <class T>
bool List_iterator<T>::operator!=(const List_iterator<T>& other) const {
  return (this->pointee != other.pointee);
}

// !! for the backtracking to work the lists must be allocated on the heap
// therefore the hashmap from TNode to List<TNode> should store pointers!
template <class T>
class List {
  ListNode<T>* head;
  ListNode<T>* tail;
  ListNode<T>* ptr_to_head;
  bool uninitialized;
  Backtracker<T>* bck;
  List (const List&) {}
public:
  List(Backtracker<T>* b) : ptr_to_head(NULL), uninitialized(true), bck(b) {
    head = tail = (ListNode<T>*)calloc(1,sizeof(ListNode<T>));
    head->next = NULL;
    head->empty = true;
  }
  ~List() {delete head;}
  bool empty() {
    bck->checkConsistency();
    return head == NULL;
  }
  void append(const T& d);
  //typedef List_iterator<T> iterator;
  typedef List_iterator<T> const_iterator;

  const_iterator begin() {
    bck->checkConsistency();
    if(head->empty) {
      ListNode<T>* temp = head;
      // if the head is empty return the first non-empty element or NULL
      while(temp != NULL && temp->empty ) {
        temp = temp->next;
      }
      return List_iterator<T>(temp);
    }
    return List_iterator<T>(head);
  }

  const_iterator end() {
    bck->checkConsistency();
    return List_iterator<T>(NULL);
  }
  void concat(List<T>* other);
  void unconcat(List<T>* other);
};/* class List */

template <class T>
void List<T>::append (const T& d) {
  bck->checkConsistency();

  if(uninitialized) {
    new(head)ListNode<T> (d, head->next);
    //head->data = d;
    head->empty = false;
    //Assert(tail == head); FIXME: do I need this because this list might be empty but append to another one
    uninitialized = false;

  } else {
    ListNode<T>* new_node = new ListNode<T>(d, head);
    head = new_node;
  }

  if(ptr_to_head != NULL) {
    ptr_to_head->next = head;
  }
}

template <class T>
void List<T>::concat (List<T>* other) {
  bck->checkConsistency();
  bck->notifyConcat(this, other);
  Assert(tail->next == NULL);
  tail->next = other->head;
  Assert(other->ptr_to_head == NULL);
  other->ptr_to_head = tail;
  tail = other->tail;
}

template <class T>
void List<T>::unconcat(List<T>* other) {
  // we do not need to check consistency since this is only called by the
  // Backtracker when we are inconsistent
  Assert(other->ptr_to_head != NULL);
  other->ptr_to_head->next = NULL;
  tail = other->ptr_to_head;
  other->ptr_to_head = NULL;
}

/* Backtrackable Table */

template <class T>
class Backtracker {
  friend class List<T>;
  std::vector<std::pair<List<T>*,List<T>*> > undo_stack;

  int curr_level;
  context::CDO<int> pop_level;

  void checkConsistency();
  void notifyConcat(List<T>* a, List<T>* b);
public:
  Backtracker(context::Context* c) : undo_stack(), curr_level(0), pop_level(c, 0) {}
  ~Backtracker() {}

};/* class Backtrackable */

template <class T>  void Backtracker<T>::notifyConcat(List<T>* a, List<T>* b) {
  curr_level++;
  pop_level.set(pop_level.get()+1);
  undo_stack.push_back( std::make_pair(a, b));
}

template <class T> void Backtracker<T>::checkConsistency() {
  if( curr_level == pop_level || pop_level == -1) {
    return;
  }
  Assert(curr_level > pop_level);

  while (curr_level > pop_level) {
    curr_level--;
    List<T>* l1 = undo_stack[curr_level].first;
    List<T>* l2 = undo_stack[curr_level].second;
    l1->unconcat(l2);
    undo_stack.pop_back();
  }
  Assert(curr_level == pop_level);
}

}  // namespace cvc5

#endif /* CVC5__UTIL__BACKTRACKABLE_H */


Generated by: GCOVR (Version 3.2)

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