Remove unused `Backtracker` (#7115)

backtrackable.h was defining a datastructure Backtracker, which was
a member in ArrayInfo and Info but it was not doing anything.

6 files changed, 25 insertions, 283 deletions

diff --git a/src/context/CMakeLists.txt b/src/context/CMakeLists.txt
index 73166462c..6cc066235 100644
--- a/src/context/CMakeLists.txt
+++ b/src/context/CMakeLists.txt
@@ -14,7 +14,6 @@
 ##
 
 set(LIBCONTEXT_SOURCES
-  backtrackable.h
   cddense_set.h
   cdhashmap.h
   cdhashmap_forward.h
diff --git a/src/context/backtrackable.h b/src/context/backtrackable.h
deleted file mode 100644
index 28654dbdf..000000000
--- a/src/context/backtrackable.h
+++ /dev/null
@@ -1,221 +0,0 @@
-/******************************************************************************
- * 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 */
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 4dc7201fb..aaacee8a0 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -22,15 +22,15 @@ namespace cvc5 {
 namespace theory {
 namespace arrays {
 
-Info::Info(context::Context* c, Backtracker<TNode>* bck)
+Info::Info(context::Context* c)
     : isNonLinear(c, false),
       rIntro1Applied(c, false),
-      modelRep(c,TNode()),
-      constArr(c,TNode()),
-      weakEquivPointer(c,TNode()),
-      weakEquivIndex(c,TNode()),
-      weakEquivSecondary(c,TNode()),
-      weakEquivSecondaryReason(c,TNode())
+      modelRep(c, TNode()),
+      constArr(c, TNode()),
+      weakEquivPointer(c, TNode()),
+      weakEquivIndex(c, TNode()),
+      weakEquivSecondary(c, TNode()),
+      weakEquivSecondaryReason(c, TNode())
 {
   indices = new(true)CTNodeList(c);
   stores = new(true)CTNodeList(c);
@@ -44,10 +44,8 @@ Info::~Info() {
 }
 
 ArrayInfo::ArrayInfo(context::Context* c,
-                     Backtracker<TNode>* b,
                      std::string statisticsPrefix)
     : ct(c),
-      bck(b),
       info_map(),
       d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
           statisticsPrefix + "mergeInfoTimer")),
@@ -67,7 +65,7 @@ ArrayInfo::ArrayInfo(context::Context* c,
           statisticsPrefix + "infoTableSize", info_map))
 {
   emptyList = new(true) CTNodeList(ct);
-  emptyInfo = new Info(ct, bck);
+  emptyInfo = new Info(ct);
 }
 
 ArrayInfo::~ArrayInfo() {
@@ -102,16 +100,6 @@ void printList (CTNodeList* list) {
   Trace("arrays-info")<<"] \n";
 }
 
-void printList (List<TNode>* list) {
-  List<TNode>::const_iterator it = list->begin();
-  Trace("arrays-info")<<"   [ ";
-  for (; it != list->end(); ++it)
-  {
-    Trace("arrays-info")<<(*it)<<" ";
-  }
-  Trace("arrays-info")<<"] \n";
-}
-
 void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
   std::set<TNode> temp;
   CTNodeList::const_iterator it;
@@ -138,7 +126,7 @@ void ArrayInfo::addIndex(const Node a, const TNode i) {
 
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_indices = temp_info->indices;
     temp_indices->push_back(i);
     info_map[a] = temp_info;
@@ -163,7 +151,7 @@ void ArrayInfo::addStore(const Node a, const TNode st){
 
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_store = temp_info->stores;
     temp_store->push_back(st);
     info_map[a]=temp_info;
@@ -186,7 +174,7 @@ void ArrayInfo::addInStore(const TNode a, const TNode b){
 
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_inst = temp_info->in_stores;
     temp_inst->push_back(b);
     info_map[a] = temp_info;
@@ -204,7 +192,7 @@ void ArrayInfo::setNonLinear(const TNode a) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->isNonLinear = true;
     info_map[a] = temp_info;
   } else {
@@ -218,7 +206,7 @@ void ArrayInfo::setRIntro1Applied(const TNode a) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->rIntro1Applied = true;
     info_map[a] = temp_info;
   } else {
@@ -232,7 +220,7 @@ void ArrayInfo::setModelRep(const TNode a, const TNode b) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->modelRep = b;
     info_map[a] = temp_info;
   } else {
@@ -246,7 +234,7 @@ void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->constArr = constArr;
     info_map[a] = temp_info;
   } else {
@@ -259,7 +247,7 @@ void ArrayInfo::setWeakEquivPointer(const TNode a, const TNode pointer) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->weakEquivPointer = pointer;
     info_map[a] = temp_info;
   } else {
@@ -272,7 +260,7 @@ void ArrayInfo::setWeakEquivIndex(const TNode a, const TNode index) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->weakEquivIndex = index;
     info_map[a] = temp_info;
   } else {
@@ -285,7 +273,7 @@ void ArrayInfo::setWeakEquivSecondary(const TNode a, const TNode secondary) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->weakEquivSecondary = secondary;
     info_map[a] = temp_info;
   } else {
@@ -298,7 +286,7 @@ void ArrayInfo::setWeakEquivSecondaryReason(const TNode a, const TNode reason) {
   Info* temp_info;
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_info = new Info(ct, bck);
+    temp_info = new Info(ct);
     temp_info->weakEquivSecondaryReason = reason;
     info_map[a] = temp_info;
   } else {
@@ -497,7 +485,7 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){
       CTNodeList* listb_st = (*itb).second->stores;
       CTNodeList* listb_inst = (*itb).second->in_stores;
 
-      Info* temp_info = new Info(ct, bck);
+      Info* temp_info = new Info(ct);
 
       mergeLists(temp_info->indices, listb_i);
       mergeLists(temp_info->stores, listb_st);
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 42c6e7387..534bb2ae5 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -22,8 +22,8 @@
 #include <tuple>
 #include <unordered_map>
 
-#include "context/backtrackable.h"
 #include "context/cdlist.h"
+#include "context/cdo.h"
 #include "expr/node.h"
 #include "util/statistics_stats.h"
 
@@ -45,7 +45,6 @@ struct RowLemmaTypeHashFunction {
 };/* struct RowLemmaTypeHashFunction */
 
 void printList (CTNodeList* list);
-void printList( List<TNode>* list);
 
 bool inList(const CTNodeList* l, const TNode el);
 
@@ -69,7 +68,7 @@ public:
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck);
+  Info(context::Context* c);
   ~Info();
 
   /**
@@ -100,7 +99,6 @@ typedef std::unordered_map<Node, Info*> CNodeInfoMap;
 class ArrayInfo {
 private:
   context::Context* ct;
-  Backtracker<TNode>* bck;
   CNodeInfoMap info_map;
 
   CTNodeList* emptyList;
@@ -130,27 +128,8 @@ private:
 
 public:
   const Info* emptyInfo;
-/*
-  ArrayInfo(): ct(NULl), info
-    d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
-    d_avgIndexListLength("theory::arrays::avgIndexListLength"),
-    d_avgStoresListLength("theory::arrays::avgStoresListLength"),
-    d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
-    d_listsCount("theory::arrays::listsCount",0),
-    d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
-    d_maxList("theory::arrays::maxList",0),
-    d_tableSize("theory::arrays::infoTableSize", info_map) {
-  currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
-  currentStatisticsRegistry()->registerStat(&d_avgIndexListLength);
-  currentStatisticsRegistry()->registerStat(&d_avgStoresListLength);
-  currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
-  currentStatisticsRegistry()->registerStat(&d_listsCount);
-  currentStatisticsRegistry()->registerStat(&d_callsMergeInfo);
-  currentStatisticsRegistry()->registerStat(&d_maxList);
-  currentStatisticsRegistry()->registerStat(&d_tableSize);
-  }*/
-
-  ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix = "");
+
+  ArrayInfo(context::Context* c, std::string statisticsPrefix = "");
 
   ~ArrayInfo();
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0f0d24cde..48b6573f8 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -90,8 +90,7 @@ TheoryArrays::TheoryArrays(Env& env,
       d_isPreRegistered(getSatContext()),
       d_mayEqualEqualityEngine(getSatContext(), name + "mayEqual", true),
       d_notify(*this),
-      d_backtracker(getSatContext()),
-      d_infoMap(getSatContext(), &d_backtracker, name),
+      d_infoMap(getSatContext(), name),
       d_mergeQueue(getSatContext()),
       d_mergeInProgress(false),
       d_RowQueue(getSatContext()),
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d255e44f1..b53d0e77e 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -361,8 +361,6 @@ class TheoryArrays : public Theory {
    * type array to an Info pointer that keeps track of information useful to axiom
    * instantiation
    */
-
-  Backtracker<TNode> d_backtracker;
   ArrayInfo d_infoMap;
 
   context::CDQueue<Node> d_mergeQueue;