Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/array_info.cpp	Lines:	203	302	67.2 %
Date:	2021-05-22	Branches:	292	962	30.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Clark Barrett, Tim King
 *
 * 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 additional classes to store context dependent information
 * for each term of type array.
 */

#include "theory/arrays/array_info.h"

#include "smt/smt_statistics_registry.h"

namespace cvc5 {
namespace theory {
namespace arrays {

Info::Info(context::Context* c, Backtracker<TNode>* bck)
    : isNonLinear(c, false),
      rIntro1Applied(c, false),
      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);
  in_stores = new(true)CTNodeList(c);
}

Info::~Info() {
  indices->deleteSelf();
  stores->deleteSelf();
  in_stores->deleteSelf();
}

ArrayInfo::ArrayInfo(context::Context* c,
                     Backtracker<TNode>* b,
                     std::string statisticsPrefix)
    : ct(c),
      bck(b),
      info_map(),
      d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
          statisticsPrefix + "mergeInfoTimer")),
      d_avgIndexListLength(smtStatisticsRegistry().registerAverage(
          statisticsPrefix + "avgIndexListLength")),
      d_avgStoresListLength(smtStatisticsRegistry().registerAverage(
          statisticsPrefix + "avgStoresListLength")),
      d_avgInStoresListLength(smtStatisticsRegistry().registerAverage(
          statisticsPrefix + "avgInStoresListLength")),
      d_listsCount(
          smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")),
      d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix
                                                           + "callsMergeInfo")),
      d_maxList(
          smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")),
      d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>(
          statisticsPrefix + "infoTableSize", info_map))
{
  emptyList = new(true) CTNodeList(ct);
  emptyInfo = new Info(ct, bck);
}

ArrayInfo::~ArrayInfo() {
  CNodeInfoMap::iterator it = info_map.begin();
  for (; it != info_map.end(); ++it)
  {
    if((*it).second!= emptyInfo) {
      delete (*it).second;
    }
  }
  emptyList->deleteSelf();
  delete emptyInfo;
}

bool inList(const CTNodeList* l, const TNode el) {
  CTNodeList::const_iterator it = l->begin();
  for (; it != l->end(); ++it)
  {
    if(*it == el)
      return true;
  }
  return false;
}

void printList (CTNodeList* list) {
  CTNodeList::const_iterator it = list->begin();
  Trace("arrays-info")<<"   [ ";
  for (; it != list->end(); ++it)
  {
    Trace("arrays-info")<<(*it)<<" ";
  }
  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;
  for (it = la->begin(); it != la->end(); ++it)
  {
    temp.insert((*it));
  }

  for (it = lb->begin(); it != lb->end(); ++it)
  {
    if(temp.count(*it) == 0) {
      la->push_back(*it);
    }
  }
}

void ArrayInfo::addIndex(const Node a, const TNode i) {
  Assert(a.getType().isArray());
  Assert(!i.getType().isArray());  // temporary for flat arrays

  Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
  CTNodeList* temp_indices;
  Info* temp_info;

  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_indices = temp_info->indices;
    temp_indices->push_back(i);
    info_map[a] = temp_info;
  } else {
    temp_indices = (*it).second->indices;
    if (! inList(temp_indices, i)) {
      temp_indices->push_back(i);
    }
  }
  if(Trace.isOn("arrays-ind")) {
    printList((*(info_map.find(a))).second->indices);
  }

}

void ArrayInfo::addStore(const Node a, const TNode st){
  Assert(a.getType().isArray());
  Assert(st.getKind() == kind::STORE);  // temporary for flat arrays

  CTNodeList* temp_store;
  Info* temp_info;

  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_store = temp_info->stores;
    temp_store->push_back(st);
    info_map[a]=temp_info;
  } else {
    temp_store = (*it).second->stores;
    if(! inList(temp_store, st)) {
      temp_store->push_back(st);
    }
  }
};


