Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/int_blaster.cpp	Lines:	1	81	1.2 %
Date:	2021-08-06	Branches:	2	228	0.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Yoni Zohar
 *
 * 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.
 * ****************************************************************************
 *
 * Int-blasting utility
 */

#include "theory/bv/int_blaster.h"

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

#include "expr/node.h"
#include "expr/node_traversal.h"
#include "expr/skolem_manager.h"
#include "options/option_exception.h"
#include "options/uf_options.h"
#include "theory/rewriter.h"
#include "util/iand.h"
#include "util/rational.h"

namespace cvc5 {
using namespace cvc5::theory;

IntBlaster::IntBlaster(context::Context* c,
                       options::SolveBVAsIntMode mode,
                       uint64_t granularity,
                       bool introduceFreshIntVars)
    : d_binarizeCache(c),
      d_intblastCache(c),
      d_rangeAssertions(c),
      d_bitwiseAssertions(c),
      d_mode(mode),
      d_granularity(granularity),
      d_context(c),
      d_introduceFreshIntVars(introduceFreshIntVars)
{
  d_nm = NodeManager::currentNM();
  d_zero = d_nm->mkConst<Rational>(0);
  d_one = d_nm->mkConst<Rational>(1);
};

void IntBlaster::addRangeConstraint(Node node,
                                    uint64_t size,
                                    std::vector<Node>& lemmas)
{
}

void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint,
                                      std::vector<Node>& lemmas)
{
}

Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); }

Node IntBlaster::maxInt(uint64_t k) { return Node(); }

Node IntBlaster::pow2(uint64_t k) { return Node(); }

Node IntBlaster::modpow2(Node n, uint64_t exponent) { return Node(); }

Node IntBlaster::makeBinary(Node n)
{
  if (d_binarizeCache.find(n) != d_binarizeCache.end())
  {
    return d_binarizeCache[n];
  }
  uint64_t numChildren = n.getNumChildren();
  kind::Kind_t k = n.getKind();
  Node result = n;
  if ((numChildren > 2)
      && (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT
          || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
          || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT))
  {
    result = n[0];
    for (uint64_t i = 1; i < numChildren; i++)
    {
      result = d_nm->mkNode(n.getKind(), result, n[i]);
    }
  }
  d_binarizeCache[n] = result;
  Trace("int-blaster-debug") << "binarization result: " << result << std::endl;
  return result;
}

/**
 * Translate n to Integers via post-order traversal.
 */
Node IntBlaster::intBlast(Node n,
                          std::vector<Node>& lemmas,
                          std::map<Node, Node>& skolems)
{
  // make sure the node is re-written
  n = Rewriter::rewrite(n);

  // helper vector for traversal.
  std::vector<Node> toVisit;
  toVisit.push_back(makeBinary(n));

  while (!toVisit.empty())
  {
    Node current = toVisit.back();
    uint64_t currentNumChildren = current.getNumChildren();
    if (d_intblastCache.find(current) == d_intblastCache.end())
    {
      // This is the first time we visit this node and it is not in the cache.
      // We mark this node as visited but not translated by assiging
      // a null node to it.
      d_intblastCache[current] = Node();
      // all the node's children are added to the stack to be visited
      // before visiting this node again.
      for (const Node& child : current)
      {
        toVisit.push_back(makeBinary(child));
      }
      // If this is a UF applicatinon, we also add the function to
      // toVisit.
      if (current.getKind() == kind::APPLY_UF)
      {
        toVisit.push_back(current.getOperator());
      }
    }
    else
    {
      // We already visited and translated this node
      if (!d_intblastCache[current].get().isNull())
      {
        // We are done computing the translation for current
        toVisit.pop_back();
      }
      else
      {
        // We are now visiting current on the way back up.
        // This is when we do the actual translation.
        Node translation;
        if (currentNumChildren == 0)
        {
          translation = translateNoChildren(current, lemmas, skolems);
        }
        else
        {
          /**
           * The current node has children.
           * Since we are on the way back up,
           * these children were already translated.
           * We save their translation for easy access.
           * If the node's kind is APPLY_UF,
           * we also need to include the translated uninterpreted function in
           * this list.
           */
          std::vector<Node> translated_children;
          if (current.getKind() == kind::APPLY_UF)
          {
            translated_children.push_back(
                d_intblastCache[current.getOperator()]);
          }
          for (uint64_t i = 0; i < currentNumChildren; i++)
          {
            translated_children.push_back(d_intblastCache[current[i]]);
          }
          translation =
              translateWithChildren(current, translated_children, lemmas);
        }

        Assert(!translation.isNull());
        // Map the current node to its translation in the cache.
        d_intblastCache[current] = translation;
        // Also map the translation to itself.
        d_intblastCache[translation] = translation;
        toVisit.pop_back();
      }
    }
  }
  return d_intblastCache[n].get();
}

