Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/bool_to_bv.cpp	Lines:	176	182	96.7 %
Date:	2021-09-11	Branches:	408	783	52.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Makai Mann, Yoni Zohar, 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.
 * ****************************************************************************
 *
 * The BoolToBV preprocessing pass.
 *
 */

#include "preprocessing/passes/bool_to_bv.h"

#include <string>

#include "base/map_util.h"
#include "expr/node.h"
#include "options/bv_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
#include "theory/theory.h"

namespace cvc5 {
namespace preprocessing {
namespace passes {
using namespace cvc5::theory;

BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
{
  d_boolToBVMode = options().bv.boolToBitvector;
};

PreprocessingPassResult BoolToBV::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  d_preprocContext->spendResource(Resource::PreprocessStep);

  size_t size = assertionsToPreprocess->size();

  if (d_boolToBVMode == options::BoolToBVMode::ALL)
  {
    for (size_t i = 0; i < size; ++i)
    {
      Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
      assertionsToPreprocess->replace(i, rewrite(newAssertion));
    }
  }
  else
  {
    Assert(d_boolToBVMode == options::BoolToBVMode::ITE);
    for (size_t i = 0; i < size; ++i)
    {
      assertionsToPreprocess->replace(
          i, rewrite(lowerIte((*assertionsToPreprocess)[i])));
    }
  }

  return PreprocessingPassResult::NO_CONFLICT;
}

void BoolToBV::updateCache(TNode n, TNode rebuilt)
{
  // check more likely case first
  if ((n.getKind() != kind::ITE) || !n[1].getType().isBitVector())
  {
    d_lowerCache[n] = rebuilt;
  }
  else
  {
    d_iteBVLowerCache[n] = rebuilt;
  }
}

Node BoolToBV::fromCache(TNode n) const
{
  // check more likely case first
  if (n.getKind() != kind::ITE)
  {
    if (d_lowerCache.find(n) != d_lowerCache.end())
    {
      return d_lowerCache.at(n);
    }
  }
  else
  {
    if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end())
    {
      return d_iteBVLowerCache.at(n);
    }
  }
  return n;
}

inline bool BoolToBV::inCache(const Node& n) const
{
  return (ContainsKey(d_lowerCache, n) || ContainsKey(d_iteBVLowerCache, n));
}

bool BoolToBV::needToRebuild(TNode n) const
{
  // check if any children were rebuilt
  for (const Node& nn : n)
  {
    if (inCache(nn))
    {
      return true;
    }
  }
  return false;
}

Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction)
{
  // first try to lower all the children
  for (const Node& c : assertion)
  {
    lowerNode(c, allowIteIntroduction);
  }

  // now try lowering the assertion, but don't force it with an ITE (even in mode all)
  lowerNode(assertion, false);
  Node newAssertion = fromCache(assertion);
  TypeNode newAssertionType = newAssertion.getType();
  if (newAssertionType.isBitVector())
  {
    Assert(newAssertionType.getBitVectorSize() == 1);
    newAssertion = NodeManager::currentNM()->mkNode(
        kind::EQUAL, newAssertion, bv::utils::mkOne(1));
    newAssertionType = newAssertion.getType();
  }
  Assert(newAssertionType.isBoolean());
  return newAssertion;
}

Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction)
{
  std::vector<TNode> to_visit;
  to_visit.push_back(node);
  std::unordered_set<TNode> visited;

  while (!to_visit.empty())
  {
    TNode n = to_visit.back();
    to_visit.pop_back();

    Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
                        << n << " and visited = " << ContainsKey(visited, n)
                        << std::endl;

    // Mark as visited
    if (ContainsKey(visited, n))
    {
      visit(n, allowIteIntroduction);
    }
    else
    {
      visited.insert(n);
      to_visit.push_back(n);

      // insert children in reverse order so that they're processed in order
      //    important for rewriting which sorts by node id
      // NOTE: size_t is unsigned, so using underflow for termination condition
      size_t numChildren = n.getNumChildren();
      for (size_t i = numChildren - 1; i < numChildren; --i)
      {
        to_visit.push_back(n[i]);
      }
    }
  }

  return fromCache(node);
}

