Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/bv_to_bool.cpp	Lines:	152	156	97.4 %
Date:	2021-05-22	Branches:	370	914	40.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Yoni Zohar, Liana Hadarean, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Preprocessing pass that lifts bit-vectors of size 1 to booleans.
 *
 * Implemented recursively.
 */

#include "preprocessing/passes/bv_to_bool.h"

#include <string>
#include <unordered_map>
#include <vector>

#include "expr/node.h"
#include "expr/node_visitor.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 std;
using namespace cvc5::theory;

BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "bv-to-bool"),
      d_liftCache(),
      d_boolCache(),
      d_one(bv::utils::mkOne(1)),
      d_zero(bv::utils::mkZero(1)),
      d_statistics(){};

PreprocessingPassResult BVToBool::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  d_preprocContext->spendResource(Resource::PreprocessStep);
  std::vector<Node> new_assertions;
  liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
  {
    assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
  }
  return PreprocessingPassResult::NO_CONFLICT;
}

void BVToBool::addToLiftCache(TNode term, Node new_term)
{
  Assert(new_term != Node());
  Assert(!hasLiftCache(term));
  Assert(term.getType() == new_term.getType());
  d_liftCache[term] = new_term;
}

Node BVToBool::getLiftCache(TNode term) const
{
  Assert(hasLiftCache(term));
  return d_liftCache.find(term)->second;
}

bool BVToBool::hasLiftCache(TNode term) const
{
  return d_liftCache.find(term) != d_liftCache.end();
}

void BVToBool::addToBoolCache(TNode term, Node new_term)
{
  Assert(new_term != Node());
  Assert(!hasBoolCache(term));
  Assert(bv::utils::getSize(term) == 1);
  Assert(new_term.getType().isBoolean());
  d_boolCache[term] = new_term;
}

Node BVToBool::getBoolCache(TNode term) const
{
  Assert(hasBoolCache(term));
  return d_boolCache.find(term)->second;
}

bool BVToBool::hasBoolCache(TNode term) const
{
  return d_boolCache.find(term) != d_boolCache.end();
}
bool BVToBool::isConvertibleBvAtom(TNode node)
{
  Kind kind = node.getKind();
  return (kind == kind::EQUAL && node[0].getType().isBitVector()
          && node[0].getType().getBitVectorSize() == 1
          && node[1].getType().isBitVector()
          && node[1].getType().getBitVectorSize() == 1
          && node[0].getKind() != kind::BITVECTOR_EXTRACT
          && node[1].getKind() != kind::BITVECTOR_EXTRACT);
}

bool BVToBool::isConvertibleBvTerm(TNode node)
{
  if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
    return false;

  Kind kind = node.getKind();

  if (kind == kind::CONST_BITVECTOR || kind == kind::ITE
      || kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
      || kind == kind::BITVECTOR_NOT || kind == kind::BITVECTOR_XOR
      || kind == kind::BITVECTOR_COMP)
  {
    return true;
  }

  return false;
}

Node BVToBool::convertBvAtom(TNode node)
{
  Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
  Assert(bv::utils::getSize(node[0]) == 1);
  Assert(bv::utils::getSize(node[1]) == 1);
  Node a = convertBvTerm(node[0]);
  Node b = convertBvTerm(node[1]);
  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
  Debug("bv-to-bool") << "BVToBool::convertBvAtom " << node << " => " << result
                      << "\n";

  ++(d_statistics.d_numAtomsLifted);
  return result;
}

