fixed build failure

1 files changed, 0 insertions, 230 deletions

diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.h
deleted file mode 100644
index 91ef866bd..000000000
--- a/src/theory/bv/eager_bitblaster.h
+++ /dev/null
@@ -1,230 +0,0 @@
-/*********************                                                        */
-/*! \file eager_bitblaster.h
- ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): lianah
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief 
- **
- ** Bitblaster for the lazy bv solver. 
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__EAGER__BITBLASTER_H
-#define __CVC4__EAGER__BITBLASTER_H
-
-
-#include "theory/theory_registrar.h"
-#include "theory/bv/bitblaster_template.h"
-#include "theory/bv/options.h"
-#include "theory/theory_model.h"
-#include "prop/cnf_stream.h"
-#include "prop/sat_solver_factory.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-
-class BitblastingRegistrar: public prop::Registrar {
-  EagerBitblaster* d_bitblaster; 
-public:
-  BitblastingRegistrar(EagerBitblaster* bb)
-    : d_bitblaster(bb)
-  {}
-  void preRegister(Node n) {
-    d_bitblaster->bbAtom(n); 
-  };
-
-};/* class Registrar */
-
-EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
-  : TBitblaster<Node>()
-  , d_bv(theory_bv)
-  , d_bbAtoms()
-  , d_variables()
-{
-  d_bitblastingRegistrar = new BitblastingRegistrar(this); 
-  d_nullContext = new context::Context();
-
-  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
-  
-  MinisatEmptyNotify* notify = new MinisatEmptyNotify();
-  d_satSolver->setNotify(notify);
-}
-
-EagerBitblaster::~EagerBitblaster() {
-  delete d_cnfStream;
-  delete d_satSolver;
-  delete d_nullContext;
-  delete d_bitblastingRegistrar;
-}
-
-void EagerBitblaster::bbFormula(TNode node) {
-  d_cnfStream->convertAndAssert(node, false, false); 
-}
-
-/**
- * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
- * NOTE: duplicate clauses are not detected because of marker literal
- * @param node the atom to be bitblasted
- *
- */
-void EagerBitblaster::bbAtom(TNode node) {
-  node = node.getKind() == kind::NOT?  node[0] : node;
-  if (node.getKind() == kind::BITVECTOR_BITOF)
-    return; 
-  if (hasBBAtom(node)) {
-    return;
-  }
-
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
-
-  // the bitblasted definition of the atom
-  Node normalized = Rewriter::rewrite(node);
-  Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
-      Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
-      normalized;
-  // asserting that the atom is true iff the definition holds
-  Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
-
-  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); 
-  storeBBAtom(node, atom_definition);
-  d_cnfStream->convertAndAssert(atom_definition, false, false);
-}
-
-void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
-  // no need to store the definition for the lazy bit-blaster
-  d_bbAtoms.insert(atom); 
-}
-
-bool EagerBitblaster::hasBBAtom(TNode atom) const {
-  return d_bbAtoms.find(atom) != d_bbAtoms.end(); 
-}
-
-void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
-  if (hasBBTerm(node)) {
-    getBBTerm(node, bits);
-    return;
-  }
-
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
-
-  d_termBBStrategies[node.getKind()] (node, bits, this);
-
-  Assert (bits.size() == utils::getSize(node));
-
-  storeBBTerm(node, bits);
-}
-
-void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
-  Assert(bits.size() == 0);
-  for (unsigned i = 0; i < utils::getSize(var); ++i) {
-    bits.push_back(utils::mkBitOf(var, i)); 
-  }
-  d_variables.insert(var); 
-}
-
-Node EagerBitblaster::getBBAtom(TNode node) const {
-  return node; 
-}
-
-
-/**
- * Calls the solve method for the Sat Solver.
- *
- * @return true for sat, and false for unsat
- */
-
-bool EagerBitblaster::solve() {
-  if (Trace.isOn("bitvector")) {
-    Trace("bitvector") << "EagerBitblaster::solve(). \n";
-  }
-  Debug("bitvector") << "EagerBitblaster::solve(). \n";
-  // TODO: clear some memory
-  // if (something) {
-  //   NodeManager* nm= NodeManager::currentNM();
-  //   Rewriter::garbageCollect();
-  //   nm->reclaimZombiesUntil(options::zombieHuntThreshold());
-  // }
-  return prop::SAT_VALUE_TRUE == d_satSolver->solve();
-}
-
-
-/**
- * Returns the value a is currently assigned to in the SAT solver
- * or null if the value is completely unassigned.
- *
- * @param a
- * @param fullModel whether to create a "full model," i.e., add
- * constants to equivalence classes that don't already have them
- *
- * @return
- */
-Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
-  if (!hasBBTerm(a)) {
-    Assert(isSharedTerm(a));
-    return Node();
-  }
-  Bits bits;
-  getBBTerm(a, bits);
-  Integer value(0);
-  for (int i = bits.size() -1; i >= 0; --i) {
-    prop::SatValue bit_value;
-    if (d_cnfStream->hasLiteral(bits[i])) {
-      prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
-      bit_value = d_satSolver->value(bit);
-      Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
-    } else {
-      // the bit is unconstrainted so we can give it an arbitrary value
-      bit_value = prop::SAT_VALUE_FALSE;
-    }
-    Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
-    value = value * 2 + bit_int;
-  }
-  return utils::mkConst(BitVector(bits.size(), value));
-}
-
-
-void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
-  TNodeSet::const_iterator it = d_variables.begin();
-  for (; it!= d_variables.end(); ++it) {
-    TNode var = *it;
-    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
-      Node const_value = getVarValue(var, fullModel);
-      if(const_value == Node()) {
-        if( fullModel ){
-          // if the value is unassigned just set it to zero
-          const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
-        }
-      }
-      if(const_value != Node()) {
-        Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
-                                 << var << " "
-                                 << const_value << "))\n";
-        m->assertEquality(var, const_value, true);
-      }
-    }
-  }
-}
-
-bool EagerBitblaster::isSharedTerm(TNode node) {
-  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
-}
-
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-
-
-#endif