summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/bvminisat/bvminisat.h4
-rw-r--r--src/prop/bvminisat/core/Solver.h4
-rw-r--r--src/prop/prop_engine.cpp2
-rw-r--r--src/prop/prop_engine.h2
-rw-r--r--src/prop/sat_solver.h4
-rw-r--r--src/prop/theory_proxy.cpp2
-rw-r--r--src/prop/theory_proxy.h2
-rw-r--r--src/smt/options24
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/theory/bv/bitblaster_template.h8
-rw-r--r--src/theory/bv/lazy_bitblaster.cpp4
-rw-r--r--src/theory/bv/theory_bv.cpp2
-rw-r--r--src/theory/bv/theory_bv.h2
-rw-r--r--src/theory/output_channel.h2
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_engine.h4
-rw-r--r--src/util/resource_manager.cpp2
-rw-r--r--src/util/resource_manager.h2
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<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();
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<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
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback