From 331f8cccb1f5fc8806774652deb71f23c7572772 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Fri, 29 May 2015 10:18:36 -0400
Subject: changed resource step options to unsigned

---
 src/theory/bv/bitblaster_template.h | 8 ++++----
 src/theory/bv/lazy_bitblaster.cpp   | 4 ++--
 src/theory/bv/theory_bv.cpp         | 2 +-
 src/theory/bv/theory_bv.h           | 2 +-
 src/theory/output_channel.h         | 2 +-
 src/theory/theory_engine.cpp        | 2 +-
 src/theory/theory_engine.h          | 4 ++--
 7 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'src/theory')

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 4d953b03c..d42c4a8c9 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -135,8 +135,8 @@ class TLazyBitblaster :  public TBitblaster<Node> {
     {}
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
-    void spendResource(uint64_t ammount);
-    void safePoint(uint64_t ammount);
+    void spendResource(unsigned ammount);
+    void safePoint(unsigned ammount);
   };
   
   TheoryBV *d_bv;
@@ -240,10 +240,10 @@ public:
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) { return true; }
   void notify(prop::SatClause& clause) { }
-  void spendResource(uint64_t ammount) {
+  void spendResource(unsigned ammount) {
     NodeManager::currentResourceManager()->spendResource(ammount);
   }
-  void safePoint(uint64_t ammount) {}
+  void safePoint(unsigned ammount) {}
 };
 
 
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 61472fd79..59ecc7385 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -356,11 +356,11 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
-void TLazyBitblaster::MinisatNotify::spendResource(uint64_t ammount) {
+void TLazyBitblaster::MinisatNotify::spendResource(unsigned ammount) {
   d_bv->spendResource(ammount);
 }
 
-void TLazyBitblaster::MinisatNotify::safePoint(uint64_t ammount) {
+void TLazyBitblaster::MinisatNotify::safePoint(unsigned ammount) {
   d_bv->d_out->safePoint(ammount);
 }
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 6f399cb7a..95a483d34 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -107,7 +107,7 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   }
 }
 
-void TheoryBV::spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) {
   getOutputChannel().spendResource(ammount);
 }
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 3317d1b01..193de55db 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -103,7 +103,7 @@ private:
 
   Statistics d_statistics;
 
-  void spendResource(uint64_t ammount) throw(UnsafeInterruptException);
+  void spendResource(unsigned ammount) throw(UnsafeInterruptException);
 
   /**
    * Return the uninterpreted function symbol corresponding to division-by-zero
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index f340c994c..2da0f0467 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -213,7 +213,7 @@ public:
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {}
+  virtual void spendResource(unsigned ammount) throw(UnsafeInterruptException) {}
 
   /**
    * Handle user attribute.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 75dafb7f6..9b4815fd4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1756,6 +1756,6 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T
   return th->entailmentCheck(lit, params, seffects);
 }
 
-void TheoryEngine::spendResource(uint64_t ammount) {
+void TheoryEngine::spendResource(unsigned ammount) {
   d_resourceManager->spendResource(ammount);
 }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bb4d4c16d..0c1a7c081 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -347,7 +347,7 @@ class TheoryEngine {
       d_engine->setIncomplete(d_theory);
     }
 
-    void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+    void spendResource(unsigned ammount) throw(UnsafeInterruptException) {
       d_engine->spendResource(ammount);
     }
 
@@ -488,7 +488,7 @@ public:
   /**
    * "Spend" a resource during a search or preprocessing.
    */
-  void spendResource(uint64_t ammount);
+  void spendResource(unsigned ammount);
 
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if
-- 
cgit v1.2.3