From ef80ba053b022ec624ee93a29a4dbc674226b3d4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 2 Sep 2021 05:26:28 -0700 Subject: 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. --- src/context/CMakeLists.txt | 1 - src/context/backtrackable.h | 221 ------------------------------------ src/theory/arrays/array_info.cpp | 52 ++++----- src/theory/arrays/array_info.h | 29 +---- src/theory/arrays/theory_arrays.cpp | 3 +- src/theory/arrays/theory_arrays.h | 2 - 6 files changed, 25 insertions(+), 283 deletions(-) delete mode 100644 src/context/backtrackable.h 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 -#include -#include "context/cdo.h" - -namespace cvc5 { - -template class List; -template class List_iterator; -template class Backtracker; - -template -class ListNode { -private: - T data; - ListNode* next; - - bool empty; - ListNode(const T& t, ListNode* n, bool e = false) : data(t), next(n), empty(e) {} - ~ListNode() { - // maybe set to NULL - delete next; - } - - friend class List; - friend class List_iterator; -};/* class ListNode */ - -template -class List_iterator : public std::iterator { - friend class List; - -public: - const T& operator*(); - List_iterator& operator++(); - List_iterator operator++(int); - bool operator!=(const List_iterator & other) const; - -private: - const ListNode* pointee; - List_iterator(const ListNode* p) : pointee(p) {} - -};/* class List_iterator */ - -template -const T& List_iterator::operator*() { - return pointee->data; -} - -template -List_iterator& List_iterator::operator++() { - Assert(pointee != NULL); - pointee = pointee->next; - while(pointee != NULL && pointee->empty ) { - pointee = pointee->next; - } - return *this; -} - -template -List_iterator List_iterator::operator++(int) { - List_iterator it = *this; - ++*this; - return it; -} - -template -bool List_iterator::operator!=(const List_iterator& 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 should store pointers! -template -class List { - ListNode* head; - ListNode* tail; - ListNode* ptr_to_head; - bool uninitialized; - Backtracker* bck; - List (const List&) {} -public: - List(Backtracker* b) : ptr_to_head(NULL), uninitialized(true), bck(b) { - head = tail = (ListNode*)calloc(1,sizeof(ListNode)); - head->next = NULL; - head->empty = true; - } - ~List() {delete head;} - bool empty() { - bck->checkConsistency(); - return head == NULL; - } - void append(const T& d); - //typedef List_iterator iterator; - typedef List_iterator const_iterator; - - const_iterator begin() { - bck->checkConsistency(); - if(head->empty) { - ListNode* 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(temp); - } - return List_iterator(head); - } - - const_iterator end() { - bck->checkConsistency(); - return List_iterator(NULL); - } - void concat(List* other); - void unconcat(List* other); -};/* class List */ - -template -void List::append (const T& d) { - bck->checkConsistency(); - - if(uninitialized) { - new(head)ListNode (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* new_node = new ListNode(d, head); - head = new_node; - } - - if(ptr_to_head != NULL) { - ptr_to_head->next = head; - } -} - -template -void List::concat (List* 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 -void List::unconcat(List* 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 Backtracker { - friend class List; - std::vector*,List*> > undo_stack; - - int curr_level; - context::CDO pop_level; - - void checkConsistency(); - void notifyConcat(List* a, List* b); -public: - Backtracker(context::Context* c) : undo_stack(), curr_level(0), pop_level(c, 0) {} - ~Backtracker() {} - -};/* class Backtrackable */ - -template void Backtracker::notifyConcat(List* a, List* b) { - curr_level++; - pop_level.set(pop_level.get()+1); - undo_stack.push_back( std::make_pair(a, b)); -} - -template void Backtracker::checkConsistency() { - if( curr_level == pop_level || pop_level == -1) { - return; - } - Assert(curr_level > pop_level); - - while (curr_level > pop_level) { - curr_level--; - List* l1 = undo_stack[curr_level].first; - List* 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* 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* 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* list) { - List::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 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 #include -#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* list); bool inList(const CTNodeList* l, const TNode el); @@ -69,7 +68,7 @@ public: CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker* bck); + Info(context::Context* c); ~Info(); /** @@ -100,7 +99,6 @@ typedef std::unordered_map CNodeInfoMap; class ArrayInfo { private: context::Context* ct; - Backtracker* 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* 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 d_backtracker; ArrayInfo d_infoMap; context::CDQueue d_mergeQueue; -- cgit v1.2.3