/*! \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"
namespace bv {
namespace utils {
-Node mkSum(std::vector<Node>& 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<BitVector>().extract(i, i).getValue();
+ return (bit == 1u);
+}
+
+/* ------------------------------------------------------------------------- */
+
+unsigned getExtractHigh(TNode node)
+{
+ return node.getOperator().getConst<BitVectorExtract>().high;
+}
+
+unsigned getExtractLow(TNode node)
+{
+ return node.getOperator().getConst<BitVectorExtract>().low;
+}
+
+unsigned getSignExtendAmount(TNode node)
+{
+ return node.getOperator().getConst<BitVectorSignExtend>().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<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;
+}
+
+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<bool>(true);
+}
+
+Node mkFalse()
+{
+ return NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+Node mkOnes(unsigned size)
+{
+ BitVector val = mkBitVectorOnes(size);
+ return NodeManager::currentNM()->mkConst<BitVector>(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<BitVector>(val);
+}
+
+Node mkConst(unsigned size, Integer& value)
+{
+ return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value));
+}
+
+Node mkConst(const BitVector& value)
+{
+ return NodeManager::currentNM()->mkConst<BitVector>(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<Node>& 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<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);
+}
+
+/* ------------------------------------------------------------------------- */
+
+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<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;
+}
+
+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;
+}
+
+Node mkOr(TNode node1, TNode node2)
+{
+ return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);
+}
+
+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;
+}
+
+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>(BitVectorSignExtend(amount));
+ return nm->mkNode(signExtendOp, node);
+}
+
+/* ------------------------------------------------------------------------- */
+
+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);
+}
+
+Node mkBitOf(TNode node, unsigned index)
+{
+ Node bitOfOp =
+ NodeManager::currentNM()->mkConst<BitVectorBitOf>(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<Node>& 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(
kind::BITVECTOR_SUB, t, bv::utils::mkOne(bv::utils::getSize(t)));
}
+/* ------------------------------------------------------------------------- */
+
Node mkUmulo(TNode t1, TNode t2)
{
unsigned w = getSize(t1);
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<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;
}
- 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<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;
}
- 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<TNode>& 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<TNode>& nodes, std::set<TNode>& 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<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);
+}
- 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<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();
+}
- for (unsigned i = 0; i < term.getNumChildren(); ++i) {
- if (!isEqualityTerm(term[i], cache)) {
- cache[term] = false;
- return false;
+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();
+}
- cache[term]= true;
- return true;
+/* ------------------------------------------------------------------------- */
+
+// FIXME: dumb code
+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]);
+ }
+ }
}
+/* ------------------------------------------------------------------------- */
-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 */
/*! \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"
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;
-}
-
-inline unsigned getSize(TNode node) {
- return node.getType().getBitVectorSize();
-}
-
-inline unsigned getSignExtendAmount(TNode node)
-{
- 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);
- }
-}
-
-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<TNode, bool, TNodeHashFunction> TNodeBoolMap;
+typedef std::unordered_set<Node, NodeHashFunction> 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 <class T>
+T gcd(T a, T b)
{
- 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);
-}
-
-inline Node mkBitOf(TNode node, unsigned index) {
- Node bitOfOp = NodeManager::currentNM()->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
- return NodeManager::currentNM()->mkNode(bitOfOp, node);
-}
-
-Node mkSum(std::vector<Node>& 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<Node>& 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<BitVector>(val);
+ return a;
}
-inline Node mkConst(unsigned size, unsigned int value) {
- BitVector val(size, value);
- return NodeManager::currentNM()->mkConst<BitVector>(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>(BitVector(size, value));
-}
+/* Get the bit-width of given node. */
+unsigned getSize(TNode node);
-inline Node mkConst(const BitVector& value) {
- return NodeManager::currentNM()->mkConst<BitVector>(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<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);
+Node mkAnd(const std::vector<TNode>& conjunctions);
+Node mkAnd(const std::vector<Node>& conjunctions);
+/* Create node of kind OR. */
+Node mkOr(TNode node1, TNode node2);
+Node mkOr(const std::vector<Node>& 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<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.
* 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);
- }
- }
-}
+/* Create conjunction over a set of (dis)equalities. */
+Node mkConjunction(const std::set<TNode> nodes);
+Node mkConjunction(const std::vector<TNode>& nodes);
-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);
- }
-}
+/* 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);
-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;
- }
-
- 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<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;
- }
+/* Create a string representing a set of nodes. */
+std::string setToString(const std::set<TNode>& nodeSet);
- return conjunction;
-}/* mkAnd() */
+/* Create a string representing a vector of nodes. */
+std::string vectorToString(const std::vector<Node>& nodes);
-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();
-}
-
}
}
}
projects / cvc5.git / commitdiff