Node BVToBool::convertBvTerm(TNode node)
{
  Assert(node.getType().isBitVector()
         && node.getType().getBitVectorSize() == 1);

  if (hasBoolCache(node)) return getBoolCache(node);

  NodeManager* nm = NodeManager::currentNM();

  if (!isConvertibleBvTerm(node))
  {
    ++(d_statistics.d_numTermsForcedLifted);
    Node result = nm->mkNode(kind::EQUAL, node, d_one);
    addToBoolCache(node, result);
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
                        << result << "\n";
    return result;
  }

  if (node.getNumChildren() == 0)
  {
    Assert(node.getKind() == kind::CONST_BITVECTOR);
    Node result = node == d_one ? bv::utils::mkTrue() : bv::utils::mkFalse();
    // addToCache(node, result);
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
                        << result << "\n";
    return result;
  }

  ++(d_statistics.d_numTermsLifted);

  Kind kind = node.getKind();
  if (kind == kind::ITE)
  {
    Node cond = liftNode(node[0]);
    Node true_branch = convertBvTerm(node[1]);
    Node false_branch = convertBvTerm(node[2]);
    Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch);
    addToBoolCache(node, result);
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
                        << result << "\n";
    return result;
  }

  Kind new_kind;
  // special case for XOR as it has to be binary
  // while BITVECTOR_XOR can be n-ary
  if (kind == kind::BITVECTOR_XOR)
  {
    new_kind = kind::XOR;
    Node result = convertBvTerm(node[0]);
    for (unsigned i = 1; i < node.getNumChildren(); ++i)
    {
      Node converted = convertBvTerm(node[i]);
      result = nm->mkNode(kind::XOR, result, converted);
    }
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
                        << result << "\n";
    return result;
  }

  if (kind == kind::BITVECTOR_COMP)
  {
    Node result = nm->mkNode(kind::EQUAL, node[0], node[1]);
    addToBoolCache(node, result);
    Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
                        << result << "\n";
    return result;
  }

  switch (kind)
  {
    case kind::BITVECTOR_OR: new_kind = kind::OR; break;
    case kind::BITVECTOR_AND: new_kind = kind::AND; break;
    case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
    default: Unhandled();
  }

  NodeBuilder builder(new_kind);
  for (unsigned i = 0; i < node.getNumChildren(); ++i)
  {
    builder << convertBvTerm(node[i]);
  }

  Node result = builder;
  addToBoolCache(node, result);
  Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => " << result
                      << "\n";
  return result;
}

Node BVToBool::liftNode(TNode current)
{
  Node result;

  if (hasLiftCache(current))
  {
    result = getLiftCache(current);
  }
  else if (isConvertibleBvAtom(current))
  {
    result = convertBvAtom(current);
    addToLiftCache(current, result);
  }
  else
  {
    if (current.getNumChildren() == 0)
    {
      result = current;
    }
    else
    {
      NodeBuilder builder(current.getKind());
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        builder << current.getOperator();
      }
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
      {
        // Recursively lift children
        Node converted = liftNode(current[i]);
        Assert(converted.getType() == current[i].getType());
        builder << converted;
      }
      result = builder;
      addToLiftCache(current, result);
    }
  }
  Assert(result != Node());
  Assert(result.getType() == current.getType());
  Debug("bv-to-bool") << "BVToBool::liftNode " << current << " => \n"
                      << result << "\n";
  return result;
}

void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
                            std::vector<Node>& new_assertions)
{
  for (unsigned i = 0; i < assertions.size(); ++i)
  {
    Node new_assertion = liftNode(assertions[i]);
    new_assertions.push_back(Rewriter::rewrite(new_assertion));
    Trace("bv-to-bool") << "  " << assertions[i] << " => " << new_assertions[i]
                        << "\n";
  }
}