void BoolToBV::visit(const TNode& n, bool allowIteIntroduction)
{
  Kind k = n.getKind();

  // easy case -- just replace boolean constant
  if (k == kind::CONST_BOOLEAN)
  {
    updateCache(n,
                (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
                                           : bv::utils::mkZero(1));
    return;
  }

  NodeManager* nm = NodeManager::currentNM();
  Kind new_kind = k;
  switch (k)
  {
    case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
    case kind::AND: new_kind = kind::BITVECTOR_AND; break;
    case kind::OR: new_kind = kind::BITVECTOR_OR; break;
    case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
    case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
    case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break;
    case kind::ITE: new_kind = kind::BITVECTOR_ITE; break;
    case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
    case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
    case kind::BITVECTOR_ULE:
    case kind::BITVECTOR_UGT:
    case kind::BITVECTOR_UGE:
    case kind::BITVECTOR_SLE:
    case kind::BITVECTOR_SGT:
    case kind::BITVECTOR_SGE:
      // Should have been removed by rewriting.
      Unreachable();
    default: break;
  }

  // check if it's safe to lower or rebuild the node
  // Note: might have to rebuild to keep changes to children, even if this node
  // isn't being lowered

  // it's safe to lower if all the children are bit-vectors
  bool safe_to_lower =
      (new_kind != k);  // don't need to lower at all if kind hasn't changed

  // it's safe to rebuild if rebuilding doesn't change any of the types of the
  // children
  bool safe_to_rebuild = true;

  for (const Node& nn : n)
  {
    safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector();
    safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType());

    // if it's already not safe to do either, stop checking
    if (!safe_to_lower && !safe_to_rebuild)
    {
      break;
    }
  }

  Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower
                      << ", safe_to_rebuild = " << safe_to_rebuild << std::endl;

  if (new_kind != k && safe_to_lower)
  {
    // lower to BV
    rebuildNode(n, new_kind);
    return;
  }
  else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean())
  {
    // lower to BV using an ITE

    if (safe_to_rebuild && needToRebuild(n))
    {
      // need to rebuild to keep changes made to descendants
      rebuildNode(n, k);
    }

    updateCache(n,
                nm->mkNode(kind::ITE,
                           fromCache(n),
                           bv::utils::mkOne(1),
                           bv::utils::mkZero(1)));
    Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
                        << " =>\n"
                        << fromCache(n) << std::endl;
    if (d_boolToBVMode == options::BoolToBVMode::ALL)
    {
      // this statistic only makes sense for ALL mode
      ++(d_statistics.d_numIntroducedItes);
    }
    return;
  }
  else if (safe_to_rebuild && needToRebuild(n))
  {
    // rebuild to incorporate changes to children
    Assert(k == new_kind);
    rebuildNode(n, k);
  }
  else if (allowIteIntroduction && fromCache(n).getType().isBoolean())
  {
    // force booleans (which haven't already been converted) to bit-vector
    // needed to maintain the invariant that all boolean children
    // have been converted (even constants and variables) when forcing
    // with ITE introductions
    updateCache(
        n, nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)));
    Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
                        << " =>\n"
                        << fromCache(n) << std::endl;
    if (d_boolToBVMode == options::BoolToBVMode::ALL)
    {
      // this statistic only makes sense for ALL mode
      ++(d_statistics.d_numIntroducedItes);
    }
  }
  else
  {
    // do nothing
    Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n
                        << std::endl;
  }
}

