From 2821b7a47e779c7d4f189ffdffaebe4bdb5b9036 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 29 Feb 2012 20:33:43 +0000
Subject: This should fix the debian build fails:    * removed bvpicosat
 directory as it is currently not used

Cleared some of the flurry of warnings my previous merge caused in src/prop/
---
 src/theory/bv/bitblast_strategies.cpp | 13 ++++++-------
 src/theory/bv/bv_sat.cpp              |  5 +++++
 src/theory/bv/bv_sat.h                |  6 +-----
 3 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'src/theory')

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index b0a02c0a5..6967bff98 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -55,13 +55,13 @@ void inline extractBits(const Bits& b, Bits& dest, unsigned lo, unsigned hi) {
 }
 
 void inline negateBits(const Bits& bits, Bits& negated_bits) {
-  for(int i = 0; i < bits.size(); ++i) {
+  for(unsigned i = 0; i < bits.size(); ++i) {
     negated_bits.push_back(utils::mkNot(bits[i])); 
   }
 }
 
 bool inline isZero(const Bits& bits) {
-  for(int i = 0; i < bits.size(); ++i) {
+  for(unsigned i = 0; i < bits.size(); ++i) {
     if(bits[i] != mkFalse()) {
       return false; 
     }
@@ -323,7 +323,6 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
   Assert(node.getKind() == kind::CONST_BITVECTOR);
   Assert(bits.size() == 0);
   
-  NodeManager* nm = NodeManager::currentNM(); 
   for (unsigned i = 0; i < utils::getSize(node); ++i) {
     Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
     if(bit == Integer(0)){
@@ -690,12 +689,12 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
   res = a;
   Bits prev_res;
   
-  for(int s = 0; s < b.size(); ++s) {
+  for(unsigned s = 0; s < b.size(); ++s) {
     // barrel shift stage: at each stage you can either shift by 2^s bits
     // or leave the previous stage untouched
     prev_res = res; 
     int threshold = pow(2, s); 
-    for(int i = 0; i < a.size(); ++i) {
+    for(unsigned i = 0; i < a.size(); ++i) {
       if (i + threshold >= a.size()) {
         // if b[s] is true then we must have shifted by at least 2^b bits so
         // all bits above 2^s will be 0, otherwise just use previous shift value
@@ -723,12 +722,12 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
   TNode sign_bit = a.back();
   Bits prev_res;
 
-  for(int s = 0; s < b.size(); ++s) {
+  for(unsigned s = 0; s < b.size(); ++s) {
     // barrel shift stage: at each stage you can either shift by 2^s bits
     // or leave the previous stage untouched
     prev_res = res; 
     int threshold = pow(2, s); 
-    for(int i = 0; i < a.size(); ++i) {
+    for(unsigned i = 0; i < a.size(); ++i) {
       if (i + threshold >= a.size()) {
         // if b[s] is true then we must have shifted by at least 2^b bits so
         // all bits above 2^s will be the sign bit, otherwise just use previous shift value
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index 22a679693..97e886db2 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -64,6 +64,11 @@ Bitblaster::Bitblaster(context::Context* c) :
     initTermBBStrategies(); 
   }
 
+Bitblaster::~Bitblaster() {
+  delete d_cnfStream;
+  delete d_satSolver; 
+}
+
 
 /** 
  * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
index 9844cd982..ee48dbef4 100644
--- a/src/theory/bv/bv_sat.h
+++ b/src/theory/bv/bv_sat.h
@@ -109,11 +109,7 @@ public:
   
 public:
   Bitblaster(context::Context* c); 
-  ~Bitblaster() {
-    delete d_cnfStream;
-    delete d_satSolver; 
-  }
-  
+  ~Bitblaster();
   void assertToSat(TNode node);
   bool solve();
   void bitblast(TNode node);
-- 
cgit v1.2.3