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.

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index a5fa428c692b3bd55d4a5ef75ba9654b0f55c59e..d4d495486361da8d9bcc16ec3c3d55f3d6f5bb81 100644 (file)
--- 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 625abc5800a6e829ca50df2cc48ff4e149395da5..aaad25bd5a40350937091af1ad52a1cdd4638420 100644 (file)
--- 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 80890303bd85f4875780de06600ee3a079fd5356..09bb6963e06d307b4e1aa5ba3f169f70d79ae7b7 100644 (file)
--- 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 bcb1c46d7f42c77f484c737ef0b1f14936324d48..49ed1678817446022fec52144e090ce37b7c8cbc 100644 (file)
--- 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 a01237fd053e2ce089b57e56241b41ed1ae3ddab..227cb778bb51020d1a848f9aecb531b1a4b8ce53 100644 (file)
--- 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 be1d4a35bd9483a2d259ac0876bf8bb750f1d1f2..e5577d2c23ab1ecbc15392eb0bed1f22d9645c3d 100644 (file)
--- 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 7132d9b17224e88784d25afb412b03842a14146f..fbac6f4ee7c60733e2c7a1eb4bdd2a09afaacf36 100644 (file)
--- 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) {