Refactored CnfStream to work with the bv theory Bitblaster:

    * separated SatSolverInput interface class into two classes:
           - TheoryProxy for the sat solver to communicate with the theories
           - SatSolverInterface abstract class to communicate with the sat solver
    * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
    * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces 

Replaced TheoryBV with bitblasting implementation:
    * all operators bitblasted
    * only operator elimination rewrite rules so far
  

1 files changed, 0 insertions, 677 deletions

diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
deleted file mode 100644
index 80ac98001..000000000
--- a/src/theory/bv/slice_manager.h
+++ /dev/null
@@ -1,677 +0,0 @@
-/*********************                                                        */
-/*! \file slice_manager.h
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-/*
- * slice_manager.h
- *
- *  Created on: Feb 16, 2011
- *      Author: dejan
- */
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include "context/cdo.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/equality_engine.h"
-#include "theory/bv/cd_set_collection.h"
-
-#include <map>
-#include <set>
-#include <vector>
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-/**
- * Representation of the slice points in tree.
- */
-class slice_point
-{
-public:
-
-  /** Number of bits we use for the index of the slice */
-  static const size_t s_slice_index_bits = 31;
-  /** Number of bits we use for the index of the slice_point in the slice memory (reference) */
-  static const size_t s_slice_point_reference_bits = 32;
-  /** The null reference (maximal number in the given bits) */
-  static const size_t null = (1llu << s_slice_point_reference_bits) - 1;
-
-  /** Type of the reference for the outside world */
-  typedef size_t reference_type;
-
-  /** Type of the value for the outside world */
-  typedef size_t value_type;
-
-private:
-
-  /** The value of the slice point (bit index) */
-  size_t d_value       : s_slice_index_bits;
-  /** Is this the left child */
-  size_t d_isLeftChild : 1;
-  /** Reference to the left in the tree */
-  size_t d_left        : s_slice_point_reference_bits;
-  /** Reference to the right of the tree */
-  size_t d_right       : s_slice_point_reference_bits;
-  /** Reference to the parent */
-  size_t d_parent      : s_slice_point_reference_bits;
-
-public:
-
-  slice_point(size_t value, size_t left, size_t right, size_t parent, bool isLeftChild)
-  : d_value(value), d_isLeftChild(isLeftChild ? 1 : 0), d_left(left), d_right(right), d_parent(parent) {}
-
-  bool isLeft() const  { return d_isLeftChild == 1; }
-  bool isRight() const { return d_isLeftChild == 0; }
-
-  bool hasLeft() const   { return d_left   != null; }
-  bool hasRight() const  { return d_right  != null; }
-  bool hasParent() const { return d_parent != null; }
-
-  reference_type getLeft() const   { return d_left;   }
-  reference_type getRight() const  { return d_right;  }
-  reference_type getParent() const { return d_parent; }
-
-  void removeLeft()  { Assert(d_left  != null); d_left = null;  }
-  void removeRight() { Assert(d_right != null); d_right = null; }
-
-  void setLeft(reference_type left)   { Assert(d_left  == null && left  != null); d_left  = left;  }
-  void setRight(reference_type right) { Assert(d_right == null && right != null); d_right = right; }
-
-  value_type getValue() const { return d_value; }
-};
-
-/**
- * Slice manager should keep the database of slices for the core theory leaf terms, for example
- *
- * term                           core leaf terms
- * ----------------------------------------------
- * (x + y)[31:0]                  x + y
- * a[10:0]@a[11:10]@(b + c)[1:0]  a, b, (b + c)
- * (a << 5)[10]                   (a << 5)
- *
- * If an (dis-)equality is added to the system, we refine the slicing in order to align the extracts, for example
- *
- * equality                       slicing
- * ----------------------------------------------
- * x = y                          x[32,0], y[32,0]
- * x@y = z                        x[32,0], y[32,0], z[64,32,0]
- * x@y = z, x[31:16] = y[15:0]    x[32,16,0], y[32,16,0], z[64,48,32,16,0]
- *
- * As a result of the slicing the slicing equalities are added to the equality engine, using the (associative)
- * concat function that is generated for the equality manager, for example
- *
- * equality                       added equalities
- * ----------------------------------------------
- * x = y                          none
- * x@y = z                        z = concat(z[63:32],z[31:0])
- * x@y = z, x[31:16] = y[15:0]    z = concat(z[63:32],z[31:0]),
- *                                z[63:32] = concat(z[63:48], z[47:32]),
- *                                z[31:0] = concat(z[31:16], z[15:0])
- *
- * In the last example, since concat is associative, the equality engine will know that z = concat(z[63:48], z[47:32],
- * z[31:16], z[15:0]).
- *
- */
-template <class TheoryBitvector>
-class SliceManager {
-
-public:
-
-  /** The references to backtrackable sets */
-  typedef slice_point::reference_type set_reference;
-
-  /** The set collection we'll be using */
-  typedef context::BacktrackableSetCollection<std::vector<slice_point>, slice_point, set_reference> set_collection;
-
-  /** The map type from nodes to their references */
-  typedef context::CDMap<Node, set_reference, NodeHashFunction> slicing_map;
-
-  /** The equality engine theory of bit-vectors is using */
-  typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine;
-
-private:
-
-  /** The theory of bitvectors */
-  TheoryBitvector& d_theoryBitvector;
-
-  /** The equality engine */
-  EqualityEngine& d_equalityEngine;
-
-  /** The collection of backtrackable sets */
-  set_collection d_setCollection;
-
-  /**
-   * A map from base nodes to slice points. For each node, the slice points are
-   * 0 = i_1 < i_2 < ... < i_n = size, and the slices are
-   *            x[i_n-1:i_{n-1}]@x[i_{n-1}-1:i_{n-2}]@...@x[i_2-1:i_1]
-   * Each time we add a slict t = t1@t2@...@tn of a term (or a slice), we also notify the equality engine with an
-   * extra assertion. Since the equality engine is backtrackable, we will need to backtrack the slices accordingly.
-   */
-  slicing_map d_nodeSlicing;
-
-public:
-
-  SliceManager(TheoryBitvector& theoryBitvector, context::Context* context)
-  : d_theoryBitvector(theoryBitvector),
-    d_equalityEngine(theoryBitvector.getEqualityEngine()),
-    d_setCollection(context),
-    d_nodeSlicing(context)
-  {
-  }
-
-  /**
-   * Adds the equality (lhs = rhs) to the slice manager. The equality is first normalized according to the equality
-   * manager, i.e. each base term is taken from the equality manager, replaced in, and then the whole concatenation
-   * normalized and sliced wrt the current slicing. The method will not add the equalities to the equality manager,
-   * but instead will slice the equality according to the current slicing in order to align all the slices.
-   *
-   * The terms that get sliced get sent to the theory engine as equalities, i.e if we slice x[10:0] into x[10:5]@x[4:0]
-   * equality engine gets the assertion x[10:0] = concat(x[10:5], x[4:0]).
-   *
-   * input                                 output                            slicing
-   * --------------------------------------------------------------------------------------------------------------
-   * x@y = y@x                             x = y, y = x                      empty
-   * x[31:0]@x[64:32] = x                  x = x[31:0]@x[63:32]              x:{64,32,0}
-   * x@y = 0000@x@0000                     x = 0000@x[7:4], y = x[3:0]@0000  x:{8,4,0}
-   *
-   */
-  inline bool solveEquality(TNode lhs, TNode rhs);
-
-private:
-
-  inline bool solveEquality(TNode lhs, TNode rhs, const std::set<TNode>& assumptions);
-
-  /**
-   * Slices up lhs and rhs and returns the slices in lhsSlices and rhsSlices. The slices are not atomic,
-   * they are sliced in order to make one of lhs or rhs atomic, the other one can be a concatenation.
-   */
-  inline bool sliceAndSolve(std::vector<Node>& lhs, std::vector<Node>& rhs, const std::set<TNode>& assumptions);
-
-  /**
-   * Returns true if the term is already sliced wrt the current slicing. Note that, for example, even though
-   * the slicing is empty, x[i:j] is considered sliced. Sliced means that there is no slice points between i and j.
-   */
-  inline bool isSliced(TNode node) const;
-
-  /**
-   * Slices the term wrt the current slicing. When done, isSliced returns true
-   */
-  inline bool slice(TNode node, std::vector<Node>& sliced);
-
-  /**
-   * Returns the base term in the core theory of the given term, i.e.
-   * x            => x
-   * x[i:j]       => x
-   * (x + y)      => x+y
-   * (x + y)[i:j] => x+y
-   */
-  static inline TNode baseTerm(TNode node);
-
-  /**
-   * Adds a new slice to the slice set of the given term.
-   */
-  inline bool addSlice(Node term, unsigned slicePoint);
-};
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs) {
-  std::set<TNode> assumptions;
-  assumptions.insert(lhs.eqNode(rhs));
-  bool ok = solveEquality(lhs, rhs, assumptions);
-  return ok;
-}
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::solveEquality(TNode lhs, TNode rhs, const std::set<TNode>& assumptions) {
-
-  BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << push << std::endl;
-
-  bool ok;
-
-  // The concatenations on the left-hand side (reverse order, first is on top)
-  std::vector<Node> lhsTerms;
-  if (lhs.getKind() == kind::BITVECTOR_CONCAT) {
-    for (int i = (int) lhs.getNumChildren() - 1; i >= 0; -- i) {
-      lhsTerms.push_back(lhs[i]);
-    }
-  } else {
-    lhsTerms.push_back(lhs);
-  }
-
-  // The concatenations on the right-hand side (reverse order, first is on top)
-  std::vector<Node> rhsTerms;
-  if (rhs.getKind() == kind::BITVECTOR_CONCAT) {
-    for (int i = (int) rhs.getNumChildren() - 1; i >= 0; --i) {
-      rhsTerms.push_back(rhs[i]);
-    }
-  } else {
-    rhsTerms.push_back(rhs);
-  }
-
-  // Slice the individual terms to align them
-  ok = sliceAndSolve(lhsTerms, rhsTerms, assumptions);
-
-  BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << pop << std::endl;
-
-  return ok;
-}
-
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::sliceAndSolve(std::vector<Node>& lhs, std::vector<Node>& rhs, const std::set<TNode>& assumptions)
-{
-
-  BVDebug("slicing") << "SliceManager::sliceAndSolve()" << std::endl;
-
-  // Go through the work-list, solve and align
-  while (!lhs.empty()) {
-
-    Assert(!rhs.empty());
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs " << utils::vectorToString(lhs) << std::endl;
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs " << utils::vectorToString(rhs) << std::endl;
-
-    // The terms that we need to slice
-    Node lhsTerm = lhs.back();
-    Node rhsTerm = rhs.back();
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << lhsTerm << " : " << rhsTerm << std::endl;
-
-    // If the terms are not sliced wrt the current slicing, we have them sliced
-    lhs.pop_back();
-    if (!isSliced(lhsTerm)) {
-      if (!slice(lhsTerm, lhs)) return false;
-      BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs sliced" << std::endl;
-      continue;
-    }
-    rhs.pop_back();
-    if (!isSliced(rhsTerm)) {
-      if (!slice(rhsTerm, rhs)) return false;
-      // We also need to put lhs back
-      lhs.push_back(lhsTerm);
-      BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs sliced" << std::endl;
-      continue;
-    }
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): both lhs and rhs sliced already" << std::endl;
-
-    // The solving concatenation
-    std::vector<Node> concatTerms;
-
-    // If the slices are of the same size we do the additional work
-    int sizeDifference = utils::getSize(lhsTerm) - utils::getSize(rhsTerm);
-
-    // We slice constants immediately
-    if (sizeDifference > 0 && lhsTerm.getKind() == kind::CONST_BITVECTOR) {
-      Node low  = utils::mkConst(lhsTerm.getConst<BitVector>().extract(sizeDifference - 1, 0));
-      Node high = utils::mkConst(lhsTerm.getConst<BitVector>().extract(utils::getSize(lhsTerm) - 1, sizeDifference));
-      d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high);
-      lhs.push_back(low);
-      lhs.push_back(high);
-      rhs.push_back(rhsTerm);
-      continue;
-    }
-    if (sizeDifference < 0 && rhsTerm.getKind() == kind::CONST_BITVECTOR) {
-      Node low  = utils::mkConst(rhsTerm.getConst<BitVector>().extract(-sizeDifference - 1, 0));
-      Node high = utils::mkConst(rhsTerm.getConst<BitVector>().extract(utils::getSize(rhsTerm) - 1, -sizeDifference));
-      d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high);
-      rhs.push_back(low);
-      rhs.push_back(high);
-      lhs.push_back(lhsTerm);
-      continue;
-    }
-
-    enum SolvingFor {
-      SOLVING_FOR_LHS,
-      SOLVING_FOR_RHS
-    } solvingFor = sizeDifference < 0 || lhsTerm.getKind() == kind::CONST_BITVECTOR ? SOLVING_FOR_RHS : SOLVING_FOR_LHS;
-
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << (solvingFor == SOLVING_FOR_LHS ? "solving for LHS" : "solving for RHS") << std::endl;
-
-    // When we slice in order to align, we might have to reslice the one we are solving for
-    bool reslice = false;
-
-    switch (solvingFor) {
-    case SOLVING_FOR_RHS: {
-      concatTerms.push_back(lhsTerm);
-      // Maybe we need to add more lhs to make them equal
-      while (sizeDifference < 0 && !reslice) {
-        Assert(lhs.size() > 0);
-        // Get the next part for lhs
-        lhsTerm = lhs.back();
-        lhs.pop_back();
-        // Slice if necessary
-        if (!isSliced(lhsTerm)) {
-          if (!slice(lhsTerm, lhs)) return false;
-          continue;
-        }
-        // If we go above 0, we need to cut it
-        if (sizeDifference + (int)utils::getSize(lhsTerm) > 0) {
-          // Slice it so it fits
-          addSlice(lhsTerm, (int)utils::getSize(lhsTerm) + sizeDifference);
-          if (!slice(lhsTerm, lhs)) return false;
-          if (!isSliced(rhsTerm)) {
-            if (!slice(rhsTerm, rhs)) return false;
-            while(!concatTerms.empty()) {
-              lhs.push_back(concatTerms.back());
-              concatTerms.pop_back();
-            }
-            reslice = true;
-          }
-          continue;
-        }
-        concatTerms.push_back(lhsTerm);
-        sizeDifference += utils::getSize(lhsTerm);
-      }
-      break;
-    }
-    case SOLVING_FOR_LHS: {
-      concatTerms.push_back(rhsTerm);
-      // Maybe we need to add more rhs to make them equal
-      while (sizeDifference > 0 && !reslice) {
-        Assert(rhs.size() > 0);
-        // Get the next part for lhs
-        rhsTerm = rhs.back();
-        rhs.pop_back();
-        // Slice if necessary
-        if (!isSliced(rhsTerm)) {
-          if (!slice(rhsTerm, rhs)) return false;
-          continue;
-        }
-        // If we go below 0, we need to cut it
-        if (sizeDifference - (int)utils::getSize(rhsTerm) < 0) {
-          // Slice it so it fits
-          addSlice(rhsTerm, (int)utils::getSize(rhsTerm) - sizeDifference);
-          if (!slice(rhsTerm, rhs)) return false;
-	  if (!isSliced(lhsTerm)) {
-            if (!slice(lhsTerm, lhs)) return false;
-            while(!concatTerms.empty()) {
-              rhs.push_back(concatTerms.back());
-              concatTerms.pop_back();
-            }
-            reslice = true;
-          }
-          continue;
-        }
-        concatTerms.push_back(rhsTerm);
-        sizeDifference -= utils::getSize(rhsTerm);
-      }
-      break;
-    }
-    }
-
-    // If we need to reslice
-    if (reslice) {
-	continue;
-    }
-
-    Assert(sizeDifference == 0);
-
-    Node concat = utils::mkConcat(concatTerms);
-    BVDebug("slicing") << "SliceManager::sliceAndSolve(): concatenation " << concat << std::endl;
-
-    // We have them equal size now. If the base term of the one we are solving is solved into a
-    // non-trivial concatenation already, we have to normalize. A concatenation is non-trivial if
-    // it is not a direct slicing, i.e it is a concat, and normalize(x) != x
-    switch (solvingFor) {
-    case SOLVING_FOR_LHS: {
-      TNode lhsTermRepresentative = d_equalityEngine.getRepresentative(lhsTerm);
-      if (lhsTermRepresentative != lhsTerm &&
-          (lhsTermRepresentative.getKind() == kind::BITVECTOR_CONCAT || lhsTermRepresentative.getKind() == kind::CONST_BITVECTOR)) {
-        // We need to normalize and solve the normalized equations
-        std::vector<TNode> explanation;
-        d_equalityEngine.getExplanation(lhsTerm, lhsTermRepresentative, explanation);
-        std::set<TNode> additionalAssumptions(assumptions);
-        utils::getConjuncts(explanation, additionalAssumptions);
-        bool ok = solveEquality(lhsTermRepresentative, concat, additionalAssumptions);
-        if (!ok) return false;
-      } else {
-        // We're fine, just add the equality
-        BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << lhsTerm << " = " << concat << " " << utils::setToString(assumptions) << std::endl;
-        d_equalityEngine.addTerm(concat);
-        bool ok = d_equalityEngine.addEquality(lhsTerm, concat, utils::mkConjunction(assumptions));
-        if (!ok) return false;
-      }
-      break;
-    }
-    case SOLVING_FOR_RHS: {
-      TNode rhsTermRepresentative = d_equalityEngine.getRepresentative(rhsTerm);
-      if (rhsTermRepresentative != rhsTerm &&
-          (rhsTermRepresentative.getKind() == kind::BITVECTOR_CONCAT || rhsTermRepresentative.getKind() == kind::CONST_BITVECTOR)) {
-        // We need to normalize and solve the normalized equations
-        std::vector<TNode> explanation;
-        d_equalityEngine.getExplanation(rhsTerm, rhsTermRepresentative, explanation);
-        std::set<TNode> additionalAssumptions(assumptions);
-        utils::getConjuncts(explanation, additionalAssumptions);
-        bool ok = solveEquality(rhsTermRepresentative, concat, additionalAssumptions);
-        if (!ok) return false;
-      } else {
-        // We're fine, just add the equality
-        BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << rhsTerm << " = " << concat << utils::setToString(assumptions) << std::endl;
-        d_equalityEngine.addTerm(concat);
-        bool ok = d_equalityEngine.addEquality(rhsTerm, concat, utils::mkConjunction(assumptions));
-        if (!ok) return false;
-      }
-      break;
-    }
-    }
-  }
-
-  return true;
-}
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::isSliced(TNode node) const {
-
-  BVDebug("slicing") << "SliceManager::isSliced(" << node << ")" << std::endl;
-
-  bool result = false;
-
-  // Constants are always sliced
-  if (node.getKind() == kind::CONST_BITVECTOR) {
-    result = true;
-  } else {
-    // The indices of the beginning and end
-    Kind nodeKind = node.getKind();
-    unsigned high = nodeKind == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) : utils::getSize(node) - 1;
-    unsigned low  = nodeKind == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-
-    // Get the base term
-    TNode nodeBase = baseTerm(node);
-    Assert(nodeBase.getKind() != kind::BITVECTOR_CONCAT);
-    Assert(nodeBase.getKind() != kind::CONST_BITVECTOR);
-
-    // Get the base term slice set
-    slicing_map::const_iterator find = d_nodeSlicing.find(nodeBase);
-    // If no slices, it's just a term, so we are done, UNLESS it's an extract
-    if (find == d_nodeSlicing.end()) {
-      result = nodeKind != kind::BITVECTOR_EXTRACT;
-    } else {
-      set_reference sliceSet = (*find).second;
-      Assert(d_setCollection.size(sliceSet) >= 2);
-      // The term is not sliced if one of the borders is not in the slice set or
-      // there is a point between the borders      
-      result = 
-	d_setCollection.contains(sliceSet, low) && d_setCollection.contains(sliceSet, high + 1) &&
-        (low == high || d_setCollection.count(sliceSet, low + 1, high) == 0);
-    }
-  }
-
-  BVDebug("slicing") << "SliceManager::isSliced(" << node << ") => " << (result ? "true" : "false") << std::endl;
-  return result;
-}
-
-template <class TheoryBitvector>
-bool SliceManager<TheoryBitvector>::addSlice(Node node, unsigned slicePoint) {
-  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl;
-
-  bool ok = true;
-
-  int low  = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-  int high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1: utils::getSize(node);
-  slicePoint += low;
-
-  TNode nodeBase = baseTerm(node);
-
-  Assert(nodeBase.getKind() != kind::CONST_BITVECTOR);
-
-  set_reference sliceSet;
-  slicing_map::iterator find = d_nodeSlicing.find(nodeBase);
-  if (find == d_nodeSlicing.end()) {
-    d_nodeSlicing[nodeBase] = sliceSet = d_setCollection.newSet(0);
-    d_setCollection.insert(sliceSet, utils::getSize(nodeBase));
-  } else {
-    sliceSet = (*find).second;
-  }
-
-  Assert(d_setCollection.size(sliceSet) >= 2);
-
-  // What are the points surrounding the new slice point
-  int prev = d_setCollection.prev(sliceSet, slicePoint);
-  int next = d_setCollection.next(sliceSet, slicePoint);
-
-  // Add the slice to the set
-  d_setCollection.insert(sliceSet, slicePoint);
-  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl;
-
-  // Add the terms and the equality to the equality engine
-  Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint);
-  Node t2 = utils::mkExtract(nodeBase, slicePoint - 1, prev);
-  Node nodeSlice = (next == high && prev == low) ? node : utils::mkExtract(nodeBase, next - 1, prev);
-  Node concat = utils::mkConcat(t1, t2);
-
-  d_equalityEngine.addTerm(t1);
-  d_equalityEngine.addTerm(t2);
-  d_equalityEngine.addTerm(nodeSlice);
-  d_equalityEngine.addTerm(concat);
-
-  // We are free to add this slice, unless the slice has a representative that's already a concat
-  TNode nodeSliceRepresentative = d_equalityEngine.getRepresentative(nodeSlice);
-  if (nodeSliceRepresentative.getKind() != kind::BITVECTOR_CONCAT) {
-    // Add the slice to the equality engine
-    ok = d_equalityEngine.addEquality(nodeSlice, concat, utils::mkTrue());
-  } else {
-    // If the representative is a concat, we must solve it
-    // There is no need do add nodeSlice = concat as we will solve the representative of nodeSlice
-    std::set<TNode> assumptions;
-    std::vector<TNode> equalities;
-    d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities);
-    utils::getConjuncts(equalities, assumptions);
-    ok = solveEquality(nodeSliceRepresentative, concat, assumptions);
-  }
-
-  BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl;
-
-  return ok;
-}
-
-template <class TheoryBitvector>
-inline bool SliceManager<TheoryBitvector>::slice(TNode node, std::vector<Node>& sliced) {
-
-  BVDebug("slicing") << "SliceManager::slice(" << node << ")" << std::endl;
-
-  Assert(!isSliced(node));
-
-  // The indices of the beginning and (one past) end
-  unsigned high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1 : utils::getSize(node);
-  unsigned low  = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0;
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): low: " << low << std::endl;
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): high: " << high << std::endl;
-
-  // Get the base term
-  TNode nodeBase = baseTerm(node);
-  Assert(nodeBase.getKind() != kind::BITVECTOR_CONCAT);
-  Assert(nodeBase.getKind() != kind::CONST_BITVECTOR);
-
-  // The nodes slice set
-  set_reference nodeSliceSet;
-
-  // Find the current one or construct it
-  slicing_map::iterator findSliceSet = d_nodeSlicing.find(nodeBase);
-  if (findSliceSet == d_nodeSlicing.end()) {
-    d_nodeSlicing[nodeBase] = nodeSliceSet = d_setCollection.newSet(0);
-    d_setCollection.insert(nodeSliceSet, utils::getSize(nodeBase));
-  } else {
-    nodeSliceSet = d_nodeSlicing[nodeBase];
-  }
-
-  Assert(d_setCollection.size(nodeSliceSet) >= 2);
-
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl;
-  
-  // Go through all the points i_0 <= low < i_1 < ... < i_{n-1} < high <= i_n from the slice set
-  // and generate the slices [i_0:low-1][low:i_1-1] [i_1:i2] ... [i_{n-1}:high-1][high:i_n-1]. They are in reverse order,
-  // as they should be
-  
-  // The high bound already in the slicing
-  size_t i_n = high == utils::getSize(nodeBase) ? high: d_setCollection.next(nodeSliceSet, high - 1);
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): i_n: " << i_n << std::endl;  
-  // Add the new point to the slice set (they might be there already)
-  if (high < i_n) {
-    if (!addSlice(nodeBase, high)) return false;
-  }
-  // The low bound already in the slicing (slicing might have changed after adding high)
-  size_t i_0 = low == 0 ? 0 : d_setCollection.prev(nodeSliceSet, low + 1);
-  BVDebug("slicing") << "SliceManager::slice(" << node << "): i_0: " << i_0 << std::endl;
-  // Add the new points to the slice set (they might be there already)
-  if (i_0 < low) {
-    if (!addSlice(nodeBase, low)) return false;
-  }
-
-  // Get the slice points
-  std::vector<size_t> slicePoints;
-  if (low + 1 < high) {
-    d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints);
-  }
-
-  // Construct the actuall slicing
-  if (slicePoints.size() > 0) {
-    BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[0] - 1, low) << std::endl;
-    sliced.push_back(utils::mkExtract(nodeBase, slicePoints[0] - 1, low));
-    for (unsigned i = 1; i < slicePoints.size(); ++ i) {
-      BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1])<< std::endl;
-      sliced.push_back(utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1]));
-    }
-    BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, high-1, slicePoints.back()) << std::endl;
-    sliced.push_back(utils::mkExtract(nodeBase, high-1, slicePoints.back()));
-  } else {
-    sliced.push_back(utils::mkExtract(nodeBase, high - 1, low));
-  }
-  
-  return true;
-}
-
-template <class TheoryBitvector>
-TNode SliceManager<TheoryBitvector>::baseTerm(TNode node) {
-  if (node.getKind() == kind::BITVECTOR_EXTRACT) {
-    Assert(node[0].getKind() != kind::BITVECTOR_EXTRACT);
-    Assert(node[0].getKind() != kind::CONST_BITVECTOR);
-    return node[0];
-  } else {
-    Assert(node.getKind() != kind::BITVECTOR_CONCAT);
-    return node;
-  }
-}
-
-} // Namespace bv
-} // Namespace theory
-} // Namespace CVC4