diff options
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 3 | ||||
-rw-r--r-- | src/theory/output_channel.h | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 10 | ||||
-rw-r--r-- | src/theory/theory_test_utils.h | 3 | ||||
-rw-r--r-- | src/util/options.cpp | 24 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 3 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 2 |
7 files changed, 30 insertions, 19 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index a5fa428c6..d4d495486 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -242,6 +242,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet void ArithStaticLearner::replaceWithPseudoboolean(TNode var) { AssertArgument(var.getMetaKind() == kind::metakind::VARIABLE, var); + // [MGD 10/21/2011] disable pseudobooleans for now (as discussed in today's meeting) + /* TypeNode pbType = NodeManager::currentNM()->pseudobooleanType(); Node pbVar = NodeManager::currentNM()->mkVar(string("PB[") + var.toString() + ']', pbType); d_pbSubstitutions.addSubstitution(var, pbVar); @@ -250,6 +252,7 @@ void ArithStaticLearner::replaceWithPseudoboolean(TNode var) { Expr::printtypes::Scope pts(Debug("pb"), true); Debug("pb") << "will replace " << var << " with " << pbVar << endl; } + */ } void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 625abc580..aaad25bd5 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -85,8 +85,10 @@ public: * * @param n - a theory lemma valid at decision level 0 * @param removable - whether the lemma can be removed at any point + * @return the user level at which the lemma resides; it will be + * removed when this user level pops */ - virtual void lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + virtual unsigned lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; /** * Request a split on a new theory atom. This is equivalent to diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 80890303b..09bb6963e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -200,10 +200,10 @@ class TheoryEngine { d_engine->propagate(literal, d_theory); } - void lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + unsigned lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; - d_engine->lemma(lemma, false, removable); + return d_engine->lemma(lemma, false, removable); } void setIncomplete() throw(AssertionException) { @@ -346,7 +346,7 @@ class TheoryEngine { /** * Adds a new lemma */ - void lemma(TNode node, bool negated, bool removable) { + unsigned lemma(TNode node, bool negated, bool removable) { if(Dump.isOn("t-lemmas")) { Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << std::endl @@ -363,6 +363,10 @@ class TheoryEngine { // Mark that we added some lemmas d_lemmasAdded = true; + + // Lemma analysis isn't online yet; this lemma may only live for this + // user level. + return d_userContext->getLevel(); } public: diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index bcb1c46d7..49ed16788 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -81,8 +81,9 @@ public: push(PROPAGATE, n); } - void lemma(TNode n, bool removable) throw(AssertionException) { + unsigned lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); + return 0; } void setIncomplete() throw(AssertionException) {} diff --git a/src/util/options.cpp b/src/util/options.cpp index a01237fd0..227cb778b 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -139,10 +139,10 @@ static const string optionsDescription = "\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\ --incremental | -i enable incremental solving\n\ - --time-limit=MS enable time limiting (give milliseconds)\n\ - --time-limit-per=MS enable time limiting per query (give milliseconds)\n\ - --limit=N enable resource limiting\n\ - --limit-per=N enable resource limiting per query\n"; + --tlimit=MS enable time limiting (give milliseconds)\n\ + --tlimit-per=MS enable time limiting per query (give milliseconds)\n\ + --rlimit=N enable resource limiting\n\ + --rlimit-per=N enable resource limiting per query\n"; #warning "Change CL options as --disable-variable-removal cannot do anything currently." @@ -303,8 +303,8 @@ enum OptionValue { DISABLE_SYMMETRY_BREAKER, TIME_LIMIT, TIME_LIMIT_PER, - LIMIT, - LIMIT_PER + RESOURCE_LIMIT, + RESOURCE_LIMIT_PER };/* enum OptionValue */ /** @@ -379,10 +379,10 @@ static struct option cmdlineOptions[] = { { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, - { "time-limit" , required_argument, NULL, TIME_LIMIT }, - { "time-limit-per", required_argument, NULL, TIME_LIMIT_PER }, - { "limit" , required_argument, NULL, LIMIT }, - { "limit-per" , required_argument, NULL, LIMIT_PER }, + { "tlimit" , required_argument, NULL, TIME_LIMIT }, + { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER }, + { "rlimit" , required_argument, NULL, RESOURCE_LIMIT }, + { "rlimit-per" , required_argument, NULL, RESOURCE_LIMIT_PER }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -707,7 +707,7 @@ throw(OptionException) { perCallMillisecondLimit = (unsigned long) i; } break; - case LIMIT: + case RESOURCE_LIMIT: { int i = atoi(optarg); if(i < 0) { @@ -716,7 +716,7 @@ throw(OptionException) { cumulativeResourceLimit = (unsigned long) i; } break; - case LIMIT_PER: + case RESOURCE_LIMIT_PER: { int i = atoi(optarg); if(i < 0) { diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index be1d4a35b..e5577d2c2 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -62,9 +62,10 @@ public: push(PROPAGATE, n); } - void lemma(TNode n, bool removable) + unsigned lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); + return 0; } void setIncomplete() diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 7132d9b17..fbac6f4ee 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -54,7 +54,7 @@ class FakeOutputChannel : public OutputChannel { void propagate(TNode n) throw(AssertionException) { Unimplemented(); } - void lemma(TNode n, bool removable) throw(AssertionException) { + unsigned lemma(TNode n, bool removable) throw(AssertionException) { Unimplemented(); } void explanation(TNode n) throw(AssertionException) { |