Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/int_to_bv.cpp	Lines:	94	134	70.1 %
Date:	2021-05-24	Branches:	193	612	31.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli, Yoni Zohar, Alex Ozdemir
 *
 * 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 IntToBV preprocessing pass.
 *
 * Converts integer operations into bitvector operations. The width of the
 * bitvectors is controlled through the `--solve-int-as-bv` command line
 * option.
 */

#include "preprocessing/passes/int_to_bv.h"

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

#include "expr/node.h"
#include "expr/node_traversal.h"
#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "theory/rewriter.h"
#include "theory/theory.h"

namespace cvc5 {
namespace preprocessing {
namespace passes {

using namespace std;
using namespace cvc5::theory;

using NodeMap = std::unordered_map<Node, Node>;

namespace {

bool childrenTypesChanged(Node n, NodeMap& cache) {
  for (Node child : n) {
    TypeNode originalType = child.getType();
    TypeNode newType = cache[child].getType();
    if (! newType.isSubtypeOf(originalType)) {
      return true;
    }
  }
  return false;
}


Node intToBVMakeBinary(TNode n, NodeMap& cache)
{
  for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER,
           [&cache](TNode nn) { return cache.count(nn) > 0; }))
  {
    Node result;
    NodeManager* nm = NodeManager::currentNM();
    if (current.getNumChildren() == 0)
    {
      result = current;
    }
    else if (current.getNumChildren() > 2
             && (current.getKind() == kind::PLUS
                 || current.getKind() == kind::MULT))
    {
      Assert(cache.find(current[0]) != cache.end());
      result = cache[current[0]];
      for (unsigned i = 1; i < current.getNumChildren(); ++i)
      {
        Assert(cache.find(current[i]) != cache.end());
        Node child = current[i];
        Node childRes = cache[current[i]];
        result = nm->mkNode(current.getKind(), result, childRes);
      }
    }
    else
    {
      NodeBuilder builder(current.getKind());
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
        builder << current.getOperator();
      }

      for (unsigned i = 0; i < current.getNumChildren(); ++i)
      {
        Assert(cache.find(current[i]) != cache.end());
        builder << cache[current[i]];
      }
      result = builder;
    }
    cache[current] = result;
  }
  return cache[n];
}

Node intToBV(TNode n, NodeMap& cache)
{
  int size = options::solveIntAsBV();
  AlwaysAssert(size > 0);
  AlwaysAssert(!options::incrementalSolving());

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  NodeMap binaryCache;
  Node n_binary = intToBVMakeBinary(n, binaryCache);

  for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
           [&cache](TNode nn) { return cache.count(nn) > 0; }))
  {
    if (current.getNumChildren() > 0)
    {
      // Not a leaf
      vector<Node> children;
      unsigned max = 0;
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
      {
        Assert(cache.find(current[i]) != cache.end());
        TNode childRes = cache[current[i]];
        TypeNode type = childRes.getType();
        if (type.isBitVector())
        {
          unsigned bvsize = type.getBitVectorSize();
          if (bvsize > max)
          {
            max = bvsize;
          }
        }
        children.push_back(childRes);
      }

      kind::Kind_t newKind = current.getKind();
      if (max > 0)
      {
        switch (newKind)
        {
          case kind::PLUS:
            Assert(children.size() == 2);
            newKind = kind::BITVECTOR_ADD;
            max = max + 1;
            break;
          case kind::MULT:
            Assert(children.size() == 2);
            newKind = kind::BITVECTOR_MULT;
            max = max * 2;
            break;
          case kind::MINUS:
            Assert(children.size() == 2);
            newKind = kind::BITVECTOR_SUB;
            max = max + 1;
            break;
          case kind::UMINUS:
            Assert(children.size() == 1);
            newKind = kind::BITVECTOR_NEG;
            max = max + 1;
            break;
          case kind::LT: newKind = kind::BITVECTOR_SLT; break;
          case kind::LEQ: newKind = kind::BITVECTOR_SLE; break;
          case kind::GT: newKind = kind::BITVECTOR_SGT; break;
          case kind::GEQ: newKind = kind::BITVECTOR_SGE; break;
          case kind::EQUAL:
          case kind::ITE: break;
          default:
            if (childrenTypesChanged(current, cache)) {
              throw TypeCheckingExceptionPrivate(
                  current,
                  string("Cannot translate to BV: ") + current.toString());
            }
            break;
        }
        for (unsigned i = 0; i < children.size(); ++i)
        {
          TypeNode type = children[i].getType();
          if (!type.isBitVector())
          {
            continue;
          }
          unsigned bvsize = type.getBitVectorSize();
          if (bvsize < max)
          {
            // sign extend
            Node signExtendOp = nm->mkConst<BitVectorSignExtend>(
                BitVectorSignExtend(max - bvsize));
            children[i] = nm->mkNode(signExtendOp, children[i]);
          }
        }
      }
      NodeBuilder builder(newKind);
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
        builder << current.getOperator();
      }
      for (unsigned i = 0; i < children.size(); ++i)
      {
        builder << children[i];
      }
      // Mark the substitution and continue
      Node result = builder;

      result = Rewriter::rewrite(result);
      cache[current] = result;
    }
    else
    {
      // It's a leaf: could be a variable or a numeral
      Node result = current;
      if (current.isVar())
      {
        if (current.getType() == nm->integerType())
        {
          result = sm->mkDummySkolem("__intToBV_var",
                                     nm->mkBitVectorType(size),
                                     "Variable introduced in intToBV pass");
        }
      }
      else if (current.isConst())
      {
        switch (current.getKind())
        {
          case kind::CONST_RATIONAL:
          {
            Rational constant = current.getConst<Rational>();
            if (constant.isIntegral()) {
              AlwaysAssert(constant >= 0);
              BitVector bv(size, constant.getNumerator());
              if (bv.toSignedInteger() != constant.getNumerator())
              {
                throw TypeCheckingExceptionPrivate(
                    current,
                    string("Not enough bits for constant in intToBV: ")
                        + current.toString());
              }
              result = nm->mkConst(bv);
            }
            break;
          }
          default: break;
        }
      }
      else
      {
        throw TypeCheckingExceptionPrivate(
            current, string("Cannot translate to BV: ") + current.toString());
      }
      cache[current] = result;
    }
  }
  return cache[n_binary];
}
}  // namespace

IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "int-to-bv"){};

PreprocessingPassResult IntToBV::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  NodeMap cache;
  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
  {
    assertionsToPreprocess->replace(
        i, intToBV((*assertionsToPreprocess)[i], cache));
  }
  return PreprocessingPassResult::NO_CONFLICT;
}


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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andres Noetzli, Yoni Zohar, Alex Ozdemir
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 IntToBV preprocessing pass.
14		*
15		* Converts integer operations into bitvector operations. The width of the
16		* bitvectors is controlled through the `--solve-int-as-bv` command line
17		* option.
18		*/
19
20		#include "preprocessing/passes/int_to_bv.h"
21
22		#include <string>
23		#include <unordered_map>
24		#include <vector>
25
26		#include "expr/node.h"
27		#include "expr/node_traversal.h"
28		#include "expr/skolem_manager.h"
29		#include "options/smt_options.h"
30		#include "preprocessing/assertion_pipeline.h"
31		#include "theory/rewriter.h"
32		#include "theory/theory.h"
33
34		namespace cvc5 {
35		namespace preprocessing {
36		namespace passes {
37
38		using namespace std;
39		using namespace cvc5::theory;
40
41		using NodeMap = std::unordered_map<Node, Node>;
42
43		namespace {
44
45	4	bool childrenTypesChanged(Node n, NodeMap& cache) {
46	8	for (Node child : n) {
47	8	TypeNode originalType = child.getType();
48	8	TypeNode newType = cache[child].getType();
49	4	if (! newType.isSubtypeOf(originalType)) {
50		return true;
51		}
52		}
53	4	return false;
54		}
55
56
57	18	Node intToBVMakeBinary(TNode n, NodeMap& cache)
58		{
59	42	for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER,
60	120	[&cache](TNode nn) { return cache.count(nn) > 0; }))
61		{
62	84	Node result;
63	42	NodeManager* nm = NodeManager::currentNM();
64	42	if (current.getNumChildren() == 0)
65		{
66	26	result = current;
67		}
68	32	else if (current.getNumChildren() > 2
69	16	&& (current.getKind() == kind::PLUS
70		\|\| current.getKind() == kind::MULT))
71		{
72		Assert(cache.find(current[0]) != cache.end());
73		result = cache[current[0]];
74		for (unsigned i = 1; i < current.getNumChildren(); ++i)
75		{
76		Assert(cache.find(current[i]) != cache.end());
77		Node child = current[i];
78		Node childRes = cache[current[i]];
79		result = nm->mkNode(current.getKind(), result, childRes);
80		}
81		}
82		else
83		{
84	32	NodeBuilder builder(current.getKind());
85	16	if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
86	4	builder << current.getOperator();
87		}
88
89	42	for (unsigned i = 0; i < current.getNumChildren(); ++i)
90		{
91	26	Assert(cache.find(current[i]) != cache.end());
92	26	builder << cache[current[i]];
93		}
94	16	result = builder;
95		}
96	42	cache[current] = result;
97		}
98	18	return cache[n];
99		}
100
101	18	Node intToBV(TNode n, NodeMap& cache)
102		{
103	37264	int size = options::solveIntAsBV();
104	18	AlwaysAssert(size > 0);
105	18	AlwaysAssert(!options::incrementalSolving());
106
107	18	NodeManager* nm = NodeManager::currentNM();
108	18	SkolemManager* sm = nm->getSkolemManager();
109	36	NodeMap binaryCache;
110	36	Node n_binary = intToBVMakeBinary(n, binaryCache);
111
112	40	for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
113	118	[&cache](TNode nn) { return cache.count(nn) > 0; }))
114		{
115	40	if (current.getNumChildren() > 0)
116		{
117		// Not a leaf
118	32	vector<Node> children;
119	16	unsigned max = 0;
120	42	for (unsigned i = 0; i < current.getNumChildren(); ++i)
121		{
122	26	Assert(cache.find(current[i]) != cache.end());
123	52	TNode childRes = cache[current[i]];
124	52	TypeNode type = childRes.getType();
125	26	if (type.isBitVector())
126		{
127	8	unsigned bvsize = type.getBitVectorSize();
128	8	if (bvsize > max)
129		{
130	6	max = bvsize;
131		}
132		}
133	26	children.push_back(childRes);
134		}
135
136	16	kind::Kind_t newKind = current.getKind();
137	16	if (max > 0)
138		{
139	6	switch (newKind)
140		{
141		case kind::PLUS:
142		Assert(children.size() == 2);
143		newKind = kind::BITVECTOR_ADD;
144		max = max + 1;
145		break;
146		case kind::MULT:
147		Assert(children.size() == 2);
148		newKind = kind::BITVECTOR_MULT;
149		max = max * 2;
150		break;
151		case kind::MINUS:
152		Assert(children.size() == 2);
153		newKind = kind::BITVECTOR_SUB;
154		max = max + 1;
155		break;
156		case kind::UMINUS:
157		Assert(children.size() == 1);
158		newKind = kind::BITVECTOR_NEG;
159		max = max + 1;
160		break;
161		case kind::LT: newKind = kind::BITVECTOR_SLT; break;
162		case kind::LEQ: newKind = kind::BITVECTOR_SLE; break;
163		case kind::GT: newKind = kind::BITVECTOR_SGT; break;
164		case kind::GEQ: newKind = kind::BITVECTOR_SGE; break;
165	2	case kind::EQUAL:
166	2	case kind::ITE: break;
167	4	default:
168	4	if (childrenTypesChanged(current, cache)) {
169		throw TypeCheckingExceptionPrivate(
170		current,
171		string("Cannot translate to BV: ") + current.toString());
172		}
173	4	break;
174		}
175	14	for (unsigned i = 0; i < children.size(); ++i)
176		{
177	16	TypeNode type = children[i].getType();
178	8	if (!type.isBitVector())
179		{
180		continue;
181		}
182	8	unsigned bvsize = type.getBitVectorSize();
183	8	if (bvsize < max)
184		{
185		// sign extend
186		Node signExtendOp = nm->mkConst<BitVectorSignExtend>(
187		BitVectorSignExtend(max - bvsize));
188		children[i] = nm->mkNode(signExtendOp, children[i]);
189		}
190		}
191		}
192	32	NodeBuilder builder(newKind);
193	16	if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
194	4	builder << current.getOperator();
195		}
196	42	for (unsigned i = 0; i < children.size(); ++i)
197		{
198	26	builder << children[i];
199		}
200		// Mark the substitution and continue
201	32	Node result = builder;
202
203	16	result = Rewriter::rewrite(result);
204	16	cache[current] = result;
205		}
206		else
207		{
208		// It's a leaf: could be a variable or a numeral
209	48	Node result = current;
210	24	if (current.isVar())
211		{
212	6	if (current.getType() == nm->integerType())
213		{
214	6	result = sm->mkDummySkolem("__intToBV_var",
215	4	nm->mkBitVectorType(size),
216		"Variable introduced in intToBV pass");
217		}
218		}
219	18	else if (current.isConst())
220		{
221	18	switch (current.getKind())
222		{
223	2	case kind::CONST_RATIONAL:
224		{
225	4	Rational constant = current.getConst<Rational>();
226	2	if (constant.isIntegral()) {
227	2	AlwaysAssert(constant >= 0);
228	4	BitVector bv(size, constant.getNumerator());
229	2	if (bv.toSignedInteger() != constant.getNumerator())
230		{
231		throw TypeCheckingExceptionPrivate(
232		current,
233		string("Not enough bits for constant in intToBV: ")
234		+ current.toString());
235		}
236	2	result = nm->mkConst(bv);
237		}
238	2	break;
239		}
240	16	default: break;
241		}
242		}
243		else
244		{
245		throw TypeCheckingExceptionPrivate(
246		current, string("Cannot translate to BV: ") + current.toString());
247		}
248	24	cache[current] = result;
249		}
250		}
251	36	return cache[n_binary];
252		}
253		} // namespace
254
255	9459	IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
256	9459	: PreprocessingPass(preprocContext, "int-to-bv"){};
257
258	8	PreprocessingPassResult IntToBV::applyInternal(
259		AssertionPipeline* assertionsToPreprocess)
260		{
261	16	NodeMap cache;
262	26	for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
263		{
264	18	assertionsToPreprocess->replace(
265	36	i, intToBV((*assertionsToPreprocess)[i], cache));
266		}
267	16	return PreprocessingPassResult::NO_CONFLICT;
268		}
269
270
271		} // namespace passes
272		} // namespace preprocessing
273	65437	} // namespace cvc5