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.

2 files changed, 816 insertions, 584 deletions

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<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(
@@ -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<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 */
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<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;
-}
-
-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.
@@ -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<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();
-}
-
 }
 }
 }