--- /dev/null
+/******************************************************************************
+ * 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
** Tr((bvult a b)) = Tr(a) < Tr(b)
** Similar transformations are done for bvule, bvugt, and bvuge.
**
-** Bit-vector operators that are not listed above are either eliminated using
-** the function eliminationPass, or go through the following default
-*translation, that also works for non-bit-vector operators
+** Bit-vector operators that are not listed above are either
+** eliminated using the BV rewriter,
+** or go through the following default
+** translation, that also works for non-bit-vector operators
** with result type BV:
** Tr((op t1 ... tn)) = (bv2nat (op (cast t1) ... (cast tn)))
** where (cast x) is ((_ nat2bv k) x) or just x,
* ff((bv2nat x))), where k is the bit-width of the domain of f, i is the
* bit-width of its range, and ff is a Int->Int function that corresponds to
* f. For functions with other signatures this is similar
- * @return integer node that corresponds to n, or a null node if d_supportNoBV
- * is set to false and n is note purely BV.
+ * @return integer node that corresponds to n
*/
Node intBlast(Node n,
std::vector<Node>& lemmas,
*/
Node mkRangeConstraint(Node newVar, uint64_t k);
- /**
- * In the translation to integers, it is convenient to assume that certain
- * bit-vector operators do not occur in the original formula (e.g., repeat).
- * This function eliminates all these operators.
- */
- Node eliminationPass(Node n);
-
/**
* Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more
* than two arguments as a syntactic sugar.
* For example, we can have a node for (bvand x y z),
* that represents (bvand (x (bvand y z))).
- * This function makes all such operators strictly binary.
+ * This function locally binarizes these operators.
+ * In the above example, this means that x,y,z
+ * are not handled recursively, but will require a separate
+ * call to the function.
+ *
*/
Node makeBinary(Node n);
* binary representation of n is the same as the
* signed binary representation of m.
*/
- Node unsignedTosigned(Node n, uint64_t bvsize);
+ Node unsignedToSigned(Node n, uint64_t bvsize);
/**
* Performs the actual translation to integers for nodes
/** Caches for the different functions */
CDNodeMap d_binarizeCache;
- CDNodeMap d_eliminationCache;
- CDNodeMap d_rebuildCache;
CDNodeMap d_intblastCache;
/** Node manager that is used throughout the pass */
projects / cvc5.git / commitdiff