BVToBool::Statistics::Statistics()
    : d_numTermsLifted(smtStatisticsRegistry().registerInt(
        "preprocessing::passes::BVToBool::NumTermsLifted")),
      d_numAtomsLifted(smtStatisticsRegistry().registerInt(
          "preprocessing::passes::BVToBool::NumAtomsLifted")),
      d_numTermsForcedLifted(smtStatisticsRegistry().registerInt(
          "preprocessing::passes::BVToBool::NumTermsForcedLifted"))
{
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Yoni Zohar, Liana Hadarean, Aina Niemetz
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		* Preprocessing pass that lifts bit-vectors of size 1 to booleans.
14		*
15		* Implemented recursively.
16		*/
17
18		#include "preprocessing/passes/bv_to_bool.h"
19
20		#include <string>
21		#include <unordered_map>
22		#include <vector>
23
24		#include "expr/node.h"
25		#include "expr/node_visitor.h"
26		#include "preprocessing/assertion_pipeline.h"
27		#include "preprocessing/preprocessing_pass_context.h"
28		#include "smt/smt_statistics_registry.h"
29		#include "theory/bv/theory_bv_utils.h"
30		#include "theory/rewriter.h"
31		#include "theory/theory.h"
32
33		namespace cvc5 {
34		namespace preprocessing {
35		namespace passes {
36
37		using namespace std;
38		using namespace cvc5::theory;
39
40	9459	BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
41		: PreprocessingPass(preprocContext, "bv-to-bool"),
42		d_liftCache(),
43		d_boolCache(),
44		d_one(bv::utils::mkOne(1)),
45		d_zero(bv::utils::mkZero(1)),
46	9459	d_statistics(){};
47
48	155	PreprocessingPassResult BVToBool::applyInternal(
49		AssertionPipeline* assertionsToPreprocess)
50		{
51	155	d_preprocContext->spendResource(Resource::PreprocessStep);
52	310	std::vector<Node> new_assertions;
53	155	liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
54	600	for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
55		{
56	445	assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
57		}
58	310	return PreprocessingPassResult::NO_CONFLICT;
59		}
60
61	989	void BVToBool::addToLiftCache(TNode term, Node new_term)
62		{
63	989	Assert(new_term != Node());
64	989	Assert(!hasLiftCache(term));
65	989	Assert(term.getType() == new_term.getType());
66	989	d_liftCache[term] = new_term;
67	989	}
68
69	81	Node BVToBool::getLiftCache(TNode term) const
70		{
71	81	Assert(hasLiftCache(term));
72	81	return d_liftCache.find(term)->second;
73		}
74
75	3158	bool BVToBool::hasLiftCache(TNode term) const
76		{
77	3158	return d_liftCache.find(term) != d_liftCache.end();
78		}
79
80	148	void BVToBool::addToBoolCache(TNode term, Node new_term)
81		{
82	148	Assert(new_term != Node());
83	148	Assert(!hasBoolCache(term));
84	148	Assert(bv::utils::getSize(term) == 1);
85	148	Assert(new_term.getType().isBoolean());
86	148	d_boolCache[term] = new_term;
87	148	}
88
89	36	Node BVToBool::getBoolCache(TNode term) const
90		{
91	36	Assert(hasBoolCache(term));
92	36	return d_boolCache.find(term)->second;
93		}
94
95	524	bool BVToBool::hasBoolCache(TNode term) const
96		{
97	524	return d_boolCache.find(term) != d_boolCache.end();
98		}
99	2007	bool BVToBool::isConvertibleBvAtom(TNode node)
100		{
101	2007	Kind kind = node.getKind();
102	2278	return (kind == kind::EQUAL && node[0].getType().isBitVector()
103	2240	&& node[0].getType().getBitVectorSize() == 1
104	2107	&& node[1].getType().isBitVector()
105	2107	&& node[1].getType().getBitVectorSize() == 1
106	2107	&& node[0].getKind() != kind::BITVECTOR_EXTRACT
107	4112	&& node[1].getKind() != kind::BITVECTOR_EXTRACT);
108		}
109
110	304	bool BVToBool::isConvertibleBvTerm(TNode node)
111		{
112	304	if (!node.getType().isBitVector() \|\| node.getType().getBitVectorSize() != 1)
113		return false;
114
115	304	Kind kind = node.getKind();
116
117	304	if (kind == kind::CONST_BITVECTOR \|\| kind == kind::ITE
118	98	\|\| kind == kind::BITVECTOR_AND \|\| kind == kind::BITVECTOR_OR
119	90	\|\| kind == kind::BITVECTOR_NOT \|\| kind == kind::BITVECTOR_XOR
120	88	\|\| kind == kind::BITVECTOR_COMP)
121		{
122	230	return true;
123		}
124
125	74	return false;
126		}
127
128	98	Node BVToBool::convertBvAtom(TNode node)
129		{
130	98	Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
131	98	Assert(bv::utils::getSize(node[0]) == 1);
132	98	Assert(bv::utils::getSize(node[1]) == 1);
133	196	Node a = convertBvTerm(node[0]);
134	196	Node b = convertBvTerm(node[1]);
135	98	Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
136	196	Debug("bv-to-bool") << "BVToBool::convertBvAtom " << node << " => " << result
137	98	<< "\n";
138
139	98	++(d_statistics.d_numAtomsLifted);
140	196	return result;
141		}
142
143	340	Node BVToBool::convertBvTerm(TNode node)
144		{
145	340	Assert(node.getType().isBitVector()
146		&& node.getType().getBitVectorSize() == 1);
147
148	340	if (hasBoolCache(node)) return getBoolCache(node);
149
150	304	NodeManager* nm = NodeManager::currentNM();
151
152	304	if (!isConvertibleBvTerm(node))
153		{
154	74	++(d_statistics.d_numTermsForcedLifted);
155	148	Node result = nm->mkNode(kind::EQUAL, node, d_one);
156	74	addToBoolCache(node, result);
157	148	Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
158	74	<< result << "\n";
159	74	return result;
160		}
161
162	230	if (node.getNumChildren() == 0)
163		{
164	154	Assert(node.getKind() == kind::CONST_BITVECTOR);
165	308	Node result = node == d_one ? bv::utils::mkTrue() : bv::utils::mkFalse();
166		// addToCache(node, result);
167	308	Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
168	154	<< result << "\n";
169	154	return result;
170		}
171
172	76	++(d_statistics.d_numTermsLifted);
173
174	76	Kind kind = node.getKind();
175	76	if (kind == kind::ITE)
176		{
177	104	Node cond = liftNode(node[0]);
178	104	Node true_branch = convertBvTerm(node[1]);
179	104	Node false_branch = convertBvTerm(node[2]);
180	104	Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch);
181	52	addToBoolCache(node, result);
182	104	Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
183	52	<< result << "\n";
184	52	return result;
185		}
186
187		Kind new_kind;
188		// special case for XOR as it has to be binary
189		// while BITVECTOR_XOR can be n-ary
190	24	if (kind == kind::BITVECTOR_XOR)
191		{
192	2	new_kind = kind::XOR;
193	4	Node result = convertBvTerm(node[0]);
194	4	for (unsigned i = 1; i < node.getNumChildren(); ++i)
195		{
196	4	Node converted = convertBvTerm(node[i]);
197	2	result = nm->mkNode(kind::XOR, result, converted);
198		}
199	4	Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
200	2	<< result << "\n";
201	2	return result;
202		}
203
204	22	if (kind == kind::BITVECTOR_COMP)
205		{
206	28	Node result = nm->mkNode(kind::EQUAL, node[0], node[1]);
207	14	addToBoolCache(node, result);
208	28	Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
209	14	<< result << "\n";
210	14	return result;
211		}
212
213	8	switch (kind)
214		{
215		case kind::BITVECTOR_OR: new_kind = kind::OR; break;
216	8	case kind::BITVECTOR_AND: new_kind = kind::AND; break;
217		case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
218		default: Unhandled();
219		}
220
221	16	NodeBuilder builder(new_kind);
222	44	for (unsigned i = 0; i < node.getNumChildren(); ++i)
223		{
224	36	builder << convertBvTerm(node[i]);
225		}
226
227	16	Node result = builder;
228	8	addToBoolCache(node, result);
229	16	Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => " << result
230	8	<< "\n";
231	8	return result;
232		}
233
234	2088	Node BVToBool::liftNode(TNode current)
235		{
236	2088	Node result;
237
238	2088	if (hasLiftCache(current))
239		{
240	81	result = getLiftCache(current);
241		}
242	2007	else if (isConvertibleBvAtom(current))
243		{
244	98	result = convertBvAtom(current);
245	98	addToLiftCache(current, result);
246		}
247		else
248		{
249	1909	if (current.getNumChildren() == 0)
250		{
251	1018	result = current;
252		}
253		else
254		{
255	1782	NodeBuilder builder(current.getKind());
256	891	if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
257		{
258	118	builder << current.getOperator();
259		}
260	2482	for (unsigned i = 0; i < current.getNumChildren(); ++i)
261		{
262		// Recursively lift children
263	3182	Node converted = liftNode(current[i]);
264	1591	Assert(converted.getType() == current[i].getType());
265	1591	builder << converted;
266		}
267	891	result = builder;
268	891	addToLiftCache(current, result);
269		}
270		}
271	2088	Assert(result != Node());
272	2088	Assert(result.getType() == current.getType());
273	4176	Debug("bv-to-bool") << "BVToBool::liftNode " << current << " => \n"
274	2088	<< result << "\n";
275	2088	return result;
276		}
277
278	155	void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
279		std::vector<Node>& new_assertions)
280		{
281	600	for (unsigned i = 0; i < assertions.size(); ++i)
282		{
283	890	Node new_assertion = liftNode(assertions[i]);
284	445	new_assertions.push_back(Rewriter::rewrite(new_assertion));
285	890	Trace("bv-to-bool") << " " << assertions[i] << " => " << new_assertions[i]
286	445	<< "\n";
287		}
288	155	}
289
290	9459	BVToBool::Statistics::Statistics()
291	9459	: d_numTermsLifted(smtStatisticsRegistry().registerInt(
292	18918	"preprocessing::passes::BVToBool::NumTermsLifted")),
293	9459	d_numAtomsLifted(smtStatisticsRegistry().registerInt(
294	18918	"preprocessing::passes::BVToBool::NumAtomsLifted")),
295	9459	d_numTermsForcedLifted(smtStatisticsRegistry().registerInt(
296	28377	"preprocessing::passes::BVToBool::NumTermsForcedLifted"))
297		{
298	9459	}
299
300		} // namespace passes
301		} // namespace preprocessing
302	28191	} // namespace cvc5