diff options
author | lianah <lianahady@gmail.com> | 2015-05-29 10:18:36 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2015-05-29 10:18:36 -0400 |
commit | 331f8cccb1f5fc8806774652deb71f23c7572772 (patch) | |
tree | 1cf4b0d6356840f0543b301f8e90544f5ca3dbe3 /src/prop | |
parent | b4aaa40ca834958130a8ee5a922ac45c6de84ce1 (diff) |
changed resource step options to unsigned
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 4 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 2 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 4 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 2 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 2 |
7 files changed, 10 insertions, 10 deletions
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 2c9662655..0bf4edf6a 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -46,10 +46,10 @@ private: d_notify->notify(satClause); } - void spendResource(uint64_t ammount) { + void spendResource(unsigned ammount) { d_notify->spendResource(ammount); } - void safePoint(uint64_t ammount) { + void safePoint(unsigned ammount) { d_notify->safePoint(ammount); } }; diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 7d2a978b9..016a0c225 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -52,8 +52,8 @@ public: */ virtual void notify(vec<Lit>& learnt) = 0; - virtual void spendResource(uint64_t ammount) = 0; - virtual void safePoint(uint64_t ammount) = 0; + virtual void spendResource(unsigned ammount) = 0; + virtual void safePoint(unsigned ammount) = 0; }; //================================================================================================= diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e6d965f8f..794e36e2c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -281,7 +281,7 @@ void PropEngine::interrupt() throw(ModalException) { Debug("prop") << "interrupt()" << endl; } -void PropEngine::spendResource(uint64_t ammount) throw (UnsafeInterruptException) { +void PropEngine::spendResource(unsigned ammount) throw (UnsafeInterruptException) { d_resourceManager->spendResource(ammount); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 17ac394c3..768f07108 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -228,7 +228,7 @@ public: * Informs the ResourceManager that a resource has been spent. If out of * resources, can throw an UnsafeInterruptException exception. */ - void spendResource(uint64_t ammount) throw (UnsafeInterruptException); + void spendResource(unsigned ammount) throw (UnsafeInterruptException); /** * For debugging. Return true if "expl" is a well-formed diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 79758a425..50d308541 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -97,8 +97,8 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; - virtual void spendResource(uint64_t ammount) = 0; - virtual void safePoint(uint64_t ammount) = 0; + virtual void spendResource(unsigned ammount) = 0; + virtual void safePoint(unsigned ammount) = 0; };/* class BVSatSolverInterface::Notify */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 5b80b7596..9c6da703a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -179,7 +179,7 @@ void TheoryProxy::logDecision(SatLiteral lit) { #endif /* CVC4_REPLAY */ } -void TheoryProxy::spendResource(uint64_t ammount) { +void TheoryProxy::spendResource(unsigned ammount) { d_theoryEngine->spendResource(ammount); } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index d978edefd..90ad558f5 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -111,7 +111,7 @@ public: void logDecision(SatLiteral lit); - void spendResource(uint64_t ammount); + void spendResource(unsigned ammount); bool isDecisionEngineDone(); |