diff options
Diffstat (limited to 'src/theory/bv/theory_bv_utils.h')
| -rw-r--r-- | src/theory/bv/theory_bv_utils.h | 661 |
1 files changed, 148 insertions, 513 deletions
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index e304e4801..f6784621f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -2,17 +2,16 @@ /*! \file theory_bv_utils.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Dejan Jovanovic, Morgan Deters + ** Aina Niemetz, Dejan Jovanovic, Morgan Deters ** 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 ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Util functions for theory BV. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Util functions for theory BV. **/ #include "cvc4_private.h" @@ -36,205 +35,153 @@ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; namespace utils { -inline uint32_t pow2(uint32_t power) { - Assert (power < 32); - uint32_t one = 1; - return one << power; -} - -inline unsigned getExtractHigh(TNode node) { - return node.getOperator().getConst<BitVectorExtract>().high; -} - -inline unsigned getExtractLow(TNode node) { - return node.getOperator().getConst<BitVectorExtract>().low; -} +typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; -inline unsigned getSize(TNode node) { - return node.getType().getBitVectorSize(); -} +/* Compute 2^n. */ +uint32_t pow2(uint32_t n); -inline unsigned getSignExtendAmount(TNode node) +/* Compute the greatest common divisor for two objects of Type T. */ +template <class T> +T gcd(T a, T b) { - return node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; -} - -inline const bool getBit(TNode node, unsigned i) { - Assert (i < utils::getSize(node) && - node.getKind() == kind::CONST_BITVECTOR); - Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); - return (bit == 1u); -} - -inline Node mkTrue() { - return NodeManager::currentNM()->mkConst<bool>(true); -} - -inline Node mkFalse() { - return NodeManager::currentNM()->mkConst<bool>(false); -} - -inline Node mkVar(unsigned size) { - NodeManager* nm = NodeManager::currentNM(); - - return nm->mkSkolem("BVSKOLEM$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); -} - - -inline Node mkSortedNode(Kind kind, std::vector<Node>& children) { - Assert (kind == kind::BITVECTOR_AND || - kind == kind::BITVECTOR_OR || - kind == kind::BITVECTOR_XOR); - Assert(children.size() > 0); - if (children.size() == 1) { - return children[0]; - } - std::sort(children.begin(), children.end()); - return NodeManager::currentNM()->mkNode(kind, children); -} - - -inline Node mkNode(Kind kind, std::vector<Node>& children) { - Assert (children.size() > 0); - if (children.size() == 1) { - return children[0]; - } - return NodeManager::currentNM()->mkNode(kind, children); -} - -inline Node mkNode(Kind kind, TNode child) { - return NodeManager::currentNM()->mkNode(kind, child); -} - -inline Node mkNode(Kind kind, TNode child1, TNode child2) { - return NodeManager::currentNM()->mkNode(kind, child1, child2); -} - - -inline Node mkSortedNode(Kind kind, TNode child1, TNode child2) { - Assert (kind == kind::BITVECTOR_AND || - kind == kind::BITVECTOR_OR || - kind == kind::BITVECTOR_XOR); - - if (child1 < child2) { - return NodeManager::currentNM()->mkNode(kind, child1, child2); - } else { - return NodeManager::currentNM()->mkNode(kind, child2, child1); + while (b != 0) + { + T t = b; + b = a % t; + a = t; } + return a; } -inline Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { - return NodeManager::currentNM()->mkNode(kind, child1, child2, child3); -} - - -inline Node mkNot(Node child) { - return NodeManager::currentNM()->mkNode(kind::NOT, child); -} - -inline Node mkAnd(TNode node1, TNode node2) { - return NodeManager::currentNM()->mkNode(kind::AND, node1, node2); -} - -inline Node mkOr(TNode node1, TNode node2) { - return NodeManager::currentNM()->mkNode(kind::OR, node1, node2); -} - -inline Node mkXor(TNode node1, TNode node2) { - return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); -} - -inline Node mkSignExtend(TNode node, unsigned amount) -{ - NodeManager* nm = NodeManager::currentNM(); - Node signExtendOp = - nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount)); - return nm->mkNode(signExtendOp, node); -} - -inline Node mkExtract(TNode node, unsigned high, unsigned low) { - Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low)); - std::vector<Node> children; - children.push_back(node); - return NodeManager::currentNM()->mkNode(extractOp, children); -} +/* Create bit-vector of ones of given size. */ +BitVector mkBitVectorOnes(unsigned size); +/* Create bit-vector representing the minimum signed value of given size. */ +BitVector mkBitVectorMinSigned(unsigned size); +/* Create bit-vector representing the maximum signed value of given size. */ +BitVector mkBitVectorMaxSigned(unsigned size); -inline Node mkBitOf(TNode node, unsigned index) { - Node bitOfOp = NodeManager::currentNM()->mkConst<BitVectorBitOf>(BitVectorBitOf(index)); - return NodeManager::currentNM()->mkNode(bitOfOp, node); -} +/* Get the bit-width of given node. */ +unsigned getSize(TNode node); -Node mkSum(std::vector<Node>& children, unsigned width); +/* Get bit at given index. */ +const bool getBit(TNode node, unsigned i); -inline Node mkConcat(TNode node, unsigned repeat) { - Assert (repeat); - if(repeat == 1) { - return node; - } - NodeBuilder<> result(kind::BITVECTOR_CONCAT); - for (unsigned i = 0; i < repeat; ++i) { - result << node; - } - Node resultNode = result; - return resultNode; -} +/* Get the upper index of given extract node. */ +unsigned getExtractHigh(TNode node); +/* Get the lower index of given extract node. */ +unsigned getExtractLow(TNode node); -inline Node mkConcat(std::vector<Node>& children) { - if (children.size() > 1) - return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); - else - return children[0]; -} +/* Get the number of bits by which a given node is extended. */ +unsigned getSignExtendAmount(TNode node); -inline Node mkConcat(TNode t1, TNode t2) { - return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2); -} - - -inline BitVector mkBitVectorOnes(unsigned size) { - Assert(size > 0); - return BitVector(1, Integer(1)).signExtend(size - 1); -} - -inline BitVector mkBitVectorMinSigned(unsigned size) +/* Returns true if given node represents a zero bit-vector. */ +bool isZero(TNode node); +/* If node is a constant of the form 2^c or -2^c, then this function returns + * c+1. Otherwise, this function returns 0. The flag isNeg is updated to + * indicate whether node is negative. */ +unsigned isPow2Const(TNode node, bool& isNeg); +/* Returns true if node or all of its children is const. */ +bool isBvConstTerm(TNode node); +/* Returns true if node is a predicate over bit-vector nodes. */ +bool isBVPredicate(TNode node); +/* Returns true if given term is a THEORY_BV term. */ +bool isCoreTerm(TNode term, TNodeBoolMap& cache); +/* Returns true if given term is a bv constant, variable or equality term. */ +bool isEqualityTerm(TNode term, TNodeBoolMap& cache); +/* Returns true if given node is an atom that is bit-blasted. */ +bool isBitblastAtom(Node lit); + +/* Create Boolean node representing true. */ +Node mkTrue(); +/* Create Boolean node representing false. */ +Node mkFalse(); +/* Create bit-vector node representing a bit-vector of ones of given size. */ +Node mkOnes(unsigned size); +/* Create bit-vector node representing a zero bit-vector of given size. */ +Node mkZero(unsigned size); +/* Create bit-vector node representing a bit-vector value one of given size. */ +Node mkOne(unsigned size); + +/* Create bit-vector constant of given size and value. */ +Node mkConst(unsigned size, unsigned int value); +Node mkConst(unsigned size, Integer& value); +/* Create bit-vector constant from given bit-vector. */ +Node mkConst(const BitVector& value); + +/* Create bit-vector variable. */ +Node mkVar(unsigned size); + +/* Create n-ary node of given kind. */ +Node mkNode(Kind kind, TNode child); +Node mkNode(Kind kind, TNode child1, TNode child2); +Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); +Node mkNode(Kind kind, std::vector<Node>& children); + +/* Create n-ary bit-vector node of kind BITVECTOR_AND, BITVECTOR_OR or + * BITVECTOR_XOR where its children are sorted */ +Node mkSortedNode(Kind kind, TNode child1, TNode child2); +Node mkSortedNode(Kind kind, std::vector<Node>& children); + +/* Create node of kind NOT. */ +Node mkNot(Node child); +/* Create node of kind AND. */ +Node mkAnd(TNode node1, TNode node2); +/* Create n-ary node of kind AND. */ +template<bool ref_count> +Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) { - Assert(size > 0); - return BitVector(size).setBit(size - 1); -} + std::set<TNode> all(conjunctions.begin(), conjunctions.end()); -inline BitVector mkBitVectorMaxSigned(unsigned size) -{ - Assert(size > 0); - return ~mkBitVectorMinSigned(size); -} + if (all.size() == 0) { return mkTrue(); } -inline Node mkOnes(unsigned size) { - BitVector val = mkBitVectorOnes(size); - return NodeManager::currentNM()->mkConst<BitVector>(val); -} + /* All the same, or just one */ + if (all.size() == 1) { return conjunctions[0]; } -inline Node mkConst(unsigned size, unsigned int value) { - BitVector val(size, value); - return NodeManager::currentNM()->mkConst<BitVector>(val); + NodeBuilder<> conjunction(kind::AND); + for (const Node& n : all) { conjunction << n; } + return conjunction; } - -inline Node mkConst(unsigned size, Integer& value) +/* Create node of kind OR. */ +Node mkOr(TNode node1, TNode node2); +/* Create n-ary node of kind OR. */ +template<bool ref_count> +Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes) { - return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value)); -} + std::set<TNode> all(nodes.begin(), nodes.end()); -inline Node mkConst(const BitVector& value) { - return NodeManager::currentNM()->mkConst<BitVector>(value); -} + if (all.size() == 0) { return mkTrue(); } -inline Node mkZero(unsigned size) { return mkConst(size, 0u); } + /* All the same, or just one */ + if (all.size() == 1) { return nodes[0]; } -inline Node mkOne(unsigned size) { return mkConst(size, 1u); } - -/* Increment */ + NodeBuilder<> disjunction(kind::OR); + for (const Node& n : all) { disjunction << n; } + return disjunction; +} +/* Create node of kind XOR. */ +Node mkXor(TNode node1, TNode node2); + +/* Create signed extension node where given node is extended by given amount. */ +Node mkSignExtend(TNode node, unsigned amount); + +/* Create extract node where bits from index high to index low are extracted + * from given node. */ +Node mkExtract(TNode node, unsigned high, unsigned low); +/* Create extract node of bit-width 1 where the resulting node represents + * the bit at given index. */ +Node mkBitOf(TNode node, unsigned index); + +/* Create n-ary concat node of given children. */ +Node mkConcat(TNode t1, TNode t2); +Node mkConcat(std::vector<Node>& children); +/* Create concat by repeating given node n times. + * Returns given node if n = 1. */ +Node mkConcat(TNode node, unsigned repeat); + +/* Create bit-vector addition node representing the increment of given node. */ Node mkInc(TNode t); - -/* Decrement */ +/* Create bit-vector addition node representing the decrement of given node. */ Node mkDec(TNode t); /* Unsigned multiplication overflow detection. @@ -243,345 +190,33 @@ Node mkDec(TNode t); * http://ieeexplore.ieee.org/document/987767 */ Node mkUmulo(TNode t1, TNode t2); -inline void getConjuncts(TNode node, std::set<TNode>& conjuncts) { - if (node.getKind() != kind::AND) { - conjuncts.insert(node); - } else { - for (unsigned i = 0; i < node.getNumChildren(); ++ i) { - getConjuncts(node[i], conjuncts); - } - } -} - -inline void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts) { - for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) { - getConjuncts(nodes[i], conjuncts); - } -} +/* Create conjunction over a set of (dis)equalities. */ +Node mkConjunction(const std::set<TNode> nodes); +Node mkConjunction(const std::vector<TNode>& nodes); -inline Node mkConjunction(const std::set<TNode> nodes) { - std::set<TNode> expandedNodes; - - std::set<TNode>::const_iterator it = nodes.begin(); - std::set<TNode>::const_iterator it_end = nodes.end(); - while (it != it_end) { - TNode current = *it; - if (current != mkTrue()) { - Assert(current.getKind() == kind::EQUAL || (current.getKind() == kind::NOT && current[0].getKind() == kind::EQUAL)); - expandedNodes.insert(current); - } - ++ it; - } +/* Get a set of all operands of nested and nodes. */ +void getConjuncts(TNode node, std::set<TNode>& conjuncts); +void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts); +/* Create a flattened and node. */ +Node flattenAnd(std::vector<TNode>& queue); - Assert(expandedNodes.size() > 0); - if (expandedNodes.size() == 1) { - return *expandedNodes.begin(); - } +/* Create a string representing a set of nodes. */ +std::string setToString(const std::set<TNode>& nodeSet); - NodeBuilder<> conjunction(kind::AND); +/* Create a string representing a vector of nodes. */ +std::string vectorToString(const std::vector<Node>& nodes); - it = expandedNodes.begin(); - it_end = expandedNodes.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -} - -/** - * If node is a constant of the form 2^c or -2^c, then this function returns - * c+1. Otherwise, this function returns 0. The flag isNeg is updated to - * indicate whether node is negative. - */ -inline unsigned isPow2Const(TNode node, bool& isNeg) -{ - if (node.getKind() != kind::CONST_BITVECTOR) { - return false; - } - - BitVector bv = node.getConst<BitVector>(); - unsigned p = bv.isPow2(); - if (p != 0) - { - isNeg = false; - return p; - } - BitVector nbv = -bv; - p = nbv.isPow2(); - if (p != 0) - { - isNeg = true; - return p; - } - return false; -} - -inline Node mkOr(const std::vector<Node>& nodes) { - std::set<TNode> all; - all.insert(nodes.begin(), nodes.end()); - - if (all.size() == 0) { - return mkTrue(); - } - - if (all.size() == 1) { - // All the same, or just one - return nodes[0]; - } - - - NodeBuilder<> disjunction(kind::OR); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - disjunction << *it; - ++ it; - } - - return disjunction; -}/* mkOr() */ - - -inline Node mkAnd(const std::vector<TNode>& conjunctions) { - std::set<TNode> all; - all.insert(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 0) { - return mkTrue(); - } - - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -}/* mkAnd() */ - -inline Node mkAnd(const std::vector<Node>& conjunctions) { - std::set<TNode> all; - all.insert(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 0) { - return mkTrue(); - } - - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -}/* mkAnd() */ - -inline bool isZero(TNode node) { - if (!node.isConst()) return false; - return node == utils::mkConst(utils::getSize(node), 0u); -} - -inline Node flattenAnd(std::vector<TNode>& queue) { - TNodeSet nodes; - while(!queue.empty()) { - TNode current = queue.back(); - queue.pop_back(); - if (current.getKind() == kind::AND) { - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - if (nodes.count(current[i]) == 0) { - queue.push_back(current[i]); - } - } - } else { - nodes.insert(current); - } - } - std::vector<TNode> children; - for (TNodeSet::const_iterator it = nodes.begin(); it!= nodes.end(); ++it) { - children.push_back(*it); - } - return mkAnd(children); -} - - -// need a better name, this is not technically a ground term -inline bool isBVGroundTerm(TNode node) { - if (node.getNumChildren() == 0) { - return node.isConst(); - } - - for (size_t i = 0; i < node.getNumChildren(); ++i) { - if(! node[i].isConst()) { - return false; - } - } - return true; -} - -inline 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))) - { - return true; - } - else - { - return false; - } -} - -inline Node mkConjunction(const std::vector<TNode>& nodes) { - std::vector<TNode> expandedNodes; - - std::vector<TNode>::const_iterator it = nodes.begin(); - std::vector<TNode>::const_iterator it_end = nodes.end(); - while (it != it_end) { - TNode current = *it; - - if (current != mkTrue()) { - Assert(isBVPredicate(current)); - expandedNodes.push_back(current); - } - ++ it; - } - - if (expandedNodes.size() == 0) { - return mkTrue(); - } - - if (expandedNodes.size() == 1) { - return *expandedNodes.begin(); - } - - NodeBuilder<> conjunction(kind::AND); - - it = expandedNodes.begin(); - it_end = expandedNodes.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -} - - - -// Turn a set into a string -inline std::string setToString(const std::set<TNode>& nodeSet) { - std::stringstream out; - out << "["; - std::set<TNode>::const_iterator it = nodeSet.begin(); - std::set<TNode>::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(); -} - -// Turn a vector into a string -inline std::string vectorToString(const std::vector<Node>& 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 -inline void intersect(const std::vector<uint32_t>& v1, - const std::vector<uint32_t>& v2, - std::vector<uint32_t>& intersection) { - for (unsigned i = 0; i < v1.size(); ++i) { - bool found = false; - for (unsigned j = 0; j < v2.size(); ++j) { - if (v2[j] == v1[i]) { - found = true; - break; - } - } - if (found) { - intersection.push_back(v1[i]); - } - } -} - -template <class T> -inline T gcd(T a, T b) { - while (b != 0) { - T t = b; - b = a % t; - a = t; - } - return a; -} - -typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; - -bool isCoreTerm(TNode term, TNodeBoolMap& cache); -bool isEqualityTerm(TNode term, TNodeBoolMap& cache); -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +/* Create the intersection of two vectors of uint32_t. */ +void intersect(const std::vector<uint32_t>& v1, + const std::vector<uint32_t>& v2, + std::vector<uint32_t>& intersection); +/* Determine the total number of nodes that a given node consists of. */ uint64_t numNodes(TNode node, NodeSet& seen); +/* Collect all variables under a given a node. */ void collectVariables(TNode node, NodeSet& vars); -// is bitblast atom -inline bool isBitblastAtom( Node lit ) { - TNode atom = lit.getKind()==kind::NOT ? lit[0] : lit; - return atom.getKind()!=kind::EQUAL || atom[0].getType().isBitVector(); -} - } } } |