void ArrayInfo::addInStore(const TNode a, const TNode b){
  Trace("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
  Assert(a.getType().isArray());
  Assert(b.getType().isArray());

  CTNodeList* temp_inst;
  Info* temp_info;

  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_inst = temp_info->in_stores;
    temp_inst->push_back(b);
    info_map[a] = temp_info;
  } else {
    temp_inst = (*it).second->in_stores;
    if(! inList(temp_inst, b)) {
      temp_inst->push_back(b);
    }
  }
};


void ArrayInfo::setNonLinear(const TNode a) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->isNonLinear = true;
    info_map[a] = temp_info;
  } else {
    (*it).second->isNonLinear = true;
  }

}

void ArrayInfo::setRIntro1Applied(const TNode a) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->rIntro1Applied = true;
    info_map[a] = temp_info;
  } else {
    (*it).second->rIntro1Applied = true;
  }

}

void ArrayInfo::setModelRep(const TNode a, const TNode b) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->modelRep = b;
    info_map[a] = temp_info;
  } else {
    (*it).second->modelRep = b;
  }

}

void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->constArr = constArr;
    info_map[a] = temp_info;
  } else {
    (*it).second->constArr = constArr;
  }
}

void ArrayInfo::setWeakEquivPointer(const TNode a, const TNode pointer) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->weakEquivPointer = pointer;
    info_map[a] = temp_info;
  } else {
    (*it).second->weakEquivPointer = pointer;
  }
}

void ArrayInfo::setWeakEquivIndex(const TNode a, const TNode index) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->weakEquivIndex = index;
    info_map[a] = temp_info;
  } else {
    (*it).second->weakEquivIndex = index;
  }
}

void ArrayInfo::setWeakEquivSecondary(const TNode a, const TNode secondary) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->weakEquivSecondary = secondary;
    info_map[a] = temp_info;
  } else {
    (*it).second->weakEquivSecondary = secondary;
  }
}

void ArrayInfo::setWeakEquivSecondaryReason(const TNode a, const TNode reason) {
  Assert(a.getType().isArray());
  Info* temp_info;
  CNodeInfoMap::iterator it = info_map.find(a);
  if(it == info_map.end()) {
    temp_info = new Info(ct, bck);
    temp_info->weakEquivSecondaryReason = reason;
    info_map[a] = temp_info;
  } else {
    (*it).second->weakEquivSecondaryReason = reason;
  }
}

/**
 * Returns the information associated with TNode a
 */

const Info* ArrayInfo::getInfo(const TNode a) const{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
      return (*it).second;
  }
  return emptyInfo;
}

const bool ArrayInfo::isNonLinear(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->isNonLinear;
  }
  return false;
}

const bool ArrayInfo::rIntro1Applied(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->rIntro1Applied;
  }
  return false;
}

const TNode ArrayInfo::getModelRep(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->modelRep;
  }
  return TNode();
}

const TNode ArrayInfo::getConstArr(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->constArr;
  }
  return TNode();
}

const TNode ArrayInfo::getWeakEquivPointer(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->weakEquivPointer;
  }
  return TNode();
}

const TNode ArrayInfo::getWeakEquivIndex(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->weakEquivIndex;
  }
  return TNode();
}

const TNode ArrayInfo::getWeakEquivSecondary(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->weakEquivSecondary;
  }
  return TNode();
}

const TNode ArrayInfo::getWeakEquivSecondaryReason(const TNode a) const
{
  CNodeInfoMap::const_iterator it = info_map.find(a);

  if(it!= info_map.end()) {
    return (*it).second->weakEquivSecondaryReason;
  }
  return TNode();
}

const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
  CNodeInfoMap::const_iterator it = info_map.find(a);
  if(it!= info_map.end()) {
    return (*it).second->indices;
  }
  return emptyList;
}

const CTNodeList* ArrayInfo::getStores(const TNode a) const{
  CNodeInfoMap::const_iterator it = info_map.find(a);
  if(it!= info_map.end()) {
    return (*it).second->stores;
  }
  return emptyList;
}

const CTNodeList* ArrayInfo::getInStores(const TNode a) const{
  CNodeInfoMap::const_iterator it = info_map.find(a);
  if(it!= info_map.end()) {
    return (*it).second->in_stores;
  }
  return emptyList;
}


