From 18f710cbfb5ce1ea13c8e929445abc211c732a81 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 23 Oct 2011 00:45:57 +0000 Subject: [PATCH] Implement changes from yesterday morning's meeting (10/21/2011): * OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want). * Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch. * --limit / --time-limit options renamed --rlimit and --tlimit. There may be slowdown from disabling pseudobooleans. --- src/theory/arith/arith_static_learner.cpp | 3 +++ src/theory/output_channel.h | 4 +++- src/theory/theory_engine.h | 10 +++++++--- src/theory/theory_test_utils.h | 3 ++- src/util/options.cpp | 24 +++++++++++------------ test/unit/theory/theory_black.h | 3 ++- 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) { -- 2.30.2