From 331f8cccb1f5fc8806774652deb71f23c7572772 Mon Sep 17 00:00:00 2001 From: lianah Date: Fri, 29 May 2015 10:18:36 -0400 Subject: [PATCH] changed resource step options to unsigned --- src/prop/bvminisat/bvminisat.h | 4 ++-- src/prop/bvminisat/core/Solver.h | 4 ++-- src/prop/prop_engine.cpp | 2 +- src/prop/prop_engine.h | 2 +- src/prop/sat_solver.h | 4 ++-- src/prop/theory_proxy.cpp | 2 +- src/prop/theory_proxy.h | 2 +- src/smt/options | 24 ++++++++++++------------ src/smt/smt_engine.cpp | 2 +- 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 ++-- src/util/resource_manager.cpp | 2 +- src/util/resource_manager.h | 2 +- 18 files changed, 37 insertions(+), 37 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& 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(); diff --git a/src/smt/options b/src/smt/options index dbee33f5a..077acc6e9 100644 --- a/src/smt/options +++ b/src/smt/options @@ -105,40 +105,40 @@ common-option cpuTime cpu-time --cpu-time bool :default false measures CPU time if set to true and wall time if false (default false) # Resource spending options for SPARK -expert-option rewriteStep rewrite-step --rewrite-step uint64_t :default 1 +expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1 ammount of resources spent for each rewrite step -expert-option theoryCheckStep theory-check-step --theory-check-step uint64_t :default 1 +expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1 ammount of resources spent for each theory check call -expert-option decisionStep decision-step --decision-step uint64_t :default 1 +expert-option decisionStep decision-step --decision-step unsigned :default 1 ammount of getNext decision calls in the decision engine -expert-option bitblastStep bitblast-step --bitblast-step uint64_t :default 1 +expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1 ammount of resources spent for each bitblast step -expert-option parseStep parse-step --parse-step uint64_t :default 1 +expert-option parseStep parse-step --parse-step unsigned :default 1 ammount of resources spent for each command/expression parsing -expert-option lemmaStep lemma-step --lemma-step uint64_t :default 1 +expert-option lemmaStep lemma-step --lemma-step unsigned :default 1 ammount of resources spent when adding lemmas -expert-option restartStep restart-step --restart-step uint64_t :default 1 +expert-option restartStep restart-step --restart-step unsigned :default 1 ammount of resources spent for each theory restart -expert-option cnfStep cnf-step --cnf-step uint64_t :default 1 +expert-option cnfStep cnf-step --cnf-step unsigned :default 1 ammount of resources spent for each call to cnf conversion -expert-option preprocessStep preprocess-step --preprocess-step uint64_t :default 1 +expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1 ammount of resources spent for each preprocessing step in SmtEngine -expert-option quantifierStep quantifier-step --quantifier-step uint64_t :default 1 +expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1 ammount of resources spent for quantifier instantiations -expert-option satConflictStep sat-conflict-step --sat-conflict-step uint64_t :default 1 +expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1 ammount of resources spent for each sat conflict (main sat solver) -expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step uint64_t :default 1 +expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1 ammount of resources spent for each sat conflict (bitvectors) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c7c0bc71a..11a412c75 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -492,7 +492,7 @@ public: } ResourceManager* getResourceManager() { return d_resourceManager; } - void spendResource(uint64_t ammount) throw(UnsafeInterruptException) { + void spendResource(unsigned ammount) throw(UnsafeInterruptException) { d_resourceManager->spendResource(ammount); } 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 { {} 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 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 diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 37fea2c67..22496a433 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -170,7 +170,7 @@ uint64_t ResourceManager::getTimeRemaining() const { return d_thisCallTimeBudget - time_passed; } -void ResourceManager::spendResource(uint64_t ammount) throw (UnsafeInterruptException) { +void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) { ++d_spendResourceCalls; d_cumulativeResourceUsed += ammount; if (!d_on) return; diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 9c2812f0f..e84917db0 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -128,7 +128,7 @@ public: return d_thisCallResourceBudget; } - void spendResource(uint64_t ammount) throw(UnsafeInterruptException); + void spendResource(unsigned ammount) throw(UnsafeInterruptException); void setHardLimit(bool value); void setResourceLimit(uint64_t units, bool cumulative = false); -- 2.30.2