void ArrayInfo::mergeInfo(const TNode a, const TNode b){
  // can't have assertion that find(b) = a !
  TimerStat::CodeTimer codeTimer(d_mergeInfoTimer);
  ++d_callsMergeInfo;

  Trace("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
  Trace("arrays-mergei")<<"                      and "<<b<<"\n";

  CNodeInfoMap::iterator ita = info_map.find(a);
  CNodeInfoMap::iterator itb = info_map.find(b);

  if(ita != info_map.end()) {
    Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
    if(Trace.isOn("arrays-mergei"))
      (*ita).second->print();

    if(itb != info_map.end()) {
      Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
      if(Trace.isOn("arrays-mergei"))
        (*itb).second->print();

      CTNodeList* lista_i = (*ita).second->indices;
      CTNodeList* lista_st = (*ita).second->stores;
      CTNodeList* lista_inst = (*ita).second->in_stores;


      CTNodeList* listb_i = (*itb).second->indices;
      CTNodeList* listb_st = (*itb).second->stores;
      CTNodeList* listb_inst = (*itb).second->in_stores;

      mergeLists(lista_i, listb_i);
      mergeLists(lista_st, listb_st);
      mergeLists(lista_inst, listb_inst);

      /* sketchy stats */

      //FIXME
      int s = 0;//lista_i->size();
      d_maxList.maxAssign(s);


      if(s!= 0) {
        d_avgIndexListLength << s;
        ++d_listsCount;
      }
      s = lista_st->size();
      d_maxList.maxAssign(s);
      if(s!= 0) {
        d_avgStoresListLength << s;
        ++d_listsCount;
      }

      s = lista_inst->size();
      d_maxList.maxAssign(s);
      if(s!=0) {
        d_avgInStoresListLength << s;
        ++d_listsCount;
      }

      /* end sketchy stats */

    }

  } else {
    Trace("arrays-mergei")<<" First element has no info \n";
    if(itb != info_map.end()) {
      Trace("arrays-mergei")<<" adding second element's info \n";
      (*itb).second->print();

      CTNodeList* listb_i = (*itb).second->indices;
      CTNodeList* listb_st = (*itb).second->stores;
      CTNodeList* listb_inst = (*itb).second->in_stores;

      Info* temp_info = new Info(ct, bck);

      mergeLists(temp_info->indices, listb_i);
      mergeLists(temp_info->stores, listb_st);
      mergeLists(temp_info->in_stores, listb_inst);
      info_map[a] = temp_info;

    } else {
    Trace("arrays-mergei")<<" Second element has no info \n";
    }

   }
  Trace("arrays-mergei")<<"Arrays::mergeInfo done \n";

}

}  // namespace arrays
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Clark Barrett, Tim King
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 additional classes to store context dependent information
14		* for each term of type array.
15		*/
16
17		#include "theory/arrays/array_info.h"
18
19		#include "smt/smt_statistics_registry.h"
20
21		namespace cvc5 {
22		namespace theory {
23		namespace arrays {
24
25	12400	Info::Info(context::Context* c, Backtracker<TNode>* bck)
26		: isNonLinear(c, false),
27		rIntro1Applied(c, false),
28	24800	modelRep(c,TNode()),
29	24800	constArr(c,TNode()),
30	24800	weakEquivPointer(c,TNode()),
31	24800	weakEquivIndex(c,TNode()),
32	24800	weakEquivSecondary(c,TNode()),
33	136400	weakEquivSecondaryReason(c,TNode())
34		{
35	12400	indices = new(true)CTNodeList(c);
36	12400	stores = new(true)CTNodeList(c);
37	12400	in_stores = new(true)CTNodeList(c);
38	12400	}
39
40	24800	Info::~Info() {
41	12400	indices->deleteSelf();
42	12400	stores->deleteSelf();
43	12400	in_stores->deleteSelf();
44	12400	}
45
46	9459	ArrayInfo::ArrayInfo(context::Context* c,
47		Backtracker<TNode>* b,
48	9459	std::string statisticsPrefix)
49		: ct(c),
50		bck(b),
51		info_map(),
52	9459	d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
53	18918	statisticsPrefix + "mergeInfoTimer")),
54	9459	d_avgIndexListLength(smtStatisticsRegistry().registerAverage(
55	18918	statisticsPrefix + "avgIndexListLength")),
56	9459	d_avgStoresListLength(smtStatisticsRegistry().registerAverage(
57	18918	statisticsPrefix + "avgStoresListLength")),
58	9459	d_avgInStoresListLength(smtStatisticsRegistry().registerAverage(
59	18918	statisticsPrefix + "avgInStoresListLength")),
60		d_listsCount(
61	18918	smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")),
62	9459	d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix
63	18918	+ "callsMergeInfo")),
64		d_maxList(
65	18918	smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")),
66	9459	d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>(
67	85131	statisticsPrefix + "infoTableSize", info_map))
68		{
69	9459	emptyList = new(true) CTNodeList(ct);
70	9459	emptyInfo = new Info(ct, bck);
71	9459	}
72
73	18918	ArrayInfo::~ArrayInfo() {
74	9459	CNodeInfoMap::iterator it = info_map.begin();
75	15341	for (; it != info_map.end(); ++it)
76		{
77	2941	if((*it).second!= emptyInfo) {
78	2941	delete (*it).second;
79		}
80		}
81	9459	emptyList->deleteSelf();
82	9459	delete emptyInfo;
83	9459	}
84
85	22194	bool inList(const CTNodeList* l, const TNode el) {
86	22194	CTNodeList::const_iterator it = l->begin();
87	372742	for (; it != l->end(); ++it)
88		{
89	177212	if(*it == el)
90	1938	return true;
91		}
92	20256	return false;
93		}
94
95	396	void printList (CTNodeList* list) {
96	396	CTNodeList::const_iterator it = list->begin();
97	396	Trace("arrays-info")<<" [ ";
98	832	for (; it != list->end(); ++it)
99		{
100	218	Trace("arrays-info")<<(*it)<<" ";
101		}
102	396	Trace("arrays-info")<<"] \n";
103	396	}
104
105		void printList (List<TNode>* list) {
106		List<TNode>::const_iterator it = list->begin();
107		Trace("arrays-info")<<" [ ";
108		for (; it != list->end(); ++it)
109		{
110		Trace("arrays-info")<<(*it)<<" ";
111		}
112		Trace("arrays-info")<<"] \n";
113		}
114
115	11034	void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
116	22068	std::set<TNode> temp;
117	11034	CTNodeList::const_iterator it;
118	51071	for (it = la->begin(); it != la->end(); ++it)
119		{
120	40037	temp.insert((*it));
121		}
122
123	28109	for (it = lb->begin(); it != lb->end(); ++it)
124		{
125	17075	if(temp.count(*it) == 0) {
126	7467	la->push_back(*it);
127		}
128		}
129	11034	}
130
131	21841	void ArrayInfo::addIndex(const Node a, const TNode i) {
132	21841	Assert(a.getType().isArray());
133	21841	Assert(!i.getType().isArray()); // temporary for flat arrays
134
135	21841	Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
136		CTNodeList* temp_indices;
137		Info* temp_info;
138
139	21841	CNodeInfoMap::iterator it = info_map.find(a);
140	21841	if(it == info_map.end()) {
141	2477	temp_info = new Info(ct, bck);
142	2477	temp_indices = temp_info->indices;
143	2477	temp_indices->push_back(i);
144	2477	info_map[a] = temp_info;
145		} else {
146	19364	temp_indices = (*it).second->indices;
147	19364	if (! inList(temp_indices, i)) {
148	17426	temp_indices->push_back(i);
149		}
150		}
151	21841	if(Trace.isOn("arrays-ind")) {
152		printList((*(info_map.find(a))).second->indices);
153		}
154
155	21841	}
156
157	1562	void ArrayInfo::addStore(const Node a, const TNode st){
158	1562	Assert(a.getType().isArray());
159	1562	Assert(st.getKind() == kind::STORE); // temporary for flat arrays
160
161		CTNodeList* temp_store;
162		Info* temp_info;
163
164	1562	CNodeInfoMap::iterator it = info_map.find(a);
165	1562	if(it == info_map.end()) {
166		temp_info = new Info(ct, bck);
167		temp_store = temp_info->stores;
168		temp_store->push_back(st);
169		info_map[a]=temp_info;
170		} else {
171	1562	temp_store = (*it).second->stores;
172	1562	if(! inList(temp_store, st)) {
173	1562	temp_store->push_back(st);
174		}
175		}
176	1562	};
177
178
179	1562	void ArrayInfo::addInStore(const TNode a, const TNode b){
180	1562	Trace("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
181	1562	Assert(a.getType().isArray());
182	1562	Assert(b.getType().isArray());
183
184		CTNodeList* temp_inst;
185		Info* temp_info;
186
187	1562	CNodeInfoMap::iterator it = info_map.find(a);
188	1562	if(it == info_map.end()) {
189	294	temp_info = new Info(ct, bck);
190	294	temp_inst = temp_info->in_stores;
191	294	temp_inst->push_back(b);
192	294	info_map[a] = temp_info;
193		} else {
194	1268	temp_inst = (*it).second->in_stores;
195	1268	if(! inList(temp_inst, b)) {
196	1268	temp_inst->push_back(b);
197		}
198		}
199	1562	};
200
201
202	1130	void ArrayInfo::setNonLinear(const TNode a) {
203	1130	Assert(a.getType().isArray());
204		Info* temp_info;
205	1130	CNodeInfoMap::iterator it = info_map.find(a);
206	1130	if(it == info_map.end()) {
207	6	temp_info = new Info(ct, bck);
208	6	temp_info->isNonLinear = true;
209	6	info_map[a] = temp_info;
210		} else {
211	1124	(*it).second->isNonLinear = true;
212		}
213
214	1130	}
215
216		void ArrayInfo::setRIntro1Applied(const TNode a) {
217		Assert(a.getType().isArray());
218		Info* temp_info;
219		CNodeInfoMap::iterator it = info_map.find(a);
220		if(it == info_map.end()) {
221		temp_info = new Info(ct, bck);
222		temp_info->rIntro1Applied = true;
223		info_map[a] = temp_info;
224		} else {
225		(*it).second->rIntro1Applied = true;
226		}
227
228		}
229
230	1562	void ArrayInfo::setModelRep(const TNode a, const TNode b) {
231	1562	Assert(a.getType().isArray());
232		Info* temp_info;
233	1562	CNodeInfoMap::iterator it = info_map.find(a);
234	1562	if(it == info_map.end()) {
235		temp_info = new Info(ct, bck);
236		temp_info->modelRep = b;
237		info_map[a] = temp_info;
238		} else {
239	1562	(*it).second->modelRep = b;
240		}
241
242	1562	}
243
244	42	void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
245	42	Assert(a.getType().isArray());
246		Info* temp_info;
247	42	CNodeInfoMap::iterator it = info_map.find(a);
248	42	if(it == info_map.end()) {
249	32	temp_info = new Info(ct, bck);
250	32	temp_info->constArr = constArr;
251	32	info_map[a] = temp_info;
252		} else {
253	10	(*it).second->constArr = constArr;
254		}
255	42	}
256
257		void ArrayInfo::setWeakEquivPointer(const TNode a, const TNode pointer) {
258		Assert(a.getType().isArray());
259		Info* temp_info;
260		CNodeInfoMap::iterator it = info_map.find(a);
261		if(it == info_map.end()) {
262		temp_info = new Info(ct, bck);
263		temp_info->weakEquivPointer = pointer;
264		info_map[a] = temp_info;
265		} else {
266		(*it).second->weakEquivPointer = pointer;
267		}
268		}
269
270		void ArrayInfo::setWeakEquivIndex(const TNode a, const TNode index) {
271		Assert(a.getType().isArray());
272		Info* temp_info;
273		CNodeInfoMap::iterator it = info_map.find(a);
274		if(it == info_map.end()) {
275		temp_info = new Info(ct, bck);
276		temp_info->weakEquivIndex = index;
277		info_map[a] = temp_info;
278		} else {
279		(*it).second->weakEquivIndex = index;
280		}
281		}
282
283		void ArrayInfo::setWeakEquivSecondary(const TNode a, const TNode secondary) {
284		Assert(a.getType().isArray());
285		Info* temp_info;
286		CNodeInfoMap::iterator it = info_map.find(a);
287		if(it == info_map.end()) {
288		temp_info = new Info(ct, bck);
289		temp_info->weakEquivSecondary = secondary;
290		info_map[a] = temp_info;
291		} else {
292		(*it).second->weakEquivSecondary = secondary;
293		}
294		}
295
296		void ArrayInfo::setWeakEquivSecondaryReason(const TNode a, const TNode reason) {
297		Assert(a.getType().isArray());
298		Info* temp_info;
299		CNodeInfoMap::iterator it = info_map.find(a);
300		if(it == info_map.end()) {
301		temp_info = new Info(ct, bck);
302		temp_info->weakEquivSecondaryReason = reason;
303		info_map[a] = temp_info;
304		} else {
305		(*it).second->weakEquivSecondaryReason = reason;
306		}
307		}
308
309		/**
310		* Returns the information associated with TNode a
311		*/
312
313		const Info* ArrayInfo::getInfo(const TNode a) const{
314		CNodeInfoMap::const_iterator it = info_map.find(a);
315
316		if(it!= info_map.end()) {
317		return (*it).second;
318		}
319		return emptyInfo;
320		}
321
322	29175	const bool ArrayInfo::isNonLinear(const TNode a) const
323		{
324	29175	CNodeInfoMap::const_iterator it = info_map.find(a);
325
326	29175	if(it!= info_map.end()) {
327	28045	return (*it).second->isNonLinear;
328		}
329	1130	return false;
330		}
331
332		const bool ArrayInfo::rIntro1Applied(const TNode a) const
333		{
334		CNodeInfoMap::const_iterator it = info_map.find(a);
335
336		if(it!= info_map.end()) {
337		return (*it).second->rIntro1Applied;
338		}
339		return false;
340		}
341
342		const TNode ArrayInfo::getModelRep(const TNode a) const
343		{
344		CNodeInfoMap::const_iterator it = info_map.find(a);
345
346		if(it!= info_map.end()) {
347		return (*it).second->modelRep;
348		}
349		return TNode();
350		}
351
352	38703	const TNode ArrayInfo::getConstArr(const TNode a) const
353		{
354	38703	CNodeInfoMap::const_iterator it = info_map.find(a);
355
356	38703	if(it!= info_map.end()) {
357	37099	return (*it).second->constArr;
358		}
359	1604	return TNode();
360		}
361
362		const TNode ArrayInfo::getWeakEquivPointer(const TNode a) const
363		{
364		CNodeInfoMap::const_iterator it = info_map.find(a);
365
366		if(it!= info_map.end()) {
367		return (*it).second->weakEquivPointer;
368		}
369		return TNode();
370		}
371
372		const TNode ArrayInfo::getWeakEquivIndex(const TNode a) const
373		{
374		CNodeInfoMap::const_iterator it = info_map.find(a);
375
376		if(it!= info_map.end()) {
377		return (*it).second->weakEquivIndex;
378		}
379		return TNode();
380		}
381
382		const TNode ArrayInfo::getWeakEquivSecondary(const TNode a) const
383		{
384		CNodeInfoMap::const_iterator it = info_map.find(a);
385
386		if(it!= info_map.end()) {
387		return (*it).second->weakEquivSecondary;
388		}
389		return TNode();
390		}
391
392		const TNode ArrayInfo::getWeakEquivSecondaryReason(const TNode a) const
393		{
394		CNodeInfoMap::const_iterator it = info_map.find(a);
395
396		if(it!= info_map.end()) {
397		return (*it).second->weakEquivSecondaryReason;
398		}
399		return TNode();
400		}
401
402	9807	const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
403	9807	CNodeInfoMap::const_iterator it = info_map.find(a);
404	9807	if(it!= info_map.end()) {
405	9005	return (*it).second->indices;
406		}
407	802	return emptyList;
408		}
409
410	36751	const CTNodeList* ArrayInfo::getStores(const TNode a) const{
411	36751	CNodeInfoMap::const_iterator it = info_map.find(a);
412	36751	if(it!= info_map.end()) {
413	35390	return (*it).second->stores;
414		}
415	1361	return emptyList;
416		}
417
418	38786	const CTNodeList* ArrayInfo::getInStores(const TNode a) const{
419	38786	CNodeInfoMap::const_iterator it = info_map.find(a);
420	38786	if(it!= info_map.end()) {
421	37984	return (*it).second->in_stores;
422		}
423	802	return emptyList;
424		}
425
426
427	4214	void ArrayInfo::mergeInfo(const TNode a, const TNode b){
428		// can't have assertion that find(b) = a !
429	8428	TimerStat::CodeTimer codeTimer(d_mergeInfoTimer);
430	4214	++d_callsMergeInfo;
431
432	4214	Trace("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
433	4214	Trace("arrays-mergei")<<" and "<<b<<"\n";
434
435	4214	CNodeInfoMap::iterator ita = info_map.find(a);
436	4214	CNodeInfoMap::iterator itb = info_map.find(b);
437
438	4214	if(ita != info_map.end()) {
439	3948	Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
440	3948	if(Trace.isOn("arrays-mergei"))
441		(*ita).second->print();
442
443	3948	if(itb != info_map.end()) {
444	3546	Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
445	3546	if(Trace.isOn("arrays-mergei"))
446		(*itb).second->print();
447
448	3546	CTNodeList* lista_i = (*ita).second->indices;
449	3546	CTNodeList* lista_st = (*ita).second->stores;
450	3546	CTNodeList* lista_inst = (*ita).second->in_stores;
451
452
453	3546	CTNodeList* listb_i = (*itb).second->indices;
454	3546	CTNodeList* listb_st = (*itb).second->stores;
455	3546	CTNodeList* listb_inst = (*itb).second->in_stores;
456
457	3546	mergeLists(lista_i, listb_i);
458	3546	mergeLists(lista_st, listb_st);
459	3546	mergeLists(lista_inst, listb_inst);
460
461		/* sketchy stats */
462
463		//FIXME
464	3546	int s = 0;//lista_i->size();
465	3546	d_maxList.maxAssign(s);
466
467
468	3546	if(s!= 0) {
469		d_avgIndexListLength << s;
470		++d_listsCount;
471		}
472	3546	s = lista_st->size();
473	3546	d_maxList.maxAssign(s);
474	3546	if(s!= 0) {
475	1814	d_avgStoresListLength << s;
476	1814	++d_listsCount;
477		}
478
479	3546	s = lista_inst->size();
480	3546	d_maxList.maxAssign(s);
481	3546	if(s!=0) {
482	2323	d_avgInStoresListLength << s;
483	2323	++d_listsCount;
484		}
485
486		/* end sketchy stats */
487
488		}
489
490		} else {
491	266	Trace("arrays-mergei")<<" First element has no info \n";
492	266	if(itb != info_map.end()) {
493	132	Trace("arrays-mergei")<<" adding second element's info \n";
494	132	(*itb).second->print();
495
496	132	CTNodeList* listb_i = (*itb).second->indices;
497	132	CTNodeList* listb_st = (*itb).second->stores;
498	132	CTNodeList* listb_inst = (*itb).second->in_stores;
499
500	132	Info* temp_info = new Info(ct, bck);
501
502	132	mergeLists(temp_info->indices, listb_i);
503	132	mergeLists(temp_info->stores, listb_st);
504	132	mergeLists(temp_info->in_stores, listb_inst);
505	132	info_map[a] = temp_info;
506
507		} else {
508	134	Trace("arrays-mergei")<<" Second element has no info \n";
509		}
510
511		}
512	4214	Trace("arrays-mergei")<<"Arrays::mergeInfo done \n";
513
514	4214	}
515
516		} // namespace arrays
517		} // namespace theory
518	28191	} // namespace cvc5