Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/int_to_bv.cpp	Lines:	125	142	88.0 %
Date:	2021-09-15	Branches:	274	650	42.2 %


/******************************************************************************
 * 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/base_options.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "util/bitvector.h"
#include "util/rational.h"

namespace cvc5 {
namespace preprocessing {
namespace passes {

using namespace std;
using namespace cvc5::theory;


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
                 || current.getKind() == kind::NONLINEAR_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];
}
}  // namespace

Node IntToBV::intToBV(TNode n, NodeMap& cache)
{
  int size = options().smt.solveIntAsBV;
  AlwaysAssert(size > 0);
  AlwaysAssert(!options().base.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;
      uint64_t max = 0;
      for (const Node& nc : current)
      {
        Assert(cache.find(nc) != cache.end());
        TNode childRes = cache[nc];
        TypeNode type = childRes.getType();
        if (type.isBitVector())
        {
          uint32_t 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:
          case kind::NONLINEAR_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 (size_t i = 0, csize = children.size(); i < csize; ++i)
        {
          TypeNode type = children[i].getType();
          if (!type.isBitVector())
          {
            continue;
          }
          uint32_t 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();
      }
      builder.append(children);
      // Mark the substitution and continue
      Node result = builder;

      result = 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");
          /**
           * Correctly convert signed/unsigned BV values to Integers as follows
           * x < 0 ? -nat(-x) : nat(x)
           * where x refers to the bit-vector term `result`.
           */
          BitVector bvzero(size, Integer(0));
          Node negResult = nm->mkNode(kind::BITVECTOR_TO_NAT,
                                      nm->mkNode(kind::BITVECTOR_NEG, result));
          Node bv2int = nm->mkNode(
              kind::ITE,
              nm->mkNode(kind::BITVECTOR_SLT, result, nm->mkConst(bvzero)),
              nm->mkNode(kind::UMINUS, negResult),
              nm->mkNode(kind::BITVECTOR_TO_NAT, result));
          d_preprocContext->addSubstitution(current, bv2int);
        }
      }
      else if (current.isConst())
      {
        switch (current.getKind())
        {
          case kind::CONST_RATIONAL:
          {
            Rational constant = current.getConst<Rational>();
            if (constant.isIntegral()) {
              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;
    }
  }
  Trace("int-to-bv-debug") << "original: " << n << std::endl;
  Trace("int-to-bv-debug") << "binary: " << n_binary << std::endl;
  Trace("int-to-bv-debug") << "result: " << cache[n_binary] << std::endl;
  return cache[n_binary];
}

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