summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/arith_static_learner.cpp3
-rw-r--r--src/theory/output_channel.h4
-rw-r--r--src/theory/theory_engine.h10
-rw-r--r--src/theory/theory_test_utils.h3
-rw-r--r--src/util/options.cpp24
-rw-r--r--test/unit/theory/theory_black.h3
-rw-r--r--test/unit/theory/theory_engine_white.h2
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback