From: Aina Niemetz Date: Wed, 7 Feb 2018 05:42:25 +0000 (-0800) Subject: Split and document theory_bv_utils. (#1566) X-Git-Tag: cvc5-1.0.0~5320 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9488458ba6dac653289d7d025239c1501f626369;p=cvc5.git Split and document theory_bv_utils. (#1566) This moves the implementation from the header to the .cpp file. It further documents all functions in the header file. --- diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 783d04492..c514a2538 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -2,17 +2,16 @@ /*! \file theory_bv_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Paul Meng + ** Aina Niemetz, Liana Hadarean, 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 ** - ** \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 "theory/bv/theory_bv_utils.h" @@ -26,21 +25,506 @@ namespace theory { namespace bv { namespace utils { -Node mkSum(std::vector& children, unsigned width) +/* ------------------------------------------------------------------------- */ + +uint32_t pow2(uint32_t n) +{ + Assert(n < 32); + uint32_t one = 1; + return one << n; +} + +/* ------------------------------------------------------------------------- */ + +BitVector mkBitVectorOnes(unsigned size) +{ + Assert(size > 0); + return BitVector(1, Integer(1)).signExtend(size - 1); +} + +BitVector mkBitVectorMinSigned(unsigned size) +{ + Assert(size > 0); + return BitVector(size).setBit(size - 1); +} + +BitVector mkBitVectorMaxSigned(unsigned size) +{ + Assert(size > 0); + return ~mkBitVectorMinSigned(size); +} + +/* ------------------------------------------------------------------------- */ + +unsigned getSize(TNode node) +{ + return node.getType().getBitVectorSize(); +} + +const bool getBit(TNode node, unsigned i) +{ + Assert(i < utils::getSize(node) && node.getKind() == kind::CONST_BITVECTOR); + Integer bit = node.getConst().extract(i, i).getValue(); + return (bit == 1u); +} + +/* ------------------------------------------------------------------------- */ + +unsigned getExtractHigh(TNode node) +{ + return node.getOperator().getConst().high; +} + +unsigned getExtractLow(TNode node) +{ + return node.getOperator().getConst().low; +} + +unsigned getSignExtendAmount(TNode node) +{ + return node.getOperator().getConst().signExtendAmount; +} + +/* ------------------------------------------------------------------------- */ + +bool isZero(TNode node) +{ + if (!node.isConst()) return false; + return node == utils::mkConst(utils::getSize(node), 0u); +} + +unsigned isPow2Const(TNode node, bool& isNeg) +{ + if (node.getKind() != kind::CONST_BITVECTOR) + { + return false; + } + + BitVector bv = node.getConst(); + 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; +} + +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; +} + +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; + } +} + +bool isCoreTerm(TNode term, TNodeBoolMap& cache) +{ + term = term.getKind() == kind::NOT ? term[0] : term; + TNodeBoolMap::const_iterator it = cache.find(term); + if (it != cache.end()) + { + return it->second; + } + + if (term.getNumChildren() == 0) return true; + + if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) + { + Kind k = term.getKind(); + if (k != kind::CONST_BITVECTOR && k != kind::BITVECTOR_CONCAT + && k != kind::BITVECTOR_EXTRACT && k != kind::EQUAL + && term.getMetaKind() != kind::metakind::VARIABLE) + { + cache[term] = false; + return false; + } + } + + for (unsigned i = 0; i < term.getNumChildren(); ++i) + { + if (!isCoreTerm(term[i], cache)) + { + cache[term] = false; + return false; + } + } + + cache[term] = true; + return true; +} + +bool isEqualityTerm(TNode term, TNodeBoolMap& cache) { - std::size_t nchildren = children.size(); + term = term.getKind() == kind::NOT ? term[0] : term; + TNodeBoolMap::const_iterator it = cache.find(term); + if (it != cache.end()) + { + return it->second; + } + + if (term.getNumChildren() == 0) return true; - if (nchildren == 0) + if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) { - return mkZero(width); + Kind k = term.getKind(); + if (k != kind::CONST_BITVECTOR && k != kind::EQUAL + && term.getMetaKind() != kind::metakind::VARIABLE) + { + cache[term] = false; + return false; + } } - else if (nchildren == 1) + + for (unsigned i = 0; i < term.getNumChildren(); ++i) + { + if (!isEqualityTerm(term[i], cache)) + { + cache[term] = false; + return false; + } + } + + cache[term] = true; + return true; +} + +bool isBitblastAtom(Node lit) +{ + TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit; + return atom.getKind() != kind::EQUAL || atom[0].getType().isBitVector(); +} + +/* ------------------------------------------------------------------------- */ + +Node mkTrue() +{ + return NodeManager::currentNM()->mkConst(true); +} + +Node mkFalse() +{ + return NodeManager::currentNM()->mkConst(false); +} + +Node mkOnes(unsigned size) +{ + BitVector val = mkBitVectorOnes(size); + return NodeManager::currentNM()->mkConst(val); +} + +Node mkZero(unsigned size) +{ + return mkConst(size, 0u); +} + +Node mkOne(unsigned size) +{ + return mkConst(size, 1u); +} + +/* ------------------------------------------------------------------------- */ + +Node mkConst(unsigned size, unsigned int value) +{ + BitVector val(size, value); + return NodeManager::currentNM()->mkConst(val); +} + +Node mkConst(unsigned size, Integer& value) +{ + return NodeManager::currentNM()->mkConst(BitVector(size, value)); +} + +Node mkConst(const BitVector& value) +{ + return NodeManager::currentNM()->mkConst(value); +} + +/* ------------------------------------------------------------------------- */ + +Node mkVar(unsigned size) +{ + NodeManager* nm = NodeManager::currentNM(); + + return nm->mkSkolem("BVSKOLEM$$", + nm->mkBitVectorType(size), + "is a variable created by the theory of bitvectors"); +} + +/* ------------------------------------------------------------------------- */ + +Node mkNode(Kind kind, TNode child) +{ + return NodeManager::currentNM()->mkNode(kind, child); +} + +Node mkNode(Kind kind, TNode child1, TNode child2) +{ + return NodeManager::currentNM()->mkNode(kind, child1, child2); +} + +Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) +{ + return NodeManager::currentNM()->mkNode(kind, child1, child2, child3); +} + +Node mkNode(Kind kind, std::vector& children) +{ + Assert(children.size() > 0); + if (children.size() == 1) { return children[0]; } - return NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, children); + return NodeManager::currentNM()->mkNode(kind, children); +} + +/* ------------------------------------------------------------------------- */ + +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); + } } +Node mkSortedNode(Kind kind, std::vector& 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); +} + +/* ------------------------------------------------------------------------- */ + +Node mkNot(Node child) +{ + return NodeManager::currentNM()->mkNode(kind::NOT, child); +} + +Node mkAnd(TNode node1, TNode node2) +{ + return NodeManager::currentNM()->mkNode(kind::AND, node1, node2); +} + +Node mkAnd(const std::vector& conjunctions) +{ + std::set 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::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) + { + conjunction << *it; + ++it; + } + + return conjunction; +} + +Node mkAnd(const std::vector& conjunctions) +{ + std::set 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::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) + { + conjunction << *it; + ++it; + } + + return conjunction; +} + +Node mkOr(TNode node1, TNode node2) +{ + return NodeManager::currentNM()->mkNode(kind::OR, node1, node2); +} + +Node mkOr(const std::vector& nodes) +{ + std::set 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::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) + { + disjunction << *it; + ++it; + } + + return disjunction; +} + +Node mkXor(TNode node1, TNode node2) +{ + return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); +} + +/* ------------------------------------------------------------------------- */ + +Node mkSignExtend(TNode node, unsigned amount) +{ + NodeManager* nm = NodeManager::currentNM(); + Node signExtendOp = + nm->mkConst(BitVectorSignExtend(amount)); + return nm->mkNode(signExtendOp, node); +} + +/* ------------------------------------------------------------------------- */ + +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); +} + +Node mkBitOf(TNode node, unsigned index) +{ + Node bitOfOp = + NodeManager::currentNM()->mkConst(BitVectorBitOf(index)); + return NodeManager::currentNM()->mkNode(bitOfOp, node); +} + +/* ------------------------------------------------------------------------- */ + +Node mkConcat(TNode t1, TNode t2) +{ + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2); +} + +Node mkConcat(std::vector& children) +{ + if (children.size() > 1) + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); + else + return children[0]; +} + +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; +} + +/* ------------------------------------------------------------------------- */ + Node mkInc(TNode t) { return NodeManager::currentNM()->mkNode( @@ -53,6 +537,8 @@ Node mkDec(TNode t) kind::BITVECTOR_SUB, t, bv::utils::mkOne(bv::utils::getSize(t))); } +/* ------------------------------------------------------------------------- */ + Node mkUmulo(TNode t1, TNode t2) { unsigned w = getSize(t1); @@ -76,96 +562,233 @@ Node mkUmulo(TNode t1, TNode t2) return nm->mkNode(kind::EQUAL, nm->mkNode(kind::BITVECTOR_OR, tmp), mkOne(1)); } -bool isCoreTerm(TNode term, TNodeBoolMap& cache) { - term = term.getKind() == kind::NOT ? term[0] : term; - TNodeBoolMap::const_iterator it = cache.find(term); - if (it != cache.end()) { - return it->second; +/* ------------------------------------------------------------------------- */ + +Node mkConjunction(const std::set nodes) +{ + std::set expandedNodes; + + std::set::const_iterator it = nodes.begin(); + std::set::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; } - if (term.getNumChildren() == 0) - return true; + Assert(expandedNodes.size() > 0); + if (expandedNodes.size() == 1) + { + return *expandedNodes.begin(); + } - if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) { - Kind k = term.getKind(); - if (k != kind::CONST_BITVECTOR && - k != kind::BITVECTOR_CONCAT && - k != kind::BITVECTOR_EXTRACT && - k != kind::EQUAL && - term.getMetaKind() != kind::metakind::VARIABLE) { - cache[term] = false; - return false; + NodeBuilder<> conjunction(kind::AND); + + it = expandedNodes.begin(); + it_end = expandedNodes.end(); + while (it != it_end) + { + conjunction << *it; + ++it; + } + + return conjunction; +} + +Node mkConjunction(const std::vector& nodes) +{ + std::vector expandedNodes; + + std::vector::const_iterator it = nodes.begin(); + std::vector::const_iterator it_end = nodes.end(); + while (it != it_end) + { + TNode current = *it; + + if (current != mkTrue()) + { + Assert(isBVPredicate(current)); + expandedNodes.push_back(current); } + ++it; } - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - if (!isCoreTerm(term[i], cache)) { - cache[term] = false; - return false; + 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; +} + +/* ------------------------------------------------------------------------- */ + +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); } } +} - cache[term]= true; - return true; +void getConjuncts(std::vector& nodes, std::set& conjuncts) +{ + for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++i) + { + getConjuncts(nodes[i], conjuncts); + } } -bool isEqualityTerm(TNode term, TNodeBoolMap& cache) { - term = term.getKind() == kind::NOT ? term[0] : term; - TNodeBoolMap::const_iterator it = cache.find(term); - if (it != cache.end()) { - return it->second; +Node flattenAnd(std::vector& 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 children; + for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) + { + children.push_back(*it); } + return mkAnd(children); +} - if (term.getNumChildren() == 0) - return true; +/* ------------------------------------------------------------------------- */ - if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) { - Kind k = term.getKind(); - if (k != kind::CONST_BITVECTOR && - k != kind::EQUAL && - term.getMetaKind() != kind::metakind::VARIABLE) { - cache[term] = false; - return false; +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(); +} - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - if (!isEqualityTerm(term[i], cache)) { - cache[term] = false; - return false; +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(); +} - cache[term]= true; - return true; +/* ------------------------------------------------------------------------- */ + +// FIXME: dumb code +void intersect(const std::vector& v1, + const std::vector& v2, + std::vector& 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]); + } + } } +/* ------------------------------------------------------------------------- */ -uint64_t numNodes(TNode node, NodeSet& seen) { - if (seen.find(node) != seen.end()) - return 0; +uint64_t numNodes(TNode node, NodeSet& seen) +{ + if (seen.find(node) != seen.end()) return 0; uint64_t size = 1; - for (unsigned i = 0; i < node.getNumChildren(); ++i) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { size += numNodes(node[i], seen); } seen.insert(node); return size; } -void collectVariables(TNode node, NodeSet& vars) { - if (vars.find(node) != vars.end()) - return; +/* ------------------------------------------------------------------------- */ - if (Theory::isLeafOf(node, THEORY_BV) && node.getKind() != kind::CONST_BITVECTOR) { +void collectVariables(TNode node, NodeSet& vars) +{ + if (vars.find(node) != vars.end()) return; + + if (Theory::isLeafOf(node, THEORY_BV) + && node.getKind() != kind::CONST_BITVECTOR) + { vars.insert(node); return; } - for (unsigned i = 0; i < node.getNumChildren(); ++i) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { collectVariables(node[i], vars); } } +/* ------------------------------------------------------------------------- */ + }/* CVC4::theory::bv::utils namespace */ }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index e304e4801..4554d371c 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,127 @@ typedef std::unordered_set 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().high; -} - -inline unsigned getExtractLow(TNode node) { - return node.getOperator().getConst().low; -} - -inline unsigned getSize(TNode node) { - return node.getType().getBitVectorSize(); -} - -inline unsigned getSignExtendAmount(TNode node) -{ - return node.getOperator().getConst().signExtendAmount; -} - -inline const bool getBit(TNode node, unsigned i) { - Assert (i < utils::getSize(node) && - node.getKind() == kind::CONST_BITVECTOR); - Integer bit = node.getConst().extract(i, i).getValue(); - return (bit == 1u); -} - -inline Node mkTrue() { - return NodeManager::currentNM()->mkConst(true); -} - -inline Node mkFalse() { - return NodeManager::currentNM()->mkConst(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& 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& 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); - } -} - -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); -} +typedef std::unordered_map TNodeBoolMap; +typedef std::unordered_set NodeSet; -inline Node mkXor(TNode node1, TNode node2) { - return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); -} +/* Compute 2^n. */ +uint32_t pow2(uint32_t n); -inline Node mkSignExtend(TNode node, unsigned amount) +/* Compute the greatest common divisor for two objects of Type T. */ +template +T gcd(T a, T b) { - NodeManager* nm = NodeManager::currentNM(); - Node signExtendOp = - nm->mkConst(BitVectorSignExtend(amount)); - return nm->mkNode(signExtendOp, node); -} - -inline 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); -} - -inline Node mkBitOf(TNode node, unsigned index) { - Node bitOfOp = NodeManager::currentNM()->mkConst(BitVectorBitOf(index)); - return NodeManager::currentNM()->mkNode(bitOfOp, node); -} - -Node mkSum(std::vector& children, unsigned width); - -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; + while (b != 0) + { + T t = b; + b = a % t; + a = t; } - Node resultNode = result; - return resultNode; -} - -inline Node mkConcat(std::vector& children) { - if (children.size() > 1) - return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); - else - return children[0]; -} - -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) -{ - Assert(size > 0); - return BitVector(size).setBit(size - 1); -} - -inline BitVector mkBitVectorMaxSigned(unsigned size) -{ - Assert(size > 0); - return ~mkBitVectorMinSigned(size); -} - -inline Node mkOnes(unsigned size) { - BitVector val = mkBitVectorOnes(size); - return NodeManager::currentNM()->mkConst(val); + return a; } -inline Node mkConst(unsigned size, unsigned int value) { - BitVector val(size, value); - return NodeManager::currentNM()->mkConst(val); -} +/* 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 mkConst(unsigned size, Integer& value) -{ - return NodeManager::currentNM()->mkConst(BitVector(size, value)); -} +/* Get the bit-width of given node. */ +unsigned getSize(TNode node); -inline Node mkConst(const BitVector& value) { - return NodeManager::currentNM()->mkConst(value); -} +/* Get bit at given index. */ +const bool getBit(TNode node, unsigned i); -inline Node mkZero(unsigned size) { return mkConst(size, 0u); } +/* 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 mkOne(unsigned size) { return mkConst(size, 1u); } +/* Get the number of bits by which a given node is extended. */ +unsigned getSignExtendAmount(TNode node); -/* Increment */ +/* 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); +// TODO: need a better name, this is not technically a ground term +/* Returns true if node or all of its children is const. */ +bool isBVGroundTerm(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& 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& children); + +/* Create node of kind NOT. */ +Node mkNot(Node child); +/* Create node of kind AND. */ +Node mkAnd(TNode node1, TNode node2); +Node mkAnd(const std::vector& conjunctions); +Node mkAnd(const std::vector& conjunctions); +/* Create node of kind OR. */ +Node mkOr(TNode node1, TNode node2); +Node mkOr(const std::vector& nodes); +/* 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& 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 +164,33 @@ Node mkDec(TNode t); * http://ieeexplore.ieee.org/document/987767 */ Node mkUmulo(TNode t1, TNode t2); -inline 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); - } - } -} +/* Create conjunction over a set of (dis)equalities. */ +Node mkConjunction(const std::set nodes); +Node mkConjunction(const std::vector& nodes); -inline void getConjuncts(std::vector& nodes, std::set& conjuncts) { - for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) { - getConjuncts(nodes[i], conjuncts); - } -} +/* 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); -inline Node mkConjunction(const std::set nodes) { - std::set expandedNodes; - - std::set::const_iterator it = nodes.begin(); - std::set::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; - } - - Assert(expandedNodes.size() > 0); - 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; -} - -/** - * 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(); - 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& nodes) { - std::set 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::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - disjunction << *it; - ++ it; - } - - return disjunction; -}/* mkOr() */ - - -inline Node mkAnd(const std::vector& conjunctions) { - std::set 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::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -}/* mkAnd() */ - -inline Node mkAnd(const std::vector& conjunctions) { - std::set 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::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } +/* Create a string representing a set of nodes. */ +std::string setToString(const std::set& nodeSet); - return conjunction; -}/* mkAnd() */ +/* Create a string representing a vector of nodes. */ +std::string vectorToString(const std::vector& nodes); -inline bool isZero(TNode node) { - if (!node.isConst()) return false; - return node == utils::mkConst(utils::getSize(node), 0u); -} - -inline Node flattenAnd(std::vector& 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 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& nodes) { - std::vector expandedNodes; - - std::vector::const_iterator it = nodes.begin(); - std::vector::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& 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(); -} - -// Turn a vector into a string -inline 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 -inline void intersect(const std::vector& v1, - const std::vector& v2, - std::vector& 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 -inline T gcd(T a, T b) { - while (b != 0) { - T t = b; - b = a % t; - a = t; - } - return a; -} - -typedef std::unordered_map TNodeBoolMap; - -bool isCoreTerm(TNode term, TNodeBoolMap& cache); -bool isEqualityTerm(TNode term, TNodeBoolMap& cache); -typedef std::unordered_set NodeSet; +/* Create the intersection of two vectors of uint32_t. */ +void intersect(const std::vector& v1, + const std::vector& v2, + std::vector& 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(); -} - } } }