summaryrefslogtreecommitdiff
path: root/src/context
diff options
context:
space:
mode:
Diffstat (limited to 'src/context')
-rw-r--r--src/context/backtrackable.h222
-rw-r--r--src/context/cdchunk_list.h3
-rw-r--r--src/context/cdhashmap.h6
-rw-r--r--src/context/cdhashset.h3
-rw-r--r--src/context/cdinsert_hashmap.h15
-rw-r--r--src/context/cdlist.h5
-rw-r--r--src/context/cdo.h3
-rw-r--r--src/context/cdtrail_hashmap.h13
-rw-r--r--src/context/cdvector.h6
-rw-r--r--src/context/context.cpp3
-rw-r--r--src/context/context.h4
-rw-r--r--src/context/context_mm.cpp5
12 files changed, 258 insertions, 30 deletions
diff --git a/src/context/backtrackable.h b/src/context/backtrackable.h
new file mode 100644
index 000000000..5492dd8b5
--- /dev/null
+++ b/src/context/backtrackable.h
@@ -0,0 +1,222 @@
+/********************* */
+/*! \file backtrackable.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Contains a backtrackable list
+ **
+ ** Contains a backtrackable list.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UTIL__BACKTRACKABLE_H
+#define __CVC4__UTIL__BACKTRACKABLE_H
+
+#include <cstdlib>
+#include <vector>
+#include "context/cdo.h"
+
+namespace CVC4 {
+
+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);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UTIL__BACKTRACKABLE_H */
diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
index 8c2e4066e..62a87ffcc 100644
--- a/src/context/cdchunk_list.h
+++ b/src/context/cdchunk_list.h
@@ -24,9 +24,10 @@
#include <iterator>
#include <memory>
+#include "base/cvc4_assert.h"
#include "context/context.h"
#include "context/context_mm.h"
-#include "util/cvc4_assert.h"
+
namespace CVC4 {
namespace context {
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 338c46b0d..51fd3b411 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -95,12 +95,12 @@
#ifndef __CVC4__CONTEXT__CDHASHMAP_H
#define __CVC4__CONTEXT__CDHASHMAP_H
-#include <vector>
-#include <iterator>
#include <ext/hash_map>
+#include <iterator>
+#include <vector>
+#include "base/cvc4_assert.h"
#include "context/context.h"
-#include "util/cvc4_assert.h"
#include "context/cdhashmap_forward.h"
namespace CVC4 {
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index 76bab5a94..533a09a0a 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -19,9 +19,10 @@
#ifndef __CVC4__CONTEXT__CDHASHSET_H
#define __CVC4__CONTEXT__CDHASHSET_H
+#include "base/cvc4_assert.h"
#include "context/context.h"
#include "context/cdinsert_hashmap.h"
-#include "util/cvc4_assert.h"
+
namespace CVC4 {
namespace context {
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index 1c8f94143..b65784ddf 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -33,16 +33,17 @@
#include "cvc4_private.h"
-#include "context/context.h"
-#include "context/cdinsert_hashmap_forward.h"
-#include <utility>
-#include <ext/hash_map>
+#include <boost/static_assert.hpp>
#include <deque>
-#include "util/cvc4_assert.h"
-#include "util/output.h"
+#include <ext/hash_map>
+#include <utility>
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "context/context.h"
+#include "context/cdinsert_hashmap_forward.h"
#include "expr/node.h"
-#include <boost/static_assert.hpp>
+
#pragma once
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 7c673a4be..dbc00bd69 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -20,17 +20,16 @@
#ifndef __CVC4__CONTEXT__CDLIST_H
#define __CVC4__CONTEXT__CDLIST_H
+#include <boost/static_assert.hpp>
#include <iterator>
#include <memory>
#include <string>
#include <sstream>
+#include "base/cvc4_assert.h"
#include "context/context.h"
#include "context/context_mm.h"
#include "context/cdlist_forward.h"
-#include "util/cvc4_assert.h"
-
-#include <boost/static_assert.hpp>
namespace CVC4 {
namespace context {
diff --git a/src/context/cdo.h b/src/context/cdo.h
index 5fa0a4d8b..486626ae5 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -19,8 +19,9 @@
#ifndef __CVC4__CONTEXT__CDO_H
#define __CVC4__CONTEXT__CDO_H
+#include "base/cvc4_assert.h"
#include "context/context.h"
-#include "util/cvc4_assert.h"
+
namespace CVC4 {
namespace context {
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index f4220ef43..befd396a9 100644
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -44,17 +44,16 @@
#pragma once
-#include "context/context.h"
-#include "context/cdtrail_hashmap_forward.h"
-#include <utility>
+#include <boost/static_assert.hpp>
#include <ext/hash_map>
#include <deque>
-#include "util/cvc4_assert.h"
-#include "util/output.h"
+#include <utility>
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "context/context.h"
+#include "context/cdtrail_hashmap_forward.h"
#include "expr/node.h"
-#include <boost/static_assert.hpp>
-
namespace CVC4 {
namespace context {
diff --git a/src/context/cdvector.h b/src/context/cdvector.h
index 30699670f..fe8f77c6d 100644
--- a/src/context/cdvector.h
+++ b/src/context/cdvector.h
@@ -20,11 +20,11 @@
#ifndef __CVC4__CONTEXT__CDVECTOR_H
#define __CVC4__CONTEXT__CDVECTOR_H
-#include "context/context.h"
-#include "context/cdlist.h"
-#include "util/cvc4_assert.h"
#include <vector>
+#include "base/cvc4_assert.h"
+#include "context/context.h"
+#include "context/cdlist.h"
namespace CVC4 {
namespace context {
diff --git a/src/context/context.cpp b/src/context/context.cpp
index c427e89c9..99a98e63f 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -18,8 +18,9 @@
#include <iostream>
#include <vector>
+#include "base/cvc4_assert.h"
#include "context/context.h"
-#include "util/cvc4_assert.h"
+
namespace CVC4 {
namespace context {
diff --git a/src/context/context.h b/src/context/context.h
index 9c631b202..b88f36786 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -26,8 +26,10 @@
#include <new>
#include <typeinfo>
+#include "base/cvc4_assert.h"
+#include "base/output.h"
#include "context/context_mm.h"
-#include "util/cvc4_assert.h"
+
namespace CVC4 {
namespace context {
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index e7b234a95..f30413650 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -19,9 +19,10 @@
#include <vector>
#include <deque>
#include <new>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
#include "context/context_mm.h"
-#include "util/cvc4_assert.h"
-#include "util/output.h"
namespace CVC4 {
namespace context {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback