summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/options38
-rw-r--r--src/smt/smt_engine.cpp30
2 files changed, 53 insertions, 15 deletions
diff --git a/src/smt/options b/src/smt/options
index b23d73943..dbee33f5a 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -104,6 +104,44 @@ common-option hardLimit hard-limit --hard-limit bool :default false
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
+ ammount of resources spent for each rewrite step
+
+expert-option theoryCheckStep theory-check-step --theory-check-step uint64_t :default 1
+ ammount of resources spent for each theory check call
+
+expert-option decisionStep decision-step --decision-step uint64_t :default 1
+ ammount of getNext decision calls in the decision engine
+
+expert-option bitblastStep bitblast-step --bitblast-step uint64_t :default 1
+ ammount of resources spent for each bitblast step
+
+expert-option parseStep parse-step --parse-step uint64_t :default 1
+ ammount of resources spent for each command/expression parsing
+
+expert-option lemmaStep lemma-step --lemma-step uint64_t :default 1
+ ammount of resources spent when adding lemmas
+
+expert-option restartStep restart-step --restart-step uint64_t :default 1
+ ammount of resources spent for each theory restart
+
+expert-option cnfStep cnf-step --cnf-step uint64_t :default 1
+ ammount of resources spent for each call to cnf conversion
+
+expert-option preprocessStep preprocess-step --preprocess-step uint64_t :default 1
+ ammount of resources spent for each preprocessing step in SmtEngine
+
+expert-option quantifierStep quantifier-step --quantifier-step uint64_t :default 1
+ ammount of resources spent for quantifier instantiations
+
+expert-option satConflictStep sat-conflict-step --sat-conflict-step uint64_t :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
+ ammount of resources spent for each sat conflict (bitvectors)
+
+
expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bc594a47e..c7c0bc71a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -492,8 +492,8 @@ public:
}
ResourceManager* getResourceManager() { return d_resourceManager; }
- void spendResource() throw(UnsafeInterruptException) {
- d_resourceManager->spendResource();
+ void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+ d_resourceManager->spendResource(ammount);
}
void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
@@ -1776,7 +1776,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
// or upward pass).
do {
- spendResource();
+ spendResource(options::preprocessStep());
n = worklist.top().first; // n is the input / original
Node node = worklist.top().second; // node is the output / result
bool childrenPushed = worklist.top().third;
@@ -1912,7 +1912,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
void SmtEnginePrivate::removeITEs() {
d_smt.finalOptionsAreSet();
- spendResource();
+ spendResource(options::preprocessStep());
Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
// Remove all of the ITE occurrences and normalize
@@ -1924,7 +1924,7 @@ void SmtEnginePrivate::removeITEs() {
void SmtEnginePrivate::staticLearning() {
d_smt.finalOptionsAreSet();
- spendResource();
+ spendResource(options::preprocessStep());
TimerStat::CodeTimer staticLearningTimer(d_smt.d_stats->d_staticLearningTime);
@@ -1957,7 +1957,7 @@ static void dumpAssertions(const char* key, const AssertionPipeline& assertionLi
// returns false if it learns a conflict
bool SmtEnginePrivate::nonClausalSimplify() {
- spendResource();
+ spendResource(options::preprocessStep());
d_smt.finalOptionsAreSet();
if(options::unsatCores()) {
@@ -2286,7 +2286,7 @@ void SmtEnginePrivate::bvAbstraction() {
void SmtEnginePrivate::bvToBool() {
Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
- spendResource();
+ spendResource(options::preprocessStep());
std::vector<Node> new_assertions;
d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
@@ -2297,13 +2297,13 @@ void SmtEnginePrivate::bvToBool() {
bool SmtEnginePrivate::simpITE() {
TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
- spendResource();
+ spendResource(options::preprocessStep());
Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
unsigned numAssertionOnEntry = d_assertions.size();
for (unsigned i = 0; i < d_assertions.size(); ++i) {
- spendResource();
+ spendResource(options::preprocessStep());
Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
d_assertions.replace(i, result);
if(result.isConst() && !result.getConst<bool>()){
@@ -2350,7 +2350,7 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
void SmtEnginePrivate::unconstrainedSimp() {
TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
- spendResource();
+ spendResource(options::preprocessStep());
Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
}
@@ -2799,7 +2799,7 @@ void SmtEnginePrivate::doMiplibTrick() {
// returns false if simplification led to "false"
bool SmtEnginePrivate::simplifyAssertions()
throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
- spendResource();
+ spendResource(options::preprocessStep());
Assert(d_smt.d_pendingPops == 0);
try {
ScopeCounter depth(d_simplifyAssertionsDepth);
@@ -3042,7 +3042,7 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
- spendResource();
+ spendResource(options::preprocessStep());
if(d_booleanTermConverter == NULL) {
// This needs to be initialized _after_ the whole SMT framework is in place, subscribed
@@ -3077,7 +3077,7 @@ Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
void SmtEnginePrivate::processAssertions() {
TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
- spendResource();
+ spendResource(options::preprocessStep());
Assert(d_smt.d_fullyInited);
Assert(d_smt.d_pendingPops == 0);
@@ -3199,7 +3199,7 @@ void SmtEnginePrivate::processAssertions() {
<< "applying substitutions" << endl;
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
Trace("simplify") << "applying to " << d_assertions[i] << endl;
- spendResource();
+ spendResource(options::preprocessStep());
d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
Trace("simplify") << " got " << d_assertions[i] << endl;
}
@@ -3759,7 +3759,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
}
Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
- d_private->spendResource();
+ d_private->spendResource(options::preprocessStep());
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback