##
set(LIBCONTEXT_SOURCES
- backtrackable.h
cddense_set.h
cdhashmap.h
cdhashmap_forward.h
+++ /dev/null
-/******************************************************************************
- * 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 */
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);
}
ArrayInfo::ArrayInfo(context::Context* c,
- Backtracker<TNode>* b,
std::string statisticsPrefix)
: ct(c),
- bck(b),
info_map(),
d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
statisticsPrefix + "mergeInfoTimer")),
statisticsPrefix + "infoTableSize", info_map))
{
emptyList = new(true) CTNodeList(ct);
- emptyInfo = new Info(ct, bck);
+ emptyInfo = new Info(ct);
}
ArrayInfo::~ArrayInfo() {
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;
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;
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;
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;
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 {
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 {
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 {
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 {
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 {
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 {
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 {
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 {
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);
#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"
};/* struct RowLemmaTypeHashFunction */
void printList (CTNodeList* list);
-void printList( List<TNode>* list);
bool inList(const CTNodeList* l, const TNode el);
CTNodeList* stores;
CTNodeList* in_stores;
- Info(context::Context* c, Backtracker<TNode>* bck);
+ Info(context::Context* c);
~Info();
/**
class ArrayInfo {
private:
context::Context* ct;
- Backtracker<TNode>* bck;
CNodeInfoMap info_map;
CTNodeList* emptyList;
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();
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()),
* 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;
projects / cvc5.git / commitdiff