From: yoni206 Date: Tue, 22 Jun 2021 19:11:22 +0000 (-0700) Subject: modular bv2int: Stubs and some implementations (#6760) X-Git-Tag: cvc5-1.0.0~1570 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=40bee7cad0f2b6a5f9eac7e8fda2199e582e18d1;p=cvc5.git modular bv2int: Stubs and some implementations (#6760) This PR adds the file int_blaster.cpp. Most of the functions are not yet implemented. Two main functions are implemented. Additionally, code that will no longer be needed is removed from the BV rewriter. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b3f27b703..74db7c941 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -596,6 +596,7 @@ libcvc5_add_sources( theory/bv/bv_subtheory_core.h theory/bv/bv_subtheory_inequality.cpp theory/bv/bv_subtheory_inequality.h + theory/bv/int_blaster.cpp theory/bv/int_blaster.h theory/bv/proof_checker.cpp theory/bv/proof_checker.h diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp new file mode 100644 index 000000000..9da9d1c2b --- /dev/null +++ b/src/theory/bv/int_blaster.cpp @@ -0,0 +1,240 @@ +/****************************************************************************** + * 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 +#include +#include +#include + +#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(0); + d_one = d_nm->mkConst(1); +}; + +void IntBlaster::addRangeConstraint(Node node, + uint64_t size, + std::vector& lemmas) +{ +} + +void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint, + std::vector& 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& lemmas, + std::map& skolems) +{ + // make sure the node is re-written + n = Rewriter::rewrite(n); + + // helper vector for traversal. + std::vector 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 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& translated_children, + std::vector& lemmas) +{ + Node binarized = makeBinary(original); + // continue to process the binarized version + return Node(); +} + +Node IntBlaster::translateNoChildren(Node original, + std::vector& lemmas, + std::map& skolems) +{ + return Node(); +} + +Node IntBlaster::defineBVUFAsIntUF(Node bvUF, Node intUF) { return Node(); } + +Node IntBlaster::translateFunctionSymbol(Node bvUF, + std::map& 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& translated_children) +{ + return Node(); +} + +Node IntBlaster::createShiftNode(std::vector 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 diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h index f8717e045..444eb88a7 100644 --- a/src/theory/bv/int_blaster.h +++ b/src/theory/bv/int_blaster.h @@ -75,9 +75,10 @@ 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, @@ -118,8 +119,7 @@ class IntBlaster * 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& lemmas, @@ -164,19 +164,16 @@ class IntBlaster */ 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); @@ -287,7 +284,7 @@ class IntBlaster * 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 @@ -308,8 +305,6 @@ class IntBlaster /** 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 */