Node BoolToBV::lowerIte(const TNode& node)
{
  std::vector<TNode> visit;
  visit.push_back(node);
  std::unordered_set<TNode> visited;

  while (!visit.empty())
  {
    TNode n = visit.back();
    visit.pop_back();

    Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
                        << " and visited = " << ContainsKey(visited, n)
                        << std::endl;

    // Look for ITEs and mark visited
    if (!ContainsKey(visited, n))
    {
      if ((n.getKind() == kind::ITE) && n[1].getType().isBitVector())
      {
        Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0]
                            << " to set of ite conditions" << std::endl;
        // don't force in this case -- forcing only introduces more ITEs
        Node loweredNode = lowerNode(n, false);
        // some of the lowered nodes might appear elsewhere but not in an ITE
        // reset the cache to prevent lowering them
        // the bit-vector ITEs are still tracked in d_iteBVLowerCache though
        d_lowerCache.clear();
      }
      else
      {
        visit.push_back(n);
        visited.insert(n);
        // insert in reverse order so that they're processed in order
        for (int i = n.getNumChildren() - 1; i >= 0; --i)
        {
          visit.push_back(n[i]);
        }
      }
    }
    else if (needToRebuild(n))
    {
      // Note: it's always safe to rebuild here, because we've only lowered
      //       ITEs of type bit-vector to BITVECTOR_ITE
      rebuildNode(n, n.getKind());
    }
    else
    {
      Debug("bool-to-bv")
          << "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
          << std::endl;
    }
  }
  return fromCache(node);
}

void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
{
  Kind k = n.getKind();
  NodeManager* nm = NodeManager::currentNM();
  NodeBuilder builder(new_kind);

  Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
                      << " and new_kind = " << kindToString(new_kind)
                      << std::endl;

  if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
  {
    // this statistic only makes sense for ALL mode
    ++(d_statistics.d_numTermsLowered);
  }

  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
  {
    builder << n.getOperator();
  }

  // special case IMPLIES because needs to be rewritten
  if ((k == kind::IMPLIES) && (new_kind != k))
  {
    builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0]));
    builder << fromCache(n[1]);
  }
  else
  {
    for (const Node& nn : n)
    {
      builder << fromCache(nn);
    }
  }

  Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n"
                      << builder << std::endl;

  updateCache(n, builder.constructNode());
}