Node IntBlaster::unsignedToSigned(Node n, uint64_t bw) { return Node(); }

Node IntBlaster::translateWithChildren(
    Node original,
    const std::vector<Node>& translated_children,
    std::vector<Node>& lemmas)
{
  Node binarized = makeBinary(original);
  // continue to process the binarized version
  return Node();
}

Node IntBlaster::translateNoChildren(Node original,
                                     std::vector<Node>& lemmas,
                                     std::map<Node, Node>& skolems)
{
  return Node();
}

Node IntBlaster::defineBVUFAsIntUF(Node bvUF, Node intUF) { return Node(); }

Node IntBlaster::translateFunctionSymbol(Node bvUF,
                                         std::map<Node, Node>& skolems)
{
  return Node();
}

bool IntBlaster::childrenTypesChanged(Node n) { return true; }

Node IntBlaster::castToType(Node n, TypeNode tn) { return Node(); }

Node IntBlaster::reconstructNode(Node originalNode,
                                 TypeNode resultType,
                                 const std::vector<Node>& translated_children)
{
  return Node();
}

Node IntBlaster::createShiftNode(std::vector<Node> children,
                                 uint64_t bvsize,
                                 bool isLeftShift)
{
  return Node();
}

Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode)
{
  return Node();
}

Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) { return Node(); }

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Yoni Zohar
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		* Int-blasting utility
14		*/
15
16		#include "theory/bv/int_blaster.h"
17
18		#include <cmath>
19		#include <string>
20		#include <unordered_map>
21		#include <vector>
22
23		#include "expr/node.h"
24		#include "expr/node_traversal.h"
25		#include "expr/skolem_manager.h"
26		#include "options/option_exception.h"
27		#include "options/uf_options.h"
28		#include "theory/rewriter.h"
29		#include "util/iand.h"
30		#include "util/rational.h"
31
32		namespace cvc5 {
33		using namespace cvc5::theory;
34
35		IntBlaster::IntBlaster(context::Context* c,
36		options::SolveBVAsIntMode mode,
37		uint64_t granularity,
38		bool introduceFreshIntVars)
39		: d_binarizeCache(c),
40		d_intblastCache(c),
41		d_rangeAssertions(c),
42		d_bitwiseAssertions(c),
43		d_mode(mode),
44		d_granularity(granularity),
45		d_context(c),
46		d_introduceFreshIntVars(introduceFreshIntVars)
47		{
48		d_nm = NodeManager::currentNM();
49		d_zero = d_nm->mkConst<Rational>(0);
50		d_one = d_nm->mkConst<Rational>(1);
51		};
52
53		void IntBlaster::addRangeConstraint(Node node,
54		uint64_t size,
55		std::vector<Node>& lemmas)
56		{
57		}
58
59		void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint,
60		std::vector<Node>& lemmas)
61		{
62		}
63
64		Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); }
65
66		Node IntBlaster::maxInt(uint64_t k) { return Node(); }
67
68		Node IntBlaster::pow2(uint64_t k) { return Node(); }
69
70		Node IntBlaster::modpow2(Node n, uint64_t exponent) { return Node(); }
71
72		Node IntBlaster::makeBinary(Node n)
73		{
74		if (d_binarizeCache.find(n) != d_binarizeCache.end())
75		{
76		return d_binarizeCache[n];
77		}
78		uint64_t numChildren = n.getNumChildren();
79		kind::Kind_t k = n.getKind();
80		Node result = n;
81		if ((numChildren > 2)
82		&& (k == kind::BITVECTOR_ADD \|\| k == kind::BITVECTOR_MULT
83		\|\| k == kind::BITVECTOR_AND \|\| k == kind::BITVECTOR_OR
84		\|\| k == kind::BITVECTOR_XOR \|\| k == kind::BITVECTOR_CONCAT))
85		{
86		result = n[0];
87		for (uint64_t i = 1; i < numChildren; i++)
88		{
89		result = d_nm->mkNode(n.getKind(), result, n[i]);
90		}
91		}
92		d_binarizeCache[n] = result;
93		Trace("int-blaster-debug") << "binarization result: " << result << std::endl;
94		return result;
95		}
96
97		/**
98		* Translate n to Integers via post-order traversal.
99		*/
100		Node IntBlaster::intBlast(Node n,
101		std::vector<Node>& lemmas,
102		std::map<Node, Node>& skolems)
103		{
104		// make sure the node is re-written
105		n = Rewriter::rewrite(n);
106
107		// helper vector for traversal.
108		std::vector<Node> toVisit;
109		toVisit.push_back(makeBinary(n));
110
111		while (!toVisit.empty())
112		{
113		Node current = toVisit.back();
114		uint64_t currentNumChildren = current.getNumChildren();
115		if (d_intblastCache.find(current) == d_intblastCache.end())
116		{
117		// This is the first time we visit this node and it is not in the cache.
118		// We mark this node as visited but not translated by assiging
119		// a null node to it.
120		d_intblastCache[current] = Node();
121		// all the node's children are added to the stack to be visited
122		// before visiting this node again.
123		for (const Node& child : current)
124		{
125		toVisit.push_back(makeBinary(child));
126		}
127		// If this is a UF applicatinon, we also add the function to
128		// toVisit.
129		if (current.getKind() == kind::APPLY_UF)
130		{
131		toVisit.push_back(current.getOperator());
132		}
133		}
134		else
135		{
136		// We already visited and translated this node
137		if (!d_intblastCache[current].get().isNull())
138		{
139		// We are done computing the translation for current
140		toVisit.pop_back();
141		}
142		else
143		{
144		// We are now visiting current on the way back up.
145		// This is when we do the actual translation.
146		Node translation;
147		if (currentNumChildren == 0)
148		{
149		translation = translateNoChildren(current, lemmas, skolems);
150		}
151		else
152		{
153		/**
154		* The current node has children.
155		* Since we are on the way back up,
156		* these children were already translated.
157		* We save their translation for easy access.
158		* If the node's kind is APPLY_UF,
159		* we also need to include the translated uninterpreted function in
160		* this list.
161		*/
162		std::vector<Node> translated_children;
163		if (current.getKind() == kind::APPLY_UF)
164		{
165		translated_children.push_back(
166		d_intblastCache[current.getOperator()]);
167		}
168		for (uint64_t i = 0; i < currentNumChildren; i++)
169		{
170		translated_children.push_back(d_intblastCache[current[i]]);
171		}
172		translation =
173		translateWithChildren(current, translated_children, lemmas);
174		}
175
176		Assert(!translation.isNull());
177		// Map the current node to its translation in the cache.
178		d_intblastCache[current] = translation;
179		// Also map the translation to itself.
180		d_intblastCache[translation] = translation;
181		toVisit.pop_back();
182		}
183		}
184		}
185		return d_intblastCache[n].get();
186		}
187
188		Node IntBlaster::unsignedToSigned(Node n, uint64_t bw) { return Node(); }
189
190		Node IntBlaster::translateWithChildren(
191		Node original,
192		const std::vector<Node>& translated_children,
193		std::vector<Node>& lemmas)
194		{
195		Node binarized = makeBinary(original);
196		// continue to process the binarized version
197		return Node();
198		}
199
200		Node IntBlaster::translateNoChildren(Node original,
201		std::vector<Node>& lemmas,
202		std::map<Node, Node>& skolems)
203		{
204		return Node();
205		}
206
207		Node IntBlaster::defineBVUFAsIntUF(Node bvUF, Node intUF) { return Node(); }
208
209		Node IntBlaster::translateFunctionSymbol(Node bvUF,
210		std::map<Node, Node>& skolems)
211		{
212		return Node();
213		}
214
215		bool IntBlaster::childrenTypesChanged(Node n) { return true; }
216
217		Node IntBlaster::castToType(Node n, TypeNode tn) { return Node(); }
218
219		Node IntBlaster::reconstructNode(Node originalNode,
220		TypeNode resultType,
221		const std::vector<Node>& translated_children)
222		{
223		return Node();
224		}
225
226		Node IntBlaster::createShiftNode(std::vector<Node> children,
227		uint64_t bvsize,
228		bool isLeftShift)
229		{
230		return Node();
231		}
232
233		Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode)
234		{
235		return Node();
236		}
237
238		Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize) { return Node(); }
239
240	29322	} // namespace cvc5