Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/array_info.cpp	Lines:	203	302	67.2 %
Date:	2021-08-16	Branches:	292	960	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	12462	Info::Info(context::Context* c, Backtracker<TNode>* bck)
26		: isNonLinear(c, false),
27		rIntro1Applied(c, false),
28	24924	modelRep(c,TNode()),
29	24924	constArr(c,TNode()),
30	24924	weakEquivPointer(c,TNode()),
31	24924	weakEquivIndex(c,TNode()),
32	24924	weakEquivSecondary(c,TNode()),
33	137082	weakEquivSecondaryReason(c,TNode())
34		{
35	12462	indices = new(true)CTNodeList(c);
36	12462	stores = new(true)CTNodeList(c);
37	12462	in_stores = new(true)CTNodeList(c);
38	12462	}
39
40	24924	Info::~Info() {
41	12462	indices->deleteSelf();
42	12462	stores->deleteSelf();
43	12462	in_stores->deleteSelf();
44	12462	}
45
46	9853	ArrayInfo::ArrayInfo(context::Context* c,
47		Backtracker<TNode>* b,
48	9853	std::string statisticsPrefix)
49		: ct(c),
50		bck(b),
51		info_map(),
52	9853	d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
53	19706	statisticsPrefix + "mergeInfoTimer")),
54	9853	d_avgIndexListLength(smtStatisticsRegistry().registerAverage(
55	19706	statisticsPrefix + "avgIndexListLength")),
56	9853	d_avgStoresListLength(smtStatisticsRegistry().registerAverage(
57	19706	statisticsPrefix + "avgStoresListLength")),
58	9853	d_avgInStoresListLength(smtStatisticsRegistry().registerAverage(
59	19706	statisticsPrefix + "avgInStoresListLength")),
60		d_listsCount(
61	19706	smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")),
62	9853	d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix
63	19706	+ "callsMergeInfo")),
64		d_maxList(
65	19706	smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")),
66	9853	d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>(
67	88677	statisticsPrefix + "infoTableSize", info_map))
68		{
69	9853	emptyList = new(true) CTNodeList(ct);
70	9853	emptyInfo = new Info(ct, bck);
71	9853	}
72
73	19706	ArrayInfo::~ArrayInfo() {
74	9853	CNodeInfoMap::iterator it = info_map.begin();
75	15071	for (; it != info_map.end(); ++it)
76		{
77	2609	if((*it).second!= emptyInfo) {
78	2609	delete (*it).second;
79		}
80		}
81	9853	emptyList->deleteSelf();
82	9853	delete emptyInfo;
83	9853	}
84
85	23865	bool inList(const CTNodeList* l, const TNode el) {
86	23865	CTNodeList::const_iterator it = l->begin();
87	367547	for (; it != l->end(); ++it)
88		{
89	174384	if(*it == el)
90	2543	return true;
91		}
92	21322	return false;
93		}
94
95	474	void printList (CTNodeList* list) {
96	474	CTNodeList::const_iterator it = list->begin();
97	474	Trace("arrays-info")<<" [ ";
98	1024	for (; it != list->end(); ++it)
99		{
100	275	Trace("arrays-info")<<(*it)<<" ";
101		}
102	474	Trace("arrays-info")<<"] \n";
103	474	}
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	15609	void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
116	31218	std::set<TNode> temp;
117	15609	CTNodeList::const_iterator it;
118	50845	for (it = la->begin(); it != la->end(); ++it)
119		{
120	35236	temp.insert((*it));
121		}
122
123	41442	for (it = lb->begin(); it != lb->end(); ++it)
124		{
125	25833	if(temp.count(*it) == 0) {
126	12984	la->push_back(*it);
127		}
128		}
129	15609	}
130
131	24028	void ArrayInfo::addIndex(const Node a, const TNode i) {
132	24028	Assert(a.getType().isArray());
133	24028	Assert(!i.getType().isArray()); // temporary for flat arrays
134
135	24028	Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
136		CTNodeList* temp_indices;
137		Info* temp_info;
138
139	24028	CNodeInfoMap::iterator it = info_map.find(a);
140	24028	if(it == info_map.end()) {
141	2079	temp_info = new Info(ct, bck);
142	2079	temp_indices = temp_info->indices;
143	2079	temp_indices->push_back(i);
144	2079	info_map[a] = temp_info;
145		} else {
146	21949	temp_indices = (*it).second->indices;
147	21949	if (! inList(temp_indices, i)) {
148	19406	temp_indices->push_back(i);
149		}
150		}
151	24028	if(Trace.isOn("arrays-ind")) {
152		printList((*(info_map.find(a))).second->indices);
153		}
154
155	24028	}
156
157	1112	void ArrayInfo::addStore(const Node a, const TNode st){
158	1112	Assert(a.getType().isArray());
159	1112	Assert(st.getKind() == kind::STORE); // temporary for flat arrays
160
161		CTNodeList* temp_store;
162		Info* temp_info;
163
164	1112	CNodeInfoMap::iterator it = info_map.find(a);
165	1112	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	1112	temp_store = (*it).second->stores;
172	1112	if(! inList(temp_store, st)) {
173	1112	temp_store->push_back(st);
174		}
175		}
176	1112	};
177
178
179	1112	void ArrayInfo::addInStore(const TNode a, const TNode b){
180	1112	Trace("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
181	1112	Assert(a.getType().isArray());
182	1112	Assert(b.getType().isArray());
183
184		CTNodeList* temp_inst;
185		Info* temp_info;
186
187	1112	CNodeInfoMap::iterator it = info_map.find(a);
188	1112	if(it == info_map.end()) {
189	308	temp_info = new Info(ct, bck);
190	308	temp_inst = temp_info->in_stores;
191	308	temp_inst->push_back(b);
192	308	info_map[a] = temp_info;
193		} else {
194	804	temp_inst = (*it).second->in_stores;
195	804	if(! inList(temp_inst, b)) {
196	804	temp_inst->push_back(b);
197		}
198		}
199	1112	};
200
201
202	1732	void ArrayInfo::setNonLinear(const TNode a) {
203	1732	Assert(a.getType().isArray());
204		Info* temp_info;
205	1732	CNodeInfoMap::iterator it = info_map.find(a);
206	1732	if(it == info_map.end()) {
207	8	temp_info = new Info(ct, bck);
208	8	temp_info->isNonLinear = true;
209	8	info_map[a] = temp_info;
210		} else {
211	1724	(*it).second->isNonLinear = true;
212		}
213
214	1732	}
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	1112	void ArrayInfo::setModelRep(const TNode a, const TNode b) {
231	1112	Assert(a.getType().isArray());
232		Info* temp_info;
233	1112	CNodeInfoMap::iterator it = info_map.find(a);
234	1112	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	1112	(*it).second->modelRep = b;
240		}
241
242	1112	}
243
244	66	void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
245	66	Assert(a.getType().isArray());
246		Info* temp_info;
247	66	CNodeInfoMap::iterator it = info_map.find(a);
248	66	if(it == info_map.end()) {
249	56	temp_info = new Info(ct, bck);
250	56	temp_info->constArr = constArr;
251	56	info_map[a] = temp_info;
252		} else {
253	10	(*it).second->constArr = constArr;
254		}
255	66	}
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	36827	const bool ArrayInfo::isNonLinear(const TNode a) const
323		{
324	36827	CNodeInfoMap::const_iterator it = info_map.find(a);
325
326	36827	if(it!= info_map.end()) {
327	35654	return (*it).second->isNonLinear;
328		}
329	1173	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	47250	const TNode ArrayInfo::getConstArr(const TNode a) const
353		{
354	47250	CNodeInfoMap::const_iterator it = info_map.find(a);
355
356	47250	if(it!= info_map.end()) {
357	45460	return (*it).second->constArr;
358		}
359	1790	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	13598	const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
403	13598	CNodeInfoMap::const_iterator it = info_map.find(a);
404	13598	if(it!= info_map.end()) {
405	12703	return (*it).second->indices;
406		}
407	895	return emptyList;
408		}
409
410	44942	const CTNodeList* ArrayInfo::getStores(const TNode a) const{
411	44942	CNodeInfoMap::const_iterator it = info_map.find(a);
412	44942	if(it!= info_map.end()) {
413	43468	return (*it).second->stores;
414		}
415	1474	return emptyList;
416		}
417
418	44180	const CTNodeList* ArrayInfo::getInStores(const TNode a) const{
419	44180	CNodeInfoMap::const_iterator it = info_map.find(a);
420	44180	if(it!= info_map.end()) {
421	43285	return (*it).second->in_stores;
422		}
423	895	return emptyList;
424		}
425
426
427	5804	void ArrayInfo::mergeInfo(const TNode a, const TNode b){
428		// can't have assertion that find(b) = a !
429	11608	TimerStat::CodeTimer codeTimer(d_mergeInfoTimer);
430	5804	++d_callsMergeInfo;
431
432	5804	Trace("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
433	5804	Trace("arrays-mergei")<<" and "<<b<<"\n";
434
435	5804	CNodeInfoMap::iterator ita = info_map.find(a);
436	5804	CNodeInfoMap::iterator itb = info_map.find(b);
437
438	5804	if(ita != info_map.end()) {
439	5510	Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
440	5510	if(Trace.isOn("arrays-mergei"))
441		(*ita).second->print();
442
443	5510	if(itb != info_map.end()) {
444	5045	Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
445	5045	if(Trace.isOn("arrays-mergei"))
446		(*itb).second->print();
447
448	5045	CTNodeList* lista_i = (*ita).second->indices;
449	5045	CTNodeList* lista_st = (*ita).second->stores;
450	5045	CTNodeList* lista_inst = (*ita).second->in_stores;
451
452
453	5045	CTNodeList* listb_i = (*itb).second->indices;
454	5045	CTNodeList* listb_st = (*itb).second->stores;
455	5045	CTNodeList* listb_inst = (*itb).second->in_stores;
456
457	5045	mergeLists(lista_i, listb_i);
458	5045	mergeLists(lista_st, listb_st);
459	5045	mergeLists(lista_inst, listb_inst);
460
461		/* sketchy stats */
462
463		//FIXME
464	5045	int s = 0;//lista_i->size();
465	5045	d_maxList.maxAssign(s);
466
467
468	5045	if(s!= 0) {
469		d_avgIndexListLength << s;
470		++d_listsCount;
471		}
472	5045	s = lista_st->size();
473	5045	d_maxList.maxAssign(s);
474	5045	if(s!= 0) {
475	3234	d_avgStoresListLength << s;
476	3234	++d_listsCount;
477		}
478
479	5045	s = lista_inst->size();
480	5045	d_maxList.maxAssign(s);
481	5045	if(s!=0) {
482	2626	d_avgInStoresListLength << s;
483	2626	++d_listsCount;
484		}
485
486		/* end sketchy stats */
487
488		}
489
490		} else {
491	294	Trace("arrays-mergei")<<" First element has no info \n";
492	294	if(itb != info_map.end()) {
493	158	Trace("arrays-mergei")<<" adding second element's info \n";
494	158	(*itb).second->print();
495
496	158	CTNodeList* listb_i = (*itb).second->indices;
497	158	CTNodeList* listb_st = (*itb).second->stores;
498	158	CTNodeList* listb_inst = (*itb).second->in_stores;
499
500	158	Info* temp_info = new Info(ct, bck);
501
502	158	mergeLists(temp_info->indices, listb_i);
503	158	mergeLists(temp_info->stores, listb_st);
504	158	mergeLists(temp_info->in_stores, listb_inst);
505	158	info_map[a] = temp_info;
506
507		} else {
508	136	Trace("arrays-mergei")<<" Second element has no info \n";
509		}
510
511		}
512	5804	Trace("arrays-mergei")<<"Arrays::mergeInfo done \n";
513
514	5804	}
515
516		} // namespace arrays
517		} // namespace theory
518	29340	} // namespace cvc5