From: Aina Niemetz Date: Thu, 8 Feb 2018 23:19:36 +0000 (-0800) Subject: Clean up bv utils (part one). (#1580) X-Git-Tag: cvc5-1.0.0~5302 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a4fc643283549556ae3f9c93ead7bbc3066f0fc;p=cvc5.git Clean up bv utils (part one). (#1580) This is part one of an effort to clean up bv utils. It addresses review comments not addressed in #1566 (changes of moved code), removes unused functions and moves a helper to compute the gcd over Index. --- diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index bf5152893..f70eed096 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -2,9 +2,9 @@ /*! \file slicer.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Paul Meng + ** Liana Hadarean, Aina Niemetz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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.\endverbatim @@ -39,15 +39,15 @@ Base::Base(uint32_t size) Assert (d_size > 0); } - -void Base::sliceAt(Index index) { +void Base::sliceAt(Index index) +{ Index vector_index = index / 32; if (vector_index == d_repr.size()) return; - + Index int_index = index % 32; - uint32_t bit_mask = utils::pow2(int_index); - d_repr[vector_index] = d_repr[vector_index] | bit_mask; + uint32_t bit_mask = 1u << int_index; + d_repr[vector_index] = d_repr[vector_index] | bit_mask; } void Base::sliceWith(const Base& other) { @@ -57,17 +57,18 @@ void Base::sliceWith(const Base& other) { } } -bool Base::isCutPoint (Index index) const { +bool Base::isCutPoint (Index index) const +{ // there is an implicit cut point at the end and begining of the bv if (index == d_size || index == 0) return true; - + Index vector_index = index / 32; - Assert (vector_index < d_size); + Assert (vector_index < d_size); Index int_index = index % 32; - uint32_t bit_mask = utils::pow2(int_index); + uint32_t bit_mask = 1u << int_index; - return (bit_mask & d_repr[vector_index]) != 0; + return (bit_mask & d_repr[vector_index]) != 0; } void Base::diffCutPoints(const Base& other, Base& res) const { @@ -311,6 +312,19 @@ void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) getDecomposition(high_child, decomp); } } + +/* Compute the greatest common divisor of two indices. */ +static Index gcd(Index a, Index b) +{ + while (b != 0) + { + Index t = b; + b = a % t; + a = t; + } + return a; +} + /** * May cause reslicings of the decompositions. Must not assume the decompositons * are the current normal form. @@ -347,7 +361,7 @@ void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposit Assert (overlap > 0); Index diff = common_size - overlap; Assert (diff >= 0); - Index granularity = utils::gcd(diff, overlap); + Index granularity = gcd(diff, overlap); // split the common part for (unsigned i = 0; i < common_size; i+= granularity) { split(common, i); diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 9e05ef516..affdd05bb 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -27,15 +27,6 @@ namespace utils { /* ------------------------------------------------------------------------- */ -uint32_t pow2(uint32_t n) -{ - Assert(n < 32); - uint32_t one = 1; - return one << n; -} - -/* ------------------------------------------------------------------------- */ - BitVector mkBitVectorOnes(unsigned size) { Assert(size > 0); @@ -63,7 +54,7 @@ unsigned getSize(TNode node) const bool getBit(TNode node, unsigned i) { - Assert(i < utils::getSize(node) && node.getKind() == kind::CONST_BITVECTOR); + Assert(i < getSize(node) && node.getKind() == kind::CONST_BITVECTOR); Integer bit = node.getConst().extract(i, i).getValue(); return (bit == 1u); } @@ -90,7 +81,7 @@ unsigned getSignExtendAmount(TNode node) bool isZero(TNode node) { if (!node.isConst()) return false; - return node == utils::mkConst(utils::getSize(node), 0u); + return node == mkZero(getSize(node)); } unsigned isPow2Const(TNode node, bool& isNeg) @@ -136,35 +127,23 @@ bool isBvConstTerm(TNode node) bool isBVPredicate(TNode node) { - if (node.getKind() == kind::EQUAL || node.getKind() == kind::BITVECTOR_ULT - || node.getKind() == kind::BITVECTOR_SLT - || node.getKind() == kind::BITVECTOR_UGT - || node.getKind() == kind::BITVECTOR_UGE - || node.getKind() == kind::BITVECTOR_SGT - || node.getKind() == kind::BITVECTOR_SGE - || node.getKind() == kind::BITVECTOR_ULE - || node.getKind() == kind::BITVECTOR_SLE - || node.getKind() == kind::BITVECTOR_REDOR - || node.getKind() == kind::BITVECTOR_REDAND - || (node.getKind() == kind::NOT - && (node[0].getKind() == kind::EQUAL - || node[0].getKind() == kind::BITVECTOR_ULT - || node[0].getKind() == kind::BITVECTOR_SLT - || node[0].getKind() == kind::BITVECTOR_UGT - || node[0].getKind() == kind::BITVECTOR_UGE - || node[0].getKind() == kind::BITVECTOR_SGT - || node[0].getKind() == kind::BITVECTOR_SGE - || node[0].getKind() == kind::BITVECTOR_ULE - || node[0].getKind() == kind::BITVECTOR_SLE - || node[0].getKind() == kind::BITVECTOR_REDOR - || node[0].getKind() == kind::BITVECTOR_REDAND))) + Kind k = node.getKind(); + if (k == kind::NOT) { - return true; - } - else - { - return false; - } + node = node[0]; + k = node.getKind(); + } + return k == kind::EQUAL + || k == kind::BITVECTOR_ULT + || k == kind::BITVECTOR_SLT + || k == kind::BITVECTOR_UGT + || k == kind::BITVECTOR_UGE + || k == kind::BITVECTOR_SGT + || k == kind::BITVECTOR_SGE + || k == kind::BITVECTOR_ULE + || k == kind::BITVECTOR_SLE + || k == kind::BITVECTOR_REDOR + || k == kind::BITVECTOR_REDAND; } bool isCoreTerm(TNode term, TNodeBoolMap& cache) @@ -394,18 +373,16 @@ Node mkSignExtend(TNode node, unsigned amount) Node mkExtract(TNode node, unsigned high, unsigned low) { - Node extractOp = NodeManager::currentNM()->mkConst( - BitVectorExtract(high, low)); - std::vector children; - children.push_back(node); - return NodeManager::currentNM()->mkNode(extractOp, children); + NodeManager *nm = NodeManager::currentNM(); + Node extractOp = nm->mkConst(BitVectorExtract(high, low)); + return nm->mkNode(extractOp, node); } Node mkBitOf(TNode node, unsigned index) { - Node bitOfOp = - NodeManager::currentNM()->mkConst(BitVectorBitOf(index)); - return NodeManager::currentNM()->mkNode(bitOfOp, node); + NodeManager *nm = NodeManager::currentNM(); + Node bitOfOp = nm->mkConst(BitVectorBitOf(index)); + return nm->mkNode(bitOfOp, node); } /* ------------------------------------------------------------------------- */ @@ -444,13 +421,13 @@ Node mkConcat(TNode node, unsigned repeat) Node mkInc(TNode t) { return NodeManager::currentNM()->mkNode( - kind::BITVECTOR_PLUS, t, bv::utils::mkOne(bv::utils::getSize(t))); + kind::BITVECTOR_PLUS, t, mkOne(getSize(t))); } Node mkDec(TNode t) { return NodeManager::currentNM()->mkNode( - kind::BITVECTOR_SUB, t, bv::utils::mkOne(bv::utils::getSize(t))); + kind::BITVECTOR_SUB, t, mkOne(getSize(t))); } /* ------------------------------------------------------------------------- */ @@ -500,29 +477,6 @@ Node mkConjunction(const std::vector& nodes) /* ------------------------------------------------------------------------- */ -void getConjuncts(TNode node, std::set& conjuncts) -{ - if (node.getKind() != kind::AND) - { - conjuncts.insert(node); - } - else - { - for (unsigned i = 0; i < node.getNumChildren(); ++i) - { - getConjuncts(node[i], conjuncts); - } - } -} - -void getConjuncts(std::vector& nodes, std::set& conjuncts) -{ - for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++i) - { - getConjuncts(nodes[i], conjuncts); - } -} - Node flattenAnd(std::vector& queue) { TNodeSet nodes; @@ -555,42 +509,6 @@ Node flattenAnd(std::vector& queue) /* ------------------------------------------------------------------------- */ -std::string setToString(const std::set& nodeSet) { - std::stringstream out; - out << "["; - std::set::const_iterator it = nodeSet.begin(); - std::set::const_iterator it_end = nodeSet.end(); - bool first = true; - while (it != it_end) { - if (!first) { - out << ","; - } - first = false; - out << *it; - ++ it; - } - out << "]"; - return out.str(); -} - -std::string vectorToString(const std::vector& nodes) -{ - std::stringstream out; - out << "["; - for (unsigned i = 0; i < nodes.size(); ++i) - { - if (i > 0) - { - out << ","; - } - out << nodes[i]; - } - out << "]"; - return out.str(); -} - -/* ------------------------------------------------------------------------- */ - // FIXME: dumb code void intersect(const std::vector& v1, const std::vector& v2, diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 6f1300632..727f5040f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -38,22 +38,6 @@ namespace utils { typedef std::unordered_map TNodeBoolMap; typedef std::unordered_set NodeSet; -/* Compute 2^n. */ -uint32_t pow2(uint32_t n); - -/* Compute the greatest common divisor for two objects of Type T. */ -template -T gcd(T a, T b) -{ - while (b != 0) - { - T t = b; - b = a % t; - a = t; - } - return a; -} - /* Create bit-vector of ones of given size. */ BitVector mkBitVectorOnes(unsigned size); /* Create bit-vector representing the minimum signed value of given size. */ @@ -193,18 +177,9 @@ Node mkUmulo(TNode t1, TNode t2); /* Create conjunction. */ Node mkConjunction(const std::vector& nodes); -/* Get a set of all operands of nested and nodes. */ -void getConjuncts(TNode node, std::set& conjuncts); -void getConjuncts(std::vector& nodes, std::set& conjuncts); /* Create a flattened and node. */ Node flattenAnd(std::vector& queue); -/* Create a string representing a set of nodes. */ -std::string setToString(const std::set& nodeSet); - -/* Create a string representing a vector of nodes. */ -std::string vectorToString(const std::vector& nodes); - /* Create the intersection of two vectors of uint32_t. */ void intersect(const std::vector& v1, const std::vector& v2,