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.

4 files changed, 15 insertions, 5 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) {}