Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/array_info.cpp	Lines:	203	295	68.8 %
Date:	2021-09-17	Branches:	292	932	31.3 %


/******************************************************************************
 * 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)
    : 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,
                     std::string statisticsPrefix)
    : ct(c),
      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);
}

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 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);
    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);
    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);
    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);
    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);
    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);
    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);
    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);
    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);
    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);
    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);
    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);

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