Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv_rewrite_rules_core.h	Lines:	144	144	100.0 %
Date:	2021-05-22	Branches:	265	460	57.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Liana Hadarean, Clark Barrett
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"

#pragma once

#include "theory/bv/theory_bv_rewrite_rules.h"
#include "theory/bv/theory_bv_utils.h"

namespace cvc5 {
namespace theory {
namespace bv {

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ConcatFlatten>::applies(TNode node) {
  return (node.getKind() == kind::BITVECTOR_CONCAT);
}

template<> inline
Node RewriteRule<ConcatFlatten>::apply(TNode node) {
  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
  NodeBuilder result(kind::BITVECTOR_CONCAT);
  std::vector<Node> processing_stack;
  processing_stack.push_back(node);
  while (!processing_stack.empty()) {
    Node current = processing_stack.back();
    processing_stack.pop_back();
    if (current.getKind() == kind::BITVECTOR_CONCAT) {
      for (int i = current.getNumChildren() - 1; i >= 0; i--)
        processing_stack.push_back(current[i]);
    } else {
      result << current;
    }
  }
  Node resultNode = result;
  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
  return resultNode;
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ConcatExtractMerge>::applies(TNode node) {
  return (node.getKind() == kind::BITVECTOR_CONCAT);
}

template<> inline
Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {

  Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;

  std::vector<Node> mergedExtracts;

  Node current = node[0];
  bool mergeStarted = false;
  unsigned currentHigh = 0;
  unsigned currentLow  = 0;

  for(size_t i = 1, end = node.getNumChildren(); i < end; ++ i) {
    // The next candidate for merging
    Node next = node[i];
    // If the current is not an extract we just go to the next
    if (current.getKind() != kind::BITVECTOR_EXTRACT) {
      mergedExtracts.push_back(current);
      current = next;
      continue;
    }
    // If it is an extract and the first one, get the extract parameters
    else if (!mergeStarted) {
      currentHigh = utils::getExtractHigh(current);
      currentLow = utils::getExtractLow(current);
    }

    // If the next one can be merged, try to merge
    bool merged = false;
    if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) {
      // x[i : j] @ x[j - 1 : k] -> c x[i : k]
      unsigned nextHigh = utils::getExtractHigh(next);
      unsigned nextLow  = utils::getExtractLow(next);
      if(nextHigh + 1 == currentLow) {
        currentLow = nextLow;
        mergeStarted = true;
        merged = true;
      }
    }
    // If we haven't merged anything, add the previous merge and continue with the next
    if (!merged) {
      if (!mergeStarted) mergedExtracts.push_back(current);
      else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow));
      current = next;
      mergeStarted = false;
    }
  }

  // Add the last child
  if (!mergeStarted) mergedExtracts.push_back(current);
  else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow));

  // Return the result
  return utils::mkConcat(mergedExtracts);
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
  return node.getKind() == kind::BITVECTOR_CONCAT;
}

template<> inline
Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {

  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;

  std::vector<Node> mergedConstants;
  for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
    if (node[i].getKind() != kind::CONST_BITVECTOR) {
      // If not a constant, just add it
      mergedConstants.push_back(node[i]);
      ++i;
    } else {
      // Find the longest sequence of constants
      unsigned j = i + 1;
      while (j < end) {
        if (node[j].getKind() != kind::CONST_BITVECTOR) {
          break;
        } else {
          ++ j;
        }
      }
      // Append all the constants
      BitVector current = node[i].getConst<BitVector>();
      for (unsigned k = i + 1; k < j; ++ k) {
        current = current.concat(node[k].getConst<BitVector>());
      }
      // Add the new merged constant
      mergedConstants.push_back(utils::mkConst(current));
      i = j;
    }
  }

  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;

  return utils::mkConcat(mergedConstants);
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ExtractWhole>::applies(TNode node) {
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
  unsigned length = utils::getSize(node[0]);
  unsigned extractHigh = utils::getExtractHigh(node);
  if (extractHigh != length - 1) return false;
  unsigned extractLow  = utils::getExtractLow(node);
  if (extractLow != 0) return false;
  return true;
}