BoolToBV::Statistics::Statistics()
    : d_numIteToBvite(smtStatisticsRegistry().registerInt(
        "preprocessing::passes::BoolToBV::NumIteToBvite")),
      // the following two statistics are not correct in the ITE mode, because
      // we might discard rebuilt nodes if we fails to convert a bool to
      // width-one bit-vector (never forces)
      d_numTermsLowered(smtStatisticsRegistry().registerInt(
          "preprocessing::passes:BoolToBV::NumTermsLowered")),
      d_numIntroducedItes(smtStatisticsRegistry().registerInt(
          "preprocessing::passes::BoolToBV::NumTermsForcedLowered"))
{
}

}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Makai Mann, Yoni Zohar, 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		* The BoolToBV preprocessing pass.
14		*
15		*/
16
17		#include "preprocessing/passes/bool_to_bv.h"
18
19		#include <string>
20
21		#include "base/map_util.h"
22		#include "expr/node.h"
23		#include "options/bv_options.h"
24		#include "preprocessing/assertion_pipeline.h"
25		#include "preprocessing/preprocessing_pass_context.h"
26		#include "smt/smt_statistics_registry.h"
27		#include "theory/bv/theory_bv_utils.h"
28		#include "theory/rewriter.h"
29		#include "theory/theory.h"
30
31		namespace cvc5 {
32		namespace preprocessing {
33		namespace passes {
34		using namespace cvc5::theory;
35
36	9915	BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
37	9915	: PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
38		{
39	9915	d_boolToBVMode = options().bv.boolToBitvector;
40	9915	};
41
42	12	PreprocessingPassResult BoolToBV::applyInternal(
43		AssertionPipeline* assertionsToPreprocess)
44		{
45	12	d_preprocContext->spendResource(Resource::PreprocessStep);
46
47	12	size_t size = assertionsToPreprocess->size();
48
49	12	if (d_boolToBVMode == options::BoolToBVMode::ALL)
50		{
51	74	for (size_t i = 0; i < size; ++i)
52		{
53	132	Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true);
54	66	assertionsToPreprocess->replace(i, rewrite(newAssertion));
55		}
56		}
57		else
58		{
59	4	Assert(d_boolToBVMode == options::BoolToBVMode::ITE);
60	24	for (size_t i = 0; i < size; ++i)
61		{
62	20	assertionsToPreprocess->replace(
63	40	i, rewrite(lowerIte((*assertionsToPreprocess)[i])));
64		}
65		}
66
67	12	return PreprocessingPassResult::NO_CONFLICT;
68		}
69
70	158	void BoolToBV::updateCache(TNode n, TNode rebuilt)
71		{
72		// check more likely case first
73	158	if ((n.getKind() != kind::ITE) \|\| !n[1].getType().isBitVector())
74		{
75	154	d_lowerCache[n] = rebuilt;
76		}
77		else
78		{
79	4	d_iteBVLowerCache[n] = rebuilt;
80		}
81	158	}
82
83	1342	Node BoolToBV::fromCache(TNode n) const
84		{
85		// check more likely case first
86	1342	if (n.getKind() != kind::ITE)
87		{
88	1326	if (d_lowerCache.find(n) != d_lowerCache.end())
89		{
90	734	return d_lowerCache.at(n);
91		}
92		}
93		else
94		{
95	16	if (d_iteBVLowerCache.find(n) != d_iteBVLowerCache.end())
96		{
97	8	return d_iteBVLowerCache.at(n);
98		}
99		}
100	600	return n;
101		}
102
103	216	inline bool BoolToBV::inCache(const Node& n) const
104		{
105	216	return (ContainsKey(d_lowerCache, n) \|\| ContainsKey(d_iteBVLowerCache, n));
106		}
107
108	536	bool BoolToBV::needToRebuild(TNode n) const
109		{
110		// check if any children were rebuilt
111	748	for (const Node& nn : n)
112		{
113	216	if (inCache(nn))
114		{
115	4	return true;
116		}
117		}
118	532	return false;
119		}
120
121	66	Node BoolToBV::lowerAssertion(const TNode& assertion, bool allowIteIntroduction)
122		{
123		// first try to lower all the children
124	168	for (const Node& c : assertion)
125		{
126	102	lowerNode(c, allowIteIntroduction);
127		}
128
129		// now try lowering the assertion, but don't force it with an ITE (even in mode all)
130	66	lowerNode(assertion, false);
131	66	Node newAssertion = fromCache(assertion);
132	132	TypeNode newAssertionType = newAssertion.getType();
133	66	if (newAssertionType.isBitVector())
134		{
135	62	Assert(newAssertionType.getBitVectorSize() == 1);
136	124	newAssertion = NodeManager::currentNM()->mkNode(
137	124	kind::EQUAL, newAssertion, bv::utils::mkOne(1));
138	62	newAssertionType = newAssertion.getType();
139		}
140	66	Assert(newAssertionType.isBoolean());
141	132	return newAssertion;
142		}
143
144	172	Node BoolToBV::lowerNode(const TNode& node, bool allowIteIntroduction)
145		{
146	344	std::vector<TNode> to_visit;
147	172	to_visit.push_back(node);
148	344	std::unordered_set<TNode> visited;
149
150	2540	while (!to_visit.empty())
151		{
152	2368	TNode n = to_visit.back();
153	1184	to_visit.pop_back();
154
155	2368	Debug("bool-to-bv") << "BoolToBV::lowerNode: Post-order traversal with "
156	2368	<< n << " and visited = " << ContainsKey(visited, n)
157	1184	<< std::endl;
158
159		// Mark as visited
160	1184	if (ContainsKey(visited, n))
161		{
162	614	visit(n, allowIteIntroduction);
163		}
164		else
165		{
166	570	visited.insert(n);
167	570	to_visit.push_back(n);
168
169		// insert children in reverse order so that they're processed in order
170		// important for rewriting which sorts by node id
171		// NOTE: size_t is unsigned, so using underflow for termination condition
172	570	size_t numChildren = n.getNumChildren();
173	1012	for (size_t i = numChildren - 1; i < numChildren; --i)
174		{
175	442	to_visit.push_back(n[i]);
176		}
177		}
178		}
179
180	344	return fromCache(node);
181		}
182
183	614	void BoolToBV::visit(const TNode& n, bool allowIteIntroduction)
184		{
185	614	Kind k = n.getKind();
186
187		// easy case -- just replace boolean constant
188	614	if (k == kind::CONST_BOOLEAN)
189		{
190	10	updateCache(n,
191	20	(n == bv::utils::mkTrue()) ? bv::utils::mkOne(1)
192		: bv::utils::mkZero(1));
193	132	return;
194		}
195
196	604	NodeManager* nm = NodeManager::currentNM();
197	604	Kind new_kind = k;
198	604	switch (k)
199		{
200	38	case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
201	10	case kind::AND: new_kind = kind::BITVECTOR_AND; break;
202	4	case kind::OR: new_kind = kind::BITVECTOR_OR; break;
203	26	case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
204	6	case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
205	20	case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break;
206	12	case kind::ITE: new_kind = kind::BITVECTOR_ITE; break;
207	16	case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
208	4	case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
209		case kind::BITVECTOR_ULE:
210		case kind::BITVECTOR_UGT:
211		case kind::BITVECTOR_UGE:
212		case kind::BITVECTOR_SLE:
213		case kind::BITVECTOR_SGT:
214		case kind::BITVECTOR_SGE:
215		// Should have been removed by rewriting.
216		Unreachable();
217	468	default: break;
218		}
219
220		// check if it's safe to lower or rebuild the node
221		// Note: might have to rebuild to keep changes to children, even if this node
222		// isn't being lowered
223
224		// it's safe to lower if all the children are bit-vectors
225	604	bool safe_to_lower =
226	604	(new_kind != k); // don't need to lower at all if kind hasn't changed
227
228		// it's safe to rebuild if rebuilding doesn't change any of the types of the
229		// children
230	604	bool safe_to_rebuild = true;
231
232	998	for (const Node& nn : n)
233		{
234	434	safe_to_lower = safe_to_lower && fromCache(nn).getType().isBitVector();
235	434	safe_to_rebuild = safe_to_rebuild && (fromCache(nn).getType() == nn.getType());
236
237		// if it's already not safe to do either, stop checking
238	434	if (!safe_to_lower && !safe_to_rebuild)
239		{
240	40	break;
241		}
242		}
243
244	1208	Debug("bool-to-bv") << "safe_to_lower = " << safe_to_lower
245	604	<< ", safe_to_rebuild = " << safe_to_rebuild << std::endl;
246
247	604	if (new_kind != k && safe_to_lower)
248		{
249		// lower to BV
250	104	rebuildNode(n, new_kind);
251	104	return;
252		}
253	500	else if (new_kind != k && allowIteIntroduction && fromCache(n).getType().isBoolean())
254		{
255		// lower to BV using an ITE
256
257	8	if (safe_to_rebuild && needToRebuild(n))
258		{
259		// need to rebuild to keep changes made to descendants
260		rebuildNode(n, k);
261		}
262
263	8	updateCache(n,
264	48	nm->mkNode(kind::ITE,
265	16	fromCache(n),
266	16	bv::utils::mkOne(1),
267	16	bv::utils::mkZero(1)));
268	16	Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
269	8	<< " =>\n"
270	8	<< fromCache(n) << std::endl;
271	8	if (d_boolToBVMode == options::BoolToBVMode::ALL)
272		{
273		// this statistic only makes sense for ALL mode
274	8	++(d_statistics.d_numIntroducedItes);
275		}
276	8	return;
277		}
278	492	else if (safe_to_rebuild && needToRebuild(n))
279		{
280		// rebuild to incorporate changes to children
281		Assert(k == new_kind);
282		rebuildNode(n, k);
283		}
284	492	else if (allowIteIntroduction && fromCache(n).getType().isBoolean())
285		{
286		// force booleans (which haven't already been converted) to bit-vector
287		// needed to maintain the invariant that all boolean children
288		// have been converted (even constants and variables) when forcing
289		// with ITE introductions
290	32	updateCache(
291	64	n, nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)));
292	64	Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
293	32	<< " =>\n"
294	32	<< fromCache(n) << std::endl;
295	32	if (d_boolToBVMode == options::BoolToBVMode::ALL)
296		{
297		// this statistic only makes sense for ALL mode
298	32	++(d_statistics.d_numIntroducedItes);
299		}
300		}
301		else
302		{
303		// do nothing
304	920	Debug("bool-to-bv") << "BoolToBV::visit skipping: " << n
305	460	<< std::endl;
306		}
307		}
308
309	20	Node BoolToBV::lowerIte(const TNode& node)
310		{
311	40	std::vector<TNode> visit;
312	20	visit.push_back(node);
313	40	std::unordered_set<TNode> visited;
314
315	316	while (!visit.empty())
316		{
317	296	TNode n = visit.back();
318	148	visit.pop_back();
319
320	296	Debug("bool-to-bv") << "BoolToBV::lowerIte: Post-order traversal with " << n
321	296	<< " and visited = " << ContainsKey(visited, n)
322	148	<< std::endl;
323
324		// Look for ITEs and mark visited
325	148	if (!ContainsKey(visited, n))
326		{
327	72	if ((n.getKind() == kind::ITE) && n[1].getType().isBitVector())
328		{
329	8	Debug("bool-to-bv") << "BoolToBV::lowerIte: adding " << n[0]
330	4	<< " to set of ite conditions" << std::endl;
331		// don't force in this case -- forcing only introduces more ITEs
332	8	Node loweredNode = lowerNode(n, false);
333		// some of the lowered nodes might appear elsewhere but not in an ITE
334		// reset the cache to prevent lowering them
335		// the bit-vector ITEs are still tracked in d_iteBVLowerCache though
336	4	d_lowerCache.clear();
337		}
338		else
339		{
340	68	visit.push_back(n);
341	68	visited.insert(n);
342		// insert in reverse order so that they're processed in order
343	128	for (int i = n.getNumChildren() - 1; i >= 0; --i)
344		{
345	60	visit.push_back(n[i]);
346		}
347		}
348		}
349	76	else if (needToRebuild(n))
350		{
351		// Note: it's always safe to rebuild here, because we've only lowered
352		// ITEs of type bit-vector to BITVECTOR_ITE
353	4	rebuildNode(n, n.getKind());
354		}
355		else
356		{
357	144	Debug("bool-to-bv")
358	72	<< "BoolToBV::lowerIte Skipping because don't need to rebuild: " << n
359	72	<< std::endl;
360		}
361		}
362	40	return fromCache(node);
363		}
364
365	108	void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
366		{
367	108	Kind k = n.getKind();
368	108	NodeManager* nm = NodeManager::currentNM();
369	216	NodeBuilder builder(new_kind);
370
371	216	Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
372	216	<< " and new_kind = " << kindToString(new_kind)
373	108	<< std::endl;
374
375	108	if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
376		{
377		// this statistic only makes sense for ALL mode
378	96	++(d_statistics.d_numTermsLowered);
379		}
380
381	108	if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
382		{
383		builder << n.getOperator();
384		}
385
386		// special case IMPLIES because needs to be rewritten
387	108	if ((k == kind::IMPLIES) && (new_kind != k))
388		{
389	20	builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0]));
390	20	builder << fromCache(n[1]);
391		}
392		else
393		{
394	250	for (const Node& nn : n)
395		{
396	162	builder << fromCache(nn);
397		}
398		}
399
400	216	Debug("bool-to-bv") << "BoolToBV::rebuildNode " << n << " =>\n"
401	108	<< builder << std::endl;
402
403	108	updateCache(n, builder.constructNode());
404	108	}
405
406	9915	BoolToBV::Statistics::Statistics()
407	9915	: d_numIteToBvite(smtStatisticsRegistry().registerInt(
408	19830	"preprocessing::passes::BoolToBV::NumIteToBvite")),
409		// the following two statistics are not correct in the ITE mode, because
410		// we might discard rebuilt nodes if we fails to convert a bool to
411		// width-one bit-vector (never forces)
412	9915	d_numTermsLowered(smtStatisticsRegistry().registerInt(
413	19830	"preprocessing::passes:BoolToBV::NumTermsLowered")),
414	9915	d_numIntroducedItes(smtStatisticsRegistry().registerInt(
415	29745	"preprocessing::passes::BoolToBV::NumTermsForcedLowered"))
416		{
417	9915	}
418
419		} // namespace passes
420		} // namespace preprocessing
421	29511	} // namespace cvc5