template<> inline
Node RewriteRule<ExtractWhole>::apply(TNode node) {
  Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
  return node[0];
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ExtractConstant>::applies(TNode node) {
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
  if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
  return true;
}

template<> inline
Node RewriteRule<ExtractConstant>::apply(TNode node) {
  Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
  Node child = node[0];
  BitVector childValue = child.getConst<BitVector>();
  return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ExtractConcat>::applies(TNode node) {
  //Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
  if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
  return true;
}

template<> inline
Node RewriteRule<ExtractConcat>::apply(TNode node) {
  Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
  int extract_high = utils::getExtractHigh(node);
  int extract_low = utils::getExtractLow(node);

  std::vector<Node> resultChildren;

  Node concat = node[0];
  for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) {
    Node concatChild = concat[i];
    int concatChildSize = utils::getSize(concatChild);
    if (extract_low < concatChildSize) {
      int extract_start = extract_low < 0 ? 0 : extract_low;
      int extract_end = extract_high < concatChildSize ? extract_high : concatChildSize - 1;
      resultChildren.push_back(utils::mkExtract(concatChild, extract_end, extract_start));
    }
    extract_low -= concatChildSize;
    extract_high -= concatChildSize;
  }

  std::reverse(resultChildren.begin(), resultChildren.end());

  return utils::mkConcat(resultChildren);
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ExtractExtract>::applies(TNode node) {
  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
  if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false;
  return true;
}

template<> inline
Node RewriteRule<ExtractExtract>::apply(TNode node) {
  Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;

  // x[i:j][k:l] ~>  x[k+j:l+j]
  Node child = node[0];
  unsigned k = utils::getExtractHigh(node);
  unsigned l = utils::getExtractLow(node);
  unsigned j = utils::getExtractLow(child);

  Node result = utils::mkExtract(child[0], k + j, l + j);
  return result;
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<FailEq>::applies(TNode node) {
  //Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
  if (node.getKind() != kind::EQUAL) return false;
  if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
  if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
  return node[0] != node[1];
}

template<> inline
Node RewriteRule<FailEq>::apply(TNode node) {
  return utils::mkFalse();
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<SimplifyEq>::applies(TNode node) {
  if (node.getKind() != kind::EQUAL) return false;
  return node[0] == node[1];
}

template<> inline
Node RewriteRule<SimplifyEq>::apply(TNode node) {
  Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
  return utils::mkTrue();
}

/* -------------------------------------------------------------------------- */

template<> inline
bool RewriteRule<ReflexivityEq>::applies(TNode node) {
  return (node.getKind() == kind::EQUAL && node[0] < node[1]);
}

template<> inline
Node RewriteRule<ReflexivityEq>::apply(TNode node) {
  Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
  Node res = node[1].eqNode(node[0]);
  return res;
}

}
}
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Liana Hadarean, Clark Barrett
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "cvc5_private.h"
20
21		#pragma once
22
23		#include "theory/bv/theory_bv_rewrite_rules.h"
24		#include "theory/bv/theory_bv_utils.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace bv {
29
30		/* -------------------------------------------------------------------------- */
31
32		template<> inline
33	371728	bool RewriteRule<ConcatFlatten>::applies(TNode node) {
34	371728	return (node.getKind() == kind::BITVECTOR_CONCAT);
35		}
36
37		template<> inline
38	185864	Node RewriteRule<ConcatFlatten>::apply(TNode node) {
39	185864	Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
40	371728	NodeBuilder result(kind::BITVECTOR_CONCAT);
41	371728	std::vector<Node> processing_stack;
42	185864	processing_stack.push_back(node);
43	1681050	while (!processing_stack.empty()) {
44	1495186	Node current = processing_stack.back();
45	747593	processing_stack.pop_back();
46	747593	if (current.getKind() == kind::BITVECTOR_CONCAT) {
47	753204	for (int i = current.getNumChildren() - 1; i >= 0; i--)
48	561729	processing_stack.push_back(current[i]);
49		} else {
50	556118	result << current;
51		}
52		}
53	185864	Node resultNode = result;
54	185864	Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
55	371728	return resultNode;
56		}
57
58		/* -------------------------------------------------------------------------- */
59
60		template<> inline
61	371728	bool RewriteRule<ConcatExtractMerge>::applies(TNode node) {
62	371728	return (node.getKind() == kind::BITVECTOR_CONCAT);
63		}
64
65		template<> inline
66	185864	Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
67
68	185864	Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
69
70	371728	std::vector<Node> mergedExtracts;
71
72	371728	Node current = node[0];
73	185864	bool mergeStarted = false;
74	185864	unsigned currentHigh = 0;
75	185864	unsigned currentLow = 0;
76
77	556118	for(size_t i = 1, end = node.getNumChildren(); i < end; ++ i) {
78		// The next candidate for merging
79	440263	Node next = node[i];
80		// If the current is not an extract we just go to the next
81	670499	if (current.getKind() != kind::BITVECTOR_EXTRACT) {
82	300245	mergedExtracts.push_back(current);
83	300245	current = next;
84	300245	continue;
85		}
86		// If it is an extract and the first one, get the extract parameters
87	70009	else if (!mergeStarted) {
88	69973	currentHigh = utils::getExtractHigh(current);
89	69973	currentLow = utils::getExtractLow(current);
90		}
91
92		// If the next one can be merged, try to merge
93	70009	bool merged = false;
94	70009	if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) {
95		// x[i : j] @ x[j - 1 : k] -> c x[i : k]
96	25222	unsigned nextHigh = utils::getExtractHigh(next);
97	25222	unsigned nextLow = utils::getExtractLow(next);
98	25222	if(nextHigh + 1 == currentLow) {
99	79	currentLow = nextLow;
100	79	mergeStarted = true;
101	79	merged = true;
102		}
103		}
104		// If we haven't merged anything, add the previous merge and continue with the next
105	70009	if (!merged) {
106	69930	if (!mergeStarted) mergedExtracts.push_back(current);
107	12	else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow));
108	69930	current = next;
109	69930	mergeStarted = false;
110		}
111		}
112
113		// Add the last child
114	185864	if (!mergeStarted) mergedExtracts.push_back(current);
115	43	else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow));
116
117		// Return the result
118	371728	return utils::mkConcat(mergedExtracts);
119		}
120
121		/* -------------------------------------------------------------------------- */
122
123		template<> inline
124	371695	bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
125	371695	return node.getKind() == kind::BITVECTOR_CONCAT;
126		}
127
128		template<> inline
129	185831	Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
130
131	185831	Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
132
133	371662	std::vector<Node> mergedConstants;
134	705568	for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
135	519737	if (node[i].getKind() != kind::CONST_BITVECTOR) {
136		// If not a constant, just add it
137	363232	mergedConstants.push_back(node[i]);
138	363232	++i;
139		} else {
140		// Find the longest sequence of constants
141	156505	unsigned j = i + 1;
142	229043	while (j < end) {
143	133995	if (node[j].getKind() != kind::CONST_BITVECTOR) {
144	97726	break;
145		} else {
146	36269	++ j;
147		}
148		}
149		// Append all the constants
150	313010	BitVector current = node[i].getConst<BitVector>();
151	192774	for (unsigned k = i + 1; k < j; ++ k) {
152	36269	current = current.concat(node[k].getConst<BitVector>());
153		}
154		// Add the new merged constant
155	156505	mergedConstants.push_back(utils::mkConst(current));
156	156505	i = j;
157		}
158		}
159
160	185831	Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
161
162	371662	return utils::mkConcat(mergedConstants);
163		}
164
165		/* -------------------------------------------------------------------------- */
166
167		template<> inline
168	663690	bool RewriteRule<ExtractWhole>::applies(TNode node) {
169	663690	if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
170	198415	unsigned length = utils::getSize(node[0]);
171	198415	unsigned extractHigh = utils::getExtractHigh(node);
172	198415	if (extractHigh != length - 1) return false;
173	85510	unsigned extractLow = utils::getExtractLow(node);
174	85510	if (extractLow != 0) return false;
175	16720	return true;
176		}
177
178		template<> inline
179	12535	Node RewriteRule<ExtractWhole>::apply(TNode node) {
180	12535	Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
181	12535	return node[0];
182		}
183
184		/* -------------------------------------------------------------------------- */
185
186		template<> inline
187	182351	bool RewriteRule<ExtractConstant>::applies(TNode node) {
188	182351	if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
189	182351	if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
190	85232	return true;
191		}
192
193		template<> inline
194	42616	Node RewriteRule<ExtractConstant>::apply(TNode node) {
195	42616	Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
196	85232	Node child = node[0];
197	85232	BitVector childValue = child.getConst<BitVector>();
198	85232	return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
199		}
200
201		/* -------------------------------------------------------------------------- */
202
203		template<> inline
204	159987	bool RewriteRule<ExtractConcat>::applies(TNode node) {
205		//Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
206	159987	if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
207	159987	if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
208	17824	return true;
209		}
210
211		template<> inline
212	8912	Node RewriteRule<ExtractConcat>::apply(TNode node) {
213	8912	Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
214	8912	int extract_high = utils::getExtractHigh(node);
215	8912	int extract_low = utils::getExtractLow(node);
216
217	17824	std::vector<Node> resultChildren;
218
219	17824	Node concat = node[0];
220	27640	for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) {
221	37456	Node concatChild = concat[i];
222	18728	int concatChildSize = utils::getSize(concatChild);
223	18728	if (extract_low < concatChildSize) {
224	16438	int extract_start = extract_low < 0 ? 0 : extract_low;
225	16438	int extract_end = extract_high < concatChildSize ? extract_high : concatChildSize - 1;
226	16438	resultChildren.push_back(utils::mkExtract(concatChild, extract_end, extract_start));
227		}
228	18728	extract_low -= concatChildSize;
229	18728	extract_high -= concatChildSize;
230		}
231
232	8912	std::reverse(resultChildren.begin(), resultChildren.end());
233
234	17824	return utils::mkConcat(resultChildren);
235		}
236
237		/* -------------------------------------------------------------------------- */
238
239		template<> inline
240	141737	bool RewriteRule<ExtractExtract>::applies(TNode node) {
241	141737	if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
242	99121	if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false;
243	4004	return true;
244		}
245
246		template<> inline
247	2002	Node RewriteRule<ExtractExtract>::apply(TNode node) {
248	2002	Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
249
250		// x[i:j][k:l] ~> x[k+j:l+j]
251	4004	Node child = node[0];
252	2002	unsigned k = utils::getExtractHigh(node);
253	2002	unsigned l = utils::getExtractLow(node);
254	2002	unsigned j = utils::getExtractLow(child);
255
256	2002	Node result = utils::mkExtract(child[0], k + j, l + j);
257	4004	return result;
258		}
259
260		/* -------------------------------------------------------------------------- */
261
262		template<> inline
263	507982	bool RewriteRule<FailEq>::applies(TNode node) {
264		//Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
265	507982	if (node.getKind() != kind::EQUAL) return false;
266	507982	if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
267	107492	if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
268	88374	return node[0] != node[1];
269		}
270
271		template<> inline
272	42415	Node RewriteRule<FailEq>::apply(TNode node) {
273	42415	return utils::mkFalse();
274		}
275
276		/* -------------------------------------------------------------------------- */
277
278		template<> inline
279	474593	bool RewriteRule<SimplifyEq>::applies(TNode node) {
280	474593	if (node.getKind() != kind::EQUAL) return false;
281	432178	return node[0] == node[1];
282		}
283
284		template<> inline
285	9026	Node RewriteRule<SimplifyEq>::apply(TNode node) {
286	9026	Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
287	9026	return utils::mkTrue();
288		}
289
290		/* -------------------------------------------------------------------------- */
291
292		template<> inline
293	510601	bool RewriteRule<ReflexivityEq>::applies(TNode node) {
294	510601	return (node.getKind() == kind::EQUAL && node[0] < node[1]);
295		}
296
297		template<> inline
298	45034	Node RewriteRule<ReflexivityEq>::apply(TNode node) {
299	45034	Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
300	45034	Node res = node[1].eqNode(node[0]);
301	45034	return res;
302		}
303
304		}
305		}
306		} // namespace cvc5